Welcome to Abella 2.0.7-dev.

Abella < Kind nat Type.

Abella < Type z nat.

Abella < Type s nat -> nat.

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

Abella < Close nat.

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

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

Abella < Theorem plus_1_is_nat : 
forall X Y Z, plus X Y Z -> is_nat X.

============================
 forall X Y Z, plus X Y Z -> is_nat X

plus_1_is_nat < induction on 1.

IH : forall X Y Z, plus X Y Z * -> is_nat X
============================
 forall X Y Z, plus X Y Z @ -> is_nat X

plus_1_is_nat < intros.

Variables: X Y Z
IH : forall X Y Z, plus X Y Z * -> is_nat X
H1 : plus X Y Z @
============================
 is_nat X

plus_1_is_nat < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, plus X Y Z * -> is_nat X
H2 : is_nat Z
============================
 is_nat z

Subgoal 2 is:
 is_nat (s X1)

plus_1_is_nat < search.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> is_nat X
H2 : plus X1 Y Z1 *
============================
 is_nat (s X1)

plus_1_is_nat < apply IH to H2.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> is_nat X
H2 : plus X1 Y Z1 *
H3 : is_nat X1
============================
 is_nat (s X1)

plus_1_is_nat < search.
Proof completed.

Abella < Theorem plus_2_is_nat : 
forall X Y Z, plus X Y Z -> is_nat Y.

============================
 forall X Y Z, plus X Y Z -> is_nat Y

plus_2_is_nat < induction on 1.

IH : forall X Y Z, plus X Y Z * -> is_nat Y
============================
 forall X Y Z, plus X Y Z @ -> is_nat Y

plus_2_is_nat < intros.

Variables: X Y Z
IH : forall X Y Z, plus X Y Z * -> is_nat Y
H1 : plus X Y Z @
============================
 is_nat Y

plus_2_is_nat < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, plus X Y Z * -> is_nat Y
H2 : is_nat Z
============================
 is_nat Z

Subgoal 2 is:
 is_nat Y

plus_2_is_nat < search.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> is_nat Y
H2 : plus X1 Y Z1 *
============================
 is_nat Y

plus_2_is_nat < apply IH to H2.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> is_nat Y
H2 : plus X1 Y Z1 *
H3 : is_nat Y
============================
 is_nat Y

plus_2_is_nat < search.
Proof completed.

Abella < Theorem plus_3_is_nat : 
forall X Y Z, plus X Y Z -> is_nat Z.

============================
 forall X Y Z, plus X Y Z -> is_nat Z

plus_3_is_nat < induction on 1.

IH : forall X Y Z, plus X Y Z * -> is_nat Z
============================
 forall X Y Z, plus X Y Z @ -> is_nat Z

plus_3_is_nat < intros.

Variables: X Y Z
IH : forall X Y Z, plus X Y Z * -> is_nat Z
H1 : plus X Y Z @
============================
 is_nat Z

plus_3_is_nat < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, plus X Y Z * -> is_nat Z
H2 : is_nat Z
============================
 is_nat Z

Subgoal 2 is:
 is_nat (s Z1)

plus_3_is_nat < search.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> is_nat Z
H2 : plus X1 Y Z1 *
============================
 is_nat (s Z1)

plus_3_is_nat < apply IH to H2.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> is_nat Z
H2 : plus X1 Y Z1 *
H3 : is_nat Z1
============================
 is_nat (s Z1)

plus_3_is_nat < search.
Proof completed.

Abella < Theorem leq_1_is_nat : 
forall X Y, leq X Y -> is_nat X.

============================
 forall X Y, leq X Y -> is_nat X

leq_1_is_nat < induction on 1.

IH : forall X Y, leq X Y * -> is_nat X
============================
 forall X Y, leq X Y @ -> is_nat X

leq_1_is_nat < intros.

Variables: X Y
IH : forall X Y, leq X Y * -> is_nat X
H1 : leq X Y @
============================
 is_nat X

leq_1_is_nat < case H1.

Subgoal 1:

Variables: Y
IH : forall X Y, leq X Y * -> is_nat X
H2 : is_nat Y
============================
 is_nat z

Subgoal 2 is:
 is_nat (s X1)

leq_1_is_nat < search.

Subgoal 2:

Variables: Y1 X1
IH : forall X Y, leq X Y * -> is_nat X
H2 : leq X1 Y1 *
============================
 is_nat (s X1)

leq_1_is_nat < apply IH to H2.

Subgoal 2:

Variables: Y1 X1
IH : forall X Y, leq X Y * -> is_nat X
H2 : leq X1 Y1 *
H3 : is_nat X1
============================
 is_nat (s X1)

leq_1_is_nat < search.
Proof completed.

Abella < Theorem leq_2_is_nat : 
forall X Y, leq X Y -> is_nat Y.

============================
 forall X Y, leq X Y -> is_nat Y

leq_2_is_nat < induction on 1.

IH : forall X Y, leq X Y * -> is_nat Y
============================
 forall X Y, leq X Y @ -> is_nat Y

leq_2_is_nat < intros.

Variables: X Y
IH : forall X Y, leq X Y * -> is_nat Y
H1 : leq X Y @
============================
 is_nat Y

leq_2_is_nat < case H1.

Subgoal 1:

Variables: Y
IH : forall X Y, leq X Y * -> is_nat Y
H2 : is_nat Y
============================
 is_nat Y

Subgoal 2 is:
 is_nat (s Y1)

leq_2_is_nat < search.

Subgoal 2:

Variables: Y1 X1
IH : forall X Y, leq X Y * -> is_nat Y
H2 : leq X1 Y1 *
============================
 is_nat (s Y1)

leq_2_is_nat < apply IH to H2.

Subgoal 2:

Variables: Y1 X1
IH : forall X Y, leq X Y * -> is_nat Y
H2 : leq X1 Y1 *
H3 : is_nat Y1
============================
 is_nat (s Y1)

leq_2_is_nat < search.
Proof completed.

Abella < Theorem plus_z : 
forall X, is_nat X -> plus X z X.

============================
 forall X, is_nat X -> plus X z X

plus_z < induction on 1.

IH : forall X, is_nat X * -> plus X z X
============================
 forall X, is_nat X @ -> plus X z X

plus_z < intros.

Variables: X
IH : forall X, is_nat X * -> plus X z X
H1 : is_nat X @
============================
 plus X z X

plus_z < case H1.

Subgoal 1:

IH : forall X, is_nat X * -> plus X z X
============================
 plus z z z

Subgoal 2 is:
 plus (s X1) z (s X1)

plus_z < search.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> plus X z X
H2 : is_nat X1 *
============================
 plus (s X1) z (s X1)

plus_z < apply IH to H2.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> plus X z X
H2 : is_nat X1 *
H3 : plus X1 z X1
============================
 plus (s X1) z (s X1)

plus_z < search.
Proof completed.

Abella < Theorem plus_z_char : 
forall X Y, plus Y X Y -> X = z.

============================
 forall X Y, plus Y X Y -> X = z

plus_z_char < induction on 1.

IH : forall X Y, plus Y X Y * -> X = z
============================
 forall X Y, plus Y X Y @ -> X = z

plus_z_char < intros.

Variables: X Y
IH : forall X Y, plus Y X Y * -> X = z
H1 : plus Y X Y @
============================
 X = z

plus_z_char < case H1.

Subgoal 1:

IH : forall X Y, plus Y X Y * -> X = z
H2 : is_nat z
============================
 z = z

Subgoal 2 is:
 X = z

plus_z_char < search.

Subgoal 2:

Variables: X X1
IH : forall X Y, plus Y X Y * -> X = z
H2 : plus X1 X X1 *
============================
 X = z

plus_z_char < apply IH to H2.

Subgoal 2:

Variables: X1
IH : forall X Y, plus Y X Y * -> X = z
H2 : plus X1 z X1 *
============================
 z = z

plus_z_char < search.
Proof completed.

Abella < Theorem plus_s : 
forall X Y Z, plus X Y Z -> plus X (s Y) (s Z).

============================
 forall X Y Z, plus X Y Z -> plus X (s Y) (s Z)

plus_s < induction on 1.

IH : forall X Y Z, plus X Y Z * -> plus X (s Y) (s Z)
============================
 forall X Y Z, plus X Y Z @ -> plus X (s Y) (s Z)

plus_s < intros.

Variables: X Y Z
IH : forall X Y Z, plus X Y Z * -> plus X (s Y) (s Z)
H1 : plus X Y Z @
============================
 plus X (s Y) (s Z)

plus_s < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, plus X Y Z * -> plus X (s Y) (s Z)
H2 : is_nat Z
============================
 plus z (s Z) (s Z)

Subgoal 2 is:
 plus (s X1) (s Y) (s (s Z1))

plus_s < search.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> plus X (s Y) (s Z)
H2 : plus X1 Y Z1 *
============================
 plus (s X1) (s Y) (s (s Z1))

plus_s < apply IH to H2.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> plus X (s Y) (s Z)
H2 : plus X1 Y Z1 *
H3 : plus X1 (s Y) (s Z1)
============================
 plus (s X1) (s Y) (s (s Z1))

plus_s < search.
Proof completed.

Abella < Theorem plus_comm : 
forall X Y Z, plus X Y Z -> plus Y X Z.

============================
 forall X Y Z, plus X Y Z -> plus Y X Z

plus_comm < induction on 1.

IH : forall X Y Z, plus X Y Z * -> plus Y X Z
============================
 forall X Y Z, plus X Y Z @ -> plus Y X Z

plus_comm < intros.

Variables: X Y Z
IH : forall X Y Z, plus X Y Z * -> plus Y X Z
H1 : plus X Y Z @
============================
 plus Y X Z

plus_comm < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, plus X Y Z * -> plus Y X Z
H2 : is_nat Z
============================
 plus Z z Z

Subgoal 2 is:
 plus Y (s X1) (s Z1)

plus_comm < backchain plus_z.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> plus Y X Z
H2 : plus X1 Y Z1 *
============================
 plus Y (s X1) (s Z1)

plus_comm < apply IH to H2.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> plus Y X Z
H2 : plus X1 Y Z1 *
H3 : plus Y X1 Z1
============================
 plus Y (s X1) (s Z1)

plus_comm < backchain plus_s.
Proof completed.

Abella < Theorem leq_refl : 
forall X, is_nat X -> leq X X.

============================
 forall X, is_nat X -> leq X X

leq_refl < induction on 1.

IH : forall X, is_nat X * -> leq X X
============================
 forall X, is_nat X @ -> leq X X

leq_refl < intros.

Variables: X
IH : forall X, is_nat X * -> leq X X
H1 : is_nat X @
============================
 leq X X

leq_refl < case H1.

Subgoal 1:

IH : forall X, is_nat X * -> leq X X
============================
 leq z z

Subgoal 2 is:
 leq (s X1) (s X1)

leq_refl < search.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> leq X X
H2 : is_nat X1 *
============================
 leq (s X1) (s X1)

leq_refl < apply IH to H2.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> leq X X
H2 : is_nat X1 *
H3 : leq X1 X1
============================
 leq (s X1) (s X1)

leq_refl < search.
Proof completed.

Abella < Theorem leq_trans : 
forall X Y Z, leq X Y -> leq Y Z -> leq X Z.

============================
 forall X Y Z, leq X Y -> leq Y Z -> leq X Z

leq_trans < induction on 1.

IH : forall X Y Z, leq X Y * -> leq Y Z -> leq X Z
============================
 forall X Y Z, leq X Y @ -> leq Y Z -> leq X Z

leq_trans < intros.

Variables: X Y Z
IH : forall X Y Z, leq X Y * -> leq Y Z -> leq X Z
H1 : leq X Y @
H2 : leq Y Z
============================
 leq X Z

leq_trans < case H1.

Subgoal 1:

Variables: Y Z
IH : forall X Y Z, leq X Y * -> leq Y Z -> leq X Z
H2 : leq Y Z
H3 : is_nat Y
============================
 leq z Z

Subgoal 2 is:
 leq (s X1) Z

leq_trans < apply leq_2_is_nat to H2.

Subgoal 1:

Variables: Y Z
IH : forall X Y Z, leq X Y * -> leq Y Z -> leq X Z
H2 : leq Y Z
H3 : is_nat Y
H4 : is_nat Z
============================
 leq z Z

Subgoal 2 is:
 leq (s X1) Z

leq_trans < search.

Subgoal 2:

Variables: Z Y1 X1
IH : forall X Y Z, leq X Y * -> leq Y Z -> leq X Z
H2 : leq (s Y1) Z
H3 : leq X1 Y1 *
============================
 leq (s X1) Z

leq_trans < case H2.

Subgoal 2:

Variables: Y1 X1 Y2
IH : forall X Y Z, leq X Y * -> leq Y Z -> leq X Z
H3 : leq X1 Y1 *
H4 : leq Y1 Y2
============================
 leq (s X1) (s Y2)

leq_trans < apply IH to H3 H4.

Subgoal 2:

Variables: Y1 X1 Y2
IH : forall X Y Z, leq X Y * -> leq Y Z -> leq X Z
H3 : leq X1 Y1 *
H4 : leq Y1 Y2
H5 : leq X1 Y2
============================
 leq (s X1) (s Y2)

leq_trans < search.
Proof completed.

Abella < Theorem leq_s : 
forall X, is_nat X -> leq X (s X).

============================
 forall X, is_nat X -> leq X (s X)

leq_s < induction on 1.

IH : forall X, is_nat X * -> leq X (s X)
============================
 forall X, is_nat X @ -> leq X (s X)

leq_s < intros.

Variables: X
IH : forall X, is_nat X * -> leq X (s X)
H1 : is_nat X @
============================
 leq X (s X)

leq_s < case H1.

Subgoal 1:

IH : forall X, is_nat X * -> leq X (s X)
============================
 leq z (s z)

Subgoal 2 is:
 leq (s X1) (s (s X1))

leq_s < search.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> leq X (s X)
H2 : is_nat X1 *
============================
 leq (s X1) (s (s X1))

leq_s < apply IH to H2.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> leq X (s X)
H2 : is_nat X1 *
H3 : leq X1 (s X1)
============================
 leq (s X1) (s (s X1))

leq_s < search.
Proof completed.

Abella < Theorem leq_antisym : 
forall X Y, leq X Y -> leq Y X -> X = Y.

============================
 forall X Y, leq X Y -> leq Y X -> X = Y

leq_antisym < induction on 1.

IH : forall X Y, leq X Y * -> leq Y X -> X = Y
============================
 forall X Y, leq X Y @ -> leq Y X -> X = Y

leq_antisym < intros.

Variables: X Y
IH : forall X Y, leq X Y * -> leq Y X -> X = Y
H1 : leq X Y @
H2 : leq Y X
============================
 X = Y

leq_antisym < case H1.

Subgoal 1:

Variables: Y
IH : forall X Y, leq X Y * -> leq Y X -> X = Y
H2 : leq Y z
H3 : is_nat Y
============================
 z = Y

Subgoal 2 is:
 s X1 = s Y1

leq_antisym < case H2.

Subgoal 1:

IH : forall X Y, leq X Y * -> leq Y X -> X = Y
H3 : is_nat z
H4 : is_nat z
============================
 z = z

Subgoal 2 is:
 s X1 = s Y1

leq_antisym < search.

Subgoal 2:

Variables: Y1 X1
IH : forall X Y, leq X Y * -> leq Y X -> X = Y
H2 : leq (s Y1) (s X1)
H3 : leq X1 Y1 *
============================
 s X1 = s Y1

leq_antisym < case H2.

Subgoal 2:

Variables: Y1 X1
IH : forall X Y, leq X Y * -> leq Y X -> X = Y
H3 : leq X1 Y1 *
H4 : leq Y1 X1
============================
 s X1 = s Y1

leq_antisym < apply IH to H3 H4.

Subgoal 2:

Variables: Y1
IH : forall X Y, leq X Y * -> leq Y X -> X = Y
H3 : leq Y1 Y1 *
H4 : leq Y1 Y1
============================
 s Y1 = s Y1

leq_antisym < search.
Proof completed.

Abella < Theorem leq_total : 
forall X Y, is_nat X -> is_nat Y -> leq X Y \/ leq Y X.

============================
 forall X Y, is_nat X -> is_nat Y -> leq X Y \/ leq Y X

leq_total < induction on 1.

IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
============================
 forall X Y, is_nat X @ -> is_nat Y -> leq X Y \/ leq Y X

leq_total < intros.

Variables: X Y
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H1 : is_nat X @
H2 : is_nat Y
============================
 leq X Y \/ leq Y X

leq_total < case H1.

Subgoal 1:

Variables: Y
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H2 : is_nat Y
============================
 leq z Y \/ leq Y z

Subgoal 2 is:
 leq (s X1) Y \/ leq Y (s X1)

leq_total < search.

Subgoal 2:

Variables: Y X1
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H2 : is_nat Y
H3 : is_nat X1 *
============================
 leq (s X1) Y \/ leq Y (s X1)

leq_total < case H2.

Subgoal 2.1:

Variables: X1
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H3 : is_nat X1 *
============================
 leq (s X1) z \/ leq z (s X1)

Subgoal 2.2 is:
 leq (s X1) (s X2) \/ leq (s X2) (s X1)

leq_total < search.

Subgoal 2.2:

Variables: X1 X2
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H3 : is_nat X1 *
H4 : is_nat X2
============================
 leq (s X1) (s X2) \/ leq (s X2) (s X1)

leq_total < apply IH to *H3 *H4.

Subgoal 2.2:

Variables: X1 X2
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H5 : leq X1 X2 \/ leq X2 X1
============================
 leq (s X1) (s X2) \/ leq (s X2) (s X1)

leq_total < case H5.

Subgoal 2.2.1:

Variables: X1 X2
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H6 : leq X1 X2
============================
 leq (s X1) (s X2) \/ leq (s X2) (s X1)

Subgoal 2.2.2 is:
 leq (s X1) (s X2) \/ leq (s X2) (s X1)

leq_total < search.

Subgoal 2.2.2:

Variables: X1 X2
IH : forall X Y, is_nat X * -> is_nat Y -> leq X Y \/ leq Y X
H6 : leq X2 X1
============================
 leq (s X1) (s X2) \/ leq (s X2) (s X1)

leq_total < search.
Proof completed.

Abella < Theorem one_nleq_zero_lem : 
forall X, is_nat X -> leq (s X) X -> false.

============================
 forall X, is_nat X -> leq (s X) X -> false

one_nleq_zero_lem < induction on 1.

IH : forall X, is_nat X * -> leq (s X) X -> false
============================
 forall X, is_nat X @ -> leq (s X) X -> false

one_nleq_zero_lem < intros.

Variables: X
IH : forall X, is_nat X * -> leq (s X) X -> false
H1 : is_nat X @
H2 : leq (s X) X
============================
 false

one_nleq_zero_lem < case H1.

Subgoal 1:

IH : forall X, is_nat X * -> leq (s X) X -> false
H2 : leq (s z) z
============================
 false

Subgoal 2 is:
 false

one_nleq_zero_lem < case H2.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> leq (s X) X -> false
H2 : leq (s (s X1)) (s X1)
H3 : is_nat X1 *
============================
 false

one_nleq_zero_lem < case H2.

Subgoal 2:

Variables: X1
IH : forall X, is_nat X * -> leq (s X) X -> false
H3 : is_nat X1 *
H4 : leq (s X1) X1
============================
 false

one_nleq_zero_lem < backchain IH.
Proof completed.

Abella < Theorem one_nleq_zero : 
forall X, leq (s X) X -> false.

============================
 forall X, leq (s X) X -> false

one_nleq_zero < intros.

Variables: X
H1 : leq (s X) X
============================
 false

one_nleq_zero < apply leq_2_is_nat to H1.

Variables: X
H1 : leq (s X) X
H2 : is_nat X
============================
 false

one_nleq_zero < backchain one_nleq_zero_lem.
Proof completed.

Abella < Theorem plus_leq : 
forall X Y Z, plus X Y Z -> leq X Z /\ leq Y Z.

============================
 forall X Y Z, plus X Y Z -> leq X Z /\ leq Y Z

plus_leq < induction on 1.

IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
============================
 forall X Y Z, plus X Y Z @ -> leq X Z /\ leq Y Z

plus_leq < intros.

Variables: X Y Z
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H1 : plus X Y Z @
============================
 leq X Z /\ leq Y Z

plus_leq < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H2 : is_nat Z
============================
 leq z Z /\ leq Z Z

Subgoal 2 is:
 leq (s X1) (s Z1) /\ leq Y (s Z1)

plus_leq < apply leq_refl to H2.

Subgoal 1:

Variables: Z
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H2 : is_nat Z
H3 : leq Z Z
============================
 leq z Z /\ leq Z Z

Subgoal 2 is:
 leq (s X1) (s Z1) /\ leq Y (s Z1)

plus_leq < search.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H2 : plus X1 Y Z1 *
============================
 leq (s X1) (s Z1) /\ leq Y (s Z1)

plus_leq < apply IH to H2.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H2 : plus X1 Y Z1 *
H3 : leq X1 Z1
H4 : leq Y Z1
============================
 leq (s X1) (s Z1) /\ leq Y (s Z1)

plus_leq < apply leq_2_is_nat to H4.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H2 : plus X1 Y Z1 *
H3 : leq X1 Z1
H4 : leq Y Z1
H5 : is_nat Z1
============================
 leq (s X1) (s Z1) /\ leq Y (s Z1)

plus_leq < apply leq_s to *H5.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H2 : plus X1 Y Z1 *
H3 : leq X1 Z1
H4 : leq Y Z1
H6 : leq Z1 (s Z1)
============================
 leq (s X1) (s Z1) /\ leq Y (s Z1)

plus_leq < apply leq_trans to H4 *H6.

Subgoal 2:

Variables: Y Z1 X1
IH : forall X Y Z, plus X Y Z * -> leq X Z /\ leq Y Z
H2 : plus X1 Y Z1 *
H3 : leq X1 Z1
H4 : leq Y Z1
H7 : leq Y (s Z1)
============================
 leq (s X1) (s Z1) /\ leq Y (s Z1)

plus_leq < search.
Proof completed.

Abella < Theorem plus_det_1 : 
forall X1 X2 Y Z, plus X1 Y Z -> plus X2 Y Z -> X1 = X2.

============================
 forall X1 X2 Y Z, plus X1 Y Z -> plus X2 Y Z -> X1 = X2

plus_det_1 < induction on 1.

IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
============================
 forall X1 X2 Y Z, plus X1 Y Z @ -> plus X2 Y Z -> X1 = X2

plus_det_1 < intros.

Variables: X1 X2 Y Z
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H1 : plus X1 Y Z @
H2 : plus X2 Y Z
============================
 X1 = X2

plus_det_1 < case H1.

Subgoal 1:

Variables: X2 Z
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H2 : plus X2 Z Z
H3 : is_nat Z
============================
 z = X2

Subgoal 2 is:
 s X = X2

plus_det_1 < apply plus_comm to *H2.

Subgoal 1:

Variables: X2 Z
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H3 : is_nat Z
H4 : plus Z X2 Z
============================
 z = X2

Subgoal 2 is:
 s X = X2

plus_det_1 < apply plus_z_char to *H4.

Subgoal 1:

Variables: Z
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H3 : is_nat Z
============================
 z = z

Subgoal 2 is:
 s X = X2

plus_det_1 < search.

Subgoal 2:

Variables: X2 Y Z1 X
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H2 : plus X2 Y (s Z1)
H3 : plus X Y Z1 *
============================
 s X = X2

plus_det_1 < case H2.

Subgoal 2.1:

Variables: Z1 X
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H3 : plus X (s Z1) Z1 *
H4 : is_nat (s Z1)
============================
 s X = z

Subgoal 2.2 is:
 s X = s X3

plus_det_1 < apply plus_leq to *H3.

Subgoal 2.1:

Variables: Z1 X
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H4 : is_nat (s Z1)
H5 : leq X Z1
H6 : leq (s Z1) Z1
============================
 s X = z

Subgoal 2.2 is:
 s X = s X3

plus_det_1 < apply one_nleq_zero to H6.

Subgoal 2.2:

Variables: Y Z1 X X3
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H3 : plus X Y Z1 *
H4 : plus X3 Y Z1
============================
 s X = s X3

plus_det_1 < apply IH to H3 H4.

Subgoal 2.2:

Variables: Y Z1 X3
IH : forall X1 X2 Y Z, plus X1 Y Z * -> plus X2 Y Z -> X1 = X2
H3 : plus X3 Y Z1 *
H4 : plus X3 Y Z1
============================
 s X3 = s X3

plus_det_1 < search.
Proof completed.

Abella < Theorem plus_det_2 : 
forall X Y1 Y2 Z, plus X Y1 Z -> plus X Y2 Z -> Y1 = Y2.

============================
 forall X Y1 Y2 Z, plus X Y1 Z -> plus X Y2 Z -> Y1 = Y2

plus_det_2 < intros.

Variables: X Y1 Y2 Z
H1 : plus X Y1 Z
H2 : plus X Y2 Z
============================
 Y1 = Y2

plus_det_2 < apply plus_comm to *H1.

Variables: X Y1 Y2 Z
H2 : plus X Y2 Z
H3 : plus Y1 X Z
============================
 Y1 = Y2

plus_det_2 < apply plus_comm to *H2.

Variables: X Y1 Y2 Z
H3 : plus Y1 X Z
H4 : plus Y2 X Z
============================
 Y1 = Y2

plus_det_2 < backchain plus_det_1.
Proof completed.

Abella < Theorem plus_det_3 : 
forall X Y Z1 Z2, plus X Y Z1 -> plus X Y Z2 -> Z1 = Z2.

============================
 forall X Y Z1 Z2, plus X Y Z1 -> plus X Y Z2 -> Z1 = Z2

plus_det_3 < induction on 1.

IH : forall X Y Z1 Z2, plus X Y Z1 * -> plus X Y Z2 -> Z1 = Z2
============================
 forall X Y Z1 Z2, plus X Y Z1 @ -> plus X Y Z2 -> Z1 = Z2

plus_det_3 < intros.

Variables: X Y Z1 Z2
IH : forall X Y Z1 Z2, plus X Y Z1 * -> plus X Y Z2 -> Z1 = Z2
H1 : plus X Y Z1 @
H2 : plus X Y Z2
============================
 Z1 = Z2

plus_det_3 < case H1.

Subgoal 1:

Variables: Z1 Z2
IH : forall X Y Z1 Z2, plus X Y Z1 * -> plus X Y Z2 -> Z1 = Z2
H2 : plus z Z1 Z2
H3 : is_nat Z1
============================
 Z1 = Z2

Subgoal 2 is:
 s Z = Z2

plus_det_3 < case H2.

Subgoal 1:

Variables: Z2
IH : forall X Y Z1 Z2, plus X Y Z1 * -> plus X Y Z2 -> Z1 = Z2
H3 : is_nat Z2
H4 : is_nat Z2
============================
 Z2 = Z2

Subgoal 2 is:
 s Z = Z2

plus_det_3 < search.

Subgoal 2:

Variables: Y Z2 Z X1
IH : forall X Y Z1 Z2, plus X Y Z1 * -> plus X Y Z2 -> Z1 = Z2
H2 : plus (s X1) Y Z2
H3 : plus X1 Y Z *
============================
 s Z = Z2

plus_det_3 < case H2.

Subgoal 2:

Variables: Y Z X1 Z3
IH : forall X Y Z1 Z2, plus X Y Z1 * -> plus X Y Z2 -> Z1 = Z2
H3 : plus X1 Y Z *
H4 : plus X1 Y Z3
============================
 s Z = s Z3

plus_det_3 < apply IH to H3 H4.

Subgoal 2:

Variables: Y X1 Z3
IH : forall X Y Z1 Z2, plus X Y Z1 * -> plus X Y Z2 -> Z1 = Z2
H3 : plus X1 Y Z3 *
H4 : plus X1 Y Z3
============================
 s Z3 = s Z3

plus_det_3 < search.
Proof completed.

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

Abella < Theorem max_1_is : 
forall X Y Z, max X Y Z -> is_nat X /\ is_nat Y /\ is_nat Z.

============================
 forall X Y Z, max X Y Z -> is_nat X /\ is_nat Y /\ is_nat Z

max_1_is < induction on 1.

IH : forall X Y Z, max X Y Z * -> is_nat X /\ is_nat Y /\ is_nat Z
============================
 forall X Y Z, max X Y Z @ -> is_nat X /\ is_nat Y /\ is_nat Z

max_1_is < intros.

Variables: X Y Z
IH : forall X Y Z, max X Y Z * -> is_nat X /\ is_nat Y /\ is_nat Z
H1 : max X Y Z @
============================
 is_nat X /\ is_nat Y /\ is_nat Z

max_1_is < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, max X Y Z * -> is_nat X /\ is_nat Y /\ is_nat Z
H2 : is_nat Z
============================
 is_nat z /\ is_nat Z /\ is_nat Z

Subgoal 2 is:
 is_nat Z /\ is_nat z /\ is_nat Z

Subgoal 3 is:
 is_nat (s X1) /\ is_nat (s Y1) /\ is_nat (s Z1)

max_1_is < search.

Subgoal 2:

Variables: Z
IH : forall X Y Z, max X Y Z * -> is_nat X /\ is_nat Y /\ is_nat Z
H2 : is_nat Z
============================
 is_nat Z /\ is_nat z /\ is_nat Z

Subgoal 3 is:
 is_nat (s X1) /\ is_nat (s Y1) /\ is_nat (s Z1)

max_1_is < search.

Subgoal 3:

Variables: Z1 Y1 X1
IH : forall X Y Z, max X Y Z * -> is_nat X /\ is_nat Y /\ is_nat Z
H2 : max X1 Y1 Z1 *
============================
 is_nat (s X1) /\ is_nat (s Y1) /\ is_nat (s Z1)

max_1_is < apply IH to H2.

Subgoal 3:

Variables: Z1 Y1 X1
IH : forall X Y Z, max X Y Z * -> is_nat X /\ is_nat Y /\ is_nat Z
H2 : max X1 Y1 Z1 *
H3 : is_nat X1
H4 : is_nat Y1
H5 : is_nat Z1
============================
 is_nat (s X1) /\ is_nat (s Y1) /\ is_nat (s Z1)

max_1_is < search.
Proof completed.

Abella < Theorem max_exists : 
forall X Y, is_nat X -> is_nat Y -> (exists Z, max X Y Z).

============================
 forall X Y, is_nat X -> is_nat Y -> (exists Z, max X Y Z)

max_exists < induction on 1.

IH : forall X Y, is_nat X * -> is_nat Y -> (exists Z, max X Y Z)
============================
 forall X Y, is_nat X @ -> is_nat Y -> (exists Z, max X Y Z)

max_exists < intros.

Variables: X Y
IH : forall X Y, is_nat X * -> is_nat Y -> (exists Z, max X Y Z)
H1 : is_nat X @
H2 : is_nat Y
============================
 exists Z, max X Y Z

max_exists < case H1.

Subgoal 1:

Variables: Y
IH : forall X Y, is_nat X * -> is_nat Y -> (exists Z, max X Y Z)
H2 : is_nat Y
============================
 exists Z, max z Y Z

Subgoal 2 is:
 exists Z, max (s X1) Y Z

max_exists < search.

Subgoal 2:

Variables: Y X1
IH : forall X Y, is_nat X * -> is_nat Y -> (exists Z, max X Y Z)
H2 : is_nat Y
H3 : is_nat X1 *
============================
 exists Z, max (s X1) Y Z

max_exists < case H2.

Subgoal 2.1:

Variables: X1
IH : forall X Y, is_nat X * -> is_nat Y -> (exists Z, max X Y Z)
H3 : is_nat X1 *
============================
 exists Z, max (s X1) z Z

Subgoal 2.2 is:
 exists Z, max (s X1) (s X2) Z

max_exists < search.

Subgoal 2.2:

Variables: X1 X2
IH : forall X Y, is_nat X * -> is_nat Y -> (exists Z, max X Y Z)
H3 : is_nat X1 *
H4 : is_nat X2
============================
 exists Z, max (s X1) (s X2) Z

max_exists < apply IH to H3 H4.

Subgoal 2.2:

Variables: X1 X2 Z
IH : forall X Y, is_nat X * -> is_nat Y -> (exists Z, max X Y Z)
H3 : is_nat X1 *
H4 : is_nat X2
H5 : max X1 X2 Z
============================
 exists Z, max (s X1) (s X2) Z

max_exists < search.
Proof completed.

Abella < Theorem max_eq : 
forall X Y Z, max X Y Z -> Z = X \/ Z = Y.

============================
 forall X Y Z, max X Y Z -> Z = X \/ Z = Y

max_eq < induction on 1.

IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
============================
 forall X Y Z, max X Y Z @ -> Z = X \/ Z = Y

max_eq < intros.

Variables: X Y Z
IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
H1 : max X Y Z @
============================
 Z = X \/ Z = Y

max_eq < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
H2 : is_nat Z
============================
 Z = z \/ Z = Z

Subgoal 2 is:
 Z = Z \/ Z = z

Subgoal 3 is:
 s Z1 = s X1 \/ s Z1 = s Y1

max_eq < search.

Subgoal 2:

Variables: Z
IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
H2 : is_nat Z
============================
 Z = Z \/ Z = z

Subgoal 3 is:
 s Z1 = s X1 \/ s Z1 = s Y1

max_eq < search.

Subgoal 3:

Variables: Z1 Y1 X1
IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
H2 : max X1 Y1 Z1 *
============================
 s Z1 = s X1 \/ s Z1 = s Y1

max_eq < apply IH to H2.

Subgoal 3:

Variables: Z1 Y1 X1
IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
H2 : max X1 Y1 Z1 *
H3 : Z1 = X1 \/ Z1 = Y1
============================
 s Z1 = s X1 \/ s Z1 = s Y1

max_eq < case H3.

Subgoal 3.1:

Variables: Y1 X1
IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
H2 : max X1 Y1 X1 *
============================
 s X1 = s X1 \/ s X1 = s Y1

Subgoal 3.2 is:
 s Y1 = s X1 \/ s Y1 = s Y1

max_eq < search.

Subgoal 3.2:

Variables: Y1 X1
IH : forall X Y Z, max X Y Z * -> Z = X \/ Z = Y
H2 : max X1 Y1 Y1 *
============================
 s Y1 = s X1 \/ s Y1 = s Y1

max_eq < search.
Proof completed.

Abella < Theorem max_leq : 
forall X Y Z, max X Y Z -> leq X Z /\ leq Y Z.

============================
 forall X Y Z, max X Y Z -> leq X Z /\ leq Y Z

max_leq < induction on 1.

IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
============================
 forall X Y Z, max X Y Z @ -> leq X Z /\ leq Y Z

max_leq < intros.

Variables: X Y Z
IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
H1 : max X Y Z @
============================
 leq X Z /\ leq Y Z

max_leq < case H1.

Subgoal 1:

Variables: Z
IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
H2 : is_nat Z
============================
 leq z Z /\ leq Z Z

Subgoal 2 is:
 leq Z Z /\ leq z Z

Subgoal 3 is:
 leq (s X1) (s Z1) /\ leq (s Y1) (s Z1)

max_leq < apply leq_refl to H2.

Subgoal 1:

Variables: Z
IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
H2 : is_nat Z
H3 : leq Z Z
============================
 leq z Z /\ leq Z Z

Subgoal 2 is:
 leq Z Z /\ leq z Z

Subgoal 3 is:
 leq (s X1) (s Z1) /\ leq (s Y1) (s Z1)

max_leq < search.

Subgoal 2:

Variables: Z
IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
H2 : is_nat Z
============================
 leq Z Z /\ leq z Z

Subgoal 3 is:
 leq (s X1) (s Z1) /\ leq (s Y1) (s Z1)

max_leq < apply leq_refl to H2.

Subgoal 2:

Variables: Z
IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
H2 : is_nat Z
H3 : leq Z Z
============================
 leq Z Z /\ leq z Z

Subgoal 3 is:
 leq (s X1) (s Z1) /\ leq (s Y1) (s Z1)

max_leq < search.

Subgoal 3:

Variables: Z1 Y1 X1
IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
H2 : max X1 Y1 Z1 *
============================
 leq (s X1) (s Z1) /\ leq (s Y1) (s Z1)

max_leq < apply IH to H2.

Subgoal 3:

Variables: Z1 Y1 X1
IH : forall X Y Z, max X Y Z * -> leq X Z /\ leq Y Z
H2 : max X1 Y1 Z1 *
H3 : leq X1 Z1
H4 : leq Y1 Z1
============================
 leq (s X1) (s Z1) /\ leq (s Y1) (s Z1)

max_leq < search.
Proof completed.

Abella < Theorem lequate : 
forall X Y, is_nat X -> is_nat Y -> (exists Z, leq X Z /\ leq Y Z).

============================
 forall X Y, is_nat X -> is_nat Y -> (exists Z, leq X Z /\ leq Y Z)

lequate < intros.

Variables: X Y
H1 : is_nat X
H2 : is_nat Y
============================
 exists Z, leq X Z /\ leq Y Z

lequate < apply max_exists to H1 H2.

Variables: X Y Z
H1 : is_nat X
H2 : is_nat Y
H3 : max X Y Z
============================
 exists Z, leq X Z /\ leq Y Z

lequate < apply max_leq to H3.

Variables: X Y Z
H1 : is_nat X
H2 : is_nat Y
H3 : max X Y Z
H4 : leq X Z
H5 : leq Y Z
============================
 exists Z, leq X Z /\ leq Y Z

lequate < search.
Proof completed.

Abella <