Welcome to Abella 2.0.5-dev.

Abella <Kind nat type.

Abella <Type z nat.

Abella <Type s nat -> nat.

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

Abella <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.

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

============================ forall M N, nat M -> nat N -> (exists R, nat R /\ ack M N R) ack_total <induction on 1.

IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) ============================ forall M N, nat M @ -> nat N -> (exists R, nat R /\ ack M N R) ack_total <induction on 2.

IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) ============================ forall M N, nat M @ -> nat N @@ -> (exists R, nat R /\ ack M N R) ack_total <intros.

Variables: M N IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat M @ H2 : nat N @@ ============================ exists R, nat R /\ ack M N R ack_total <case H1 (keep).

Subgoal 1: Variables: N IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat z @ H2 : nat N @@ ============================ exists R, nat R /\ ack z N R Subgoal 2 is: exists R, nat R /\ ack (s X) N R ack_total <search.

Subgoal 2: Variables: N X IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat (s X) @ H2 : nat N @@ H3 : nat X * ============================ exists R, nat R /\ ack (s X) N R ack_total <case H2.

Subgoal 2.1: Variables: X IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat (s X) @ H3 : nat X * ============================ exists R, nat R /\ ack (s X) z R Subgoal 2.2 is: exists R, nat R /\ ack (s X) (s X1) R ack_total <apply IH to H3 _ with N = s z.

Subgoal 2.1: Variables: X R IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat (s X) @ H3 : nat X * H4 : nat R H5 : ack X (s z) R ============================ exists R, nat R /\ ack (s X) z R Subgoal 2.2 is: exists R, nat R /\ ack (s X) (s X1) R ack_total <search.

Subgoal 2.2: Variables: X X1 IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat (s X) @ H3 : nat X * H4 : nat X1 ** ============================ exists R, nat R /\ ack (s X) (s X1) R ack_total <apply IH1 to H1 H4.

Subgoal 2.2: Variables: X X1 R IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat (s X) @ H3 : nat X * H4 : nat X1 ** H5 : nat R H6 : ack (s X) X1 R ============================ exists R, nat R /\ ack (s X) (s X1) R ack_total <apply IH to H3 H5.

Subgoal 2.2: Variables: X X1 R R1 IH : forall M N, nat M * -> nat N -> (exists R, nat R /\ ack M N R) IH1 : forall M N, nat M @ -> nat N ** -> (exists R, nat R /\ ack M N R) H1 : nat (s X) @ H3 : nat X * H4 : nat X1 ** H5 : nat R H6 : ack (s X) X1 R H7 : nat R1 H8 : ack X R R1 ============================ exists R, nat R /\ ack (s X) (s X1) R ack_total <search.Proof completed.

Abella <