Proof that the Ackermann function is total


[View ackermann.thm]

Click on a command or tactic to see a detailed view of its use.

%% This is a very small example that requires nested inductions.

Kind     nat     type.

Type     z       nat.
Type     s       nat -> nat.

Define nat : nat -> prop by
  nat z ;
  nat (s X) := nat X.

Define ack : nat -> nat -> nat -> prop by
  ack z N (s N) ;
  ack (s M) z R := ack M (s z) R ;
  ack (s M) (s N) R := exists R', ack (s M) N R' /\ ack M R' R.

Theorem ack_total : forall M N,
  nat M -> nat N -> exists R, nat R /\ ack M N R.