Welcome to Abella 2.0.5-dev.
Abella < Specification "add".
Reading specification "add".

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


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

add_base < induction on 1.

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

add_base < intros.

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

add_base < case H1.
Subgoal 1:

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

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

add_base < search.
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)}

add_base < search.
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)}

add_step < induction on 1.

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)}

add_step < intros.

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)}

add_step < case H1.
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))}

add_step < search.
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))}

add_step < search.
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}

add_comm < induction on 2.

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}

add_comm < intros.

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}@
============================
 {add B A C}

add_comm < case H2.
Subgoal 1:

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

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

add_comm < apply add_base to H1.
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}
============================
 {add C z C}

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

add_comm < search.
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)}

add_comm < apply add_step to H4.
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)}

add_comm < search.
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

add_det < induction on 1.

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

add_det < intros.

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

add_det < case H1.
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

add_det < case H2.
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

add_det < search.
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

add_det < case H2.
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

add_det < search.
Proof completed.
Abella < Theorem add_assoc : 
forall A B C AB ABC, {add A B AB} -> {add AB C ABC} ->
  (exists BC, {add B C BC} /\ {add A BC ABC}).


============================
 forall A B C AB ABC, {add A B AB} -> {add AB C ABC} ->
   (exists BC, {add B C BC} /\ {add A BC ABC})

add_assoc < induction on 1.

IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
       (exists BC, {add B C BC} /\ {add A BC ABC})
============================
 forall A B C AB ABC, {add A B AB}@ -> {add AB C ABC} ->
   (exists BC, {add B C BC} /\ {add A BC ABC})

add_assoc < intros.

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

add_assoc < case H1.
Subgoal 1:

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

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

add_assoc < search.
Subgoal 2:

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

add_assoc < case H2.
Subgoal 2:

Variables: B C C1 A1 C2
IH : forall A B C AB ABC, {add A B AB}* -> {add AB C ABC} ->
       (exists BC, {add B C BC} /\ {add A BC 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} ->
       (exists BC, {add B C BC} /\ {add A BC 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)}

add_assoc < search.
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 <