Abella logo (small)

ackermann.thm

%% Proof that the Ackermann function is total %% %% 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. induction on 1. induction on 2. intros. case H1 (keep). search. case H2. apply IH to H3 _ with N = s z. search. apply IH1 to H1 H4. apply IH to H3 H5. search.