2013-04-06から1日間の記事一覧
needs "Multivariate/transcendentals.ml";; needs "Examples/prover9_win.ml";; needs "Examples/sos_win.ml";; let lem01 = prove (`z 0 = Cx(&1) /\ (!n. z (SUC n) = c * z n) ==> (!n. z n = c pow n)`, STRIP_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[c…