Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
David, I should perhaps have mentioned that though your formulation of 9.1 is correct, what you have for 9.2 does not capture that theorem correctly, because your "sum n" adds the first n natural numbers, not the first n elements of a sequence. To get 9.2 you need to use the function "sigma" posted by Rob instead of your "sum". Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math
David, Good to see you are making some progress. For the examples in 9.2 you best course is probably to have a power function with type: ℝ→ℕ→ℝ ⓈHOLCONST │ pow:ℝ→ℕ→ℝ ├── │ ∀b e⦁ (pow b 0) = 1. ∧ │ (pow b (e + 1)) = b * (pow b e) ■ This will fit with Rob's suggestion for modelling sequences: Sequences are modeled as functions ℕ → ℝ. Which allows you to use mathematical induction over ℕ for reasoning about ℝ valued sequences. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
