(* Ackermann function *)
(*
The Ackerman function is recursively defined by the
following equations:
Ack 0     y     = S y
Ack (S x) 0     = Ack x 1
Ack (S x) (S y) = Ack x (Ack (S x) y)
*)

(* Complete the following inductive predicate 
   for specifying this function
*)

Inductive ackspec : nat -> nat -> nat -> Prop :=
  | A0y : forall y, ackspec O y (S y)
(* FILL IN *)
.


Theorem ack_func : 
   forall x y a b, ackspec x y a -> ackspec x y b -> a = b.
Proof.
(* FILL IN *)
Admitted.

(* Define a function ack using a suitable Fixpoint
Fixpoint ack ...
*)


(* 
*)

Theorem ack_correct : forall x y, ackspec x y (ack x y).
Proof.
(* FILL IN *)
Admitted.


Theorem ack_complete : forall x y a, ackspec x y a -> a = ack x y.
Proof.
(* FILL IN *)
Admitted.



(* -------------------------------------------------- *)