// Dafny module containing stuff pertaining to Ackermann's function.

module Ackermann {

  /* Definition of Ackermann's function.
  */
  function Ack(m: nat, n: nat): nat
    decreases m,n
  {
    if m == 0 then n+1
    else if n == 0 then Ack(m-1,1)
    else Ack(m-1, Ack(m,n-1))
  }
  
  /* Proof of lemma for Exercise 5.6 in "Program Proofs".
  */
  lemma {:induction false} Exercise5_6(n: nat)
    ensures Ack(1,n) == n+2
  {
    if n == 0 {
      calc {
        Ack(1,n);
      ==  // defn of Ack
        Ack(0,1);
      ==  // defn of Ack
        2;
      ==  // n == 0
        n+2;
      }
    }
    else {
      calc {
        Ack(1,n);
      ==  // defn of Ack
        Ack(0, Ack(1, n-1));
      ==  { Exercise5_6(n-1); assert Ack(1,n-1) == n+1; }
        Ack(0, n+1);
      ==  // defn of Ack
        n+2;
      }
    }
  }
  
  // Problem ACK.1: 
  // --------------
  
  /* Proof of lemma similar to one above.
  */
  lemma {:induction false} Exercise5_6'(n: nat)
    decreases n
    ensures Ack(2,n) == 2*n + 3
  {
    // MISSING PROOF
  }
  
}