Welcome to Abella 1.1.3-dev2 Reading clauses from add.mod

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

1 subgoal(s).

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

add_base < induction on 1.

1 subgoal(s).

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

add_base < intros.

1 subgoal(s).

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

add_base < case H1.

2 subgoal(s).

  Variables: N
  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.

1 subgoal(s).

  Variables: N, 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.

1 subgoal(s).

  Variables: N, 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)}.

1 subgoal(s).

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

add_step < induction on 1.

1 subgoal(s).

  
  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.

1 subgoal(s).

  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.

2 subgoal(s).

  Variables: A, B, 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.

1 subgoal(s).

  Variables: A, B, C, 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.

1 subgoal(s).

  Variables: A, B, C, 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}.

1 subgoal(s).

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

add_comm < induction on 2.

1 subgoal(s).

  
  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.

1 subgoal(s).

  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.

2 subgoal(s).

  Variables: A, B, 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.

2 subgoal(s).

  Variables: A, B, 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.

1 subgoal(s).

  Variables: A, B, C, 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.

1 subgoal(s).

  Variables: A, B, C, 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.

1 subgoal(s).

  Variables: A, B, C, 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.

1 subgoal(s).

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

add_det < induction on 1.

1 subgoal(s).

  
  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.

1 subgoal(s).

  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.

2 subgoal(s).

  Variables: A, B, 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.

2 subgoal(s).

  Variables: A, B, C, 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.

1 subgoal(s).

  Variables: A, B, C, 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.

1 subgoal(s).

  Variables: A, B, C, D, 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.

1 subgoal(s).

  Variables: A, B, C, D, C1, 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 BC ABC, {add A B AB} -> {add AB C ABC} -> {add B C BC} ->
  {add A BC ABC}.

1 subgoal(s).

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

add_assoc < induction on 1.

1 subgoal(s).

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

add_assoc < intros.

1 subgoal(s).

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

add_assoc < case H1.

2 subgoal(s).

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

subgoal 2 is:
 {add (s A1) BC ABC}

add_assoc < apply add_det to H2 H3.

2 subgoal(s).

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

subgoal 2 is:
 {add (s A1) BC ABC}

add_assoc < search.

1 subgoal(s).

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

add_assoc < case H2.

1 subgoal(s).

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

add_assoc < apply IH to H4 H5 H3.

1 subgoal(s).

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

add_assoc < search.
Proof completed.

Abella < Goodbye.