Welcome to Abella 2.0.4-dev
Abella < Specification "trans".
Reading specification "trans"

Abella < Theorem add_det : 
forall N1 N2 N3 N3', {add N1 N2 N3} -> {add N1 N2 N3'} -> N3 = N3'.


============================
 forall N1 N2 N3 N3', {add N1 N2 N3} -> {add N1 N2 N3'} -> N3 = N3'

add_det < induction on 1.

IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
============================
 forall N1 N2 N3 N3', {add N1 N2 N3}@ -> {add N1 N2 N3'} -> N3 = N3'

add_det < intros.

Variables: N1 N2 N3 N3'
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H1 : {add N1 N2 N3}@
H2 : {add N1 N2 N3'}
============================
 N3 = N3'

add_det < case H1.
Subgoal 1:

Variables: N3 N3'
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H2 : {add z N3 N3'}
============================
 N3 = N3'

Subgoal 2 is:
 s N4 = N3'

add_det < case H2.
Subgoal 1:

Variables: N3'
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
============================
 N3' = N3'

Subgoal 2 is:
 s N4 = N3'

add_det < search.
Subgoal 2:

Variables: N2 N3' N4 N6
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H2 : {add (s N6) N2 N3'}
H3 : {add N6 N2 N4}*
============================
 s N4 = N3'

add_det < case H2.
Subgoal 2:

Variables: N2 N4 N6 N5
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H3 : {add N6 N2 N4}*
H4 : {add N6 N2 N5}
============================
 s N4 = s N5

add_det < apply IH to H3 H4.
Subgoal 2:

Variables: N2 N6 N5
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H3 : {add N6 N2 N5}*
H4 : {add N6 N2 N5}
============================
 s N5 = s N5

add_det < search.
Proof completed.
Abella < Define le : nat -> nat -> prop by 
le N1 N2 := exists N, {add N1 N N2}.

Abella < Define lt : nat -> nat -> prop by 
lt N1 N2 := exists N, {add N1 (s N) N2}.

Abella < Theorem lt_to_le : 
forall N1 N2, lt N1 N2 -> le N1 N2.


============================
 forall N1 N2, lt N1 N2 -> le N1 N2

lt_to_le < intros.

Variables: N1 N2
H1 : lt N1 N2
============================
 le N1 N2

lt_to_le < case H1.

Variables: N1 N2 N
H2 : {add N1 (s N) N2}
============================
 le N1 N2

lt_to_le < search.
Proof completed.
Abella < Theorem le_refl : 
forall N, {is_nat N} -> le N N.


============================
 forall N, {is_nat N} -> le N N

le_refl < induction on 1.

IH : forall N, {is_nat N}* -> le N N
============================
 forall N, {is_nat N}@ -> le N N

le_refl < intros.

Variables: N
IH : forall N, {is_nat N}* -> le N N
H1 : {is_nat N}@
============================
 le N N

le_refl < case H1.
Subgoal 1:

IH : forall N, {is_nat N}* -> le N N
============================
 le z z

Subgoal 2 is:
 le (s N1) (s N1)

le_refl < search.
Subgoal 2:

Variables: N1
IH : forall N, {is_nat N}* -> le N N
H2 : {is_nat N1}*
============================
 le (s N1) (s N1)

le_refl < apply IH to H2.
Subgoal 2:

Variables: N1
IH : forall N, {is_nat N}* -> le N N
H2 : {is_nat N1}*
H3 : le N1 N1
============================
 le (s N1) (s N1)

le_refl < case H3.
Subgoal 2:

Variables: N1 N2
IH : forall N, {is_nat N}* -> le N N
H2 : {is_nat N1}*
H4 : {add N1 N2 N1}
============================
 le (s N1) (s N1)

le_refl < search.
Proof completed.
Abella < Theorem le_z : 
forall N, le N z -> N = z.


============================
 forall N, le N z -> N = z

le_z < intros.

Variables: N
H1 : le N z
============================
 N = z

le_z < case H1.

Variables: N N1
H2 : {add N N1 z}
============================
 N = z

le_z < case H2.

============================
 z = z

le_z < search.
Proof completed.
Abella < Theorem add_result_isnat : 
forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3} -> {is_nat N3}.


============================
 forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3} -> {is_nat N3}

add_result_isnat < induction on 2.

IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
============================
 forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}@ -> {is_nat N3}

add_result_isnat < intros.

Variables: N1 N2 N3
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N2}
H2 : {add N1 N2 N3}@
============================
 {is_nat N3}

add_result_isnat < case H2.
Subgoal 1:

Variables: N3
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N3}
============================
 {is_nat N3}

Subgoal 2 is:
 {is_nat (s N4)}

add_result_isnat < search.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N2}
H3 : {add N6 N2 N4}*
============================
 {is_nat (s N4)}

add_result_isnat < apply IH to H1 H3.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N2}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
============================
 {is_nat (s N4)}

add_result_isnat < search.
Proof completed.
Abella < Theorem add_arg2_isnat : 
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {is_nat N2}.


============================
 forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {is_nat N2}

add_arg2_isnat < induction on 2.

IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
============================
 forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}@ -> {is_nat N2}

add_arg2_isnat < intros.

Variables: N1 N2 N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H1 : {is_nat N3}
H2 : {add N1 N2 N3}@
============================
 {is_nat N2}

add_arg2_isnat < case H2.
Subgoal 1:

Variables: N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H1 : {is_nat N3}
============================
 {is_nat N3}

Subgoal 2 is:
 {is_nat N2}

add_arg2_isnat < search.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H1 : {is_nat (s N4)}
H3 : {add N6 N2 N4}*
============================
 {is_nat N2}

add_arg2_isnat < case H1.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
============================
 {is_nat N2}

add_arg2_isnat < backchain IH.
Proof completed.
Abella < Theorem add_arg2_det : 
forall N1 N2 N2' N3, {add N1 N2 N3} -> {add N1 N2' N3} -> N2 = N2'.


============================
 forall N1 N2 N2' N3, {add N1 N2 N3} -> {add N1 N2' N3} -> N2 = N2'

add_arg2_det < induction on 1.

IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
============================
 forall N1 N2 N2' N3, {add N1 N2 N3}@ -> {add N1 N2' N3} -> N2 = N2'

add_arg2_det < intros.

Variables: N1 N2 N2' N3
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H1 : {add N1 N2 N3}@
H2 : {add N1 N2' N3}
============================
 N2 = N2'

add_arg2_det < case H1.
Subgoal 1:

Variables: N2' N3
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H2 : {add z N2' N3}
============================
 N3 = N2'

Subgoal 2 is:
 N2 = N2'

add_arg2_det < case H2.
Subgoal 1:

Variables: N3
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
============================
 N3 = N3

Subgoal 2 is:
 N2 = N2'

add_arg2_det < search.
Subgoal 2:

Variables: N2 N2' N4 N6
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H2 : {add (s N6) N2' (s N4)}
H3 : {add N6 N2 N4}*
============================
 N2 = N2'

add_arg2_det < case H2.
Subgoal 2:

Variables: N2 N2' N4 N6
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H3 : {add N6 N2 N4}*
H4 : {add N6 N2' N4}
============================
 N2 = N2'

add_arg2_det < backchain IH.
Proof completed.
Abella < Theorem add_arg1_isnat : 
forall N1 N2 N3, {add N1 N2 N3} -> {is_nat N1}.


============================
 forall N1 N2 N3, {add N1 N2 N3} -> {is_nat N1}

add_arg1_isnat < induction on 1.

IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
============================
 forall N1 N2 N3, {add N1 N2 N3}@ -> {is_nat N1}

add_arg1_isnat < intros.

Variables: N1 N2 N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
H1 : {add N1 N2 N3}@
============================
 {is_nat N1}

add_arg1_isnat < case H1.
Subgoal 1:

Variables: N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
============================
 {is_nat z}

Subgoal 2 is:
 {is_nat (s N6)}

add_arg1_isnat < search.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
H2 : {add N6 N2 N4}*
============================
 {is_nat (s N6)}

add_arg1_isnat < apply IH to H2.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
H2 : {add N6 N2 N4}*
H3 : {is_nat N6}
============================
 {is_nat (s N6)}

add_arg1_isnat < search.
Proof completed.
Abella < Theorem add_s : 
forall N1 N2 N3, {add N1 N2 N3} -> {add N1 (s N2) (s N3)}.


============================
 forall N1 N2 N3, {add N1 N2 N3} -> {add N1 (s N2) (s N3)}

add_s < induction on 1.

IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
============================
 forall N1 N2 N3, {add N1 N2 N3}@ -> {add N1 (s N2) (s N3)}

add_s < intros.

Variables: N1 N2 N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
H1 : {add N1 N2 N3}@
============================
 {add N1 (s N2) (s N3)}

add_s < case H1.
Subgoal 1:

Variables: N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
============================
 {add z (s N3) (s N3)}

Subgoal 2 is:
 {add (s N6) (s N2) (s (s N4))}

add_s < search.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
H2 : {add N6 N2 N4}*
============================
 {add (s N6) (s N2) (s (s N4))}

add_s < apply IH to H2.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
H2 : {add N6 N2 N4}*
H3 : {add N6 (s N2) (s N4)}
============================
 {add (s N6) (s N2) (s (s N4))}

add_s < search.
Proof completed.
Abella < Theorem add_s_inv : 
forall N1 N2 N3, {add N1 (s N2) (s N3)} -> {add N1 N2 N3}.


============================
 forall N1 N2 N3, {add N1 (s N2) (s N3)} -> {add N1 N2 N3}

add_s_inv < induction on 1.

IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
============================
 forall N1 N2 N3, {add N1 (s N2) (s N3)}@ -> {add N1 N2 N3}

add_s_inv < intros.

Variables: N1 N2 N3
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H1 : {add N1 (s N2) (s N3)}@
============================
 {add N1 N2 N3}

add_s_inv < case H1.
Subgoal 1:

Variables: N3
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
============================
 {add z N3 N3}

Subgoal 2 is:
 {add (s N6) N2 N3}

add_s_inv < search.
Subgoal 2:

Variables: N2 N3 N6
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H2 : {add N6 (s N2) N3}*
============================
 {add (s N6) N2 N3}

add_s_inv < case H2 (keep).
Subgoal 2.1:

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

Subgoal 2.2 is:
 {add (s (s N7)) N2 (s N4)}

add_s_inv < search.
Subgoal 2.2:

Variables: N2 N4 N7
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H2 : {add (s N7) (s N2) (s N4)}*
H3 : {add N7 (s N2) N4}*
============================
 {add (s (s N7)) N2 (s N4)}

add_s_inv < apply IH to H2.
Subgoal 2.2:

Variables: N2 N4 N7
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H2 : {add (s N7) (s N2) (s N4)}*
H3 : {add N7 (s N2) N4}*
H4 : {add (s N7) N2 N4}
============================
 {add (s (s N7)) N2 (s N4)}

add_s_inv < search.
Proof completed.
Abella < Theorem add_z : 
forall N, {is_nat N} -> {add N z N}.


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

add_z < induction on 1.

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

add_z < intros.

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

add_z < case H1.
Subgoal 1:

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

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

add_z < search.
Subgoal 2:

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

add_z < apply IH to H2.
Subgoal 2:

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

add_z < search.
Proof completed.
Abella < Theorem add_comm : 
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {add N2 N1 N3}.


============================
 forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {add N2 N1 N3}

add_comm < induction on 2.

IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
============================
 forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}@ -> {add N2 N1 N3}

add_comm < intros.

Variables: N1 N2 N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H1 : {is_nat N3}
H2 : {add N1 N2 N3}@
============================
 {add N2 N1 N3}

add_comm < case H2.
Subgoal 1:

Variables: N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H1 : {is_nat N3}
============================
 {add N3 z N3}

Subgoal 2 is:
 {add N2 (s N6) (s N4)}

add_comm < backchain add_z.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H1 : {is_nat (s N4)}
H3 : {add N6 N2 N4}*
============================
 {add N2 (s N6) (s N4)}

add_comm < case H1.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
============================
 {add N2 (s N6) (s N4)}

add_comm < apply IH to _ H3.
Subgoal 2:

Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
H5 : {add N2 N6 N4}
============================
 {add N2 (s N6) (s N4)}

add_comm < backchain add_s.
Proof completed.
Abella < Theorem add_assoc : 
forall N1 N2 N3 N12 N123, {add N1 N2 N12} -> {add N12 N3 N123} ->
  (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123}).


============================
 forall N1 N2 N3 N12 N123, {add N1 N2 N12} -> {add N12 N3 N123} ->
   (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})

add_assoc < induction on 1.

IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
       (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
============================
 forall N1 N2 N3 N12 N123, {add N1 N2 N12}@ -> {add N12 N3 N123} ->
   (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})

add_assoc < intros.

Variables: N1 N2 N3 N12 N123
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
       (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H1 : {add N1 N2 N12}@
H2 : {add N12 N3 N123}
============================
 exists N23, {add N2 N3 N23} /\ {add N1 N23 N123}

add_assoc < case H1.
Subgoal 1:

Variables: N3 N12 N123
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
       (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H2 : {add N12 N3 N123}
============================
 exists N23, {add N12 N3 N23} /\ {add z N23 N123}

Subgoal 2 is:
 exists N23, {add N2 N3 N23} /\ {add (s N6) N23 N123}

add_assoc < search.
Subgoal 2:

Variables: N2 N3 N123 N4 N6
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
       (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H2 : {add (s N4) N3 N123}
H3 : {add N6 N2 N4}*
============================
 exists N23, {add N2 N3 N23} /\ {add (s N6) N23 N123}

add_assoc < case H2.
Subgoal 2:

Variables: N2 N3 N4 N6 N5
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
       (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H3 : {add N6 N2 N4}*
H4 : {add N4 N3 N5}
============================
 exists N23, {add N2 N3 N23} /\ {add (s N6) N23 (s N5)}

add_assoc < apply IH to H3 H4.
Subgoal 2:

Variables: N2 N3 N4 N6 N5 N23
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
       (exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H3 : {add N6 N2 N4}*
H4 : {add N4 N3 N5}
H5 : {add N2 N3 N23}
H6 : {add N6 N23 N5}
============================
 exists N23, {add N2 N3 N23} /\ {add (s N6) N23 (s N5)}

add_assoc < search.
Proof completed.
Abella < Theorem add_assoc' : 
forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123} ->
  (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123}).


============================
 forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123} ->
   (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})

add_assoc' < induction on 2.

IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
============================
 forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
   (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})

add_assoc' < intros.

Variables: N1 N2 N3 N23 N123
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
============================
 exists N12, {add N1 N2 N12} /\ {add N12 N3 N123}

add_assoc' < case H2.
Subgoal 1:

Variables: N2 N3 N123
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N123}
============================
 exists N12, {add z N2 N12} /\ {add N12 N3 N123}

Subgoal 2 is:
 exists N12, {add (s N6) N2 N12} /\ {add N12 N3 (s N4)}

add_assoc' < search.
Subgoal 2:

Variables: N2 N3 N23 N4 N6
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N23}
H3 : {add N6 N23 N4}*
============================
 exists N12, {add (s N6) N2 N12} /\ {add N12 N3 (s N4)}

add_assoc' < apply IH to _ H3.
Subgoal 2:

Variables: N2 N3 N23 N4 N6 N12
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       (exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N23}
H3 : {add N6 N23 N4}*
H4 : {add N6 N2 N12}
H5 : {add N12 N3 N4}
============================
 exists N12, {add (s N6) N2 N12} /\ {add N12 N3 (s N4)}

add_assoc' < search.
Proof completed.
Abella < Theorem le_to_lt : 
forall N1 N2, {is_nat N2} -> le N1 N2 -> N1 = N2 \/ lt N1 N2.


============================
 forall N1 N2, {is_nat N2} -> le N1 N2 -> N1 = N2 \/ lt N1 N2

le_to_lt < intros.

Variables: N1 N2
H1 : {is_nat N2}
H2 : le N1 N2
============================
 N1 = N2 \/ lt N1 N2

le_to_lt < case H2.

Variables: N1 N2 N
H1 : {is_nat N2}
H3 : {add N1 N N2}
============================
 N1 = N2 \/ lt N1 N2

le_to_lt < apply add_comm to _ H3.

Variables: N1 N2 N
H1 : {is_nat N2}
H3 : {add N1 N N2}
H4 : {add N N1 N2}
============================
 N1 = N2 \/ lt N1 N2

le_to_lt < case H4.
Subgoal 1:

Variables: N2
H1 : {is_nat N2}
H3 : {add N2 z N2}
============================
 N2 = N2 \/ lt N2 N2

Subgoal 2 is:
 N1 = s N3 \/ lt N1 (s N3)

le_to_lt < search.
Subgoal 2:

Variables: N1 N3 N5
H1 : {is_nat (s N3)}
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
============================
 N1 = s N3 \/ lt N1 (s N3)

le_to_lt < apply add_comm to _ H5.
Subgoal 2.1:

Variables: N1 N3 N5
H1 : {is_nat (s N3)}
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
============================
 {is_nat N3}

Subgoal 2 is:
 N1 = s N3 \/ lt N1 (s N3)

le_to_lt < case H1.
Subgoal 2.1:

Variables: N1 N3 N5
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
H6 : {is_nat N3}
============================
 {is_nat N3}

Subgoal 2 is:
 N1 = s N3 \/ lt N1 (s N3)

le_to_lt < search.
Subgoal 2:

Variables: N1 N3 N5
H1 : {is_nat (s N3)}
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
H6 : {add N1 N5 N3}
============================
 N1 = s N3 \/ lt N1 (s N3)

le_to_lt < search.
Proof completed.
Abella < Theorem lt_pred_le : 
forall I J, {is_nat J} -> lt I (s J) -> le I J.


============================
 forall I J, {is_nat J} -> lt I (s J) -> le I J

lt_pred_le < intros.

Variables: I J
H1 : {is_nat J}
H2 : lt I (s J)
============================
 le I J

lt_pred_le < case H2.

Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
============================
 le I J

lt_pred_le < apply add_comm to _ H3.

Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
H4 : {add (s N) I (s J)}
============================
 le I J

lt_pred_le < case H4.

Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
H5 : {add N I J}
============================
 le I J

lt_pred_le < apply add_comm to _ H5.

Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
H5 : {add N I J}
H6 : {add I N J}
============================
 le I J

lt_pred_le < search.
Proof completed.
Abella < Theorem lt_z_absurd : 
forall I, lt I z -> false.


============================
 forall I, lt I z -> false

lt_z_absurd < intros.

Variables: I
H1 : lt I z
============================
 false

lt_z_absurd < case H1.

Variables: I N
H2 : {add I (s N) z}
============================
 false

lt_z_absurd < apply add_comm to _ H2.

Variables: I N
H2 : {add I (s N) z}
H3 : {add (s N) I z}
============================
 false

lt_z_absurd < case H3.
Proof completed.
Abella < Theorem le_succ : 
forall I J, le I J -> le I (s J).


============================
 forall I J, le I J -> le I (s J)

le_succ < intros.

Variables: I J
H1 : le I J
============================
 le I (s J)

le_succ < case H1.

Variables: I J N
H2 : {add I N J}
============================
 le I (s J)

le_succ < unfold.

Variables: I J N
H2 : {add I N J}
============================
 exists N, {add I N (s J)}

le_succ < exists s N.

Variables: I J N
H2 : {add I N J}
============================
 {add I (s N) (s J)}

le_succ < backchain add_s.
Proof completed.
Abella < Theorem le_extend : 
forall I J, le I J -> le (s I) (s J).


============================
 forall I J, le I J -> le (s I) (s J)

le_extend < intros.

Variables: I J
H1 : le I J
============================
 le (s I) (s J)

le_extend < case H1.

Variables: I J N
H2 : {add I N J}
============================
 le (s I) (s J)

le_extend < unfold.

Variables: I J N
H2 : {add I N J}
============================
 exists N, {add (s I) N (s J)}

le_extend < exists N.

Variables: I J N
H2 : {add I N J}
============================
 {add (s I) N (s J)}

le_extend < search.
Proof completed.
Abella < Theorem le_to_lt_s : 
forall N1 N2, le N1 N2 -> lt N1 (s N2).


============================
 forall N1 N2, le N1 N2 -> lt N1 (s N2)

le_to_lt_s < intros.

Variables: N1 N2
H1 : le N1 N2
============================
 lt N1 (s N2)

le_to_lt_s < case H1.

Variables: N1 N2 N
H2 : {add N1 N N2}
============================
 lt N1 (s N2)

le_to_lt_s < unfold.

Variables: N1 N2 N
H2 : {add N1 N N2}
============================
 exists N, {add N1 (s N) (s N2)}

le_to_lt_s < exists N.

Variables: N1 N2 N
H2 : {add N1 N N2}
============================
 {add N1 (s N) (s N2)}

le_to_lt_s < backchain add_s.
Proof completed.
Abella < Theorem le_trans : 
forall N1 N2 N3, le N1 N2 -> le N2 N3 -> le N1 N3.


============================
 forall N1 N2 N3, le N1 N2 -> le N2 N3 -> le N1 N3

le_trans < intros.

Variables: N1 N2 N3
H1 : le N1 N2
H2 : le N2 N3
============================
 le N1 N3

le_trans < case H1.

Variables: N1 N2 N3 N
H2 : le N2 N3
H3 : {add N1 N N2}
============================
 le N1 N3

le_trans < case H2.

Variables: N1 N2 N3 N N4
H3 : {add N1 N N2}
H4 : {add N2 N4 N3}
============================
 le N1 N3

le_trans < unfold.

Variables: N1 N2 N3 N N4
H3 : {add N1 N N2}
H4 : {add N2 N4 N3}
============================
 exists N, {add N1 N N3}

le_trans < apply add_assoc to H3 H4.

Variables: N1 N2 N3 N N4 N23
H3 : {add N1 N N2}
H4 : {add N2 N4 N3}
H5 : {add N N4 N23}
H6 : {add N1 N23 N3}
============================
 exists N, {add N1 N N3}

le_trans < search.
Proof completed.
Abella < Theorem lt_le_compose : 
forall N1 N2 N3, lt N1 N2 -> le N2 N3 -> lt N1 N3.


============================
 forall N1 N2 N3, lt N1 N2 -> le N2 N3 -> lt N1 N3

lt_le_compose < intros.

Variables: N1 N2 N3
H1 : lt N1 N2
H2 : le N2 N3
============================
 lt N1 N3

lt_le_compose < case H1.

Variables: N1 N2 N3 N
H2 : le N2 N3
H3 : {add N1 (s N) N2}
============================
 lt N1 N3

lt_le_compose < case H2.

Variables: N1 N2 N3 N N4
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
============================
 lt N1 N3

lt_le_compose < unfold.

Variables: N1 N2 N3 N N4
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
============================
 exists N, {add N1 (s N) N3}

lt_le_compose < apply add_assoc to H3 H4.

Variables: N1 N2 N3 N N4 N23
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
H5 : {add (s N) N4 N23}
H6 : {add N1 N23 N3}
============================
 exists N, {add N1 (s N) N3}

lt_le_compose < case H5.

Variables: N1 N2 N3 N N4 N5
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
H6 : {add N1 (s N5) N3}
H7 : {add N N4 N5}
============================
 exists N, {add N1 (s N) N3}

lt_le_compose < search.
Proof completed.
Abella < Theorem add_result_le_to_arg1_le : 
forall N1 N2 N2' J K, {add N1 N2 J} -> {add N1 N2' K} -> le J K -> le N2 N2'.


============================
 forall N1 N2 N2' J K, {add N1 N2 J} -> {add N1 N2' K} -> le J K -> le N2 N2'

add_result_le_to_arg1_le < induction on 1.

IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
============================
 forall N1 N2 N2' J K, {add N1 N2 J}@ -> {add N1 N2' K} -> le J K ->
   le N2 N2'

add_result_le_to_arg1_le < intros.

Variables: N1 N2 N2' J K
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H1 : {add N1 N2 J}@
H2 : {add N1 N2' K}
H3 : le J K
============================
 le N2 N2'

add_result_le_to_arg1_le < case H1.
Subgoal 1:

Variables: N2' J K
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H2 : {add z N2' K}
H3 : le J K
============================
 le J N2'

Subgoal 2 is:
 le N2 N2'

add_result_le_to_arg1_le < case H2.
Subgoal 1:

Variables: J K
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H3 : le J K
============================
 le J K

Subgoal 2 is:
 le N2 N2'

add_result_le_to_arg1_le < search.
Subgoal 2:

Variables: N2 N2' K N3 N5
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H2 : {add (s N5) N2' K}
H3 : le (s N3) K
H4 : {add N5 N2 N3}*
============================
 le N2 N2'

add_result_le_to_arg1_le < case H2.
Subgoal 2:

Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
============================
 le N2 N2'

add_result_le_to_arg1_le < assert le N3 N4.
Subgoal 2.1:

Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
============================
 le N3 N4

Subgoal 2 is:
 le N2 N2'

add_result_le_to_arg1_le < case H3.
Subgoal 2.1:

Variables: N2 N2' N3 N5 N4 N
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H6 : {add (s N3) N (s N4)}
============================
 le N3 N4

Subgoal 2 is:
 le N2 N2'

add_result_le_to_arg1_le < case H6.
Subgoal 2.1:

Variables: N2 N2' N3 N5 N4 N
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H7 : {add N3 N N4}
============================
 le N3 N4

Subgoal 2 is:
 le N2 N2'

add_result_le_to_arg1_le < search.
Subgoal 2:

Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H6 : le N3 N4
============================
 le N2 N2'

add_result_le_to_arg1_le < apply IH to H4 H5 H6.
Subgoal 2:

Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
       le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H6 : le N3 N4
H7 : le N2 N2'
============================
 le N2 N2'

add_result_le_to_arg1_le < search.
Proof completed.
Abella < Theorem add_le_complement : 
forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N} ->
  {add N1' N2' N} -> le N2' N2.


============================
 forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N} ->
   {add N1' N2' N} -> le N2' N2

add_le_complement < induction on 3.

IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
============================
 forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}@ ->
   {add N1' N2' N} -> le N2' N2

add_le_complement < intros.

Variables: N1 N2 N1' N2' N
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H2 : le N1 N1'
H3 : {add N1 N2 N}@
H4 : {add N1' N2' N}
============================
 le N2' N2

add_le_complement < case H3.
Subgoal 1:

Variables: N1' N2' N
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N}
H2 : le z N1'
H4 : {add N1' N2' N}
============================
 le N2' N

Subgoal 2 is:
 le N2' N2

add_le_complement < apply add_comm to _ H4.
Subgoal 1:

Variables: N1' N2' N
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N}
H2 : le z N1'
H4 : {add N1' N2' N}
H5 : {add N2' N1' N}
============================
 le N2' N

Subgoal 2 is:
 le N2' N2

add_le_complement < search.
Subgoal 2:

Variables: N2 N1' N2' N3 N5
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H2 : le (s N5) N1'
H4 : {add N1' N2' (s N3)}
H5 : {add N5 N2 N3}*
============================
 le N2' N2

add_le_complement < case H2.
Subgoal 2:

Variables: N2 N1' N2' N3 N5 N4
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H4 : {add N1' N2' (s N3)}
H5 : {add N5 N2 N3}*
H6 : {add (s N5) N4 N1'}
============================
 le N2' N2

add_le_complement < case H6.
Subgoal 2:

Variables: N2 N2' N3 N5 N4 N6
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H4 : {add (s N6) N2' (s N3)}
H5 : {add N5 N2 N3}*
H7 : {add N5 N4 N6}
============================
 le N2' N2

add_le_complement < case H4.
Subgoal 2:

Variables: N2 N2' N3 N5 N4 N6
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H5 : {add N5 N2 N3}*
H7 : {add N5 N4 N6}
H8 : {add N6 N2' N3}
============================
 le N2' N2

add_le_complement < apply IH to H1 _ H5 H8.
Subgoal 2:

Variables: N2 N2' N3 N5 N4 N6
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
       {add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H5 : {add N5 N2 N3}*
H7 : {add N5 N4 N6}
H8 : {add N6 N2' N3}
H9 : le N2' N2
============================
 le N2' N2

add_le_complement < search.
Proof completed.
Abella < Theorem k_minus_n1 : 
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
  {add N123 N K} -> (exists K', {add N1 K' K}).


============================
 forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
   {add N123 N K} -> (exists K', {add N1 K' K})

k_minus_n1 < induction on 2.

IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N1 K' K})
============================
 forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
   {add N123 N K} -> (exists K', {add N1 K' K})

k_minus_n1 < intros.

Variables: N1 N2 N3 N23 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
H3 : {add N123 N K}
============================
 exists K', {add N1 K' K}

k_minus_n1 < case H2.
Subgoal 1:

Variables: N2 N3 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
============================
 exists K', {add z K' K}

Subgoal 2 is:
 exists K', {add (s N6) K' K}

k_minus_n1 < search.
Subgoal 2:

Variables: N2 N3 N23 N K N4 N6
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H3 : {add (s N4) N K}
H4 : {add N6 N23 N4}*
============================
 exists K', {add (s N6) K' K}

k_minus_n1 < case H3.
Subgoal 2:

Variables: N2 N3 N23 N N4 N6 N5
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
============================
 exists K', {add (s N6) K' (s N5)}

k_minus_n1 < apply IH to _ H4 _.
Subgoal 2:

Variables: N2 N3 N23 N N4 N6 N5 K'
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N6 K' N5}
============================
 exists K', {add (s N6) K' (s N5)}

k_minus_n1 < search.
Proof completed.
Abella < Theorem k_minus_n2 : 
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
  {add N123 N K} -> (exists K', {add N2 K' K}).


============================
 forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
   {add N123 N K} -> (exists K', {add N2 K' K})

k_minus_n2 < induction on 2.

IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
============================
 forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
   {add N123 N K} -> (exists K', {add N2 K' K})

k_minus_n2 < intros.

Variables: N1 N2 N3 N23 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
H3 : {add N123 N K}
============================
 exists K', {add N2 K' K}

k_minus_n2 < case H2.
Subgoal 1:

Variables: N2 N3 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
============================
 exists K', {add N2 K' K}

Subgoal 2 is:
 exists K', {add N2 K' K}

k_minus_n2 < apply add_assoc to H1 H3.
Subgoal 1:

Variables: N2 N3 N123 N K N4
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
H4 : {add N3 N N4}
H5 : {add N2 N4 K}
============================
 exists K', {add N2 K' K}

Subgoal 2 is:
 exists K', {add N2 K' K}

k_minus_n2 < search.
Subgoal 2:

Variables: N2 N3 N23 N K N4 N6
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H3 : {add (s N4) N K}
H4 : {add N6 N23 N4}*
============================
 exists K', {add N2 K' K}

k_minus_n2 < case H3.
Subgoal 2:

Variables: N2 N3 N23 N N4 N6 N5
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
============================
 exists K', {add N2 K' (s N5)}

k_minus_n2 < apply IH to _ H4 _.
Subgoal 2:

Variables: N2 N3 N23 N N4 N6 N5 K'
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N2 K' N5}
============================
 exists K', {add N2 K' (s N5)}

k_minus_n2 < apply add_s to H6.
Subgoal 2:

Variables: N2 N3 N23 N N4 N6 N5 K'
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N2 K' N5}
H7 : {add N2 (s K') (s N5)}
============================
 exists K', {add N2 K' (s N5)}

k_minus_n2 < search.
Proof completed.
Abella < Theorem k_minus_n12 : 
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
  {add N123 N K} ->
  (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}).


============================
 forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
   {add N123 N K} ->
   (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})

k_minus_n12 < induction on 2.

IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} ->
       (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
============================
 forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
   {add N123 N K} ->
   (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})

k_minus_n12 < intros.

Variables: N1 N2 N3 N23 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} ->
       (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
H3 : {add N123 N K}
============================
 exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}

k_minus_n12 < case H2.
Subgoal 1:

Variables: N2 N3 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} ->
       (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
============================
 exists K' N12, {add z N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}

Subgoal 2 is:
 exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}

k_minus_n12 < apply add_assoc to H1 H3.
Subgoal 1:

Variables: N2 N3 N123 N K N4
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} ->
       (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
H4 : {add N3 N N4}
H5 : {add N2 N4 K}
============================
 exists K' N12, {add z N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}

Subgoal 2 is:
 exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}

k_minus_n12 < search.
Subgoal 2:

Variables: N2 N3 N23 N K N4 N6
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} ->
       (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H3 : {add (s N4) N K}
H4 : {add N6 N23 N4}*
============================
 exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}

k_minus_n12 < case H3.
Subgoal 2:

Variables: N2 N3 N23 N N4 N6 N5
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} ->
       (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
============================
 exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' (s N5)}

k_minus_n12 < apply IH to _ H4 _.
Subgoal 2:

Variables: N2 N3 N23 N N4 N6 N5 K' N12
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
       {add N123 N K} ->
       (exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N6 N2 N12}
H7 : {add N3 N K'}
H8 : {add N12 K' N5}
============================
 exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' (s N5)}

k_minus_n12 < search.
Proof completed.
Abella < Theorem sum_complement_to_lt1 : 
forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
  {add N1 K' N} -> lt K (s K').


============================
 forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
   {add N1 K' N} -> lt K (s K')

sum_complement_to_lt1 < intros.

Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 K' N}
============================
 lt K (s K')

sum_complement_to_lt1 < apply add_assoc to H2 H3.

Variables: N1 N2 N12 K K' N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 K' N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
 lt K (s K')

sum_complement_to_lt1 < unfold.

Variables: N1 N2 N12 K K' N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 K' N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
 exists N, {add K (s N) (s K')}

sum_complement_to_lt1 < apply add_arg2_det to H4 H6.

Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
 exists N, {add K (s N) (s N23)}

sum_complement_to_lt1 < apply add_comm to _ H5.
Subgoal 1:

Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
 {is_nat N23}

Subgoal is:
 exists N, {add K (s N) (s N23)}

sum_complement_to_lt1 < backchain add_arg2_isnat.

Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
H7 : {add K N2 N23}
============================
 exists N, {add K (s N) (s N23)}

sum_complement_to_lt1 < apply add_s to H7.

Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
H7 : {add K N2 N23}
H8 : {add K (s N2) (s N23)}
============================
 exists N, {add K (s N) (s N23)}

sum_complement_to_lt1 < search.
Proof completed.
Abella < Theorem sum_complement_to_lt2 : 
forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
  {add N2 K' N} -> lt K (s K').


============================
 forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
   {add N2 K' N} -> lt K (s K')

sum_complement_to_lt2 < intros.

Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
============================
 lt K (s K')

sum_complement_to_lt2 < apply add_comm to _ H2.
Subgoal 1:

Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
============================
 {is_nat N12}

Subgoal is:
 lt K (s K')

sum_complement_to_lt2 < backchain add_arg1_isnat.

Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
H5 : {add N2 N1 N12}
============================
 lt K (s K')

sum_complement_to_lt2 < apply sum_complement_to_lt1 to _ H5 H3 H4.

Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
H5 : {add N2 N1 N12}
H6 : lt K (s K')
============================
 lt K (s K')

sum_complement_to_lt2 < search.
Proof completed.
Abella < Theorem npred_det : 
forall N N1 N2, {npred N N1} -> {npred N N2} -> N1 = N2.


============================
 forall N N1 N2, {npred N N1} -> {npred N N2} -> N1 = N2

npred_det < intros.

Variables: N N1 N2
H1 : {npred N N1}
H2 : {npred N N2}
============================
 N1 = N2

npred_det < case H1.
Subgoal 1:

Variables: N2
H2 : {npred z N2}
============================
 z = N2

Subgoal 2 is:
 N1 = N2

npred_det < case H2.
Subgoal 1:

============================
 z = z

Subgoal 2 is:
 N1 = N2

npred_det < search.
Subgoal 2:

Variables: N1 N2
H2 : {npred (s N1) N2}
============================
 N1 = N2

npred_det < case H2.
Subgoal 2:

Variables: N2
============================
 N2 = N2

npred_det < search.
Proof completed.
Abella < Define is_list : olist -> prop by 
is_list nil;
is_list (X :: L) := is_list L.

Abella < Define append : olist -> olist -> olist -> prop by 
append nil L L;
append (X :: L1) L2 (X :: L3) := append L1 L2 L3.

Abella < Theorem append_refl : 
forall L, is_list L -> append L nil L.


============================
 forall L, is_list L -> append L nil L

append_refl < induction on 1.

IH : forall L, is_list L * -> append L nil L
============================
 forall L, is_list L @ -> append L nil L

append_refl < intros.

Variables: L
IH : forall L, is_list L * -> append L nil L
H1 : is_list L @
============================
 append L nil L

append_refl < case H1.
Subgoal 1:

IH : forall L, is_list L * -> append L nil L
============================
 append nil nil nil

Subgoal 2 is:
 append (X :: L1) nil (X :: L1)

append_refl < search.
Subgoal 2:

Variables: L1 X
IH : forall L, is_list L * -> append L nil L
H2 : is_list L1 *
============================
 append (X :: L1) nil (X :: L1)

append_refl < unfold.
Subgoal 2:

Variables: L1 X
IH : forall L, is_list L * -> append L nil L
H2 : is_list L1 *
============================
 append L1 nil L1

append_refl < backchain IH.
Proof completed.
Abella < Theorem append_exists : 
forall L1 L2, is_list L1 -> (exists L3, append L1 L2 L3).


============================
 forall L1 L2, is_list L1 -> (exists L3, append L1 L2 L3)

append_exists < induction on 1.

IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
============================
 forall L1 L2, is_list L1 @ -> (exists L3, append L1 L2 L3)

append_exists < intros.

Variables: L1 L2
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
H1 : is_list L1 @
============================
 exists L3, append L1 L2 L3

append_exists < case H1.
Subgoal 1:

Variables: L2
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
============================
 exists L3, append nil L2 L3

Subgoal 2 is:
 exists L3, append (X :: L) L2 L3

append_exists < search.
Subgoal 2:

Variables: L2 L X
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
H2 : is_list L *
============================
 exists L3, append (X :: L) L2 L3

append_exists < apply IH to H2 with L2 = L2.
Subgoal 2:

Variables: L2 L X L3
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
H2 : is_list L *
H3 : append L L2 L3
============================
 exists L3, append (X :: L) L2 L3

append_exists < search.
Proof completed.
Abella < Theorem append_result_islist : 
forall L1 L2 L, is_list L2 -> append L1 L2 L -> is_list L.


============================
 forall L1 L2 L, is_list L2 -> append L1 L2 L -> is_list L

append_result_islist < induction on 2.

IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
============================
 forall L1 L2 L, is_list L2 -> append L1 L2 L @ -> is_list L

append_result_islist < intros.

Variables: L1 L2 L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L2
H2 : append L1 L2 L @
============================
 is_list L

append_result_islist < case H2.
Subgoal 1:

Variables: L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L
============================
 is_list L

Subgoal 2 is:
 is_list (X :: L5)

append_result_islist < search.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
 is_list (X :: L5)

append_result_islist < unfold.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
 is_list L5

append_result_islist < backchain IH.
Proof completed.
Abella < Theorem append_arg2_islist : 
forall L1 L2 L, is_list L -> append L1 L2 L -> is_list L2.


============================
 forall L1 L2 L, is_list L -> append L1 L2 L -> is_list L2

append_arg2_islist < induction on 2.

IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
============================
 forall L1 L2 L, is_list L -> append L1 L2 L @ -> is_list L2

append_arg2_islist < intros.

Variables: L1 L2 L
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list L
H2 : append L1 L2 L @
============================
 is_list L2

append_arg2_islist < case H2.
Subgoal 1:

Variables: L
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list L
============================
 is_list L

Subgoal 2 is:
 is_list L2

append_arg2_islist < search.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list (X :: L5)
H3 : append L3 L2 L5 *
============================
 is_list L2

append_arg2_islist < backchain IH with L1 = L3, L = L5.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list (X :: L5)
H3 : append L3 L2 L5 *
============================
 is_list L5

append_arg2_islist < case H1.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H3 : append L3 L2 L5 *
H4 : is_list L5
============================
 is_list L5

append_arg2_islist < search.
Proof completed.
Abella < Theorem append_arg1_islist : 
forall L1 L2 L, append L1 L2 L -> is_list L1.


============================
 forall L1 L2 L, append L1 L2 L -> is_list L1

append_arg1_islist < induction on 1.

IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
============================
 forall L1 L2 L, append L1 L2 L @ -> is_list L1

append_arg1_islist < intros.

Variables: L1 L2 L
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
H1 : append L1 L2 L @
============================
 is_list L1

append_arg1_islist < case H1.
Subgoal 1:

Variables: L
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
============================
 is_list nil

Subgoal 2 is:
 is_list (X :: L3)

append_arg1_islist < search.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
H2 : append L3 L2 L5 *
============================
 is_list (X :: L3)

append_arg1_islist < unfold.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
H2 : append L3 L2 L5 *
============================
 is_list L3

append_arg1_islist < backchain IH.
Proof completed.
Abella < Define subset : olist -> olist -> prop by 
subset nil L;
subset (X :: L1) L2 := member X L2 /\ subset L1 L2.

Abella < Theorem subset_add : 
forall L L' X, subset L L' -> subset L (X :: L').


============================
 forall L L' X, subset L L' -> subset L (X :: L')

subset_add < induction on 1.

IH : forall L L' X, subset L L' * -> subset L (X :: L')
============================
 forall L L' X, subset L L' @ -> subset L (X :: L')

subset_add < intros.

Variables: L L' X
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H1 : subset L L' @
============================
 subset L (X :: L')

subset_add < case H1.
Subgoal 1:

Variables: L' X
IH : forall L L' X, subset L L' * -> subset L (X :: L')
============================
 subset nil (X :: L')

Subgoal 2 is:
 subset (X1 :: L1) (X :: L')

subset_add < search.
Subgoal 2:

Variables: L' X L1 X1
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H2 : member X1 L'
H3 : subset L1 L' *
============================
 subset (X1 :: L1) (X :: L')

subset_add < unfold.
Subgoal 2.1:

Variables: L' X L1 X1
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H2 : member X1 L'
H3 : subset L1 L' *
============================
 member X1 (X :: L')

Subgoal 2.2 is:
 subset L1 (X :: L')

subset_add < search.
Subgoal 2.2:

Variables: L' X L1 X1
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H2 : member X1 L'
H3 : subset L1 L' *
============================
 subset L1 (X :: L')

subset_add < backchain IH.
Proof completed.
Abella < Theorem subset_refl : 
forall L, is_list L -> subset L L.


============================
 forall L, is_list L -> subset L L

subset_refl < induction on 1.

IH : forall L, is_list L * -> subset L L
============================
 forall L, is_list L @ -> subset L L

subset_refl < intros.

Variables: L
IH : forall L, is_list L * -> subset L L
H1 : is_list L @
============================
 subset L L

subset_refl < case H1.
Subgoal 1:

IH : forall L, is_list L * -> subset L L
============================
 subset nil nil

Subgoal 2 is:
 subset (X :: L1) (X :: L1)

subset_refl < search.
Subgoal 2:

Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
 subset (X :: L1) (X :: L1)

subset_refl < unfold.
Subgoal 2.1:

Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
 member X (X :: L1)

Subgoal 2.2 is:
 subset L1 (X :: L1)

subset_refl < search.
Subgoal 2.2:

Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
 subset L1 (X :: L1)

subset_refl < backchain subset_add.
Subgoal 2.2:

Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
 subset L1 L1

subset_refl < backchain IH.
Proof completed.
Abella < Theorem subset_mem_trans : 
forall L1 L2 X, subset L1 L2 -> member X L1 -> member X L2.


============================
 forall L1 L2 X, subset L1 L2 -> member X L1 -> member X L2

subset_mem_trans < induction on 2.

IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
============================
 forall L1 L2 X, subset L1 L2 -> member X L1 @ -> member X L2

subset_mem_trans < intros.

Variables: L1 L2 X
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H1 : subset L1 L2
H2 : member X L1 @
============================
 member X L2

subset_mem_trans < case H2.
Subgoal 1:

Variables: L2 X L
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H1 : subset (X :: L) L2
============================
 member X L2

Subgoal 2 is:
 member X L2

subset_mem_trans < case H1.
Subgoal 1:

Variables: L2 X L
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H3 : member X L2
H4 : subset L L2
============================
 member X L2

Subgoal 2 is:
 member X L2

subset_mem_trans < search.
Subgoal 2:

Variables: L2 X L B
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H1 : subset (B :: L) L2
H3 : member X L *
============================
 member X L2

subset_mem_trans < case H1.
Subgoal 2:

Variables: L2 X L B
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H3 : member X L *
H4 : member B L2
H5 : subset L L2
============================
 member X L2

subset_mem_trans < backchain IH.
Proof completed.
Abella < Theorem subset_trans : 
forall L1 L2 L3, subset L1 L2 -> subset L2 L3 -> subset L1 L3.


============================
 forall L1 L2 L3, subset L1 L2 -> subset L2 L3 -> subset L1 L3

subset_trans < induction on 1.

IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
============================
 forall L1 L2 L3, subset L1 L2 @ -> subset L2 L3 -> subset L1 L3

subset_trans < intros.

Variables: L1 L2 L3
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H1 : subset L1 L2 @
H2 : subset L2 L3
============================
 subset L1 L3

subset_trans < case H1.
Subgoal 1:

Variables: L2 L3
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
============================
 subset nil L3

Subgoal 2 is:
 subset (X :: L4) L3

subset_trans < search.
Subgoal 2:

Variables: L2 L3 L4 X
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
H3 : member X L2
H4 : subset L4 L2 *
============================
 subset (X :: L4) L3

subset_trans < unfold.
Subgoal 2.1:

Variables: L2 L3 L4 X
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
H3 : member X L2
H4 : subset L4 L2 *
============================
 member X L3

Subgoal 2.2 is:
 subset L4 L3

subset_trans < backchain subset_mem_trans.
Subgoal 2.2:

Variables: L2 L3 L4 X
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
H3 : member X L2
H4 : subset L4 L2 *
============================
 subset L4 L3

subset_trans < backchain IH.
Proof completed.
Abella < Theorem subset_extend : 
forall L L' X, subset L L' -> subset (X :: L) (X :: L').


============================
 forall L L' X, subset L L' -> subset (X :: L) (X :: L')

subset_extend < intros.

Variables: L L' X
H1 : subset L L'
============================
 subset (X :: L) (X :: L')

subset_extend < unfold.
Subgoal 1:

Variables: L L' X
H1 : subset L L'
============================
 member X (X :: L')

Subgoal 2 is:
 subset L (X :: L')

subset_extend < search.
Subgoal 2:

Variables: L L' X
H1 : subset L L'
============================
 subset L (X :: L')

subset_extend < backchain subset_add.
Proof completed.
Abella < Theorem append_sub1 : 
forall L1 L2 L, append L1 L2 L -> subset L1 L.


============================
 forall L1 L2 L, append L1 L2 L -> subset L1 L

append_sub1 < induction on 1.

IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
============================
 forall L1 L2 L, append L1 L2 L @ -> subset L1 L

append_sub1 < intros.

Variables: L1 L2 L
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
H1 : append L1 L2 L @
============================
 subset L1 L

append_sub1 < case H1.
Subgoal 1:

Variables: L
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
============================
 subset nil L

Subgoal 2 is:
 subset (X :: L3) (X :: L5)

append_sub1 < search.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
H2 : append L3 L2 L5 *
============================
 subset (X :: L3) (X :: L5)

append_sub1 < backchain subset_extend.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
H2 : append L3 L2 L5 *
============================
 subset L3 L5

append_sub1 < backchain IH.
Proof completed.
Abella < Theorem append_sub2 : 
forall L1 L2 L, is_list L2 -> append L1 L2 L -> subset L2 L.


============================
 forall L1 L2 L, is_list L2 -> append L1 L2 L -> subset L2 L

append_sub2 < induction on 2.

IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
============================
 forall L1 L2 L, is_list L2 -> append L1 L2 L @ -> subset L2 L

append_sub2 < intros.

Variables: L1 L2 L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L2
H2 : append L1 L2 L @
============================
 subset L2 L

append_sub2 < case H2.
Subgoal 1:

Variables: L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L
============================
 subset L L

Subgoal 2 is:
 subset L2 (X :: L5)

append_sub2 < backchain subset_refl.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
 subset L2 (X :: L5)

append_sub2 < backchain subset_add.
Subgoal 2:

Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
 subset L2 L5

append_sub2 < backchain IH.
Proof completed.
Abella < Theorem append_subset_trans : 
forall L1 L2 L L', append L1 L2 L -> subset L1 L' -> subset L2 L' ->
  subset L L'.


============================
 forall L1 L2 L L', append L1 L2 L -> subset L1 L' -> subset L2 L' ->
   subset L L'

append_subset_trans < induction on 1.

IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
       subset L L'
============================
 forall L1 L2 L L', append L1 L2 L @ -> subset L1 L' -> subset L2 L' ->
   subset L L'

append_subset_trans < intros.

Variables: L1 L2 L L'
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
       subset L L'
H1 : append L1 L2 L @
H2 : subset L1 L'
H3 : subset L2 L'
============================
 subset L L'

append_subset_trans < case H1.
Subgoal 1:

Variables: L L'
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
       subset L L'
H2 : subset nil L'
H3 : subset L L'
============================
 subset L L'

Subgoal 2 is:
 subset (X :: L5) L'

append_subset_trans < search.
Subgoal 2:

Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
       subset L L'
H2 : subset (X :: L3) L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
============================
 subset (X :: L5) L'

append_subset_trans < case H2.
Subgoal 2:

Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
       subset L L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
H5 : member X L'
H6 : subset L3 L'
============================
 subset (X :: L5) L'

append_subset_trans < unfold.
Subgoal 2.1:

Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
       subset L L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
H5 : member X L'
H6 : subset L3 L'
============================
 member X L'

Subgoal 2.2 is:
 subset L5 L'

append_subset_trans < search.
Subgoal 2.2:

Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
       subset L L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
H5 : member X L'
H6 : subset L3 L'
============================
 subset L5 L'

append_subset_trans < backchain IH.
Proof completed.
Abella < Theorem append_append_subset_trans : 
forall L1 L1' L2 L2' L L', is_list L2' -> append L1 L2 L ->
  append L1' L2' L' -> subset L1 L1' -> subset L2 L2' -> subset L L'.


============================
 forall L1 L1' L2 L2' L L', is_list L2' -> append L1 L2 L ->
   append L1' L2' L' -> subset L1 L1' -> subset L2 L2' -> subset L L'

append_append_subset_trans < intros.

Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
============================
 subset L L'

append_append_subset_trans < assert subset L1 L'.
Subgoal 1:

Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
============================
 subset L1 L'

Subgoal is:
 subset L L'

append_append_subset_trans < backchain subset_trans with L2 = L1'.
Subgoal 1:

Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
============================
 subset L1' L'

Subgoal is:
 subset L L'

append_append_subset_trans < backchain append_sub1.

Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
============================
 subset L L'

append_append_subset_trans < assert subset L2 L'.
Subgoal 2:

Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
============================
 subset L2 L'

Subgoal is:
 subset L L'

append_append_subset_trans < backchain subset_trans with L2 = L2'.
Subgoal 2:

Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
============================
 subset L2' L'

Subgoal is:
 subset L L'

append_append_subset_trans < backchain append_sub2.

Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
H7 : subset L2 L'
============================
 subset L L'

append_append_subset_trans < backchain append_subset_trans.
Proof completed.
Abella < Define tm_subset : tm_list -> tm_list -> prop by 
tm_subset snil L;
tm_subset (scons X L1) L2 := {smember X L2} /\ tm_subset L1 L2.

Abella < Define is_tm_list : tm_list -> prop by 
is_tm_list snil;
is_tm_list (scons X L) := is_tm_list L.

Abella < Theorem sappend_refl_eq : 
forall L1 L2, {sappend L1 snil L2} -> L1 = L2.


============================
 forall L1 L2, {sappend L1 snil L2} -> L1 = L2

sappend_refl_eq < induction on 1.

IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
============================
 forall L1 L2, {sappend L1 snil L2}@ -> L1 = L2

sappend_refl_eq < intros.

Variables: L1 L2
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
H1 : {sappend L1 snil L2}@
============================
 L1 = L2

sappend_refl_eq < case H1.
Subgoal 1:

IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
============================
 snil = snil

Subgoal 2 is:
 scons X L5 = scons X L3

sappend_refl_eq < search.
Subgoal 2:

Variables: L3 L5 X
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
H2 : {sappend L5 snil L3}*
============================
 scons X L5 = scons X L3

sappend_refl_eq < apply IH to H2.
Subgoal 2:

Variables: L3 X
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
H2 : {sappend L3 snil L3}*
============================
 scons X L3 = scons X L3

sappend_refl_eq < search.
Proof completed.
Abella < Theorem append_prune_tm : 
forall L1 L2 L3, nabla n, append L1 L2 (L3 n) -> (exists L3', L3 = y\L3').


============================
 forall L1 L2 L3, nabla n, append L1 L2 (L3 n) -> (exists L3', L3 = y\L3')

append_prune_tm < induction on 1.

IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
       (exists L3', L3 = y\L3')
============================
 forall L1 L2 L3, nabla n, append L1 L2 (L3 n) @ -> (exists L3', L3 = y\L3')

append_prune_tm < intros.

Variables: L1 L2 L3
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
       (exists L3', L3 = y\L3')
H1 : append L1 L2 (L3 n1) @
============================
 exists L3', L3 = y\L3'

append_prune_tm < case H1.
Subgoal 1:

Variables: L2
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
       (exists L3', L3 = y\L3')
============================
 exists L3', z1\L2 = y\L3'

Subgoal 2 is:
 exists L3', z1\L7 :: L6 z1 = y\L3'

append_prune_tm < search.
Subgoal 2:

Variables: L2 L6 L7 L8
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
       (exists L3', L3 = y\L3')
H2 : append L8 L2 (L6 n1) *
============================
 exists L3', z1\L7 :: L6 z1 = y\L3'

append_prune_tm < apply IH to H2.
Subgoal 2:

Variables: L2 L7 L8 L3'
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
       (exists L3', L3 = y\L3')
H2 : append L8 L2 L3' *
============================
 exists L3'1, z1\L7 :: L3' = y\L3'1

append_prune_tm < search.
Proof completed.
Abella < Theorem tm_subset_add : 
forall L L' X, tm_subset L L' -> tm_subset L (scons X L').


============================
 forall L L' X, tm_subset L L' -> tm_subset L (scons X L')

tm_subset_add < induction on 1.

IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
============================
 forall L L' X, tm_subset L L' @ -> tm_subset L (scons X L')

tm_subset_add < intros.

Variables: L L' X
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H1 : tm_subset L L' @
============================
 tm_subset L (scons X L')

tm_subset_add < case H1.
Subgoal 1:

Variables: L' X
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
============================
 tm_subset snil (scons X L')

Subgoal 2 is:
 tm_subset (scons X1 L1) (scons X L')

tm_subset_add < search.
Subgoal 2:

Variables: L' X L1 X1
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H2 : {smember X1 L'}
H3 : tm_subset L1 L' *
============================
 tm_subset (scons X1 L1) (scons X L')

tm_subset_add < unfold.
Subgoal 2.1:

Variables: L' X L1 X1
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H2 : {smember X1 L'}
H3 : tm_subset L1 L' *
============================
 {smember X1 (scons X L')}

Subgoal 2.2 is:
 tm_subset L1 (scons X L')

tm_subset_add < search.
Subgoal 2.2:

Variables: L' X L1 X1
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H2 : {smember X1 L'}
H3 : tm_subset L1 L' *
============================
 tm_subset L1 (scons X L')

tm_subset_add < backchain IH.
Proof completed.
Abella < Theorem tm_subset_refl : 
forall L, is_tm_list L -> tm_subset L L.


============================
 forall L, is_tm_list L -> tm_subset L L

tm_subset_refl < induction on 1.

IH : forall L, is_tm_list L * -> tm_subset L L
============================
 forall L, is_tm_list L @ -> tm_subset L L

tm_subset_refl < intros.

Variables: L
IH : forall L, is_tm_list L * -> tm_subset L L
H1 : is_tm_list L @
============================
 tm_subset L L

tm_subset_refl < case H1.
Subgoal 1:

IH : forall L, is_tm_list L * -> tm_subset L L
============================
 tm_subset snil snil

Subgoal 2 is:
 tm_subset (scons X L1) (scons X L1)

tm_subset_refl < search.
Subgoal 2:

Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
 tm_subset (scons X L1) (scons X L1)

tm_subset_refl < unfold.
Subgoal 2.1:

Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
 {smember X (scons X L1)}

Subgoal 2.2 is:
 tm_subset L1 (scons X L1)

tm_subset_refl < search.
Subgoal 2.2:

Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
 tm_subset L1 (scons X L1)

tm_subset_refl < backchain tm_subset_add.
Subgoal 2.2:

Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
 tm_subset L1 L1

tm_subset_refl < backchain IH.
Proof completed.
Abella < Theorem tm_subset_mem_trans : 
forall L1 L2 X, tm_subset L1 L2 -> {smember X L1} -> {smember X L2}.


============================
 forall L1 L2 X, tm_subset L1 L2 -> {smember X L1} -> {smember X L2}

tm_subset_mem_trans < induction on 2.

IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
============================
 forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}@ -> {smember X L2}

tm_subset_mem_trans < intros.

Variables: L1 L2 X
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H1 : tm_subset L1 L2
H2 : {smember X L1}@
============================
 {smember X L2}

tm_subset_mem_trans < case H2.
Subgoal 1:

Variables: L2 X L
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H1 : tm_subset (scons X L) L2
============================
 {smember X L2}

Subgoal 2 is:
 {smember X L2}

tm_subset_mem_trans < case H1.
Subgoal 1:

Variables: L2 X L
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H3 : {smember X L2}
H4 : tm_subset L L2
============================
 {smember X L2}

Subgoal 2 is:
 {smember X L2}

tm_subset_mem_trans < search.
Subgoal 2:

Variables: L2 X L X1
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H1 : tm_subset (scons X1 L) L2
H3 : {smember X L}*
============================
 {smember X L2}

tm_subset_mem_trans < case H1.
Subgoal 2:

Variables: L2 X L X1
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H3 : {smember X L}*
H4 : {smember X1 L2}
H5 : tm_subset L L2
============================
 {smember X L2}

tm_subset_mem_trans < backchain IH.
Proof completed.
Abella < Theorem tm_subset_trans : 
forall L1 L2 L3, tm_subset L1 L2 -> tm_subset L2 L3 -> tm_subset L1 L3.


============================
 forall L1 L2 L3, tm_subset L1 L2 -> tm_subset L2 L3 -> tm_subset L1 L3

tm_subset_trans < induction on 1.

IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
============================
 forall L1 L2 L3, tm_subset L1 L2 @ -> tm_subset L2 L3 -> tm_subset L1 L3

tm_subset_trans < intros.

Variables: L1 L2 L3
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H1 : tm_subset L1 L2 @
H2 : tm_subset L2 L3
============================
 tm_subset L1 L3

tm_subset_trans < case H1.
Subgoal 1:

Variables: L2 L3
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
============================
 tm_subset snil L3

Subgoal 2 is:
 tm_subset (scons X L4) L3

tm_subset_trans < search.
Subgoal 2:

Variables: L2 L3 L4 X
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
H3 : {smember X L2}
H4 : tm_subset L4 L2 *
============================
 tm_subset (scons X L4) L3

tm_subset_trans < unfold.
Subgoal 2.1:

Variables: L2 L3 L4 X
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
H3 : {smember X L2}
H4 : tm_subset L4 L2 *
============================
 {smember X L3}

Subgoal 2.2 is:
 tm_subset L4 L3

tm_subset_trans < backchain tm_subset_mem_trans.
Subgoal 2.2:

Variables: L2 L3 L4 X
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
H3 : {smember X L2}
H4 : tm_subset L4 L2 *
============================
 tm_subset L4 L3

tm_subset_trans < backchain IH.
Proof completed.
Abella < Theorem tm_subset_extend : 
forall L L' X, tm_subset L L' -> tm_subset (scons X L) (scons X L').


============================
 forall L L' X, tm_subset L L' -> tm_subset (scons X L) (scons X L')

tm_subset_extend < intros.

Variables: L L' X
H1 : tm_subset L L'
============================
 tm_subset (scons X L) (scons X L')

tm_subset_extend < unfold.
Subgoal 1:

Variables: L L' X
H1 : tm_subset L L'
============================
 {smember X (scons X L')}

Subgoal 2 is:
 tm_subset L (scons X L')

tm_subset_extend < search.
Subgoal 2:

Variables: L L' X
H1 : tm_subset L L'
============================
 tm_subset L (scons X L')

tm_subset_extend < backchain tm_subset_add.
Proof completed.
Abella < Define is_tm'_list : tm'_list -> prop by 
is_tm'_list cnil;
is_tm'_list (ccons X L) := is_tm'_list L.

Abella < Theorem is_tm'_list_inst : 
forall L V, nabla x, is_tm'_list (L x) -> is_tm'_list (L V).


============================
 forall L V, nabla x, is_tm'_list (L x) -> is_tm'_list (L V)

is_tm'_list_inst < induction on 1.

IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
============================
 forall L V, nabla x, is_tm'_list (L x) @ -> is_tm'_list (L V)

is_tm'_list_inst < intros.

Variables: L V
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
H1 : is_tm'_list (L n1) @
============================
 is_tm'_list (L V)

is_tm'_list_inst < case H1.
Subgoal 1:

Variables: V
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
============================
 is_tm'_list cnil

Subgoal 2 is:
 is_tm'_list (ccons (X V) (L1 V))

is_tm'_list_inst < search.
Subgoal 2:

Variables: V L1 X
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
H2 : is_tm'_list (L1 n1) *
============================
 is_tm'_list (ccons (X V) (L1 V))

is_tm'_list_inst < apply IH to H2 with V = V.
Subgoal 2:

Variables: V L1 X
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
H2 : is_tm'_list (L1 n1) *
H3 : is_tm'_list (L1 V)
============================
 is_tm'_list (ccons (X V) (L1 V))

is_tm'_list_inst < search.
Proof completed.
Abella < Define tm'_list_length : tm'_list -> nat -> prop by 
tm'_list_length cnil z;
tm'_list_length (ccons M ML) (s N) := tm'_list_length ML N.

Abella < Theorem member_prune_tm : 
forall M L, nabla x, member (M x) L -> (exists M', M = y\M').


============================
 forall M L, nabla x, member (M x) L -> (exists M', M = y\M')

member_prune_tm < induction on 1.

IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
 forall M L, nabla x, member (M x) L @ -> (exists M', M = y\M')

member_prune_tm < intros.

Variables: M L
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H1 : member (M n1) L @
============================
 exists M', M = y\M'

member_prune_tm < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
 exists M', z1\L2 = y\M'

Subgoal 2 is:
 exists M', M = y\M'

member_prune_tm < search.
Subgoal 2:

Variables: M L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member (M n1) L3 *
============================
 exists M', M = y\M'

member_prune_tm < apply IH to H2.
Subgoal 2:

Variables: L3 L2 M'
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member M' L3 *
============================
 exists M'1, z1\M' = y\M'1

member_prune_tm < search.
Proof completed.
Abella < Theorem member_prune_tm' : 
forall M L, nabla x, member (M x) L -> (exists M', M = y\M').


============================
 forall M L, nabla x, member (M x) L -> (exists M', M = y\M')

member_prune_tm' < induction on 1.

IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
 forall M L, nabla x, member (M x) L @ -> (exists M', M = y\M')

member_prune_tm' < intros.

Variables: M L
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H1 : member (M n1) L @
============================
 exists M', M = y\M'

member_prune_tm' < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
 exists M', z1\L2 = y\M'

Subgoal 2 is:
 exists M', M = y\M'

member_prune_tm' < search.
Subgoal 2:

Variables: M L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member (M n1) L3 *
============================
 exists M', M = y\M'

member_prune_tm' < apply IH to H2.
Subgoal 2:

Variables: L3 L2 M'
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member M' L3 *
============================
 exists M'1, z1\M' = y\M'1

member_prune_tm' < search.
Proof completed.
Abella < Theorem mmember_prune_tm : 
forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M').


============================
 forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M')

mmember_prune_tm < induction on 1.

IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
 forall M L, nabla x, {mmember (M x) L}@ -> (exists M', M = y\M')

mmember_prune_tm < intros.

Variables: M L
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H1 : {mmember (M n1) L}@
============================
 exists M', M = y\M'

mmember_prune_tm < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
 exists M', z1\L2 = y\M'

Subgoal 2 is:
 exists M', M = y\M'

mmember_prune_tm < search.
Subgoal 2:

Variables: M L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember (M n1) L3}*
============================
 exists M', M = y\M'

mmember_prune_tm < apply IH to H2.
Subgoal 2:

Variables: L3 L2 M'
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember M' L3}*
============================
 exists M'1, z1\M' = y\M'1

mmember_prune_tm < search.
Proof completed.
Abella < Theorem mmember_prune_tm' : 
forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M').


============================
 forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M')

mmember_prune_tm' < induction on 1.

IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
 forall M L, nabla x, {mmember (M x) L}@ -> (exists M', M = y\M')

mmember_prune_tm' < intros.

Variables: M L
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H1 : {mmember (M n1) L}@
============================
 exists M', M = y\M'

mmember_prune_tm' < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
 exists M', z1\L2 = y\M'

Subgoal 2 is:
 exists M', M = y\M'

mmember_prune_tm' < search.
Subgoal 2:

Variables: M L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember (M n1) L3}*
============================
 exists M', M = y\M'

mmember_prune_tm' < apply IH to H2.
Subgoal 2:

Variables: L3 L2 M'
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember M' L3}*
============================
 exists M'1, z1\M' = y\M'1

mmember_prune_tm' < search.
Proof completed.
Abella < Define name : tm -> prop by 
nabla n, name n.

Abella < Define name' : tm' -> prop by 
nabla n, name' n.

Abella < Theorem combine_subset : 
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} ->
  tm_subset Vs1 Vs /\ tm_subset Vs2 Vs.


============================
 forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} ->
   tm_subset Vs1 Vs /\ tm_subset Vs2 Vs

combine_subset < induction on 2.

IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
============================
 forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}@ ->
   tm_subset Vs1 Vs /\ tm_subset Vs2 Vs

combine_subset < intros.

Variables: Vs1 Vs2 Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}@
============================
 tm_subset Vs1 Vs /\ tm_subset Vs2 Vs

combine_subset < case H2.
Subgoal 1:

Variables: Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
============================
 tm_subset snil Vs /\ tm_subset Vs Vs

Subgoal 2 is:
 tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs

Subgoal 3 is:
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < split.
Subgoal 1.1:

Variables: Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
============================
 tm_subset snil Vs

Subgoal 1.2 is:
 tm_subset Vs Vs

Subgoal 2 is:
 tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs

Subgoal 3 is:
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < search.
Subgoal 1.2:

Variables: Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
============================
 tm_subset Vs Vs

Subgoal 2 is:
 tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs

Subgoal 3 is:
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < backchain tm_subset_refl.
Subgoal 2:

Variables: Vs2 Vs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H3 : {smember X Vs2}*
H4 : {combine FVs1 Vs2 Vs}*
============================
 tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs

Subgoal 3 is:
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < apply IH to _ H4.
Subgoal 2:

Variables: Vs2 Vs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H3 : {smember X Vs2}*
H4 : {combine FVs1 Vs2 Vs}*
H5 : tm_subset FVs1 Vs
H6 : tm_subset Vs2 Vs
============================
 tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs

Subgoal 3 is:
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < apply tm_subset_mem_trans to H6 H3.
Subgoal 2:

Variables: Vs2 Vs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H3 : {smember X Vs2}*
H4 : {combine FVs1 Vs2 Vs}*
H5 : tm_subset FVs1 Vs
H6 : tm_subset Vs2 Vs
H7 : {smember X Vs}
============================
 tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs

Subgoal 3 is:
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < search.
Subgoal 3:

Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list (scons X FVs)
H3 : {combine FVs1 Vs2 FVs}*
============================
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < case H1.
Subgoal 3:

Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
============================
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < apply IH to _ H3.
Subgoal 3:

Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
H5 : tm_subset FVs1 FVs
H6 : tm_subset Vs2 FVs
============================
 tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)

combine_subset < split.
Subgoal 3.1:

Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
H5 : tm_subset FVs1 FVs
H6 : tm_subset Vs2 FVs
============================
 tm_subset (scons X FVs1) (scons X FVs)

Subgoal 3.2 is:
 tm_subset Vs2 (scons X FVs)

combine_subset < backchain tm_subset_extend.
Subgoal 3.2:

Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
       tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
H5 : tm_subset FVs1 FVs
H6 : tm_subset Vs2 FVs
============================
 tm_subset Vs2 (scons X FVs)

combine_subset < backchain tm_subset_add.
Proof completed.
Abella < Theorem combine_sub1 : 
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs1 Vs.


============================
 forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs1 Vs

combine_sub1 < intros.

Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
============================
 tm_subset Vs1 Vs

combine_sub1 < apply combine_subset to _ H2.

Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
H3 : tm_subset Vs1 Vs
H4 : tm_subset Vs2 Vs
============================
 tm_subset Vs1 Vs

combine_sub1 < search.
Proof completed.
Abella < Theorem combine_sub2 : 
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs2 Vs.


============================
 forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs2 Vs

combine_sub2 < intros.

Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
============================
 tm_subset Vs2 Vs

combine_sub2 < apply combine_subset to _ H2.

Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
H3 : tm_subset Vs1 Vs
H4 : tm_subset Vs2 Vs
============================
 tm_subset Vs2 Vs

combine_sub2 < search.
Proof completed.
Abella < Kind smap type.

Abella < Kind smap_list type.

Abella < Type smap tm -> tm -> smap.

Abella < Type smnil smap_list.

Abella < Type smcons smap -> smap_list -> smap_list.

Abella < Define smmember : smap -> smap_list -> prop by 
smmember X (smcons X L);
smmember X (smcons Y L) := smmember X L.

Abella < Kind cmap type.

Abella < Kind cmap_list type.

Abella < Type cmap tm' -> tm' -> cmap.

Abella < Type cmnil cmap_list.

Abella < Type cmcons cmap -> cmap_list -> cmap_list.

Abella < Define cmmember : cmap -> cmap_list -> prop by 
cmmember X (cmcons X L);
cmmember X (cmcons Y L) := cmmember X L.

Abella < Theorem smmember_prune_tm : 
forall M L, nabla x, smmember (M x) L -> (exists M', M = y\M').


============================
 forall M L, nabla x, smmember (M x) L -> (exists M', M = y\M')

smmember_prune_tm < induction on 1.

IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
============================
 forall M L, nabla x, smmember (M x) L @ -> (exists M', M = y\M')

smmember_prune_tm < intros.

Variables: M L
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
H1 : smmember (M n1) L @
============================
 exists M', M = y\M'

smmember_prune_tm < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
============================
 exists M', z1\L2 = y\M'

Subgoal 2 is:
 exists M', M = y\M'

smmember_prune_tm < search.
Subgoal 2:

Variables: M L3 L2
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
H2 : smmember (M n1) L3 *
============================
 exists M', M = y\M'

smmember_prune_tm < apply IH to H2.
Subgoal 2:

Variables: L3 L2 M'
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
H2 : smmember M' L3 *
============================
 exists M'1, z1\M' = y\M'1

smmember_prune_tm < search.
Proof completed.
Abella < Theorem cmmember_prune_tm' : 
forall M L, nabla x, cmmember (M x) L -> (exists M', M = y\M').


============================
 forall M L, nabla x, cmmember (M x) L -> (exists M', M = y\M')

cmmember_prune_tm' < induction on 1.

IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
============================
 forall M L, nabla x, cmmember (M x) L @ -> (exists M', M = y\M')

cmmember_prune_tm' < intros.

Variables: M L
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
H1 : cmmember (M n1) L @
============================
 exists M', M = y\M'

cmmember_prune_tm' < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
============================
 exists M', z1\L2 = y\M'

Subgoal 2 is:
 exists M', M = y\M'

cmmember_prune_tm' < search.
Subgoal 2:

Variables: M L3 L2
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
H2 : cmmember (M n1) L3 *
============================
 exists M', M = y\M'

cmmember_prune_tm' < apply IH to H2.
Subgoal 2:

Variables: L3 L2 M'
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
H2 : cmmember M' L3 *
============================
 exists M'1, z1\M' = y\M'1

cmmember_prune_tm' < search.
Proof completed.
Abella < Theorem crev_det : 
forall L1 L2 L3 L3', {crev L1 L2 L3} -> {crev L1 L2 L3'} -> L3 = L3'.


============================
 forall L1 L2 L3 L3', {crev L1 L2 L3} -> {crev L1 L2 L3'} -> L3 = L3'

crev_det < induction on 1.

IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
============================
 forall L1 L2 L3 L3', {crev L1 L2 L3}@ -> {crev L1 L2 L3'} -> L3 = L3'

crev_det < intros.

Variables: L1 L2 L3 L3'
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H1 : {crev L1 L2 L3}@
H2 : {crev L1 L2 L3'}
============================
 L3 = L3'

crev_det < case H1.
Subgoal 1:

Variables: L3 L3'
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H2 : {crev cnil L3 L3'}
============================
 L3 = L3'

Subgoal 2 is:
 L3 = L3'

crev_det < case H2.
Subgoal 1:

Variables: L3'
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
============================
 L3' = L3'

Subgoal 2 is:
 L3 = L3'

crev_det < search.
Subgoal 2:

Variables: L2 L3 L3' X L5
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H2 : {crev (ccons X L5) L2 L3'}
H3 : {crev L5 (ccons X L2) L3}*
============================
 L3 = L3'

crev_det < case H2.
Subgoal 2:

Variables: L2 L3 L3' X L5
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H3 : {crev L5 (ccons X L2) L3}*
H4 : {crev L5 (ccons X L2) L3'}
============================
 L3 = L3'

crev_det < apply IH to H3 H4.
Subgoal 2:

Variables: L2 L3' X L5
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H3 : {crev L5 (ccons X L2) L3'}*
H4 : {crev L5 (ccons X L2) L3'}
============================
 L3' = L3'

crev_det < search.
Proof completed.
Abella < Theorem crev_prune : 
forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)} -> (exists L3', L3 = x\L3').


============================
 forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)} -> (exists L3', L3 = x\L3')

crev_prune < induction on 1.

IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
       (exists L3', L3 = x\L3')
============================
 forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}@ -> (exists L3', L3 = x\L3')

crev_prune < intros.

Variables: L1 L2 L3
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
       (exists L3', L3 = x\L3')
H1 : {crev L1 L2 (L3 n1)}@
============================
 exists L3', L3 = x\L3'

crev_prune < case H1.
Subgoal 1:

Variables: L2
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
       (exists L3', L3 = x\L3')
============================
 exists L3', z1\L2 = x\L3'

Subgoal 2 is:
 exists L3', L3 = x\L3'

crev_prune < search.
Subgoal 2:

Variables: L2 L3 L6 L7
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
       (exists L3', L3 = x\L3')
H2 : {crev L7 (ccons L6 L2) (L3 n1)}*
============================
 exists L3', L3 = x\L3'

crev_prune < apply IH to H2.
Subgoal 2:

Variables: L2 L6 L7 L3'
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
       (exists L3', L3 = x\L3')
H2 : {crev L7 (ccons L6 L2) L3'}*
============================
 exists L3'1, z1\L3' = x\L3'1

crev_prune < search.
Proof completed.
Abella < Theorem tm'_list_to_tuple_det : 
forall FE E E', {tm'_list_to_tuple FE E} -> {tm'_list_to_tuple FE E'} -> E =
E'.


============================
 forall FE E E', {tm'_list_to_tuple FE E} -> {tm'_list_to_tuple FE E'} -> E =
 E'

tm'_list_to_tuple_det < induction on 1.

IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
       {tm'_list_to_tuple FE E'} -> E =
     E'
============================
 forall FE E E', {tm'_list_to_tuple FE E}@ -> {tm'_list_to_tuple FE E'} ->
   E =
 E'

tm'_list_to_tuple_det < intros.

Variables: FE E E'
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
       {tm'_list_to_tuple FE E'} -> E =
     E'
H1 : {tm'_list_to_tuple FE E}@
H2 : {tm'_list_to_tuple FE E'}
============================
 E = E'

tm'_list_to_tuple_det < case H1.
Subgoal 1:

Variables: E'
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
       {tm'_list_to_tuple FE E'} -> E =
     E'
H2 : {tm'_list_to_tuple cnil E'}
============================
 unit' = E'

Subgoal 2 is:
 pair' M ML' = E'

tm'_list_to_tuple_det < case H2.
Subgoal 1:

IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
       {tm'_list_to_tuple FE E'} -> E =
     E'
============================
 unit' = unit'

Subgoal 2 is:
 pair' M ML' = E'

tm'_list_to_tuple_det < search.
Subgoal 2:

Variables: E' ML' ML M
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
       {tm'_list_to_tuple FE E'} -> E =
     E'
H2 : {tm'_list_to_tuple (ccons M ML) E'}
H3 : {tm'_list_to_tuple ML ML'}*
============================
 pair' M ML' = E'

tm'_list_to_tuple_det < case H2.
Subgoal 2:

Variables: ML' ML M ML'1
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
       {tm'_list_to_tuple FE E'} -> E =
     E'
H3 : {tm'_list_to_tuple ML ML'}*
H4 : {tm'_list_to_tuple ML ML'1}
============================
 pair' M ML' = pair' M ML'1

tm'_list_to_tuple_det < apply IH to H3 H4.
Subgoal 2:

Variables: ML M ML'1
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
       {tm'_list_to_tuple FE E'} -> E =
     E'
H3 : {tm'_list_to_tuple ML ML'1}*
H4 : {tm'_list_to_tuple ML ML'1}
============================
 pair' M ML'1 = pair' M ML'1

tm'_list_to_tuple_det < search.
Proof completed.
Abella < Theorem tm'_list_to_tuple_exists : 
forall L, is_tm'_list L -> (exists E, {tm'_list_to_tuple L E}).


============================
 forall L, is_tm'_list L -> (exists E, {tm'_list_to_tuple L E})

tm'_list_to_tuple_exists < induction on 1.

IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
============================
 forall L, is_tm'_list L @ -> (exists E, {tm'_list_to_tuple L E})

tm'_list_to_tuple_exists < intros.

Variables: L
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
H1 : is_tm'_list L @
============================
 exists E, {tm'_list_to_tuple L E}

tm'_list_to_tuple_exists < case H1.
Subgoal 1:

IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
============================
 exists E, {tm'_list_to_tuple cnil E}

Subgoal 2 is:
 exists E, {tm'_list_to_tuple (ccons X L1) E}

tm'_list_to_tuple_exists < search.
Subgoal 2:

Variables: L1 X
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
H2 : is_tm'_list L1 *
============================
 exists E, {tm'_list_to_tuple (ccons X L1) E}

tm'_list_to_tuple_exists < apply IH to H2.
Subgoal 2:

Variables: L1 X E
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
H2 : is_tm'_list L1 *
H3 : {tm'_list_to_tuple L1 E}
============================
 exists E, {tm'_list_to_tuple (ccons X L1) E}

tm'_list_to_tuple_exists < search.
Proof completed.
Abella < Theorem tm'_list_to_tuple_prune : 
forall L E, nabla x, {tm'_list_to_tuple L (E x)} -> (exists E', E = y\E').


============================
 forall L E, nabla x, {tm'_list_to_tuple L (E x)} -> (exists E', E = y\E')

tm'_list_to_tuple_prune < induction on 1.

IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
       (exists E', E = y\E')
============================
 forall L E, nabla x, {tm'_list_to_tuple L (E x)}@ -> (exists E', E = y\E')

tm'_list_to_tuple_prune < intros.

Variables: L E
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
       (exists E', E = y\E')
H1 : {tm'_list_to_tuple L (E n1)}@
============================
 exists E', E = y\E'

tm'_list_to_tuple_prune < case H1.
Subgoal 1:

IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
       (exists E', E = y\E')
============================
 exists E', z1\unit' = y\E'

Subgoal 2 is:
 exists E', z1\pair' L1 (ML' z1) = y\E'

tm'_list_to_tuple_prune < search.
Subgoal 2:

Variables: ML' L2 L1
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
       (exists E', E = y\E')
H2 : {tm'_list_to_tuple L2 (ML' n1)}*
============================
 exists E', z1\pair' L1 (ML' z1) = y\E'

tm'_list_to_tuple_prune < apply IH to H2.
Subgoal 2:

Variables: L2 L1 E'
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
       (exists E', E = y\E')
H2 : {tm'_list_to_tuple L2 E'}*
============================
 exists E'1, z1\pair' L1 E' = y\E'1

tm'_list_to_tuple_prune < search.
Proof completed.
Abella <