2013-04-17から1日間の記事一覧
チュートリアルにもありますが,以下は既存の定理や補題を統合する,普通の数学と同じ流儀の証明です. let lem1 = PV9[SQRT_POS_LT; REAL_POS_NZ; ARITH; REAL_LT ]`~(sqrt (&2) = &0)`;; let lem2 = MESON[REAL_INV_0; REAL_FIELD`~(x / y = &0) ==> ~(x =…
チュートリアルにもありますが,以下は既存の定理や補題を統合する,普通の数学と同じ流儀の証明です. let lem1 = PV9[SQRT_POS_LT; REAL_POS_NZ; ARITH; REAL_LT ]`~(sqrt (&2) = &0)`;; let lem2 = MESON[REAL_INV_0; REAL_FIELD`~(x / y = &0) ==> ~(x =…