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
