Welcome to Abella 2.0.5-dev.
```Abella < Specification "gcd".

```
```Abella < Theorem sub_total_tt :
forall X Y, {less X Y tt} -> (exists Z, {sub Y X Z}).

```
```
============================
forall X Y, {less X Y tt} -> (exists Z, {sub Y X Z})

sub_total_tt < induction on 1.
```
```
IH : forall X Y, {less X Y tt}* -> (exists Z, {sub Y X Z})
============================
forall X Y, {less X Y tt}@ -> (exists Z, {sub Y X Z})

sub_total_tt < intros.
```
```
Variables: X Y
IH : forall X Y, {less X Y tt}* -> (exists Z, {sub Y X Z})
H1 : {less X Y tt}@
============================
exists Z, {sub Y X Z}

sub_total_tt < case H1.
```
```Subgoal 1:

Variables: X1
IH : forall X Y, {less X Y tt}* -> (exists Z, {sub Y X Z})
============================
exists Z, {sub (s X1) z Z}

Subgoal 2 is:
exists Z, {sub (s Y1) (s X1) Z}

sub_total_tt < search.
```
```Subgoal 2:

Variables: Y1 X1
IH : forall X Y, {less X Y tt}* -> (exists Z, {sub Y X Z})
H2 : {less X1 Y1 tt}*
============================
exists Z, {sub (s Y1) (s X1) Z}

sub_total_tt < apply IH to H2.
```
```Subgoal 2:

Variables: Y1 X1 Z
IH : forall X Y, {less X Y tt}* -> (exists Z, {sub Y X Z})
H2 : {less X1 Y1 tt}*
H3 : {sub Y1 X1 Z}
============================
exists Z, {sub (s Y1) (s X1) Z}

sub_total_tt < search.
Proof completed.
```
```Abella < Theorem sub_total_ff :
forall X Y, {less X Y ff} -> (exists Z, {sub X Y Z}).

```
```
============================
forall X Y, {less X Y ff} -> (exists Z, {sub X Y Z})

sub_total_ff < induction on 1.
```
```
IH : forall X Y, {less X Y ff}* -> (exists Z, {sub X Y Z})
============================
forall X Y, {less X Y ff}@ -> (exists Z, {sub X Y Z})

sub_total_ff < intros.
```
```
Variables: X Y
IH : forall X Y, {less X Y ff}* -> (exists Z, {sub X Y Z})
H1 : {less X Y ff}@
============================
exists Z, {sub X Y Z}

sub_total_ff < case H1.
```
```Subgoal 1:

Variables: X
IH : forall X Y, {less X Y ff}* -> (exists Z, {sub X Y Z})
============================
exists Z, {sub X z Z}

Subgoal 2 is:
exists Z, {sub (s X1) (s Y1) Z}

sub_total_ff < search.
```
```Subgoal 2:

Variables: Y1 X1
IH : forall X Y, {less X Y ff}* -> (exists Z, {sub X Y Z})
H2 : {less X1 Y1 ff}*
============================
exists Z, {sub (s X1) (s Y1) Z}

sub_total_ff < apply IH to H2.
```
```Subgoal 2:

Variables: Y1 X1 Z
IH : forall X Y, {less X Y ff}* -> (exists Z, {sub X Y Z})
H2 : {less X1 Y1 ff}*
H3 : {sub X1 Y1 Z}
============================
exists Z, {sub (s X1) (s Y1) Z}

sub_total_ff < search.
Proof completed.
```
```Abella < Theorem less_total :
forall X Y, {nat X} -> {nat Y} -> (exists B, {bool B} /\ {less X Y B}).

```
```
============================
forall X Y, {nat X} -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})

less_total < induction on 1.
```
```
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
============================
forall X Y, {nat X}@ -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})

less_total < intros.
```
```
Variables: X Y
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
H1 : {nat X}@
H2 : {nat Y}
============================
exists B, {bool B} /\ {less X Y B}

less_total < case H1.
```
```Subgoal 1:

Variables: Y
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
H2 : {nat Y}
============================
exists B, {bool B} /\ {less z Y B}

Subgoal 2 is:
exists B, {bool B} /\ {less (s N) Y B}

less_total < case H2.
```
```Subgoal 1.1:

IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
============================
exists B, {bool B} /\ {less z z B}

Subgoal 1.2 is:
exists B, {bool B} /\ {less z (s N) B}

Subgoal 2 is:
exists B, {bool B} /\ {less (s N) Y B}

less_total < search.
```
```Subgoal 1.2:

Variables: N
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
H3 : {nat N}
============================
exists B, {bool B} /\ {less z (s N) B}

Subgoal 2 is:
exists B, {bool B} /\ {less (s N) Y B}

less_total < search.
```
```Subgoal 2:

Variables: Y N
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
H2 : {nat Y}
H3 : {nat N}*
============================
exists B, {bool B} /\ {less (s N) Y B}

less_total < case H2.
```
```Subgoal 2.1:

Variables: N
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
H3 : {nat N}*
============================
exists B, {bool B} /\ {less (s N) z B}

Subgoal 2.2 is:
exists B, {bool B} /\ {less (s N) (s N1) B}

less_total < search.
```
```Subgoal 2.2:

Variables: N N1
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
H3 : {nat N}*
H4 : {nat N1}
============================
exists B, {bool B} /\ {less (s N) (s N1) B}

less_total < apply IH to H3 H4.
```
```Subgoal 2.2:

Variables: N N1 B
IH : forall X Y, {nat X}* -> {nat Y} -> (exists B, {bool B} /\ {less X Y B})
H3 : {nat N}*
H4 : {nat N1}
H5 : {bool B}
H6 : {less N N1 B}
============================
exists B, {bool B} /\ {less (s N) (s N1) B}

less_total < search.
Proof completed.
```
```Abella < Theorem lt_trans :
forall X Y Z, {lt X (s Y)} -> {lt Y Z} -> {lt X Z}.

```
```
============================
forall X Y Z, {lt X (s Y)} -> {lt Y Z} -> {lt X Z}

lt_trans < induction on 1.
```
```
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
============================
forall X Y Z, {lt X (s Y)}@ -> {lt Y Z} -> {lt X Z}

lt_trans < intros.
```
```
Variables: X Y Z
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
H1 : {lt X (s Y)}@
H2 : {lt Y Z}
============================
{lt X Z}

lt_trans < case H1.
```
```Subgoal 1:

Variables: Y Z
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
H2 : {lt Y Z}
============================
{lt z Z}

Subgoal 2 is:
{lt (s X1) Z}

lt_trans < case H2.
```
```Subgoal 1.1:

Variables: Y1
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
============================
{lt z (s Y1)}

Subgoal 1.2 is:
{lt z (s Y1)}

Subgoal 2 is:
{lt (s X1) Z}

lt_trans < search.
```
```Subgoal 1.2:

Variables: Y1 X1
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
H3 : {lt X1 Y1}
============================
{lt z (s Y1)}

Subgoal 2 is:
{lt (s X1) Z}

lt_trans < search.
```
```Subgoal 2:

Variables: Y Z X1
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
H2 : {lt Y Z}
H3 : {lt X1 Y}*
============================
{lt (s X1) Z}

lt_trans < case H2.
```
```Subgoal 2.1:

Variables: X1 Y1
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
H3 : {lt X1 z}*
============================
{lt (s X1) (s Y1)}

Subgoal 2.2 is:
{lt (s X1) (s Y1)}

lt_trans < case H3.
```
```Subgoal 2.2:

Variables: X1 Y1 X2
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
H3 : {lt X1 (s X2)}*
H4 : {lt X2 Y1}
============================
{lt (s X1) (s Y1)}

lt_trans < apply IH to H3 H4.
```
```Subgoal 2.2:

Variables: X1 Y1 X2
IH : forall X Y Z, {lt X (s Y)}* -> {lt Y Z} -> {lt X Z}
H3 : {lt X1 (s X2)}*
H4 : {lt X2 Y1}
H5 : {lt X1 Y1}
============================
{lt (s X1) (s Y1)}

lt_trans < search.
Proof completed.
```
```Abella < Theorem lt_nat :
forall X Y, {lt X Y} -> {nat X}.

```
```
============================
forall X Y, {lt X Y} -> {nat X}

lt_nat < induction on 1.
```
```
IH : forall X Y, {lt X Y}* -> {nat X}
============================
forall X Y, {lt X Y}@ -> {nat X}

lt_nat < intros.
```
```
Variables: X Y
IH : forall X Y, {lt X Y}* -> {nat X}
H1 : {lt X Y}@
============================
{nat X}

lt_nat < case H1.
```
```Subgoal 1:

Variables: Y1
IH : forall X Y, {lt X Y}* -> {nat X}
============================
{nat z}

Subgoal 2 is:
{nat (s X1)}

lt_nat < search.
```
```Subgoal 2:

Variables: Y1 X1
IH : forall X Y, {lt X Y}* -> {nat X}
H2 : {lt X1 Y1}*
============================
{nat (s X1)}

lt_nat < apply IH to H2.
```
```Subgoal 2:

Variables: Y1 X1
IH : forall X Y, {lt X Y}* -> {nat X}
H2 : {lt X1 Y1}*
H3 : {nat X1}
============================
{nat (s X1)}

lt_nat < search.
Proof completed.
```
```Abella < Theorem lt_x_sx :
forall X, {nat X} -> {lt X (s X)}.

```
```
============================
forall X, {nat X} -> {lt X (s X)}

lt_x_sx < induction on 1.
```
```
IH : forall X, {nat X}* -> {lt X (s X)}
============================
forall X, {nat X}@ -> {lt X (s X)}

lt_x_sx < intros.
```
```
Variables: X
IH : forall X, {nat X}* -> {lt X (s X)}
H1 : {nat X}@
============================
{lt X (s X)}

lt_x_sx < case H1.
```
```Subgoal 1:

IH : forall X, {nat X}* -> {lt X (s X)}
============================
{lt z (s z)}

Subgoal 2 is:
{lt (s N) (s (s N))}

lt_x_sx < search.
```
```Subgoal 2:

Variables: N
IH : forall X, {nat X}* -> {lt X (s X)}
H2 : {nat N}*
============================
{lt (s N) (s (s N))}

lt_x_sx < apply IH to H2.
```
```Subgoal 2:

Variables: N
IH : forall X, {nat X}* -> {lt X (s X)}
H2 : {nat N}*
H3 : {lt N (s N)}
============================
{lt (s N) (s (s N))}

lt_x_sx < search.
Proof completed.
```
```Abella < Theorem lt_s :
forall X Y, {lt X Y} -> {lt X (s Y)}.

```
```
============================
forall X Y, {lt X Y} -> {lt X (s Y)}

lt_s < induction on 1.
```
```
IH : forall X Y, {lt X Y}* -> {lt X (s Y)}
============================
forall X Y, {lt X Y}@ -> {lt X (s Y)}

lt_s < intros.
```
```
Variables: X Y
IH : forall X Y, {lt X Y}* -> {lt X (s Y)}
H1 : {lt X Y}@
============================
{lt X (s Y)}

lt_s < case H1.
```
```Subgoal 1:

Variables: Y1
IH : forall X Y, {lt X Y}* -> {lt X (s Y)}
============================
{lt z (s (s Y1))}

Subgoal 2 is:
{lt (s X1) (s (s Y1))}

lt_s < search.
```
```Subgoal 2:

Variables: Y1 X1
IH : forall X Y, {lt X Y}* -> {lt X (s Y)}
H2 : {lt X1 Y1}*
============================
{lt (s X1) (s (s Y1))}

lt_s < apply IH to H2.
```
```Subgoal 2:

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

lt_s < search.
Proof completed.
```
```Abella < Theorem sub_lt :
forall X Y Z, {nat X} -> {sub X Y Z} -> {lt Z (s X)}.

```
```
============================
forall X Y Z, {nat X} -> {sub X Y Z} -> {lt Z (s X)}

sub_lt < induction on 2.
```
```
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
============================
forall X Y Z, {nat X} -> {sub X Y Z}@ -> {lt Z (s X)}

sub_lt < intros.
```
```
Variables: X Y Z
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
H1 : {nat X}
H2 : {sub X Y Z}@
============================
{lt Z (s X)}

sub_lt < case H2.
```
```Subgoal 1:

Variables: Z
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
H1 : {nat Z}
============================
{lt Z (s Z)}

Subgoal 2 is:
{lt Z (s (s X1))}

sub_lt < apply lt_x_sx to H1.
```
```Subgoal 1:

Variables: Z
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
H1 : {nat Z}
H3 : {lt Z (s Z)}
============================
{lt Z (s Z)}

Subgoal 2 is:
{lt Z (s (s X1))}

sub_lt < search.
```
```Subgoal 2:

Variables: Z Y1 X1
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
H1 : {nat (s X1)}
H3 : {sub X1 Y1 Z}*
============================
{lt Z (s (s X1))}

sub_lt < case H1.
```
```Subgoal 2:

Variables: Z Y1 X1
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
H3 : {sub X1 Y1 Z}*
H4 : {nat X1}
============================
{lt Z (s (s X1))}

sub_lt < apply IH to H4 H3.
```
```Subgoal 2:

Variables: Z Y1 X1
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
H3 : {sub X1 Y1 Z}*
H4 : {nat X1}
H5 : {lt Z (s X1)}
============================
{lt Z (s (s X1))}

sub_lt < apply lt_s to H5.
```
```Subgoal 2:

Variables: Z Y1 X1
IH : forall X Y Z, {nat X} -> {sub X Y Z}* -> {lt Z (s X)}
H3 : {sub X1 Y1 Z}*
H4 : {nat X1}
H5 : {lt Z (s X1)}
H6 : {lt Z (s (s X1))}
============================
{lt Z (s (s X1))}

sub_lt < search.
Proof completed.
```
```Abella < Theorem gcd_total_strong :
forall A B, {nat A} -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} -> (exists Z, {nat Z} /\ {gcd X Y Z})).

```
```
============================
forall A B, {nat A} -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} -> (exists Z, {nat Z} /\ {gcd X Y Z}))

gcd_total_strong < induction on 1.
```
```
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
============================
forall A B, {nat A}@ -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} -> (exists Z, {nat Z} /\ {gcd X Y Z}))

gcd_total_strong < induction on 2.
```
```
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
============================
forall A B, {nat A}@ -> {nat B}@@ ->
(forall X Y, {lt X A} -> {lt Y B} -> (exists Z, {nat Z} /\ {gcd X Y Z}))

gcd_total_strong < intros.
```
```
Variables: A B X Y
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat A}@
H2 : {nat B}@@
H3 : {lt X A}
H4 : {lt Y B}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < apply lt_nat to H3.
```
```
Variables: A B X Y
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat A}@
H2 : {nat B}@@
H3 : {lt X A}
H4 : {lt Y B}
H5 : {nat X}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < apply lt_nat to H4.
```
```
Variables: A B X Y
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat A}@
H2 : {nat B}@@
H3 : {lt X A}
H4 : {lt Y B}
H5 : {nat X}
H6 : {nat Y}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < case H1 (keep).
```
```Subgoal 1:

Variables: B X Y
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat z}@
H2 : {nat B}@@
H3 : {lt X z}
H4 : {lt Y B}
H5 : {nat X}
H6 : {nat Y}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

Subgoal 2 is:
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < case H3.
```
```Subgoal 2:

Variables: B X Y N
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat (s N)}@
H2 : {nat B}@@
H3 : {lt X (s N)}
H4 : {lt Y B}
H5 : {nat X}
H6 : {nat Y}
H7 : {nat N}*
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < case H2 (keep).
```
```Subgoal 2.1:

Variables: X Y N
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat (s N)}@
H2 : {nat z}@@
H3 : {lt X (s N)}
H4 : {lt Y z}
H5 : {nat X}
H6 : {nat Y}
H7 : {nat N}*
============================
exists Z, {nat Z} /\ {gcd X Y Z}

Subgoal 2.2 is:
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < case H4.
```
```Subgoal 2.2:

Variables: X Y N N1
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat (s N)}@
H2 : {nat (s N1)}@@
H3 : {lt X (s N)}
H4 : {lt Y (s N1)}
H5 : {nat X}
H6 : {nat Y}
H7 : {nat N}*
H8 : {nat N1}**
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < apply IH to H7 H2.
```
```Subgoal 2.2:

Variables: X Y N N1
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat (s N)}@
H2 : {nat (s N1)}@@
H3 : {lt X (s N)}
H4 : {lt Y (s N1)}
H5 : {nat X}
H6 : {nat Y}
H7 : {nat N}*
H8 : {nat N1}**
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < apply IH1 to H1 H8.
```
```Subgoal 2.2:

Variables: X Y N N1
IH : forall A B, {nat A}* -> {nat B} ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
IH1 : forall A B, {nat A}@ -> {nat B}** ->
(forall X Y, {lt X A} -> {lt Y B} ->
(exists Z, {nat Z} /\ {gcd X Y Z}))
H1 : {nat (s N)}@
H2 : {nat (s N1)}@@
H3 : {lt X (s N)}
H4 : {lt Y (s N1)}
H5 : {nat X}
H6 : {nat Y}
H7 : {nat N}*
H8 : {nat N1}**
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < clear IH IH1 H1 H2 H7 H8.
```
```Subgoal 2.2:

Variables: X Y N N1
H3 : {lt X (s N)}
H4 : {lt Y (s N1)}
H5 : {nat X}
H6 : {nat Y}
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total_strong < case H3.
```
```Subgoal 2.2.1:

Variables: Y N N1
H4 : {lt Y (s N1)}
H5 : {nat z}
H6 : {nat Y}
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
============================
exists Z, {nat Z} /\ {gcd z Y Z}

Subgoal 2.2.2 is:
exists Z, {nat Z} /\ {gcd (s X1) Y Z}

gcd_total_strong < search.
```
```Subgoal 2.2.2:

Variables: Y N N1 X1
H4 : {lt Y (s N1)}
H5 : {nat (s X1)}
H6 : {nat Y}
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
============================
exists Z, {nat Z} /\ {gcd (s X1) Y Z}

gcd_total_strong < case H4.
```
```Subgoal 2.2.2.1:

Variables: N N1 X1
H5 : {nat (s X1)}
H6 : {nat z}
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
============================
exists Z, {nat Z} /\ {gcd (s X1) z Z}

Subgoal 2.2.2.2 is:
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < search.
```
```Subgoal 2.2.2.2:

Variables: N N1 X1 X2
H5 : {nat (s X1)}
H6 : {nat (s X2)}
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < case H5.
```
```Subgoal 2.2.2.2:

Variables: N N1 X1 X2
H6 : {nat (s X2)}
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < case H6.
```
```Subgoal 2.2.2.2:

Variables: N N1 X1 X2
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply less_total to H13 H14.
```
```Subgoal 2.2.2.2:

Variables: N N1 X1 X2 B1
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H15 : {bool B1}
H16 : {less X1 X2 B1}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < case H15.
```
```Subgoal 2.2.2.2.1:

Variables: N N1 X1 X2
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 tt}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

Subgoal 2.2.2.2.2 is:
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply sub_total_tt to H16.
```
```Subgoal 2.2.2.2.1:

Variables: N N1 X1 X2 Z
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 tt}
H17 : {sub X2 X1 Z}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

Subgoal 2.2.2.2.2 is:
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply sub_lt to H14 H17.
```
```Subgoal 2.2.2.2.1:

Variables: N N1 X1 X2 Z
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 tt}
H17 : {sub X2 X1 Z}
H18 : {lt Z (s X2)}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

Subgoal 2.2.2.2.2 is:
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply lt_trans to H18 H12.
```
```Subgoal 2.2.2.2.1:

Variables: N N1 X1 X2 Z
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 tt}
H17 : {sub X2 X1 Z}
H18 : {lt Z (s X2)}
H19 : {lt Z N1}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

Subgoal 2.2.2.2.2 is:
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply H10 to _ H19 with X = s X1.
```
```Subgoal 2.2.2.2.1:

Variables: N N1 X1 X2 Z Z1
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 tt}
H17 : {sub X2 X1 Z}
H18 : {lt Z (s X2)}
H19 : {lt Z N1}
H20 : {nat Z1}
H21 : {gcd (s X1) Z Z1}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

Subgoal 2.2.2.2.2 is:
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < search.
```
```Subgoal 2.2.2.2.2:

Variables: N N1 X1 X2
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 ff}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply sub_total_ff to H16.
```
```Subgoal 2.2.2.2.2:

Variables: N N1 X1 X2 Z
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 ff}
H17 : {sub X1 X2 Z}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply sub_lt to H13 H17.
```
```Subgoal 2.2.2.2.2:

Variables: N N1 X1 X2 Z
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 ff}
H17 : {sub X1 X2 Z}
H18 : {lt Z (s X1)}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply lt_trans to H18 H11.
```
```Subgoal 2.2.2.2.2:

Variables: N N1 X1 X2 Z
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 ff}
H17 : {sub X1 X2 Z}
H18 : {lt Z (s X1)}
H19 : {lt Z N}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < apply H9 to H19 _ with Y = s X2.
```
```Subgoal 2.2.2.2.2:

Variables: N N1 X1 X2 Z Z1
H9 : forall X Y, {lt X N} -> {lt Y (s N1)} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H10 : forall X Y, {lt X (s N)} -> {lt Y N1} ->
(exists Z, {nat Z} /\ {gcd X Y Z})
H11 : {lt X1 N}
H12 : {lt X2 N1}
H13 : {nat X1}
H14 : {nat X2}
H16 : {less X1 X2 ff}
H17 : {sub X1 X2 Z}
H18 : {lt Z (s X1)}
H19 : {lt Z N}
H20 : {nat Z1}
H21 : {gcd Z (s X2) Z1}
============================
exists Z, {nat Z} /\ {gcd (s X1) (s X2) Z}

gcd_total_strong < search.
Proof completed.
```
```Abella < Theorem gcd_total :
forall X Y, {nat X} -> {nat Y} -> (exists Z, {nat Z} /\ {gcd X Y Z}).

```
```
============================
forall X Y, {nat X} -> {nat Y} -> (exists Z, {nat Z} /\ {gcd X Y Z})

gcd_total < intros.
```
```
Variables: X Y
H1 : {nat X}
H2 : {nat Y}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total < assert {nat (s X)}.
```
```
Variables: X Y
H1 : {nat X}
H2 : {nat Y}
H3 : {nat (s X)}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total < assert {nat (s Y)}.
```
```
Variables: X Y
H1 : {nat X}
H2 : {nat Y}
H3 : {nat (s X)}
H4 : {nat (s Y)}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total < apply gcd_total_strong to H3 H4.
```
```
Variables: X Y
H1 : {nat X}
H2 : {nat Y}
H3 : {nat (s X)}
H4 : {nat (s Y)}
H5 : forall X1 Y1, {lt X1 (s X)} -> {lt Y1 (s Y)} ->
(exists Z, {nat Z} /\ {gcd X1 Y1 Z})
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total < apply lt_x_sx to H1.
```
```
Variables: X Y
H1 : {nat X}
H2 : {nat Y}
H3 : {nat (s X)}
H4 : {nat (s Y)}
H5 : forall X1 Y1, {lt X1 (s X)} -> {lt Y1 (s Y)} ->
(exists Z, {nat Z} /\ {gcd X1 Y1 Z})
H6 : {lt X (s X)}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total < apply lt_x_sx to H2.
```
```
Variables: X Y
H1 : {nat X}
H2 : {nat Y}
H3 : {nat (s X)}
H4 : {nat (s Y)}
H5 : forall X1 Y1, {lt X1 (s X)} -> {lt Y1 (s Y)} ->
(exists Z, {nat Z} /\ {gcd X1 Y1 Z})
H6 : {lt X (s X)}
H7 : {lt Y (s Y)}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total < apply H5 to H6 H7.
```
```
Variables: X Y Z
H1 : {nat X}
H2 : {nat Y}
H3 : {nat (s X)}
H4 : {nat (s Y)}
H5 : forall X1 Y1, {lt X1 (s X)} -> {lt Y1 (s Y)} ->
(exists Z, {nat Z} /\ {gcd X1 Y1 Z})
H6 : {lt X (s X)}
H7 : {lt Y (s Y)}
H8 : {nat Z}
H9 : {gcd X Y Z}
============================
exists Z, {nat Z} /\ {gcd X Y Z}

gcd_total < search.
Proof completed.
```
```Abella <
```