David,
Thanks for the reference to the text you are working from, it makes it
much clearer what you are trying to do.
In example 9.2 I think he should stipulate 0 < r < 1 not just r not= 1.
I think strictly speaking if you work with real numbers you are not
doing discrete maths, but I don't know how much that matters to you.
( /"Discrete mathematics/is the study of/mathematical/structures that
are countable or otherwise distinct and separable."
This seems the most popular definition.)
However, the examples in 9.2 don't require real numbers, since he is
only dealing with finite sums, not taking limits, so the numbers here
could be the rational numbers ℚ, and the induction is over the natural
numbers.
How about working in theory "ℚ"? (that's still discrete by the above
criterion).
As to utf8, it is likely that the next release of ProofPower will work
with utf8, and in the interim there is a ProofPower contrib which
contains programs for converting between ProofPower ext character set
and utf8.
I can't see anywhere that pputf8 can be downloaded, so you might have to
clone the github depository at:
https://github.com/RobArthan/pp-contrib
Then look for build instructions in src/pputf8.
Alternatively, look here for Rob's previous advice:
http://lemma-one.com/pipermail/proofpower_lemma-one.com/2016-August/002345.html
Roger
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
