Example (23)

　あるサイトに出ていた計算機による証明の課題です．

# 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; EXP; GSYM ADD1; ADD_AC; MULT_2]]);;
val it : thm = |- !n. 1 + nsum (0..n) (\k. 2 EXP k) = 2 EXP (n + 1)