David, I missed a pair of brackets in my last.
Should be: ⓈHOLCONST │ tri : ℕ → ℕ ├────────────────────── │ ∀n⦁ tri 0 = 0 │ ∧ tri (n+1) = (tri n)+n+1 ■ ⌜∀n⦁ tri n = (n*(n+1)) Div 2⌝; val tri_p = ⌜λn⦁ tri n = (n*(n+1)) Div 2⌝; ∀_elim tri_p induction_thm; val lemma1 = rewrite_rule [] it; and of course, rewriting with the definition of "tri" helps: val lemma2 = rewrite_rule [get_spec ⌜tri⌝] lemma1; giving: val lemma2 = ⊢ 0 = 0 Div 2 ∧ (∀ m ⦁ tri m = (m * (m + 1)) Div 2 ⇒ tri m + m + 1 = ((m + 1) * ((m + 1) + 1)) Div 2) ⇒ (∀ n⦁ tri n = (n * (n + 1)) Div 2): THM and then you need to do some arithmetic! Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
