On 01/11/2019 18:38, David Topham wrote:
Adapting to the idea of using only whole numbers for a geometric
progression that sums over powers I am trying this approach:
It works up until trying to instantiate into induction_thm where it
breaks down since conjecture needs 2 variables: r and
David,
On 01/11/2019 16:13, David Topham wrote:
Ok, I can work within integers for awhile! I was trying to use the
general form of the geometric progression that may involve fractions,
but I can explore whole numbers more first. I see the "induction_thm"
won't work with R anyway since it has
Ok, I can work within integers for awhile! I was trying to use the general
form of the geometric progression that may involve fractions, but I can
explore whole numbers more first. I see the "induction_thm" won't work
with R anyway since it has the base case as 0 and SML would expect 0.0
there fo
