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

```
```Abella < Theorem add_base :
forall N, {nat N} -> {add N z N}.

```
```
============================
forall N, {nat N} -> {add N z N}

```
```
IH : forall N, {nat N}* -> {add N z N}
============================
forall N, {nat N}@ -> {add N z N}

```
```
Variables: N
IH : forall N, {nat N}* -> {add N z N}
H1 : {nat N}@
============================

```
```Subgoal 1:

IH : forall N, {nat N}* -> {add N z N}
============================

Subgoal 2 is:
{add (s N1) z (s N1)}

```
```Subgoal 2:

Variables: N1
IH : forall N, {nat N}* -> {add N z N}
H2 : {nat N1}*
============================
{add (s N1) z (s N1)}

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

Variables: N1
IH : forall N, {nat N}* -> {add N z N}
H2 : {nat N1}*
H3 : {add N1 z N1}
============================
{add (s N1) z (s N1)}

Proof completed.
```
```Abella < Theorem add_step :
forall A B C, {add A B C} -> {add A (s B) (s C)}.

```
```
============================
forall A B C, {add A B C} -> {add A (s B) (s C)}

```
```
IH : forall A B C, {add A B C}* -> {add A (s B) (s C)}
============================
forall A B C, {add A B C}@ -> {add A (s B) (s C)}

```
```
Variables: A B C
IH : forall A B C, {add A B C}* -> {add A (s B) (s C)}
H1 : {add A B C}@
============================
{add A (s B) (s C)}

```
```Subgoal 1:

Variables: C
IH : forall A B C, {add A B C}* -> {add A (s B) (s C)}
============================
{add z (s C) (s C)}

Subgoal 2 is:
{add (s A1) (s B) (s (s C1))}

```
```Subgoal 2:

Variables: B C1 A1
IH : forall A B C, {add A B C}* -> {add A (s B) (s C)}
H2 : {add A1 B C1}*
============================
{add (s A1) (s B) (s (s C1))}

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

Variables: B C1 A1
IH : forall A B C, {add A B C}* -> {add A (s B) (s C)}
H2 : {add A1 B C1}*
H3 : {add A1 (s B) (s C1)}
============================
{add (s A1) (s B) (s (s C1))}

Proof completed.
```
```Abella < Theorem add_comm :
forall A B C, {nat B} -> {add A B C} -> {add B A C}.

```
```
============================
forall A B C, {nat B} -> {add A B C} -> {add B A C}

```
```
IH : forall A B C, {nat B} -> {add A B C}* -> {add B A C}
============================
forall A B C, {nat B} -> {add A B C}@ -> {add B A C}

```
```
Variables: A B C
IH : forall A B C, {nat B} -> {add A B C}* -> {add B A C}
H1 : {nat B}
H2 : {add A B C}@
============================

```
```Subgoal 1:

Variables: C
IH : forall A B C, {nat B} -> {add A B C}* -> {add B A C}
H1 : {nat C}
============================

Subgoal 2 is:
{add B (s A1) (s C1)}

```
```Subgoal 1:

Variables: C
IH : forall A B C, {nat B} -> {add A B C}* -> {add B A C}
H1 : {nat C}
H3 : {add C z C}
============================

Subgoal 2 is:
{add B (s A1) (s C1)}

```
```Subgoal 2:

Variables: B C1 A1
IH : forall A B C, {nat B} -> {add A B C}* -> {add B A C}
H1 : {nat B}
H3 : {add A1 B C1}*
============================
{add B (s A1) (s C1)}

add_comm < apply IH to H1 H3.
```
```Subgoal 2:

Variables: B C1 A1
IH : forall A B C, {nat B} -> {add A B C}* -> {add B A C}
H1 : {nat B}
H3 : {add A1 B C1}*
H4 : {add B A1 C1}
============================
{add B (s A1) (s C1)}

```
```Subgoal 2:

Variables: B C1 A1
IH : forall A B C, {nat B} -> {add A B C}* -> {add B A C}
H1 : {nat B}
H3 : {add A1 B C1}*
H4 : {add B A1 C1}
H5 : {add B (s A1) (s C1)}
============================
{add B (s A1) (s C1)}

Proof completed.
```
```Abella < Theorem add_det :
forall A B C D, {add A B C} -> {add A B D} -> C = D.

```
```
============================
forall A B C D, {add A B C} -> {add A B D} -> C = D

```
```
IH : forall A B C D, {add A B C}* -> {add A B D} -> C = D
============================
forall A B C D, {add A B C}@ -> {add A B D} -> C = D

```
```
Variables: A B C D
IH : forall A B C D, {add A B C}* -> {add A B D} -> C = D
H1 : {add A B C}@
H2 : {add A B D}
============================
C = D

```
```Subgoal 1:

Variables: C D
IH : forall A B C D, {add A B C}* -> {add A B D} -> C = D
H2 : {add z C D}
============================
C = D

Subgoal 2 is:
s C1 = D

```
```Subgoal 1:

Variables: D
IH : forall A B C D, {add A B C}* -> {add A B D} -> C = D
============================
D = D

Subgoal 2 is:
s C1 = D

```
```Subgoal 2:

Variables: B D C1 A1
IH : forall A B C D, {add A B C}* -> {add A B D} -> C = D
H2 : {add (s A1) B D}
H3 : {add A1 B C1}*
============================
s C1 = D

```
```Subgoal 2:

Variables: B C1 A1 C2
IH : forall A B C D, {add A B C}* -> {add A B D} -> C = D
H3 : {add A1 B C1}*
H4 : {add A1 B C2}
============================
s C1 = s C2

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

Variables: B A1 C2
IH : forall A B C D, {add A B C}* -> {add A B D} -> C = D
H3 : {add A1 B C2}*
H4 : {add A1 B C2}
============================
s C2 = s C2

Proof completed.
```
```Abella < Theorem add_assoc :
forall A B C AB ABC, {add A B AB} -> {add AB C ABC} ->

```
```
============================
forall A B C AB ABC, {add A B AB} -> {add AB C ABC} ->

```
```
IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
============================
forall A B C AB ABC, {add A B AB}@ -> {add AB C ABC} ->

```
```
Variables: A B C AB ABC
IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
H1 : {add A B AB}@
H2 : {add AB C ABC}
============================

```
```Subgoal 1:

Variables: C AB ABC
IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
H2 : {add AB C ABC}
============================

Subgoal 2 is:
exists BC, {add B C BC} /\ {add (s A1) BC ABC}

```
```Subgoal 2:

Variables: B C ABC C1 A1
IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
H2 : {add (s C1) C ABC}
H3 : {add A1 B C1}*
============================
exists BC, {add B C BC} /\ {add (s A1) BC ABC}

```
```Subgoal 2:

Variables: B C C1 A1 C2
IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
H3 : {add A1 B C1}*
H4 : {add C1 C C2}
============================
exists BC, {add B C BC} /\ {add (s A1) BC (s C2)}

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

Variables: B C C1 A1 C2 BC
IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
H3 : {add A1 B C1}*
H4 : {add C1 C C2}
H5 : {add B C BC}
H6 : {add A1 BC C2}
============================
exists BC, {add B C BC} /\ {add (s A1) BC (s C2)}

Proof completed.
```
```Abella < Query {add A B (s (s (s (s z))))}.
Found solution:
A = z
B = s (s (s (s z)))

Found solution:
A = s z
B = s (s (s z))

Found solution:
A = s (s z)
B = s (s z)

Found solution:
A = s (s (s z))
B = s z

Found solution:
A = s (s (s (s z)))
B = z

No more solutions.

```
```Abella < Query {add A A (s (s (s (s z))))}.
Found solution:
A = s (s z)

No more solutions.

```
```Abella <
```