2012-01-25から1日間の記事一覧
あるサイトに出ていた計算機による証明の課題です. # prove (`!n. 1 + nsum (0..n) (\k. 2 EXP k) = 2 EXP (n + 1)`, INDUCT_TAC THENL [SIMP_TAC [NSUM_CLAUSES_NUMSEG; EXP; GSYM ADD1; MULT_CLAUSES; TWO]; ASM_SIMP_TAC [NSUM_CLAUSES_NUMSEG; LE_0; EX…
あるサイトに出ていた計算機による証明の課題です. # prove (`!n. 1 + nsum (0..n) (\k. 2 EXP k) = 2 EXP (n + 1)`, INDUCT_TAC THENL [SIMP_TAC [NSUM_CLAUSES_NUMSEG; EXP; GSYM ADD1; MULT_CLAUSES; TWO]; ASM_SIMP_TAC [NSUM_CLAUSES_NUMSEG; LE_0; EX…