1. Induction: A first simple & quick mathmatical example:
   Prove that Sum(1..n) = (n^2+n)/2 - using the recipe given in class:
   - The induction is on the number n.
   - The property is P(n): Sum(1..n) = (n^2+n)/2, for all n's from 1 on.
   - Base case - here we have 1 as the base case (but could also use 0):
       1 = Sum(1..1) = (1^2+1)/2 = 1
   - Assume Sum(1..n) = (n^2+n)/2,
     should show Sum(1..n+1) = ((n+1)^2+(n+1))/2:
       Sum(1..n+1) = 1 + ... + n + n+1
                   = Sum(1..n) + n + 1
                   = (n^2+n)/2 + n + 1     --> Here we're using the assumption
                   = (n^2+n)/2 + (2n+2)/2
                   = (n^2 + 3n + 2)/2
     but:
       ((n+1)^2+(n+1))/2 = (n^2 + 1 + 2n + n + 1) / 2
                         = (n^2 + 3n + 2)/2
     And we're done.

2. Induction example

We will do induction on N, a positive integer.

We want to prove (fact N) = N!

(define-method fact ((n <number>))
  (if (= n 1)
      1
      (* n (fact (dec n)))))


Basis 
        For the basis, we wish to show that (fact 1) ==> 1. >From the substitution model we know that 

        (fact 1)
        ==> ((define-method fact ((n <number>))
              (if (= n 1) 1 (* n (fact (dec n))))) 1)
        ==> (if (= 1 1) 1 (* 1 (fact (dec 1))))
        ==> 1

        so we are done with the basis. 

Induction step 
        Assuming that (fact N) ==> N!, we wish to show that (fact N+1) ==> (N+1)!. 

        (fact N+1)
        ==> ((define-method fact ((n <number>))
              (if (= n 1) 1 (* n (fact (dec n))))) N+1)
        ==> (if (= N+1 1) 1 (* N+1 (fact (dec N+1))))
        ==> (* N+1 (fact (dec N+1)))
        ==> (* N+1 (fact N))
        ==> (* N+1 N!)  <-- here we used the induction hypothesis
        ==> (N+1)!

        Here we have left out the APPLY steps of the substitution model. 

3. There's a strong correspondence between any [constructive] proof and a
   program that actually implements it - when you solve a problem by writing a
   program, you're actually doing the same job as _proving_ that there is a
   solution.
   An example of this matching will relate an inductive proof and a recursive
   program:
     The problem is the Towers of Hanoi:
       Initial state:
         Three piles of discs, each disc has a unique diameter, they are
         initially piled from the biggest on the bottom to the smallest on the
         top - on pile #1.
       Task:
         Move all to pile #3
       Rules:
         - Can move only one disc at a time
         - Can only move the top disc of a pile to the top of another
         - Can't put a disc on a smaller one.
   The proof is trivial - and directly corresponds to a recursive program:
     (define solve-hanoi
       (method (n-discs from-pile to-pile help-pile)
         (if (= n-discs 1)
           (move-disc 1 from-pile to-pile)
           (begin                       ; This uses side-effect...
             (solve-hanoi (- n-discs 1) from-pile help-pile to-pile)
             (move-disc n-discs from-pile to-pile)
             (solve-hanoi (- n-discs 1) help-pile to-pile from-pile)))))
     (define hanoi
       (method (n)
         (solve-hanoi n 1 3 2)))

4. Strong-induction is very similar to what we saw (weak induction) - but here
   we have a different recipe:
     STRONG INDUCTION RECIPE:
       * What variable n are you doing induction on?
       * What is the property P(n)
       * Assume P(0), P(1), ... P(n), prove P(n+1)
   Use that to prove a more general Hanoi problem - same task & goal, but the
   initial state is all discs are spread randomly on all piles.
     This is too long to show as a program - just go over the proof.
     Idea: Locate the biggest disc, "hide" it and whatever beneath it,
           Arrange all of the rest on another pile (using the assumption),
           move the biggest to the last (now empty) pile,
           pile the rest on top of it (again, using the assumption).
   A difference that we have here - we didn't had any "base case" to check -
   but our "induction step" was supposed to work also if the assumption is
   vacuously true.