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 <