Welcome to Abella 2.0.5-dev

Abella < Specification "trans".
Reading specification "/home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/./trans" (from "/home/yuting/Projects/svn_sparrow/compiler-correctness/website/wang-phd-thesis/code/.")

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 : (list A) -> prop by 
is_list nil;
is_list (X :: L) := is_list L.

Abella < Theorem is_list_inst [A,B] : 
forall L V, nabla x, is_list (L x) -> is_list (L V).

============================
 forall L V, nabla x, is_list (L x) -> is_list (L V)

is_list_inst < induction on 1.

IH : forall L V, nabla x, is_list (L x) * -> is_list (L V)
============================
 forall L V, nabla x, is_list (L x) @ -> is_list (L V)

is_list_inst < intros.

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

is_list_inst < case H1.

Subgoal 1:

Variables: V
IH : forall L V, nabla x, is_list (L x) * -> is_list (L V)
============================
 is_list nil

Subgoal 2 is:
 is_list (X V :: L1 V)

is_list_inst < search.

Subgoal 2:

Variables: V L1 X
IH : forall L V, nabla x, is_list (L x) * -> is_list (L V)
H2 : is_list (L1 n1) *
============================
 is_list (X V :: L1 V)

is_list_inst < apply IH to H2 with V = V.

Subgoal 2:

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

is_list_inst < search.
Proof completed.

Abella < Define list_length : (list A) -> nat -> prop by 
list_length nil z;
list_length (M :: ML) (s N) := list_length ML N.

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

Abella < Theorem append_refl [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 < Theorem append_prune [A,B] : 
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 < 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 < 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 < 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 < 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 < 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 < search.
Proof completed.

Abella < Define subset : (list A) -> (list A) -> prop by 
subset nil L;
subset (X :: L1) L2 := member X L2 /\ subset L1 L2.

Abella < Theorem subset_add [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 [A] : 
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 < Theorem rev_det [A] : 
forall L1 L2 L3 L3', {rev L1 L2 L3} -> {rev L1 L2 L3'} -> L3 = L3'.

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

rev_det < induction on 1.

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

rev_det < intros.

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

rev_det < case H1.

Subgoal 1:

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

Subgoal 2 is:
 L3 = L3'

rev_det < case H2.

Subgoal 1:

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

Subgoal 2 is:
 L3 = L3'

rev_det < search.

Subgoal 2:

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

rev_det < case H2.

Subgoal 2:

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

rev_det < apply IH to H3 H4.

Subgoal 2:

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

rev_det < search.
Proof completed.

Abella < Theorem rev_prune [A,B] : 
forall L1 L2 L3, nabla x, {rev L1 L2 (L3 x)} -> (exists L3', L3 = x\L3').

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

rev_prune < induction on 1.

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

rev_prune < intros.

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

rev_prune < case H1.

Subgoal 1:

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

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

rev_prune < search.

Subgoal 2:

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

rev_prune < apply IH to H2.

Subgoal 2:

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

rev_prune < search.
Proof completed.

Abella < Define ssubset : (list A) -> (list A) -> prop by 
ssubset nil L;
ssubset (X :: L1) L2 := {memb X L2} /\ ssubset L1 L2.

Abella < Theorem appd_refl_eq [A] : 
forall L1 L2, {appd L1 nil L2} -> L1 = L2.

============================
 forall L1 L2, {appd L1 nil L2} -> L1 = L2

appd_refl_eq < induction on 1.

IH : forall L1 L2, {appd L1 nil L2}* -> L1 = L2
============================
 forall L1 L2, {appd L1 nil L2}@ -> L1 = L2

appd_refl_eq < intros.

Variables: L1 L2
IH : forall L1 L2, {appd L1 nil L2}* -> L1 = L2
H1 : {appd L1 nil L2}@
============================
 L1 = L2

appd_refl_eq < case H1.

Subgoal 1:

IH : forall L1 L2, {appd L1 nil L2}* -> L1 = L2
============================
 nil = nil

Subgoal 2 is:
 X :: L5 = X :: L3

appd_refl_eq < search.

Subgoal 2:

Variables: L3 L5 X
IH : forall L1 L2, {appd L1 nil L2}* -> L1 = L2
H2 : {appd L5 nil L3}*
============================
 X :: L5 = X :: L3

appd_refl_eq < apply IH to H2.

Subgoal 2:

Variables: L3 X
IH : forall L1 L2, {appd L1 nil L2}* -> L1 = L2
H2 : {appd L3 nil L3}*
============================
 X :: L3 = X :: L3

appd_refl_eq < search.
Proof completed.

Abella < Theorem ssubset_add [A] : 
forall L L' X, ssubset L L' -> ssubset L (X :: L').

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

ssubset_add < induction on 1.

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

ssubset_add < intros.

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

ssubset_add < case H1.

Subgoal 1:

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

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

ssubset_add < search.

Subgoal 2:

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

ssubset_add < unfold.

Subgoal 2.1:

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

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

ssubset_add < search.

Subgoal 2.2:

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

ssubset_add < backchain IH.
Proof completed.

Abella < Theorem ssubset_refl [A] : 
forall L, is_list L -> ssubset L L.

============================
 forall L, is_list L -> ssubset L L

ssubset_refl < induction on 1.

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

ssubset_refl < intros.

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

ssubset_refl < case H1.

Subgoal 1:

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

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

ssubset_refl < search.

Subgoal 2:

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

ssubset_refl < unfold.

Subgoal 2.1:

Variables: L1 X
IH : forall L, is_list L * -> ssubset L L
H2 : is_list L1 *
============================
 {memb X (X :: L1)}

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

ssubset_refl < search.

Subgoal 2.2:

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

ssubset_refl < backchain ssubset_add.

Subgoal 2.2:

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

ssubset_refl < backchain IH.
Proof completed.

Abella < Theorem ssubset_mem_trans [A] : 
forall L1 L2 X, ssubset L1 L2 -> {memb X L1} -> {memb X L2}.

============================
 forall L1 L2 X, ssubset L1 L2 -> {memb X L1} -> {memb X L2}

ssubset_mem_trans < induction on 2.

IH : forall L1 L2 X, ssubset L1 L2 -> {memb X L1}* -> {memb X L2}
============================
 forall L1 L2 X, ssubset L1 L2 -> {memb X L1}@ -> {memb X L2}

ssubset_mem_trans < intros.

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

ssubset_mem_trans < case H2.

Subgoal 1:

Variables: L2 X L
IH : forall L1 L2 X, ssubset L1 L2 -> {memb X L1}* -> {memb X L2}
H1 : ssubset (X :: L) L2
============================
 {memb X L2}

Subgoal 2 is:
 {memb X L2}

ssubset_mem_trans < case H1.

Subgoal 1:

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

Subgoal 2 is:
 {memb X L2}

ssubset_mem_trans < search.

Subgoal 2:

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

ssubset_mem_trans < case H1.

Subgoal 2:

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

ssubset_mem_trans < backchain IH.
Proof completed.

Abella < Theorem ssubset_trans [A] : 
forall L1 L2 L3, ssubset L1 L2 -> ssubset L2 L3 -> ssubset L1 L3.

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

ssubset_trans < induction on 1.

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

ssubset_trans < intros.

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

ssubset_trans < case H1.

Subgoal 1:

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

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

ssubset_trans < search.

Subgoal 2:

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

ssubset_trans < unfold.

Subgoal 2.1:

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

Subgoal 2.2 is:
 ssubset L4 L3

ssubset_trans < backchain ssubset_mem_trans.

Subgoal 2.2:

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

ssubset_trans < backchain IH.
Proof completed.

Abella < Theorem ssubset_extend [A] : 
forall L L' X, ssubset L L' -> ssubset (X :: L) (X :: L').

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

ssubset_extend < intros.

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

ssubset_extend < unfold.

Subgoal 1:

Variables: L L' X
H1 : ssubset L L'
============================
 {memb X (X :: L')}

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

ssubset_extend < search.

Subgoal 2:

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

ssubset_extend < backchain ssubset_add.
Proof completed.

Abella < Theorem member_prune [A,B] : 
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 < 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 < 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 < 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 < 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 < 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 < search.
Proof completed.

Abella < Theorem memb_prune [A,B] : 
forall M L, nabla x, {memb (M x) L} -> (exists M', M = y\M').

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

memb_prune < induction on 1.

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

memb_prune < intros.

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

memb_prune < case H1.

Subgoal 1:

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

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

memb_prune < search.

Subgoal 2:

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

memb_prune < apply IH to H2.

Subgoal 2:

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

memb_prune < search.
Proof completed.

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

Abella < Theorem combine_subset [A] : 
forall L1 L2 L, is_list L -> {combine L1 L2 L} -> ssubset L1 L /\
  ssubset L2 L.

============================
 forall L1 L2 L, is_list L -> {combine L1 L2 L} -> ssubset L1 L /\
   ssubset L2 L

combine_subset < induction on 2.

IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
============================
 forall L1 L2 L, is_list L -> {combine L1 L2 L}@ -> ssubset L1 L /\
   ssubset L2 L

combine_subset < intros.

Variables: L1 L2 L
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list L
H2 : {combine L1 L2 L}@
============================
 ssubset L1 L /\ ssubset L2 L

combine_subset < case H2.

Subgoal 1:

Variables: L
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list L
============================
 ssubset nil L /\ ssubset L L

Subgoal 2 is:
 ssubset (X :: L5) L /\ ssubset L2 L

Subgoal 3 is:
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < split.

Subgoal 1.1:

Variables: L
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list L
============================
 ssubset nil L

Subgoal 1.2 is:
 ssubset L L

Subgoal 2 is:
 ssubset (X :: L5) L /\ ssubset L2 L

Subgoal 3 is:
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < search.

Subgoal 1.2:

Variables: L
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list L
============================
 ssubset L L

Subgoal 2 is:
 ssubset (X :: L5) L /\ ssubset L2 L

Subgoal 3 is:
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < backchain ssubset_refl.

Subgoal 2:

Variables: L2 L L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list L
H3 : {memb X L2}*
H4 : {combine L5 L2 L}*
============================
 ssubset (X :: L5) L /\ ssubset L2 L

Subgoal 3 is:
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < apply IH to _ H4.

Subgoal 2:

Variables: L2 L L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list L
H3 : {memb X L2}*
H4 : {combine L5 L2 L}*
H5 : ssubset L5 L
H6 : ssubset L2 L
============================
 ssubset (X :: L5) L /\ ssubset L2 L

Subgoal 3 is:
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < apply ssubset_mem_trans to H6 H3.

Subgoal 2:

Variables: L2 L L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list L
H3 : {memb X L2}*
H4 : {combine L5 L2 L}*
H5 : ssubset L5 L
H6 : ssubset L2 L
H7 : {memb X L}
============================
 ssubset (X :: L5) L /\ ssubset L2 L

Subgoal 3 is:
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < search.

Subgoal 3:

Variables: L2 L3 L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H1 : is_list (X :: L3)
H3 : {combine L5 L2 L3}*
============================
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < case H1.

Subgoal 3:

Variables: L2 L3 L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H3 : {combine L5 L2 L3}*
H4 : is_list L3
============================
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < apply IH to _ H3.

Subgoal 3:

Variables: L2 L3 L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H3 : {combine L5 L2 L3}*
H4 : is_list L3
H5 : ssubset L5 L3
H6 : ssubset L2 L3
============================
 ssubset (X :: L5) (X :: L3) /\ ssubset L2 (X :: L3)

combine_subset < split.

Subgoal 3.1:

Variables: L2 L3 L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H3 : {combine L5 L2 L3}*
H4 : is_list L3
H5 : ssubset L5 L3
H6 : ssubset L2 L3
============================
 ssubset (X :: L5) (X :: L3)

Subgoal 3.2 is:
 ssubset L2 (X :: L3)

combine_subset < backchain ssubset_extend.

Subgoal 3.2:

Variables: L2 L3 L5 X
IH : forall L1 L2 L, is_list L -> {combine L1 L2 L}* -> ssubset L1 L /\
       ssubset L2 L
H3 : {combine L5 L2 L3}*
H4 : is_list L3
H5 : ssubset L5 L3
H6 : ssubset L2 L3
============================
 ssubset L2 (X :: L3)

combine_subset < backchain ssubset_add.
Proof completed.

Abella < Theorem combine_sub1 [A] : 
forall L1 L2 L, is_list L -> {combine L1 L2 L} -> ssubset L1 L.

============================
 forall L1 L2 L, is_list L -> {combine L1 L2 L} -> ssubset L1 L

combine_sub1 < intros.

Variables: L1 L2 L
H1 : is_list L
H2 : {combine L1 L2 L}
============================
 ssubset L1 L

combine_sub1 < apply combine_subset to _ H2.

Variables: L1 L2 L
H1 : is_list L
H2 : {combine L1 L2 L}
H3 : ssubset L1 L
H4 : ssubset L2 L
============================
 ssubset L1 L

combine_sub1 < search.
Proof completed.

Abella < Theorem combine_sub2 [A] : 
forall L1 L2 L, is_list L -> {combine L1 L2 L} -> ssubset L2 L.

============================
 forall L1 L2 L, is_list L -> {combine L1 L2 L} -> ssubset L2 L

combine_sub2 < intros.

Variables: L1 L2 L
H1 : is_list L
H2 : {combine L1 L2 L}
============================
 ssubset L2 L

combine_sub2 < apply combine_subset to _ H2.

Variables: L1 L2 L
H1 : is_list L
H2 : {combine L1 L2 L}
H3 : ssubset L1 L
H4 : ssubset L2 L
============================
 ssubset L2 L

combine_sub2 < 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 nil 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 (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_list L -> (exists E, {tm'_list_to_tuple L E}).

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

tm'_list_to_tuple_exists < induction on 1.

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

tm'_list_to_tuple_exists < intros.

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

tm'_list_to_tuple_exists < case H1.

Subgoal 1:

IH : forall L, is_list L * -> (exists E, {tm'_list_to_tuple L E})
============================
 exists E, {tm'_list_to_tuple nil E}

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

tm'_list_to_tuple_exists < search.

Subgoal 2:

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

tm'_list_to_tuple_exists < apply IH to H2.

Subgoal 2:

Variables: L1 X E
IH : forall L, is_list L * -> (exists E, {tm'_list_to_tuple L E})
H2 : is_list L1 *
H3 : {tm'_list_to_tuple L1 E}
============================
 exists E, {tm'_list_to_tuple (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 < Define app_subst : (list (map A A)) -> B -> B -> prop by 
app_subst nil M M;
nabla x, app_subst (map x V :: ML) (R x) M := app_subst ML (R V) M.

Abella < Theorem app_subst_det [A,B] : 
forall ML M M' M'', app_subst ML M M' -> app_subst ML M M'' -> M' = M''.

============================
 forall ML M M' M'', app_subst ML M M' -> app_subst ML M M'' -> M' = M''

app_subst_det < induction on 1.

IH : forall ML M M' M'', app_subst ML M M' * -> app_subst ML M M'' -> M' =
     M''
============================
 forall ML M M' M'', app_subst ML M M' @ -> app_subst ML M M'' -> M' = M''

app_subst_det < intros.

Variables: ML M M' M''
IH : forall ML M M' M'', app_subst ML M M' * -> app_subst ML M M'' -> M' =
     M''
H1 : app_subst ML M M' @
H2 : app_subst ML M M''
============================
 M' = M''

app_subst_det < case H1.

Subgoal 1:

Variables: M' M''
IH : forall ML M M' M'', app_subst ML M M' * -> app_subst ML M M'' -> M' =
     M''
H2 : app_subst nil M' M''
============================
 M' = M''

Subgoal 2 is:
 M1 = M'' n1

app_subst_det < case H2.

Subgoal 1:

Variables: M''
IH : forall ML M M' M'', app_subst ML M M' * -> app_subst ML M M'' -> M' =
     M''
============================
 M'' = M''

Subgoal 2 is:
 M1 = M'' n1

app_subst_det < search.

Subgoal 2:

Variables: M M'' M1 ML1 V
IH : forall ML M M' M'', app_subst ML M M' * -> app_subst ML M M'' -> M' =
     M''
H2 : app_subst (map n1 V :: ML1) (M n1) (M'' n1)
H3 : app_subst ML1 (M V) M1 *
============================
 M1 = M'' n1

app_subst_det < case H2.

Subgoal 2:

Variables: M M1 ML1 V M2
IH : forall ML M M' M'', app_subst ML M M' * -> app_subst ML M M'' -> M' =
     M''
H3 : app_subst ML1 (M V) M1 *
H4 : app_subst ML1 (M V) M2
============================
 M1 = M2

app_subst_det < apply IH to H3 H4.

Subgoal 2:

Variables: M ML1 V M2
IH : forall ML M M' M'', app_subst ML M M' * -> app_subst ML M M'' -> M' =
     M''
H3 : app_subst ML1 (M V) M2 *
H4 : app_subst ML1 (M V) M2
============================
 M2 = M2

app_subst_det < search.
Proof completed.

Abella < Theorem app_subst_prune [A,B,C] : 
forall ML M M', nabla x, app_subst ML M (M' x) -> (exists M'', M' = y\M'').

============================
 forall ML M M', nabla x, app_subst ML M (M' x) -> (exists M'', M' = y\M'')

app_subst_prune < induction on 1.

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

app_subst_prune < intros.

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

app_subst_prune < case H1.

Subgoal 1:

Variables: M
IH : forall ML M M', nabla x, app_subst ML M (M' x) * ->
       (exists M'', M' = y\M'')
============================
 exists M'', z1\M = y\M''

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

app_subst_prune < search.

Subgoal 2:

Variables: M M2 ML3 ML2
IH : forall ML M M', nabla x, app_subst ML M (M' x) * ->
       (exists M'', M' = y\M'')
H2 : app_subst ML3 (M ML2) (M2 n1) *
============================
 exists M'', z2\M2 z2 = y\M''

app_subst_prune < apply IH to H2.

Subgoal 2:

Variables: M ML3 ML2 M''
IH : forall ML M M', nabla x, app_subst ML M (M' x) * ->
       (exists M'', M' = y\M'')
H2 : app_subst ML3 (M ML2) M'' *
============================
 exists M''1, z2\M'' = y\M''1

app_subst_prune < search.
Proof completed.

Abella < Theorem app_subst_inst [A,B,C] : 
forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
  app_subst ML (M2 x) (M2' x) -> app_subst ML (M2 M1) (M2' M1').

============================
 forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
   app_subst ML (M2 x) (M2' x) -> app_subst ML (M2 M1) (M2' M1')

app_subst_inst < induction on 2.

IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
       app_subst ML (M2 x) (M2' x) * -> app_subst ML (M2 M1) (M2' M1')
============================
 forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
   app_subst ML (M2 x) (M2' x) @ -> app_subst ML (M2 M1) (M2' M1')

app_subst_inst < intros.

Variables: ML M1 M2 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
       app_subst ML (M2 x) (M2' x) * -> app_subst ML (M2 M1) (M2' M1')
H1 : app_subst ML M1 M1'
H2 : app_subst ML (M2 n1) (M2' n1) @
============================
 app_subst ML (M2 M1) (M2' M1')

app_subst_inst < case H2.

Subgoal 1:

Variables: M1 M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
       app_subst ML (M2 x) (M2' x) * -> app_subst ML (M2 M1) (M2' M1')
H1 : app_subst nil M1 M1'
============================
 app_subst nil (M2' M1) (M2' M1')

Subgoal 2 is:
 app_subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 (M1' n2))

app_subst_inst < case H1.

Subgoal 1:

Variables: M1' M2'
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
       app_subst ML (M2 x) (M2' x) * -> app_subst ML (M2 M1) (M2' M1')
============================
 app_subst nil (M2' M1') (M2' M1')

Subgoal 2 is:
 app_subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 (M1' n2))

app_subst_inst < search.

Subgoal 2:

Variables: M1 M2 M1' M3 ML3 ML2
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
       app_subst ML (M2 x) (M2' x) * -> app_subst ML (M2 M1) (M2' M1')
H1 : app_subst (map n2 ML2 :: ML3) (M1 n2) (M1' n2)
H3 : app_subst ML3 (M2 ML2 n1) (M3 n1) *
============================
 app_subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 (M1' n2))

app_subst_inst < case H1.

Subgoal 2:

Variables: M1 M2 M3 ML3 ML2 M
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
       app_subst ML (M2 x) (M2' x) * -> app_subst ML (M2 M1) (M2' M1')
H3 : app_subst ML3 (M2 ML2 n1) (M3 n1) *
H4 : app_subst ML3 (M1 ML2) M
============================
 app_subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 M)

app_subst_inst < apply IH to H4 H3.

Subgoal 2:

Variables: M1 M2 M3 ML3 ML2 M
IH : forall ML M1 M2 M1' M2', nabla x, app_subst ML M1 M1' ->
       app_subst ML (M2 x) (M2' x) * -> app_subst ML (M2 M1) (M2' M1')
H3 : app_subst ML3 (M2 ML2 n1) (M3 n1) *
H4 : app_subst ML3 (M1 ML2) M
H5 : app_subst ML3 (M2 ML2 (M1 ML2)) (M3 M)
============================
 app_subst (map n2 ML2 :: ML3) (M2 n2 (M1 n2)) (M3 M)

app_subst_inst < search.
Proof completed.

Abella < Define app_subst_list : (list (map A A)) -> (list B) -> (list B) -> prop by 
app_subst_list nil L L;
nabla x, app_subst_list (map x V :: ML) (L x) L' := app_subst_list ML (L V) L'.

Abella < Theorem app_subst_islist_trans [A,B] : 
forall L L' ML, is_list L -> app_subst_list ML L L' -> is_list L'.

============================
 forall L L' ML, is_list L -> app_subst_list ML L L' -> is_list L'

app_subst_islist_trans < induction on 2.

IH : forall L L' ML, is_list L -> app_subst_list ML L L' * -> is_list L'
============================
 forall L L' ML, is_list L -> app_subst_list ML L L' @ -> is_list L'

app_subst_islist_trans < intros.

Variables: L L' ML
IH : forall L L' ML, is_list L -> app_subst_list ML L L' * -> is_list L'
H1 : is_list L
H2 : app_subst_list ML L L' @
============================
 is_list L'

app_subst_islist_trans < case H2.

Subgoal 1:

Variables: L'
IH : forall L L' ML, is_list L -> app_subst_list ML L L' * -> is_list L'
H1 : is_list L'
============================
 is_list L'

Subgoal 2 is:
 is_list L'1

app_subst_islist_trans < search.

Subgoal 2:

Variables: L L'1 ML1 V
IH : forall L L' ML, is_list L -> app_subst_list ML L L' * -> is_list L'
H1 : is_list (L n1)
H3 : app_subst_list ML1 (L V) L'1 *
============================
 is_list L'1

app_subst_islist_trans < apply is_list_inst to H1 with V = V.

Subgoal 2:

Variables: L L'1 ML1 V
IH : forall L L' ML, is_list L -> app_subst_list ML L L' * -> is_list L'
H1 : is_list (L n1)
H3 : app_subst_list ML1 (L V) L'1 *
H4 : is_list (L V)
============================
 is_list L'1

app_subst_islist_trans < apply IH to H4 H3.

Subgoal 2:

Variables: L L'1 ML1 V
IH : forall L L' ML, is_list L -> app_subst_list ML L L' * -> is_list L'
H1 : is_list (L n1)
H3 : app_subst_list ML1 (L V) L'1 *
H4 : is_list (L V)
H5 : is_list L'1
============================
 is_list L'1

app_subst_islist_trans < search.
Proof completed.

Abella < Theorem app_subst_list_nil_comm [A,B] : 
forall ML M, app_subst_list ML nil M -> M = nil.

============================
 forall ML M, app_subst_list ML nil M -> M = nil

app_subst_list_nil_comm < induction on 1.

IH : forall ML M, app_subst_list ML nil M * -> M = nil
============================
 forall ML M, app_subst_list ML nil M @ -> M = nil

app_subst_list_nil_comm < intros.

Variables: ML M
IH : forall ML M, app_subst_list ML nil M * -> M = nil
H1 : app_subst_list ML nil M @
============================
 M = nil

app_subst_list_nil_comm < case H1.

Subgoal 1:

IH : forall ML M, app_subst_list ML nil M * -> M = nil
============================
 nil = nil

Subgoal 2 is:
 L' = nil

app_subst_list_nil_comm < search.

Subgoal 2:

Variables: L' ML1 V
IH : forall ML M, app_subst_list ML nil M * -> M = nil
H2 : app_subst_list ML1 nil L' *
============================
 L' = nil

app_subst_list_nil_comm < apply IH to H2.

Subgoal 2:

Variables: ML1 V
IH : forall ML M, app_subst_list ML nil M * -> M = nil
H2 : app_subst_list ML1 nil nil *
============================
 nil = nil

app_subst_list_nil_comm < search.
Proof completed.

Abella < Theorem app_subst_list_comm1 [A,B] : 
forall ML X L M, app_subst_list ML (X :: L) M ->
  (exists X' L', M = X' :: L' /\ app_subst ML X X' /\ app_subst_list ML L L').

============================
 forall ML X L M, app_subst_list ML (X :: L) M ->
   (exists X' L', M = X' :: L' /\ app_subst ML X X' /\
        app_subst_list ML L L')

app_subst_list_comm1 < induction on 1.

IH : forall ML X L M, app_subst_list ML (X :: L) M * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X X' /\
            app_subst_list ML L L')
============================
 forall ML X L M, app_subst_list ML (X :: L) M @ ->
   (exists X' L', M = X' :: L' /\ app_subst ML X X' /\
        app_subst_list ML L L')

app_subst_list_comm1 < intros.

Variables: ML X L M
IH : forall ML X L M, app_subst_list ML (X :: L) M * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X X' /\
            app_subst_list ML L L')
H1 : app_subst_list ML (X :: L) M @
============================
 exists X' L', M = X' :: L' /\ app_subst ML X X' /\ app_subst_list ML L L'

app_subst_list_comm1 < case H1.

Subgoal 1:

Variables: X L
IH : forall ML X L M, app_subst_list ML (X :: L) M * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X X' /\
            app_subst_list ML L L')
============================
 exists X' L', X :: L = X' :: L' /\ app_subst nil X X' /\
   app_subst_list nil L L'

Subgoal 2 is:
 exists X' L'1, L' = X' :: L'1 /\ app_subst (map n1 V :: ML1) (X n1) X' /\
   app_subst_list (map n1 V :: ML1) (L n1) L'1

app_subst_list_comm1 < search.

Subgoal 2:

Variables: X L L' ML1 V
IH : forall ML X L M, app_subst_list ML (X :: L) M * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X X' /\
            app_subst_list ML L L')
H2 : app_subst_list ML1 (X V :: L V) L' *
============================
 exists X' L'1, L' = X' :: L'1 /\ app_subst (map n1 V :: ML1) (X n1) X' /\
   app_subst_list (map n1 V :: ML1) (L n1) L'1

app_subst_list_comm1 < apply IH to H2.

Subgoal 2:

Variables: X L ML1 V X' L'1
IH : forall ML X L M, app_subst_list ML (X :: L) M * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X X' /\
            app_subst_list ML L L')
H2 : app_subst_list ML1 (X V :: L V) (X' :: L'1) *
H3 : app_subst ML1 (X V) X'
H4 : app_subst_list ML1 (L V) L'1
============================
 exists X'1 L'2, X' :: L'1 = X'1 :: L'2 /\
   app_subst (map n1 V :: ML1) (X n1) X'1 /\
   app_subst_list (map n1 V :: ML1) (L n1) L'2

app_subst_list_comm1 < search.
Proof completed.

Abella < Theorem app_subst_list_comm2 [A,B] : 
forall ML X L M, is_list M -> app_subst_list ML M (X :: L) ->
  (exists X' L', M = X' :: L' /\ app_subst ML X' X /\ app_subst_list ML L' L).

============================
 forall ML X L M, is_list M -> app_subst_list ML M (X :: L) ->
   (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
        app_subst_list ML L' L)

app_subst_list_comm2 < induction on 2.

IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
============================
 forall ML X L M, is_list M -> app_subst_list ML M (X :: L) @ ->
   (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
        app_subst_list ML L' L)

app_subst_list_comm2 < intros.

Variables: ML X L M
IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
H1 : is_list M
H2 : app_subst_list ML M (X :: L) @
============================
 exists X' L', M = X' :: L' /\ app_subst ML X' X /\ app_subst_list ML L' L

app_subst_list_comm2 < case H2.

Subgoal 1:

Variables: X L
IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
H1 : is_list (X :: L)
============================
 exists X' L', X :: L = X' :: L' /\ app_subst nil X' X /\
   app_subst_list nil L' L

Subgoal 2 is:
 exists X' L', M n1 = X' :: L' /\ app_subst (map n1 V :: ML1) X' L'1 /\
   app_subst_list (map n1 V :: ML1) L' L'2

app_subst_list_comm2 < search.

Subgoal 2:

Variables: M L'2 L'1 ML1 V
IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
H1 : is_list (M n1)
H3 : app_subst_list ML1 (M V) (L'1 :: L'2) *
============================
 exists X' L', M n1 = X' :: L' /\ app_subst (map n1 V :: ML1) X' L'1 /\
   app_subst_list (map n1 V :: ML1) L' L'2

app_subst_list_comm2 < apply is_list_inst to H1 with V = V.

Subgoal 2:

Variables: M L'2 L'1 ML1 V
IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
H1 : is_list (M n1)
H3 : app_subst_list ML1 (M V) (L'1 :: L'2) *
H4 : is_list (M V)
============================
 exists X' L', M n1 = X' :: L' /\ app_subst (map n1 V :: ML1) X' L'1 /\
   app_subst_list (map n1 V :: ML1) L' L'2

app_subst_list_comm2 < case H1.

Subgoal 2.1:

Variables: L'2 L'1 ML1 V
IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
H3 : app_subst_list ML1 nil (L'1 :: L'2) *
H4 : is_list nil
============================
 exists X' L', nil = X' :: L' /\ app_subst (map n1 V :: ML1) X' L'1 /\
   app_subst_list (map n1 V :: ML1) L' L'2

Subgoal 2.2 is:
 exists X' L', X1 n1 :: L1 n1 = X' :: L' /\
   app_subst (map n1 V :: ML1) X' L'1 /\
   app_subst_list (map n1 V :: ML1) L' L'2

app_subst_list_comm2 < apply IH to _ H3.

Subgoal 2.2:

Variables: L'2 L'1 ML1 V L1 X1
IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
H3 : app_subst_list ML1 (X1 V :: L1 V) (L'1 :: L'2) *
H4 : is_list (X1 V :: L1 V)
H5 : is_list (L1 n1)
============================
 exists X' L', X1 n1 :: L1 n1 = X' :: L' /\
   app_subst (map n1 V :: ML1) X' L'1 /\
   app_subst_list (map n1 V :: ML1) L' L'2

app_subst_list_comm2 < apply IH to H4 H3.

Subgoal 2.2:

Variables: L'2 L'1 ML1 V L1 X1
IH : forall ML X L M, is_list M -> app_subst_list ML M (X :: L) * ->
       (exists X' L', M = X' :: L' /\ app_subst ML X' X /\
            app_subst_list ML L' L)
H3 : app_subst_list ML1 (X1 V :: L1 V) (L'1 :: L'2) *
H4 : is_list (X1 V :: L1 V)
H5 : is_list (L1 n1)
H6 : app_subst ML1 (X1 V) L'1
H7 : app_subst_list ML1 (L1 V) L'2
============================
 exists X' L', X1 n1 :: L1 n1 = X' :: L' /\
   app_subst (map n1 V :: ML1) X' L'1 /\
   app_subst_list (map n1 V :: ML1) L' L'2

app_subst_list_comm2 < search.
Proof completed.

Abella < Theorem app_subst_list_compose [A,B] : 
forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' ->
  app_subst_list ML (X :: L) (X' :: L').

============================
 forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' ->
   app_subst_list ML (X :: L) (X' :: L')

app_subst_list_compose < induction on 2.

IH : forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' * ->
       app_subst_list ML (X :: L) (X' :: L')
============================
 forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' @ ->
   app_subst_list ML (X :: L) (X' :: L')

app_subst_list_compose < intros.

Variables: ML X X' L L'
IH : forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' * ->
       app_subst_list ML (X :: L) (X' :: L')
H1 : app_subst ML X X'
H2 : app_subst_list ML L L' @
============================
 app_subst_list ML (X :: L) (X' :: L')

app_subst_list_compose < case H2.

Subgoal 1:

Variables: X X' L'
IH : forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' * ->
       app_subst_list ML (X :: L) (X' :: L')
H1 : app_subst nil X X'
============================
 app_subst_list nil (X :: L') (X' :: L')

Subgoal 2 is:
 app_subst_list (map n1 V :: ML1) (X n1 :: L n1) (X' n1 :: L'1)

app_subst_list_compose < case H1.

Subgoal 1:

Variables: X' L'
IH : forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' * ->
       app_subst_list ML (X :: L) (X' :: L')
============================
 app_subst_list nil (X' :: L') (X' :: L')

Subgoal 2 is:
 app_subst_list (map n1 V :: ML1) (X n1 :: L n1) (X' n1 :: L'1)

app_subst_list_compose < search.

Subgoal 2:

Variables: X X' L L'1 ML1 V
IH : forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' * ->
       app_subst_list ML (X :: L) (X' :: L')
H1 : app_subst (map n1 V :: ML1) (X n1) (X' n1)
H3 : app_subst_list ML1 (L V) L'1 *
============================
 app_subst_list (map n1 V :: ML1) (X n1 :: L n1) (X' n1 :: L'1)

app_subst_list_compose < case H1.

Subgoal 2:

Variables: X L L'1 ML1 V M
IH : forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' * ->
       app_subst_list ML (X :: L) (X' :: L')
H3 : app_subst_list ML1 (L V) L'1 *
H4 : app_subst ML1 (X V) M
============================
 app_subst_list (map n1 V :: ML1) (X n1 :: L n1) (M :: L'1)

app_subst_list_compose < apply IH to H4 H3.

Subgoal 2:

Variables: X L L'1 ML1 V M
IH : forall ML X X' L L', app_subst ML X X' -> app_subst_list ML L L' * ->
       app_subst_list ML (X :: L) (X' :: L')
H3 : app_subst_list ML1 (L V) L'1 *
H4 : app_subst ML1 (X V) M
H5 : app_subst_list ML1 (X V :: L V) (M :: L'1)
============================
 app_subst_list (map n1 V :: ML1) (X n1 :: L n1) (M :: L'1)

app_subst_list_compose < search.
Proof completed.

Abella < Theorem app_subst_list_prune [A,B,C] : 
forall ML M M', nabla x, app_subst_list ML M (M' x) ->
  (exists M'', M' = y\M'').

============================
 forall ML M M', nabla x, app_subst_list ML M (M' x) ->
   (exists M'', M' = y\M'')

app_subst_list_prune < induction on 1.

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

app_subst_list_prune < intros.

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

app_subst_list_prune < case H1.

Subgoal 1:

Variables: M
IH : forall ML M M', nabla x, app_subst_list ML M (M' x) * ->
       (exists M'', M' = y\M'')
============================
 exists M'', z1\M = y\M''

Subgoal 2 is:
 exists M'', z2\L'1 z2 = y\M''

app_subst_list_prune < search.

Subgoal 2:

Variables: M L'1 ML3 ML2
IH : forall ML M M', nabla x, app_subst_list ML M (M' x) * ->
       (exists M'', M' = y\M'')
H2 : app_subst_list ML3 (M ML2) (L'1 n1) *
============================
 exists M'', z2\L'1 z2 = y\M''

app_subst_list_prune < apply IH to H2.

Subgoal 2:

Variables: M ML3 ML2 M''
IH : forall ML M M', nabla x, app_subst_list ML M (M' x) * ->
       (exists M'', M' = y\M'')
H2 : app_subst_list ML3 (M ML2) M'' *
============================
 exists M''1, z2\M'' = y\M''1

app_subst_list_prune < search.
Proof completed.

Abella <