Welcome to Abella 2.0.4
Abella < Specification "trans".
Reading specification "+/trans"
Abella < Theorem add_det :
forall N1 N2 N3 N3', {add N1 N2 N3} -> {add N1 N2 N3'} -> N3 = N3'.
============================
forall N1 N2 N3 N3', {add N1 N2 N3} -> {add N1 N2 N3'} -> N3 = N3'
add_det < induction on 1.
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
============================
forall N1 N2 N3 N3', {add N1 N2 N3}@ -> {add N1 N2 N3'} -> N3 = N3'
add_det < intros.
Variables: N1 N2 N3 N3'
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H1 : {add N1 N2 N3}@
H2 : {add N1 N2 N3'}
============================
N3 = N3'
add_det < case H1.
Subgoal 1:
Variables: N3 N3'
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H2 : {add z N3 N3'}
============================
N3 = N3'
Subgoal 2 is:
s N4 = N3'
add_det < case H2.
Subgoal 1:
Variables: N3'
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
============================
N3' = N3'
Subgoal 2 is:
s N4 = N3'
add_det < search.
Subgoal 2:
Variables: N2 N3' N4 N6
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H2 : {add (s N6) N2 N3'}
H3 : {add N6 N2 N4}*
============================
s N4 = N3'
add_det < case H2.
Subgoal 2:
Variables: N2 N4 N6 N5
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H3 : {add N6 N2 N4}*
H4 : {add N6 N2 N5}
============================
s N4 = s N5
add_det < apply IH to H3 H4.
Subgoal 2:
Variables: N2 N6 N5
IH : forall N1 N2 N3 N3', {add N1 N2 N3}* -> {add N1 N2 N3'} -> N3 = N3'
H3 : {add N6 N2 N5}*
H4 : {add N6 N2 N5}
============================
s N5 = s N5
add_det < search.
Proof completed.
Abella < Define le : nat -> nat -> prop by
le N1 N2 := exists N, {add N1 N N2}.
Abella < Define lt : nat -> nat -> prop by
lt N1 N2 := exists N, {add N1 (s N) N2}.
Abella < Theorem lt_to_le :
forall N1 N2, lt N1 N2 -> le N1 N2.
============================
forall N1 N2, lt N1 N2 -> le N1 N2
lt_to_le < intros.
Variables: N1 N2
H1 : lt N1 N2
============================
le N1 N2
lt_to_le < case H1.
Variables: N1 N2 N
H2 : {add N1 (s N) N2}
============================
le N1 N2
lt_to_le < search.
Proof completed.
Abella < Theorem le_refl :
forall N, {is_nat N} -> le N N.
============================
forall N, {is_nat N} -> le N N
le_refl < induction on 1.
IH : forall N, {is_nat N}* -> le N N
============================
forall N, {is_nat N}@ -> le N N
le_refl < intros.
Variables: N
IH : forall N, {is_nat N}* -> le N N
H1 : {is_nat N}@
============================
le N N
le_refl < case H1.
Subgoal 1:
IH : forall N, {is_nat N}* -> le N N
============================
le z z
Subgoal 2 is:
le (s N1) (s N1)
le_refl < search.
Subgoal 2:
Variables: N1
IH : forall N, {is_nat N}* -> le N N
H2 : {is_nat N1}*
============================
le (s N1) (s N1)
le_refl < apply IH to H2.
Subgoal 2:
Variables: N1
IH : forall N, {is_nat N}* -> le N N
H2 : {is_nat N1}*
H3 : le N1 N1
============================
le (s N1) (s N1)
le_refl < case H3.
Subgoal 2:
Variables: N1 N2
IH : forall N, {is_nat N}* -> le N N
H2 : {is_nat N1}*
H4 : {add N1 N2 N1}
============================
le (s N1) (s N1)
le_refl < search.
Proof completed.
Abella < Theorem le_z :
forall N, le N z -> N = z.
============================
forall N, le N z -> N = z
le_z < intros.
Variables: N
H1 : le N z
============================
N = z
le_z < case H1.
Variables: N N1
H2 : {add N N1 z}
============================
N = z
le_z < case H2.
============================
z = z
le_z < search.
Proof completed.
Abella < Theorem add_result_isnat :
forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3} -> {is_nat N3}.
============================
forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3} -> {is_nat N3}
add_result_isnat < induction on 2.
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
============================
forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}@ -> {is_nat N3}
add_result_isnat < intros.
Variables: N1 N2 N3
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N2}
H2 : {add N1 N2 N3}@
============================
{is_nat N3}
add_result_isnat < case H2.
Subgoal 1:
Variables: N3
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N3}
============================
{is_nat N3}
Subgoal 2 is:
{is_nat (s N4)}
add_result_isnat < search.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N2}
H3 : {add N6 N2 N4}*
============================
{is_nat (s N4)}
add_result_isnat < apply IH to H1 H3.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N2} -> {add N1 N2 N3}* -> {is_nat N3}
H1 : {is_nat N2}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
============================
{is_nat (s N4)}
add_result_isnat < search.
Proof completed.
Abella < Theorem add_arg2_isnat :
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {is_nat N2}.
============================
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {is_nat N2}
add_arg2_isnat < induction on 2.
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
============================
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}@ -> {is_nat N2}
add_arg2_isnat < intros.
Variables: N1 N2 N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H1 : {is_nat N3}
H2 : {add N1 N2 N3}@
============================
{is_nat N2}
add_arg2_isnat < case H2.
Subgoal 1:
Variables: N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H1 : {is_nat N3}
============================
{is_nat N3}
Subgoal 2 is:
{is_nat N2}
add_arg2_isnat < search.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H1 : {is_nat (s N4)}
H3 : {add N6 N2 N4}*
============================
{is_nat N2}
add_arg2_isnat < case H1.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {is_nat N2}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
============================
{is_nat N2}
add_arg2_isnat < backchain IH.
Proof completed.
Abella < Theorem add_arg2_det :
forall N1 N2 N2' N3, {add N1 N2 N3} -> {add N1 N2' N3} -> N2 = N2'.
============================
forall N1 N2 N2' N3, {add N1 N2 N3} -> {add N1 N2' N3} -> N2 = N2'
add_arg2_det < induction on 1.
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
============================
forall N1 N2 N2' N3, {add N1 N2 N3}@ -> {add N1 N2' N3} -> N2 = N2'
add_arg2_det < intros.
Variables: N1 N2 N2' N3
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H1 : {add N1 N2 N3}@
H2 : {add N1 N2' N3}
============================
N2 = N2'
add_arg2_det < case H1.
Subgoal 1:
Variables: N2' N3
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H2 : {add z N2' N3}
============================
N3 = N2'
Subgoal 2 is:
N2 = N2'
add_arg2_det < case H2.
Subgoal 1:
Variables: N3
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
============================
N3 = N3
Subgoal 2 is:
N2 = N2'
add_arg2_det < search.
Subgoal 2:
Variables: N2 N2' N4 N6
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H2 : {add (s N6) N2' (s N4)}
H3 : {add N6 N2 N4}*
============================
N2 = N2'
add_arg2_det < case H2.
Subgoal 2:
Variables: N2 N2' N4 N6
IH : forall N1 N2 N2' N3, {add N1 N2 N3}* -> {add N1 N2' N3} -> N2 = N2'
H3 : {add N6 N2 N4}*
H4 : {add N6 N2' N4}
============================
N2 = N2'
add_arg2_det < backchain IH.
Proof completed.
Abella < Theorem add_arg1_isnat :
forall N1 N2 N3, {add N1 N2 N3} -> {is_nat N1}.
============================
forall N1 N2 N3, {add N1 N2 N3} -> {is_nat N1}
add_arg1_isnat < induction on 1.
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
============================
forall N1 N2 N3, {add N1 N2 N3}@ -> {is_nat N1}
add_arg1_isnat < intros.
Variables: N1 N2 N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
H1 : {add N1 N2 N3}@
============================
{is_nat N1}
add_arg1_isnat < case H1.
Subgoal 1:
Variables: N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
============================
{is_nat z}
Subgoal 2 is:
{is_nat (s N6)}
add_arg1_isnat < search.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
H2 : {add N6 N2 N4}*
============================
{is_nat (s N6)}
add_arg1_isnat < apply IH to H2.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {is_nat N1}
H2 : {add N6 N2 N4}*
H3 : {is_nat N6}
============================
{is_nat (s N6)}
add_arg1_isnat < search.
Proof completed.
Abella < Theorem add_s :
forall N1 N2 N3, {add N1 N2 N3} -> {add N1 (s N2) (s N3)}.
============================
forall N1 N2 N3, {add N1 N2 N3} -> {add N1 (s N2) (s N3)}
add_s < induction on 1.
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
============================
forall N1 N2 N3, {add N1 N2 N3}@ -> {add N1 (s N2) (s N3)}
add_s < intros.
Variables: N1 N2 N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
H1 : {add N1 N2 N3}@
============================
{add N1 (s N2) (s N3)}
add_s < case H1.
Subgoal 1:
Variables: N3
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
============================
{add z (s N3) (s N3)}
Subgoal 2 is:
{add (s N6) (s N2) (s (s N4))}
add_s < search.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
H2 : {add N6 N2 N4}*
============================
{add (s N6) (s N2) (s (s N4))}
add_s < apply IH to H2.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {add N1 N2 N3}* -> {add N1 (s N2) (s N3)}
H2 : {add N6 N2 N4}*
H3 : {add N6 (s N2) (s N4)}
============================
{add (s N6) (s N2) (s (s N4))}
add_s < search.
Proof completed.
Abella < Theorem add_s_inv :
forall N1 N2 N3, {add N1 (s N2) (s N3)} -> {add N1 N2 N3}.
============================
forall N1 N2 N3, {add N1 (s N2) (s N3)} -> {add N1 N2 N3}
add_s_inv < induction on 1.
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
============================
forall N1 N2 N3, {add N1 (s N2) (s N3)}@ -> {add N1 N2 N3}
add_s_inv < intros.
Variables: N1 N2 N3
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H1 : {add N1 (s N2) (s N3)}@
============================
{add N1 N2 N3}
add_s_inv < case H1.
Subgoal 1:
Variables: N3
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
============================
{add z N3 N3}
Subgoal 2 is:
{add (s N6) N2 N3}
add_s_inv < search.
Subgoal 2:
Variables: N2 N3 N6
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H2 : {add N6 (s N2) N3}*
============================
{add (s N6) N2 N3}
add_s_inv < case H2 (keep).
Subgoal 2.1:
Variables: N2
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H2 : {add z (s N2) (s N2)}*
============================
{add (s z) N2 (s N2)}
Subgoal 2.2 is:
{add (s (s N7)) N2 (s N4)}
add_s_inv < search.
Subgoal 2.2:
Variables: N2 N4 N7
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H2 : {add (s N7) (s N2) (s N4)}*
H3 : {add N7 (s N2) N4}*
============================
{add (s (s N7)) N2 (s N4)}
add_s_inv < apply IH to H2.
Subgoal 2.2:
Variables: N2 N4 N7
IH : forall N1 N2 N3, {add N1 (s N2) (s N3)}* -> {add N1 N2 N3}
H2 : {add (s N7) (s N2) (s N4)}*
H3 : {add N7 (s N2) N4}*
H4 : {add (s N7) N2 N4}
============================
{add (s (s N7)) N2 (s N4)}
add_s_inv < search.
Proof completed.
Abella < Theorem add_z :
forall N, {is_nat N} -> {add N z N}.
============================
forall N, {is_nat N} -> {add N z N}
add_z < induction on 1.
IH : forall N, {is_nat N}* -> {add N z N}
============================
forall N, {is_nat N}@ -> {add N z N}
add_z < intros.
Variables: N
IH : forall N, {is_nat N}* -> {add N z N}
H1 : {is_nat N}@
============================
{add N z N}
add_z < case H1.
Subgoal 1:
IH : forall N, {is_nat N}* -> {add N z N}
============================
{add z z z}
Subgoal 2 is:
{add (s N1) z (s N1)}
add_z < search.
Subgoal 2:
Variables: N1
IH : forall N, {is_nat N}* -> {add N z N}
H2 : {is_nat N1}*
============================
{add (s N1) z (s N1)}
add_z < apply IH to H2.
Subgoal 2:
Variables: N1
IH : forall N, {is_nat N}* -> {add N z N}
H2 : {is_nat N1}*
H3 : {add N1 z N1}
============================
{add (s N1) z (s N1)}
add_z < search.
Proof completed.
Abella < Theorem add_comm :
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {add N2 N1 N3}.
============================
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3} -> {add N2 N1 N3}
add_comm < induction on 2.
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
============================
forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}@ -> {add N2 N1 N3}
add_comm < intros.
Variables: N1 N2 N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H1 : {is_nat N3}
H2 : {add N1 N2 N3}@
============================
{add N2 N1 N3}
add_comm < case H2.
Subgoal 1:
Variables: N3
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H1 : {is_nat N3}
============================
{add N3 z N3}
Subgoal 2 is:
{add N2 (s N6) (s N4)}
add_comm < backchain add_z.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H1 : {is_nat (s N4)}
H3 : {add N6 N2 N4}*
============================
{add N2 (s N6) (s N4)}
add_comm < case H1.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
============================
{add N2 (s N6) (s N4)}
add_comm < apply IH to _ H3.
Subgoal 2:
Variables: N2 N4 N6
IH : forall N1 N2 N3, {is_nat N3} -> {add N1 N2 N3}* -> {add N2 N1 N3}
H3 : {add N6 N2 N4}*
H4 : {is_nat N4}
H5 : {add N2 N6 N4}
============================
{add N2 (s N6) (s N4)}
add_comm < backchain add_s.
Proof completed.
Abella < Theorem add_assoc :
forall N1 N2 N3 N12 N123, {add N1 N2 N12} -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123}).
============================
forall N1 N2 N3 N12 N123, {add N1 N2 N12} -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
add_assoc < induction on 1.
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
============================
forall N1 N2 N3 N12 N123, {add N1 N2 N12}@ -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
add_assoc < intros.
Variables: N1 N2 N3 N12 N123
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H1 : {add N1 N2 N12}@
H2 : {add N12 N3 N123}
============================
exists N23, {add N2 N3 N23} /\ {add N1 N23 N123}
add_assoc < case H1.
Subgoal 1:
Variables: N3 N12 N123
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H2 : {add N12 N3 N123}
============================
exists N23, {add N12 N3 N23} /\ {add z N23 N123}
Subgoal 2 is:
exists N23, {add N2 N3 N23} /\ {add (s N6) N23 N123}
add_assoc < search.
Subgoal 2:
Variables: N2 N3 N123 N4 N6
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H2 : {add (s N4) N3 N123}
H3 : {add N6 N2 N4}*
============================
exists N23, {add N2 N3 N23} /\ {add (s N6) N23 N123}
add_assoc < case H2.
Subgoal 2:
Variables: N2 N3 N4 N6 N5
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H3 : {add N6 N2 N4}*
H4 : {add N4 N3 N5}
============================
exists N23, {add N2 N3 N23} /\ {add (s N6) N23 (s N5)}
add_assoc < apply IH to H3 H4.
Subgoal 2:
Variables: N2 N3 N4 N6 N5 N23
IH : forall N1 N2 N3 N12 N123, {add N1 N2 N12}* -> {add N12 N3 N123} ->
(exists N23, {add N2 N3 N23} /\ {add N1 N23 N123})
H3 : {add N6 N2 N4}*
H4 : {add N4 N3 N5}
H5 : {add N2 N3 N23}
H6 : {add N6 N23 N5}
============================
exists N23, {add N2 N3 N23} /\ {add (s N6) N23 (s N5)}
add_assoc < search.
Proof completed.
Abella < Theorem add_assoc' :
forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123} ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123}).
============================
forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123} ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
add_assoc' < induction on 2.
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
============================
forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
add_assoc' < intros.
Variables: N1 N2 N3 N23 N123
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
============================
exists N12, {add N1 N2 N12} /\ {add N12 N3 N123}
add_assoc' < case H2.
Subgoal 1:
Variables: N2 N3 N123
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N123}
============================
exists N12, {add z N2 N12} /\ {add N12 N3 N123}
Subgoal 2 is:
exists N12, {add (s N6) N2 N12} /\ {add N12 N3 (s N4)}
add_assoc' < search.
Subgoal 2:
Variables: N2 N3 N23 N4 N6
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N23}
H3 : {add N6 N23 N4}*
============================
exists N12, {add (s N6) N2 N12} /\ {add N12 N3 (s N4)}
add_assoc' < apply IH to _ H3.
Subgoal 2:
Variables: N2 N3 N23 N4 N6 N12
IH : forall N1 N2 N3 N23 N123, {add N2 N3 N23} -> {add N1 N23 N123}* ->
(exists N12, {add N1 N2 N12} /\ {add N12 N3 N123})
H1 : {add N2 N3 N23}
H3 : {add N6 N23 N4}*
H4 : {add N6 N2 N12}
H5 : {add N12 N3 N4}
============================
exists N12, {add (s N6) N2 N12} /\ {add N12 N3 (s N4)}
add_assoc' < search.
Proof completed.
Abella < Theorem le_to_lt :
forall N1 N2, {is_nat N2} -> le N1 N2 -> N1 = N2 \/ lt N1 N2.
============================
forall N1 N2, {is_nat N2} -> le N1 N2 -> N1 = N2 \/ lt N1 N2
le_to_lt < intros.
Variables: N1 N2
H1 : {is_nat N2}
H2 : le N1 N2
============================
N1 = N2 \/ lt N1 N2
le_to_lt < case H2.
Variables: N1 N2 N
H1 : {is_nat N2}
H3 : {add N1 N N2}
============================
N1 = N2 \/ lt N1 N2
le_to_lt < apply add_comm to _ H3.
Variables: N1 N2 N
H1 : {is_nat N2}
H3 : {add N1 N N2}
H4 : {add N N1 N2}
============================
N1 = N2 \/ lt N1 N2
le_to_lt < case H4.
Subgoal 1:
Variables: N2
H1 : {is_nat N2}
H3 : {add N2 z N2}
============================
N2 = N2 \/ lt N2 N2
Subgoal 2 is:
N1 = s N3 \/ lt N1 (s N3)
le_to_lt < search.
Subgoal 2:
Variables: N1 N3 N5
H1 : {is_nat (s N3)}
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
============================
N1 = s N3 \/ lt N1 (s N3)
le_to_lt < apply add_comm to _ H5.
Subgoal 2.1:
Variables: N1 N3 N5
H1 : {is_nat (s N3)}
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
============================
{is_nat N3}
Subgoal 2 is:
N1 = s N3 \/ lt N1 (s N3)
le_to_lt < case H1.
Subgoal 2.1:
Variables: N1 N3 N5
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
H6 : {is_nat N3}
============================
{is_nat N3}
Subgoal 2 is:
N1 = s N3 \/ lt N1 (s N3)
le_to_lt < search.
Subgoal 2:
Variables: N1 N3 N5
H1 : {is_nat (s N3)}
H3 : {add N1 (s N5) (s N3)}
H5 : {add N5 N1 N3}
H6 : {add N1 N5 N3}
============================
N1 = s N3 \/ lt N1 (s N3)
le_to_lt < search.
Proof completed.
Abella < Theorem lt_pred_le :
forall I J, {is_nat J} -> lt I (s J) -> le I J.
============================
forall I J, {is_nat J} -> lt I (s J) -> le I J
lt_pred_le < intros.
Variables: I J
H1 : {is_nat J}
H2 : lt I (s J)
============================
le I J
lt_pred_le < case H2.
Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
============================
le I J
lt_pred_le < apply add_comm to _ H3.
Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
H4 : {add (s N) I (s J)}
============================
le I J
lt_pred_le < case H4.
Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
H5 : {add N I J}
============================
le I J
lt_pred_le < apply add_comm to _ H5.
Variables: I J N
H1 : {is_nat J}
H3 : {add I (s N) (s J)}
H5 : {add N I J}
H6 : {add I N J}
============================
le I J
lt_pred_le < search.
Proof completed.
Abella < Theorem lt_z_absurd :
forall I, lt I z -> false.
============================
forall I, lt I z -> false
lt_z_absurd < intros.
Variables: I
H1 : lt I z
============================
false
lt_z_absurd < case H1.
Variables: I N
H2 : {add I (s N) z}
============================
false
lt_z_absurd < apply add_comm to _ H2.
Variables: I N
H2 : {add I (s N) z}
H3 : {add (s N) I z}
============================
false
lt_z_absurd < case H3.
Proof completed.
Abella < Theorem le_succ :
forall I J, le I J -> le I (s J).
============================
forall I J, le I J -> le I (s J)
le_succ < intros.
Variables: I J
H1 : le I J
============================
le I (s J)
le_succ < case H1.
Variables: I J N
H2 : {add I N J}
============================
le I (s J)
le_succ < unfold.
Variables: I J N
H2 : {add I N J}
============================
exists N, {add I N (s J)}
le_succ < exists s N.
Variables: I J N
H2 : {add I N J}
============================
{add I (s N) (s J)}
le_succ < backchain add_s.
Proof completed.
Abella < Theorem le_extend :
forall I J, le I J -> le (s I) (s J).
============================
forall I J, le I J -> le (s I) (s J)
le_extend < intros.
Variables: I J
H1 : le I J
============================
le (s I) (s J)
le_extend < case H1.
Variables: I J N
H2 : {add I N J}
============================
le (s I) (s J)
le_extend < unfold.
Variables: I J N
H2 : {add I N J}
============================
exists N, {add (s I) N (s J)}
le_extend < exists N.
Variables: I J N
H2 : {add I N J}
============================
{add (s I) N (s J)}
le_extend < search.
Proof completed.
Abella < Theorem le_to_lt_s :
forall N1 N2, le N1 N2 -> lt N1 (s N2).
============================
forall N1 N2, le N1 N2 -> lt N1 (s N2)
le_to_lt_s < intros.
Variables: N1 N2
H1 : le N1 N2
============================
lt N1 (s N2)
le_to_lt_s < case H1.
Variables: N1 N2 N
H2 : {add N1 N N2}
============================
lt N1 (s N2)
le_to_lt_s < unfold.
Variables: N1 N2 N
H2 : {add N1 N N2}
============================
exists N, {add N1 (s N) (s N2)}
le_to_lt_s < exists N.
Variables: N1 N2 N
H2 : {add N1 N N2}
============================
{add N1 (s N) (s N2)}
le_to_lt_s < backchain add_s.
Proof completed.
Abella < Theorem le_trans :
forall N1 N2 N3, le N1 N2 -> le N2 N3 -> le N1 N3.
============================
forall N1 N2 N3, le N1 N2 -> le N2 N3 -> le N1 N3
le_trans < intros.
Variables: N1 N2 N3
H1 : le N1 N2
H2 : le N2 N3
============================
le N1 N3
le_trans < case H1.
Variables: N1 N2 N3 N
H2 : le N2 N3
H3 : {add N1 N N2}
============================
le N1 N3
le_trans < case H2.
Variables: N1 N2 N3 N N4
H3 : {add N1 N N2}
H4 : {add N2 N4 N3}
============================
le N1 N3
le_trans < unfold.
Variables: N1 N2 N3 N N4
H3 : {add N1 N N2}
H4 : {add N2 N4 N3}
============================
exists N, {add N1 N N3}
le_trans < apply add_assoc to H3 H4.
Variables: N1 N2 N3 N N4 N23
H3 : {add N1 N N2}
H4 : {add N2 N4 N3}
H5 : {add N N4 N23}
H6 : {add N1 N23 N3}
============================
exists N, {add N1 N N3}
le_trans < search.
Proof completed.
Abella < Theorem lt_le_compose :
forall N1 N2 N3, lt N1 N2 -> le N2 N3 -> lt N1 N3.
============================
forall N1 N2 N3, lt N1 N2 -> le N2 N3 -> lt N1 N3
lt_le_compose < intros.
Variables: N1 N2 N3
H1 : lt N1 N2
H2 : le N2 N3
============================
lt N1 N3
lt_le_compose < case H1.
Variables: N1 N2 N3 N
H2 : le N2 N3
H3 : {add N1 (s N) N2}
============================
lt N1 N3
lt_le_compose < case H2.
Variables: N1 N2 N3 N N4
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
============================
lt N1 N3
lt_le_compose < unfold.
Variables: N1 N2 N3 N N4
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
============================
exists N, {add N1 (s N) N3}
lt_le_compose < apply add_assoc to H3 H4.
Variables: N1 N2 N3 N N4 N23
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
H5 : {add (s N) N4 N23}
H6 : {add N1 N23 N3}
============================
exists N, {add N1 (s N) N3}
lt_le_compose < case H5.
Variables: N1 N2 N3 N N4 N5
H3 : {add N1 (s N) N2}
H4 : {add N2 N4 N3}
H6 : {add N1 (s N5) N3}
H7 : {add N N4 N5}
============================
exists N, {add N1 (s N) N3}
lt_le_compose < search.
Proof completed.
Abella < Theorem add_result_le_to_arg1_le :
forall N1 N2 N2' J K, {add N1 N2 J} -> {add N1 N2' K} -> le J K -> le N2 N2'.
============================
forall N1 N2 N2' J K, {add N1 N2 J} -> {add N1 N2' K} -> le J K -> le N2 N2'
add_result_le_to_arg1_le < induction on 1.
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
============================
forall N1 N2 N2' J K, {add N1 N2 J}@ -> {add N1 N2' K} -> le J K ->
le N2 N2'
add_result_le_to_arg1_le < intros.
Variables: N1 N2 N2' J K
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H1 : {add N1 N2 J}@
H2 : {add N1 N2' K}
H3 : le J K
============================
le N2 N2'
add_result_le_to_arg1_le < case H1.
Subgoal 1:
Variables: N2' J K
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H2 : {add z N2' K}
H3 : le J K
============================
le J N2'
Subgoal 2 is:
le N2 N2'
add_result_le_to_arg1_le < case H2.
Subgoal 1:
Variables: J K
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H3 : le J K
============================
le J K
Subgoal 2 is:
le N2 N2'
add_result_le_to_arg1_le < search.
Subgoal 2:
Variables: N2 N2' K N3 N5
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H2 : {add (s N5) N2' K}
H3 : le (s N3) K
H4 : {add N5 N2 N3}*
============================
le N2 N2'
add_result_le_to_arg1_le < case H2.
Subgoal 2:
Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
============================
le N2 N2'
add_result_le_to_arg1_le < assert le N3 N4.
Subgoal 2.1:
Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
============================
le N3 N4
Subgoal 2 is:
le N2 N2'
add_result_le_to_arg1_le < case H3.
Subgoal 2.1:
Variables: N2 N2' N3 N5 N4 N
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H6 : {add (s N3) N (s N4)}
============================
le N3 N4
Subgoal 2 is:
le N2 N2'
add_result_le_to_arg1_le < case H6.
Subgoal 2.1:
Variables: N2 N2' N3 N5 N4 N
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H7 : {add N3 N N4}
============================
le N3 N4
Subgoal 2 is:
le N2 N2'
add_result_le_to_arg1_le < search.
Subgoal 2:
Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H6 : le N3 N4
============================
le N2 N2'
add_result_le_to_arg1_le < apply IH to H4 H5 H6.
Subgoal 2:
Variables: N2 N2' N3 N5 N4
IH : forall N1 N2 N2' J K, {add N1 N2 J}* -> {add N1 N2' K} -> le J K ->
le N2 N2'
H3 : le (s N3) (s N4)
H4 : {add N5 N2 N3}*
H5 : {add N5 N2' N4}
H6 : le N3 N4
H7 : le N2 N2'
============================
le N2 N2'
add_result_le_to_arg1_le < search.
Proof completed.
Abella < Theorem add_le_complement :
forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N} ->
{add N1' N2' N} -> le N2' N2.
============================
forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N} ->
{add N1' N2' N} -> le N2' N2
add_le_complement < induction on 3.
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
============================
forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}@ ->
{add N1' N2' N} -> le N2' N2
add_le_complement < intros.
Variables: N1 N2 N1' N2' N
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H2 : le N1 N1'
H3 : {add N1 N2 N}@
H4 : {add N1' N2' N}
============================
le N2' N2
add_le_complement < case H3.
Subgoal 1:
Variables: N1' N2' N
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N}
H2 : le z N1'
H4 : {add N1' N2' N}
============================
le N2' N
Subgoal 2 is:
le N2' N2
add_le_complement < apply add_comm to _ H4.
Subgoal 1:
Variables: N1' N2' N
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N}
H2 : le z N1'
H4 : {add N1' N2' N}
H5 : {add N2' N1' N}
============================
le N2' N
Subgoal 2 is:
le N2' N2
add_le_complement < search.
Subgoal 2:
Variables: N2 N1' N2' N3 N5
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H2 : le (s N5) N1'
H4 : {add N1' N2' (s N3)}
H5 : {add N5 N2 N3}*
============================
le N2' N2
add_le_complement < case H2.
Subgoal 2:
Variables: N2 N1' N2' N3 N5 N4
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H4 : {add N1' N2' (s N3)}
H5 : {add N5 N2 N3}*
H6 : {add (s N5) N4 N1'}
============================
le N2' N2
add_le_complement < case H6.
Subgoal 2:
Variables: N2 N2' N3 N5 N4 N6
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H4 : {add (s N6) N2' (s N3)}
H5 : {add N5 N2 N3}*
H7 : {add N5 N4 N6}
============================
le N2' N2
add_le_complement < case H4.
Subgoal 2:
Variables: N2 N2' N3 N5 N4 N6
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H5 : {add N5 N2 N3}*
H7 : {add N5 N4 N6}
H8 : {add N6 N2' N3}
============================
le N2' N2
add_le_complement < apply IH to H1 _ H5 H8.
Subgoal 2:
Variables: N2 N2' N3 N5 N4 N6
IH : forall N1 N2 N1' N2' N, {is_nat N2} -> le N1 N1' -> {add N1 N2 N}* ->
{add N1' N2' N} -> le N2' N2
H1 : {is_nat N2}
H5 : {add N5 N2 N3}*
H7 : {add N5 N4 N6}
H8 : {add N6 N2' N3}
H9 : le N2' N2
============================
le N2' N2
add_le_complement < search.
Proof completed.
Abella < Theorem k_minus_n1 :
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
{add N123 N K} -> (exists K', {add N1 K' K}).
============================
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
{add N123 N K} -> (exists K', {add N1 K' K})
k_minus_n1 < induction on 2.
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N1 K' K})
============================
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
{add N123 N K} -> (exists K', {add N1 K' K})
k_minus_n1 < intros.
Variables: N1 N2 N3 N23 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
H3 : {add N123 N K}
============================
exists K', {add N1 K' K}
k_minus_n1 < case H2.
Subgoal 1:
Variables: N2 N3 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
============================
exists K', {add z K' K}
Subgoal 2 is:
exists K', {add (s N6) K' K}
k_minus_n1 < search.
Subgoal 2:
Variables: N2 N3 N23 N K N4 N6
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H3 : {add (s N4) N K}
H4 : {add N6 N23 N4}*
============================
exists K', {add (s N6) K' K}
k_minus_n1 < case H3.
Subgoal 2:
Variables: N2 N3 N23 N N4 N6 N5
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
============================
exists K', {add (s N6) K' (s N5)}
k_minus_n1 < apply IH to _ H4 _.
Subgoal 2:
Variables: N2 N3 N23 N N4 N6 N5 K'
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N1 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N6 K' N5}
============================
exists K', {add (s N6) K' (s N5)}
k_minus_n1 < search.
Proof completed.
Abella < Theorem k_minus_n2 :
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
{add N123 N K} -> (exists K', {add N2 K' K}).
============================
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
{add N123 N K} -> (exists K', {add N2 K' K})
k_minus_n2 < induction on 2.
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
============================
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
{add N123 N K} -> (exists K', {add N2 K' K})
k_minus_n2 < intros.
Variables: N1 N2 N3 N23 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
H3 : {add N123 N K}
============================
exists K', {add N2 K' K}
k_minus_n2 < case H2.
Subgoal 1:
Variables: N2 N3 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
============================
exists K', {add N2 K' K}
Subgoal 2 is:
exists K', {add N2 K' K}
k_minus_n2 < apply add_assoc to H1 H3.
Subgoal 1:
Variables: N2 N3 N123 N K N4
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
H4 : {add N3 N N4}
H5 : {add N2 N4 K}
============================
exists K', {add N2 K' K}
Subgoal 2 is:
exists K', {add N2 K' K}
k_minus_n2 < search.
Subgoal 2:
Variables: N2 N3 N23 N K N4 N6
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H3 : {add (s N4) N K}
H4 : {add N6 N23 N4}*
============================
exists K', {add N2 K' K}
k_minus_n2 < case H3.
Subgoal 2:
Variables: N2 N3 N23 N N4 N6 N5
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
============================
exists K', {add N2 K' (s N5)}
k_minus_n2 < apply IH to _ H4 _.
Subgoal 2:
Variables: N2 N3 N23 N N4 N6 N5 K'
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N2 K' N5}
============================
exists K', {add N2 K' (s N5)}
k_minus_n2 < apply add_s to H6.
Subgoal 2:
Variables: N2 N3 N23 N N4 N6 N5 K'
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} -> (exists K', {add N2 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N2 K' N5}
H7 : {add N2 (s K') (s N5)}
============================
exists K', {add N2 K' (s N5)}
k_minus_n2 < search.
Proof completed.
Abella < Theorem k_minus_n12 :
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}).
============================
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123} ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
k_minus_n12 < induction on 2.
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
============================
forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}@ ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
k_minus_n12 < intros.
Variables: N1 N2 N3 N23 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H2 : {add N1 N23 N123}@
H3 : {add N123 N K}
============================
exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}
k_minus_n12 < case H2.
Subgoal 1:
Variables: N2 N3 N123 N K
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
============================
exists K' N12, {add z N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}
Subgoal 2 is:
exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}
k_minus_n12 < apply add_assoc to H1 H3.
Subgoal 1:
Variables: N2 N3 N123 N K N4
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N123}
H3 : {add N123 N K}
H4 : {add N3 N N4}
H5 : {add N2 N4 K}
============================
exists K' N12, {add z N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}
Subgoal 2 is:
exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}
k_minus_n12 < search.
Subgoal 2:
Variables: N2 N3 N23 N K N4 N6
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H3 : {add (s N4) N K}
H4 : {add N6 N23 N4}*
============================
exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' K}
k_minus_n12 < case H3.
Subgoal 2:
Variables: N2 N3 N23 N N4 N6 N5
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
============================
exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' (s N5)}
k_minus_n12 < apply IH to _ H4 _.
Subgoal 2:
Variables: N2 N3 N23 N N4 N6 N5 K' N12
IH : forall N1 N2 N3 N23 N123 N K, {add N2 N3 N23} -> {add N1 N23 N123}* ->
{add N123 N K} ->
(exists K' N12, {add N1 N2 N12} /\ {add N3 N K'} /\ {add N12 K' K})
H1 : {add N2 N3 N23}
H4 : {add N6 N23 N4}*
H5 : {add N4 N N5}
H6 : {add N6 N2 N12}
H7 : {add N3 N K'}
H8 : {add N12 K' N5}
============================
exists K' N12, {add (s N6) N2 N12} /\ {add N3 N K'} /\ {add N12 K' (s N5)}
k_minus_n12 < search.
Proof completed.
Abella < Theorem sum_complement_to_lt1 :
forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
{add N1 K' N} -> lt K (s K').
============================
forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
{add N1 K' N} -> lt K (s K')
sum_complement_to_lt1 < intros.
Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 K' N}
============================
lt K (s K')
sum_complement_to_lt1 < apply add_assoc to H2 H3.
Variables: N1 N2 N12 K K' N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 K' N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
lt K (s K')
sum_complement_to_lt1 < unfold.
Variables: N1 N2 N12 K K' N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 K' N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
exists N, {add K (s N) (s K')}
sum_complement_to_lt1 < apply add_arg2_det to H4 H6.
Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
exists N, {add K (s N) (s N23)}
sum_complement_to_lt1 < apply add_comm to _ H5.
Subgoal 1:
Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
============================
{is_nat N23}
Subgoal is:
exists N, {add K (s N) (s N23)}
sum_complement_to_lt1 < backchain add_arg2_isnat.
Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
H7 : {add K N2 N23}
============================
exists N, {add K (s N) (s N23)}
sum_complement_to_lt1 < apply add_s to H7.
Variables: N1 N2 N12 K N N23
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N1 N23 N}
H5 : {add N2 K N23}
H6 : {add N1 N23 N}
H7 : {add K N2 N23}
H8 : {add K (s N2) (s N23)}
============================
exists N, {add K (s N) (s N23)}
sum_complement_to_lt1 < search.
Proof completed.
Abella < Theorem sum_complement_to_lt2 :
forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
{add N2 K' N} -> lt K (s K').
============================
forall N1 N2 N12 K K' N, {is_nat N} -> {add N1 N2 N12} -> {add N12 K N} ->
{add N2 K' N} -> lt K (s K')
sum_complement_to_lt2 < intros.
Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
============================
lt K (s K')
sum_complement_to_lt2 < apply add_comm to _ H2.
Subgoal 1:
Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
============================
{is_nat N12}
Subgoal is:
lt K (s K')
sum_complement_to_lt2 < backchain add_arg1_isnat.
Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
H5 : {add N2 N1 N12}
============================
lt K (s K')
sum_complement_to_lt2 < apply sum_complement_to_lt1 to _ H5 H3 H4.
Variables: N1 N2 N12 K K' N
H1 : {is_nat N}
H2 : {add N1 N2 N12}
H3 : {add N12 K N}
H4 : {add N2 K' N}
H5 : {add N2 N1 N12}
H6 : lt K (s K')
============================
lt K (s K')
sum_complement_to_lt2 < search.
Proof completed.
Abella < Theorem npred_det :
forall N N1 N2, {npred N N1} -> {npred N N2} -> N1 = N2.
============================
forall N N1 N2, {npred N N1} -> {npred N N2} -> N1 = N2
npred_det < intros.
Variables: N N1 N2
H1 : {npred N N1}
H2 : {npred N N2}
============================
N1 = N2
npred_det < case H1.
Subgoal 1:
Variables: N2
H2 : {npred z N2}
============================
z = N2
Subgoal 2 is:
N1 = N2
npred_det < case H2.
Subgoal 1:
============================
z = z
Subgoal 2 is:
N1 = N2
npred_det < search.
Subgoal 2:
Variables: N1 N2
H2 : {npred (s N1) N2}
============================
N1 = N2
npred_det < case H2.
Subgoal 2:
Variables: N2
============================
N2 = N2
npred_det < search.
Proof completed.
Abella < Define is_list : olist -> prop by
is_list nil;
is_list (X :: L) := is_list L.
Abella < Define append : olist -> olist -> olist -> prop by
append nil L L;
append (X :: L1) L2 (X :: L3) := append L1 L2 L3.
Abella < Theorem append_refl :
forall L, is_list L -> append L nil L.
============================
forall L, is_list L -> append L nil L
append_refl < induction on 1.
IH : forall L, is_list L * -> append L nil L
============================
forall L, is_list L @ -> append L nil L
append_refl < intros.
Variables: L
IH : forall L, is_list L * -> append L nil L
H1 : is_list L @
============================
append L nil L
append_refl < case H1.
Subgoal 1:
IH : forall L, is_list L * -> append L nil L
============================
append nil nil nil
Subgoal 2 is:
append (X :: L1) nil (X :: L1)
append_refl < search.
Subgoal 2:
Variables: L1 X
IH : forall L, is_list L * -> append L nil L
H2 : is_list L1 *
============================
append (X :: L1) nil (X :: L1)
append_refl < unfold.
Subgoal 2:
Variables: L1 X
IH : forall L, is_list L * -> append L nil L
H2 : is_list L1 *
============================
append L1 nil L1
append_refl < backchain IH.
Proof completed.
Abella < Theorem append_exists :
forall L1 L2, is_list L1 -> (exists L3, append L1 L2 L3).
============================
forall L1 L2, is_list L1 -> (exists L3, append L1 L2 L3)
append_exists < induction on 1.
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
============================
forall L1 L2, is_list L1 @ -> (exists L3, append L1 L2 L3)
append_exists < intros.
Variables: L1 L2
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
H1 : is_list L1 @
============================
exists L3, append L1 L2 L3
append_exists < case H1.
Subgoal 1:
Variables: L2
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
============================
exists L3, append nil L2 L3
Subgoal 2 is:
exists L3, append (X :: L) L2 L3
append_exists < search.
Subgoal 2:
Variables: L2 L X
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
H2 : is_list L *
============================
exists L3, append (X :: L) L2 L3
append_exists < apply IH to H2 with L2 = L2.
Subgoal 2:
Variables: L2 L X L3
IH : forall L1 L2, is_list L1 * -> (exists L3, append L1 L2 L3)
H2 : is_list L *
H3 : append L L2 L3
============================
exists L3, append (X :: L) L2 L3
append_exists < search.
Proof completed.
Abella < Theorem append_result_islist :
forall L1 L2 L, is_list L2 -> append L1 L2 L -> is_list L.
============================
forall L1 L2 L, is_list L2 -> append L1 L2 L -> is_list L
append_result_islist < induction on 2.
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
============================
forall L1 L2 L, is_list L2 -> append L1 L2 L @ -> is_list L
append_result_islist < intros.
Variables: L1 L2 L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L2
H2 : append L1 L2 L @
============================
is_list L
append_result_islist < case H2.
Subgoal 1:
Variables: L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L
============================
is_list L
Subgoal 2 is:
is_list (X :: L5)
append_result_islist < search.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
is_list (X :: L5)
append_result_islist < unfold.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> is_list L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
is_list L5
append_result_islist < backchain IH.
Proof completed.
Abella < Theorem append_arg2_islist :
forall L1 L2 L, is_list L -> append L1 L2 L -> is_list L2.
============================
forall L1 L2 L, is_list L -> append L1 L2 L -> is_list L2
append_arg2_islist < induction on 2.
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
============================
forall L1 L2 L, is_list L -> append L1 L2 L @ -> is_list L2
append_arg2_islist < intros.
Variables: L1 L2 L
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list L
H2 : append L1 L2 L @
============================
is_list L2
append_arg2_islist < case H2.
Subgoal 1:
Variables: L
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list L
============================
is_list L
Subgoal 2 is:
is_list L2
append_arg2_islist < search.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list (X :: L5)
H3 : append L3 L2 L5 *
============================
is_list L2
append_arg2_islist < backchain IH with L1 = L3, L = L5.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H1 : is_list (X :: L5)
H3 : append L3 L2 L5 *
============================
is_list L5
append_arg2_islist < case H1.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L -> append L1 L2 L * -> is_list L2
H3 : append L3 L2 L5 *
H4 : is_list L5
============================
is_list L5
append_arg2_islist < search.
Proof completed.
Abella < Theorem append_arg1_islist :
forall L1 L2 L, append L1 L2 L -> is_list L1.
============================
forall L1 L2 L, append L1 L2 L -> is_list L1
append_arg1_islist < induction on 1.
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
============================
forall L1 L2 L, append L1 L2 L @ -> is_list L1
append_arg1_islist < intros.
Variables: L1 L2 L
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
H1 : append L1 L2 L @
============================
is_list L1
append_arg1_islist < case H1.
Subgoal 1:
Variables: L
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
============================
is_list nil
Subgoal 2 is:
is_list (X :: L3)
append_arg1_islist < search.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
H2 : append L3 L2 L5 *
============================
is_list (X :: L3)
append_arg1_islist < unfold.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> is_list L1
H2 : append L3 L2 L5 *
============================
is_list L3
append_arg1_islist < backchain IH.
Proof completed.
Abella < Define subset : olist -> olist -> prop by
subset nil L;
subset (X :: L1) L2 := member X L2 /\ subset L1 L2.
Abella < Theorem subset_add :
forall L L' X, subset L L' -> subset L (X :: L').
============================
forall L L' X, subset L L' -> subset L (X :: L')
subset_add < induction on 1.
IH : forall L L' X, subset L L' * -> subset L (X :: L')
============================
forall L L' X, subset L L' @ -> subset L (X :: L')
subset_add < intros.
Variables: L L' X
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H1 : subset L L' @
============================
subset L (X :: L')
subset_add < case H1.
Subgoal 1:
Variables: L' X
IH : forall L L' X, subset L L' * -> subset L (X :: L')
============================
subset nil (X :: L')
Subgoal 2 is:
subset (X1 :: L1) (X :: L')
subset_add < search.
Subgoal 2:
Variables: L' X L1 X1
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H2 : member X1 L'
H3 : subset L1 L' *
============================
subset (X1 :: L1) (X :: L')
subset_add < unfold.
Subgoal 2.1:
Variables: L' X L1 X1
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H2 : member X1 L'
H3 : subset L1 L' *
============================
member X1 (X :: L')
Subgoal 2.2 is:
subset L1 (X :: L')
subset_add < search.
Subgoal 2.2:
Variables: L' X L1 X1
IH : forall L L' X, subset L L' * -> subset L (X :: L')
H2 : member X1 L'
H3 : subset L1 L' *
============================
subset L1 (X :: L')
subset_add < backchain IH.
Proof completed.
Abella < Theorem subset_refl :
forall L, is_list L -> subset L L.
============================
forall L, is_list L -> subset L L
subset_refl < induction on 1.
IH : forall L, is_list L * -> subset L L
============================
forall L, is_list L @ -> subset L L
subset_refl < intros.
Variables: L
IH : forall L, is_list L * -> subset L L
H1 : is_list L @
============================
subset L L
subset_refl < case H1.
Subgoal 1:
IH : forall L, is_list L * -> subset L L
============================
subset nil nil
Subgoal 2 is:
subset (X :: L1) (X :: L1)
subset_refl < search.
Subgoal 2:
Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
subset (X :: L1) (X :: L1)
subset_refl < unfold.
Subgoal 2.1:
Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
member X (X :: L1)
Subgoal 2.2 is:
subset L1 (X :: L1)
subset_refl < search.
Subgoal 2.2:
Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
subset L1 (X :: L1)
subset_refl < backchain subset_add.
Subgoal 2.2:
Variables: L1 X
IH : forall L, is_list L * -> subset L L
H2 : is_list L1 *
============================
subset L1 L1
subset_refl < backchain IH.
Proof completed.
Abella < Theorem subset_mem_trans :
forall L1 L2 X, subset L1 L2 -> member X L1 -> member X L2.
============================
forall L1 L2 X, subset L1 L2 -> member X L1 -> member X L2
subset_mem_trans < induction on 2.
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
============================
forall L1 L2 X, subset L1 L2 -> member X L1 @ -> member X L2
subset_mem_trans < intros.
Variables: L1 L2 X
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H1 : subset L1 L2
H2 : member X L1 @
============================
member X L2
subset_mem_trans < case H2.
Subgoal 1:
Variables: L2 X L
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H1 : subset (X :: L) L2
============================
member X L2
Subgoal 2 is:
member X L2
subset_mem_trans < case H1.
Subgoal 1:
Variables: L2 X L
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H3 : member X L2
H4 : subset L L2
============================
member X L2
Subgoal 2 is:
member X L2
subset_mem_trans < search.
Subgoal 2:
Variables: L2 X L B
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H1 : subset (B :: L) L2
H3 : member X L *
============================
member X L2
subset_mem_trans < case H1.
Subgoal 2:
Variables: L2 X L B
IH : forall L1 L2 X, subset L1 L2 -> member X L1 * -> member X L2
H3 : member X L *
H4 : member B L2
H5 : subset L L2
============================
member X L2
subset_mem_trans < backchain IH.
Proof completed.
Abella < Theorem subset_trans :
forall L1 L2 L3, subset L1 L2 -> subset L2 L3 -> subset L1 L3.
============================
forall L1 L2 L3, subset L1 L2 -> subset L2 L3 -> subset L1 L3
subset_trans < induction on 1.
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
============================
forall L1 L2 L3, subset L1 L2 @ -> subset L2 L3 -> subset L1 L3
subset_trans < intros.
Variables: L1 L2 L3
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H1 : subset L1 L2 @
H2 : subset L2 L3
============================
subset L1 L3
subset_trans < case H1.
Subgoal 1:
Variables: L2 L3
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
============================
subset nil L3
Subgoal 2 is:
subset (X :: L4) L3
subset_trans < search.
Subgoal 2:
Variables: L2 L3 L4 X
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
H3 : member X L2
H4 : subset L4 L2 *
============================
subset (X :: L4) L3
subset_trans < unfold.
Subgoal 2.1:
Variables: L2 L3 L4 X
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
H3 : member X L2
H4 : subset L4 L2 *
============================
member X L3
Subgoal 2.2 is:
subset L4 L3
subset_trans < backchain subset_mem_trans.
Subgoal 2.2:
Variables: L2 L3 L4 X
IH : forall L1 L2 L3, subset L1 L2 * -> subset L2 L3 -> subset L1 L3
H2 : subset L2 L3
H3 : member X L2
H4 : subset L4 L2 *
============================
subset L4 L3
subset_trans < backchain IH.
Proof completed.
Abella < Theorem subset_extend :
forall L L' X, subset L L' -> subset (X :: L) (X :: L').
============================
forall L L' X, subset L L' -> subset (X :: L) (X :: L')
subset_extend < intros.
Variables: L L' X
H1 : subset L L'
============================
subset (X :: L) (X :: L')
subset_extend < unfold.
Subgoal 1:
Variables: L L' X
H1 : subset L L'
============================
member X (X :: L')
Subgoal 2 is:
subset L (X :: L')
subset_extend < search.
Subgoal 2:
Variables: L L' X
H1 : subset L L'
============================
subset L (X :: L')
subset_extend < backchain subset_add.
Proof completed.
Abella < Theorem append_sub1 :
forall L1 L2 L, append L1 L2 L -> subset L1 L.
============================
forall L1 L2 L, append L1 L2 L -> subset L1 L
append_sub1 < induction on 1.
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
============================
forall L1 L2 L, append L1 L2 L @ -> subset L1 L
append_sub1 < intros.
Variables: L1 L2 L
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
H1 : append L1 L2 L @
============================
subset L1 L
append_sub1 < case H1.
Subgoal 1:
Variables: L
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
============================
subset nil L
Subgoal 2 is:
subset (X :: L3) (X :: L5)
append_sub1 < search.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
H2 : append L3 L2 L5 *
============================
subset (X :: L3) (X :: L5)
append_sub1 < backchain subset_extend.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, append L1 L2 L * -> subset L1 L
H2 : append L3 L2 L5 *
============================
subset L3 L5
append_sub1 < backchain IH.
Proof completed.
Abella < Theorem append_sub2 :
forall L1 L2 L, is_list L2 -> append L1 L2 L -> subset L2 L.
============================
forall L1 L2 L, is_list L2 -> append L1 L2 L -> subset L2 L
append_sub2 < induction on 2.
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
============================
forall L1 L2 L, is_list L2 -> append L1 L2 L @ -> subset L2 L
append_sub2 < intros.
Variables: L1 L2 L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L2
H2 : append L1 L2 L @
============================
subset L2 L
append_sub2 < case H2.
Subgoal 1:
Variables: L
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L
============================
subset L L
Subgoal 2 is:
subset L2 (X :: L5)
append_sub2 < backchain subset_refl.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
subset L2 (X :: L5)
append_sub2 < backchain subset_add.
Subgoal 2:
Variables: L2 L5 X L3
IH : forall L1 L2 L, is_list L2 -> append L1 L2 L * -> subset L2 L
H1 : is_list L2
H3 : append L3 L2 L5 *
============================
subset L2 L5
append_sub2 < backchain IH.
Proof completed.
Abella < Theorem append_subset_trans :
forall L1 L2 L L', append L1 L2 L -> subset L1 L' -> subset L2 L' ->
subset L L'.
============================
forall L1 L2 L L', append L1 L2 L -> subset L1 L' -> subset L2 L' ->
subset L L'
append_subset_trans < induction on 1.
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
subset L L'
============================
forall L1 L2 L L', append L1 L2 L @ -> subset L1 L' -> subset L2 L' ->
subset L L'
append_subset_trans < intros.
Variables: L1 L2 L L'
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
subset L L'
H1 : append L1 L2 L @
H2 : subset L1 L'
H3 : subset L2 L'
============================
subset L L'
append_subset_trans < case H1.
Subgoal 1:
Variables: L L'
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
subset L L'
H2 : subset nil L'
H3 : subset L L'
============================
subset L L'
Subgoal 2 is:
subset (X :: L5) L'
append_subset_trans < search.
Subgoal 2:
Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
subset L L'
H2 : subset (X :: L3) L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
============================
subset (X :: L5) L'
append_subset_trans < case H2.
Subgoal 2:
Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
subset L L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
H5 : member X L'
H6 : subset L3 L'
============================
subset (X :: L5) L'
append_subset_trans < unfold.
Subgoal 2.1:
Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
subset L L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
H5 : member X L'
H6 : subset L3 L'
============================
member X L'
Subgoal 2.2 is:
subset L5 L'
append_subset_trans < search.
Subgoal 2.2:
Variables: L2 L' L5 X L3
IH : forall L1 L2 L L', append L1 L2 L * -> subset L1 L' -> subset L2 L' ->
subset L L'
H3 : subset L2 L'
H4 : append L3 L2 L5 *
H5 : member X L'
H6 : subset L3 L'
============================
subset L5 L'
append_subset_trans < backchain IH.
Proof completed.
Abella < Theorem append_append_subset_trans :
forall L1 L1' L2 L2' L L', is_list L2' -> append L1 L2 L ->
append L1' L2' L' -> subset L1 L1' -> subset L2 L2' -> subset L L'.
============================
forall L1 L1' L2 L2' L L', is_list L2' -> append L1 L2 L ->
append L1' L2' L' -> subset L1 L1' -> subset L2 L2' -> subset L L'
append_append_subset_trans < intros.
Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
============================
subset L L'
append_append_subset_trans < assert subset L1 L'.
Subgoal 1:
Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
============================
subset L1 L'
Subgoal is:
subset L L'
append_append_subset_trans < backchain subset_trans with L2 = L1'.
Subgoal 1:
Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
============================
subset L1' L'
Subgoal is:
subset L L'
append_append_subset_trans < backchain append_sub1.
Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
============================
subset L L'
append_append_subset_trans < assert subset L2 L'.
Subgoal 2:
Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
============================
subset L2 L'
Subgoal is:
subset L L'
append_append_subset_trans < backchain subset_trans with L2 = L2'.
Subgoal 2:
Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
============================
subset L2' L'
Subgoal is:
subset L L'
append_append_subset_trans < backchain append_sub2.
Variables: L1 L1' L2 L2' L L'
H1 : is_list L2'
H2 : append L1 L2 L
H3 : append L1' L2' L'
H4 : subset L1 L1'
H5 : subset L2 L2'
H6 : subset L1 L'
H7 : subset L2 L'
============================
subset L L'
append_append_subset_trans < backchain append_subset_trans.
Proof completed.
Abella < Define tm_subset : tm_list -> tm_list -> prop by
tm_subset snil L;
tm_subset (scons X L1) L2 := {smember X L2} /\ tm_subset L1 L2.
Abella < Define is_tm_list : tm_list -> prop by
is_tm_list snil;
is_tm_list (scons X L) := is_tm_list L.
Abella < Theorem sappend_refl_eq :
forall L1 L2, {sappend L1 snil L2} -> L1 = L2.
============================
forall L1 L2, {sappend L1 snil L2} -> L1 = L2
sappend_refl_eq < induction on 1.
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
============================
forall L1 L2, {sappend L1 snil L2}@ -> L1 = L2
sappend_refl_eq < intros.
Variables: L1 L2
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
H1 : {sappend L1 snil L2}@
============================
L1 = L2
sappend_refl_eq < case H1.
Subgoal 1:
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
============================
snil = snil
Subgoal 2 is:
scons X L5 = scons X L3
sappend_refl_eq < search.
Subgoal 2:
Variables: L3 L5 X
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
H2 : {sappend L5 snil L3}*
============================
scons X L5 = scons X L3
sappend_refl_eq < apply IH to H2.
Subgoal 2:
Variables: L3 X
IH : forall L1 L2, {sappend L1 snil L2}* -> L1 = L2
H2 : {sappend L3 snil L3}*
============================
scons X L3 = scons X L3
sappend_refl_eq < search.
Proof completed.
Abella < Theorem append_prune_tm :
forall L1 L2 L3, nabla n, append L1 L2 (L3 n) -> (exists L3', L3 = y\L3').
============================
forall L1 L2 L3, nabla n, append L1 L2 (L3 n) -> (exists L3', L3 = y\L3')
append_prune_tm < induction on 1.
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
(exists L3', L3 = y\L3')
============================
forall L1 L2 L3, nabla n, append L1 L2 (L3 n) @ -> (exists L3', L3 = y\L3')
append_prune_tm < intros.
Variables: L1 L2 L3
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
(exists L3', L3 = y\L3')
H1 : append L1 L2 (L3 n1) @
============================
exists L3', L3 = y\L3'
append_prune_tm < case H1.
Subgoal 1:
Variables: L2
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
(exists L3', L3 = y\L3')
============================
exists L3', z1\L2 = y\L3'
Subgoal 2 is:
exists L3', z1\L7 :: L6 z1 = y\L3'
append_prune_tm < search.
Subgoal 2:
Variables: L2 L6 L7 L8
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
(exists L3', L3 = y\L3')
H2 : append L8 L2 (L6 n1) *
============================
exists L3', z1\L7 :: L6 z1 = y\L3'
append_prune_tm < apply IH to H2.
Subgoal 2:
Variables: L2 L7 L8 L3'
IH : forall L1 L2 L3, nabla n, append L1 L2 (L3 n) * ->
(exists L3', L3 = y\L3')
H2 : append L8 L2 L3' *
============================
exists L3'1, z1\L7 :: L3' = y\L3'1
append_prune_tm < search.
Proof completed.
Abella < Theorem tm_subset_add :
forall L L' X, tm_subset L L' -> tm_subset L (scons X L').
============================
forall L L' X, tm_subset L L' -> tm_subset L (scons X L')
tm_subset_add < induction on 1.
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
============================
forall L L' X, tm_subset L L' @ -> tm_subset L (scons X L')
tm_subset_add < intros.
Variables: L L' X
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H1 : tm_subset L L' @
============================
tm_subset L (scons X L')
tm_subset_add < case H1.
Subgoal 1:
Variables: L' X
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
============================
tm_subset snil (scons X L')
Subgoal 2 is:
tm_subset (scons X1 L1) (scons X L')
tm_subset_add < search.
Subgoal 2:
Variables: L' X L1 X1
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H2 : {smember X1 L'}
H3 : tm_subset L1 L' *
============================
tm_subset (scons X1 L1) (scons X L')
tm_subset_add < unfold.
Subgoal 2.1:
Variables: L' X L1 X1
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H2 : {smember X1 L'}
H3 : tm_subset L1 L' *
============================
{smember X1 (scons X L')}
Subgoal 2.2 is:
tm_subset L1 (scons X L')
tm_subset_add < search.
Subgoal 2.2:
Variables: L' X L1 X1
IH : forall L L' X, tm_subset L L' * -> tm_subset L (scons X L')
H2 : {smember X1 L'}
H3 : tm_subset L1 L' *
============================
tm_subset L1 (scons X L')
tm_subset_add < backchain IH.
Proof completed.
Abella < Theorem tm_subset_refl :
forall L, is_tm_list L -> tm_subset L L.
============================
forall L, is_tm_list L -> tm_subset L L
tm_subset_refl < induction on 1.
IH : forall L, is_tm_list L * -> tm_subset L L
============================
forall L, is_tm_list L @ -> tm_subset L L
tm_subset_refl < intros.
Variables: L
IH : forall L, is_tm_list L * -> tm_subset L L
H1 : is_tm_list L @
============================
tm_subset L L
tm_subset_refl < case H1.
Subgoal 1:
IH : forall L, is_tm_list L * -> tm_subset L L
============================
tm_subset snil snil
Subgoal 2 is:
tm_subset (scons X L1) (scons X L1)
tm_subset_refl < search.
Subgoal 2:
Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
tm_subset (scons X L1) (scons X L1)
tm_subset_refl < unfold.
Subgoal 2.1:
Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
{smember X (scons X L1)}
Subgoal 2.2 is:
tm_subset L1 (scons X L1)
tm_subset_refl < search.
Subgoal 2.2:
Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
tm_subset L1 (scons X L1)
tm_subset_refl < backchain tm_subset_add.
Subgoal 2.2:
Variables: L1 X
IH : forall L, is_tm_list L * -> tm_subset L L
H2 : is_tm_list L1 *
============================
tm_subset L1 L1
tm_subset_refl < backchain IH.
Proof completed.
Abella < Theorem tm_subset_mem_trans :
forall L1 L2 X, tm_subset L1 L2 -> {smember X L1} -> {smember X L2}.
============================
forall L1 L2 X, tm_subset L1 L2 -> {smember X L1} -> {smember X L2}
tm_subset_mem_trans < induction on 2.
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
============================
forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}@ -> {smember X L2}
tm_subset_mem_trans < intros.
Variables: L1 L2 X
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H1 : tm_subset L1 L2
H2 : {smember X L1}@
============================
{smember X L2}
tm_subset_mem_trans < case H2.
Subgoal 1:
Variables: L2 X L
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H1 : tm_subset (scons X L) L2
============================
{smember X L2}
Subgoal 2 is:
{smember X L2}
tm_subset_mem_trans < case H1.
Subgoal 1:
Variables: L2 X L
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H3 : {smember X L2}
H4 : tm_subset L L2
============================
{smember X L2}
Subgoal 2 is:
{smember X L2}
tm_subset_mem_trans < search.
Subgoal 2:
Variables: L2 X L X1
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H1 : tm_subset (scons X1 L) L2
H3 : {smember X L}*
============================
{smember X L2}
tm_subset_mem_trans < case H1.
Subgoal 2:
Variables: L2 X L X1
IH : forall L1 L2 X, tm_subset L1 L2 -> {smember X L1}* -> {smember X L2}
H3 : {smember X L}*
H4 : {smember X1 L2}
H5 : tm_subset L L2
============================
{smember X L2}
tm_subset_mem_trans < backchain IH.
Proof completed.
Abella < Theorem tm_subset_trans :
forall L1 L2 L3, tm_subset L1 L2 -> tm_subset L2 L3 -> tm_subset L1 L3.
============================
forall L1 L2 L3, tm_subset L1 L2 -> tm_subset L2 L3 -> tm_subset L1 L3
tm_subset_trans < induction on 1.
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
============================
forall L1 L2 L3, tm_subset L1 L2 @ -> tm_subset L2 L3 -> tm_subset L1 L3
tm_subset_trans < intros.
Variables: L1 L2 L3
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H1 : tm_subset L1 L2 @
H2 : tm_subset L2 L3
============================
tm_subset L1 L3
tm_subset_trans < case H1.
Subgoal 1:
Variables: L2 L3
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
============================
tm_subset snil L3
Subgoal 2 is:
tm_subset (scons X L4) L3
tm_subset_trans < search.
Subgoal 2:
Variables: L2 L3 L4 X
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
H3 : {smember X L2}
H4 : tm_subset L4 L2 *
============================
tm_subset (scons X L4) L3
tm_subset_trans < unfold.
Subgoal 2.1:
Variables: L2 L3 L4 X
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
H3 : {smember X L2}
H4 : tm_subset L4 L2 *
============================
{smember X L3}
Subgoal 2.2 is:
tm_subset L4 L3
tm_subset_trans < backchain tm_subset_mem_trans.
Subgoal 2.2:
Variables: L2 L3 L4 X
IH : forall L1 L2 L3, tm_subset L1 L2 * -> tm_subset L2 L3 -> tm_subset L1 L3
H2 : tm_subset L2 L3
H3 : {smember X L2}
H4 : tm_subset L4 L2 *
============================
tm_subset L4 L3
tm_subset_trans < backchain IH.
Proof completed.
Abella < Theorem tm_subset_extend :
forall L L' X, tm_subset L L' -> tm_subset (scons X L) (scons X L').
============================
forall L L' X, tm_subset L L' -> tm_subset (scons X L) (scons X L')
tm_subset_extend < intros.
Variables: L L' X
H1 : tm_subset L L'
============================
tm_subset (scons X L) (scons X L')
tm_subset_extend < unfold.
Subgoal 1:
Variables: L L' X
H1 : tm_subset L L'
============================
{smember X (scons X L')}
Subgoal 2 is:
tm_subset L (scons X L')
tm_subset_extend < search.
Subgoal 2:
Variables: L L' X
H1 : tm_subset L L'
============================
tm_subset L (scons X L')
tm_subset_extend < backchain tm_subset_add.
Proof completed.
Abella < Define is_tm'_list : tm'_list -> prop by
is_tm'_list cnil;
is_tm'_list (ccons X L) := is_tm'_list L.
Abella < Theorem is_tm'_list_inst :
forall L V, nabla x, is_tm'_list (L x) -> is_tm'_list (L V).
============================
forall L V, nabla x, is_tm'_list (L x) -> is_tm'_list (L V)
is_tm'_list_inst < induction on 1.
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
============================
forall L V, nabla x, is_tm'_list (L x) @ -> is_tm'_list (L V)
is_tm'_list_inst < intros.
Variables: L V
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
H1 : is_tm'_list (L n1) @
============================
is_tm'_list (L V)
is_tm'_list_inst < case H1.
Subgoal 1:
Variables: V
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
============================
is_tm'_list cnil
Subgoal 2 is:
is_tm'_list (ccons (X V) (L1 V))
is_tm'_list_inst < search.
Subgoal 2:
Variables: V L1 X
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
H2 : is_tm'_list (L1 n1) *
============================
is_tm'_list (ccons (X V) (L1 V))
is_tm'_list_inst < apply IH to H2 with V = V.
Subgoal 2:
Variables: V L1 X
IH : forall L V, nabla x, is_tm'_list (L x) * -> is_tm'_list (L V)
H2 : is_tm'_list (L1 n1) *
H3 : is_tm'_list (L1 V)
============================
is_tm'_list (ccons (X V) (L1 V))
is_tm'_list_inst < search.
Proof completed.
Abella < Define tm'_list_length : tm'_list -> nat -> prop by
tm'_list_length cnil z;
tm'_list_length (ccons M ML) (s N) := tm'_list_length ML N.
Abella < Theorem member_prune_tm :
forall M L, nabla x, member (M x) L -> (exists M', M = y\M').
============================
forall M L, nabla x, member (M x) L -> (exists M', M = y\M')
member_prune_tm < induction on 1.
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
forall M L, nabla x, member (M x) L @ -> (exists M', M = y\M')
member_prune_tm < intros.
Variables: M L
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H1 : member (M n1) L @
============================
exists M', M = y\M'
member_prune_tm < case H1.
Subgoal 1:
Variables: L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
exists M', z1\L2 = y\M'
Subgoal 2 is:
exists M', M = y\M'
member_prune_tm < search.
Subgoal 2:
Variables: M L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member (M n1) L3 *
============================
exists M', M = y\M'
member_prune_tm < apply IH to H2.
Subgoal 2:
Variables: L3 L2 M'
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member M' L3 *
============================
exists M'1, z1\M' = y\M'1
member_prune_tm < search.
Proof completed.
Abella < Theorem member_prune_tm' :
forall M L, nabla x, member (M x) L -> (exists M', M = y\M').
============================
forall M L, nabla x, member (M x) L -> (exists M', M = y\M')
member_prune_tm' < induction on 1.
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
forall M L, nabla x, member (M x) L @ -> (exists M', M = y\M')
member_prune_tm' < intros.
Variables: M L
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H1 : member (M n1) L @
============================
exists M', M = y\M'
member_prune_tm' < case H1.
Subgoal 1:
Variables: L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
============================
exists M', z1\L2 = y\M'
Subgoal 2 is:
exists M', M = y\M'
member_prune_tm' < search.
Subgoal 2:
Variables: M L3 L2
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member (M n1) L3 *
============================
exists M', M = y\M'
member_prune_tm' < apply IH to H2.
Subgoal 2:
Variables: L3 L2 M'
IH : forall M L, nabla x, member (M x) L * -> (exists M', M = y\M')
H2 : member M' L3 *
============================
exists M'1, z1\M' = y\M'1
member_prune_tm' < search.
Proof completed.
Abella < Theorem mmember_prune_tm :
forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M').
============================
forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M')
mmember_prune_tm < induction on 1.
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
forall M L, nabla x, {mmember (M x) L}@ -> (exists M', M = y\M')
mmember_prune_tm < intros.
Variables: M L
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H1 : {mmember (M n1) L}@
============================
exists M', M = y\M'
mmember_prune_tm < case H1.
Subgoal 1:
Variables: L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
exists M', z1\L2 = y\M'
Subgoal 2 is:
exists M', M = y\M'
mmember_prune_tm < search.
Subgoal 2:
Variables: M L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember (M n1) L3}*
============================
exists M', M = y\M'
mmember_prune_tm < apply IH to H2.
Subgoal 2:
Variables: L3 L2 M'
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember M' L3}*
============================
exists M'1, z1\M' = y\M'1
mmember_prune_tm < search.
Proof completed.
Abella < Theorem mmember_prune_tm' :
forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M').
============================
forall M L, nabla x, {mmember (M x) L} -> (exists M', M = y\M')
mmember_prune_tm' < induction on 1.
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
forall M L, nabla x, {mmember (M x) L}@ -> (exists M', M = y\M')
mmember_prune_tm' < intros.
Variables: M L
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H1 : {mmember (M n1) L}@
============================
exists M', M = y\M'
mmember_prune_tm' < case H1.
Subgoal 1:
Variables: L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
============================
exists M', z1\L2 = y\M'
Subgoal 2 is:
exists M', M = y\M'
mmember_prune_tm' < search.
Subgoal 2:
Variables: M L3 L2
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember (M n1) L3}*
============================
exists M', M = y\M'
mmember_prune_tm' < apply IH to H2.
Subgoal 2:
Variables: L3 L2 M'
IH : forall M L, nabla x, {mmember (M x) L}* -> (exists M', M = y\M')
H2 : {mmember M' L3}*
============================
exists M'1, z1\M' = y\M'1
mmember_prune_tm' < search.
Proof completed.
Abella < Define name : tm -> prop by
nabla n, name n.
Abella < Define name' : tm' -> prop by
nabla n, name' n.
Abella < Theorem combine_subset :
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs.
============================
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
combine_subset < induction on 2.
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
============================
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}@ ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
combine_subset < intros.
Variables: Vs1 Vs2 Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}@
============================
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
combine_subset < case H2.
Subgoal 1:
Variables: Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
============================
tm_subset snil Vs /\ tm_subset Vs Vs
Subgoal 2 is:
tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs
Subgoal 3 is:
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < split.
Subgoal 1.1:
Variables: Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
============================
tm_subset snil Vs
Subgoal 1.2 is:
tm_subset Vs Vs
Subgoal 2 is:
tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs
Subgoal 3 is:
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < search.
Subgoal 1.2:
Variables: Vs
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
============================
tm_subset Vs Vs
Subgoal 2 is:
tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs
Subgoal 3 is:
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < backchain tm_subset_refl.
Subgoal 2:
Variables: Vs2 Vs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H3 : {smember X Vs2}*
H4 : {combine FVs1 Vs2 Vs}*
============================
tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs
Subgoal 3 is:
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < apply IH to _ H4.
Subgoal 2:
Variables: Vs2 Vs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H3 : {smember X Vs2}*
H4 : {combine FVs1 Vs2 Vs}*
H5 : tm_subset FVs1 Vs
H6 : tm_subset Vs2 Vs
============================
tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs
Subgoal 3 is:
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < apply tm_subset_mem_trans to H6 H3.
Subgoal 2:
Variables: Vs2 Vs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list Vs
H3 : {smember X Vs2}*
H4 : {combine FVs1 Vs2 Vs}*
H5 : tm_subset FVs1 Vs
H6 : tm_subset Vs2 Vs
H7 : {smember X Vs}
============================
tm_subset (scons X FVs1) Vs /\ tm_subset Vs2 Vs
Subgoal 3 is:
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < search.
Subgoal 3:
Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H1 : is_tm_list (scons X FVs)
H3 : {combine FVs1 Vs2 FVs}*
============================
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < case H1.
Subgoal 3:
Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
============================
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < apply IH to _ H3.
Subgoal 3:
Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
H5 : tm_subset FVs1 FVs
H6 : tm_subset Vs2 FVs
============================
tm_subset (scons X FVs1) (scons X FVs) /\ tm_subset Vs2 (scons X FVs)
combine_subset < split.
Subgoal 3.1:
Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
H5 : tm_subset FVs1 FVs
H6 : tm_subset Vs2 FVs
============================
tm_subset (scons X FVs1) (scons X FVs)
Subgoal 3.2 is:
tm_subset Vs2 (scons X FVs)
combine_subset < backchain tm_subset_extend.
Subgoal 3.2:
Variables: Vs2 FVs FVs1 X
IH : forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs}* ->
tm_subset Vs1 Vs /\ tm_subset Vs2 Vs
H3 : {combine FVs1 Vs2 FVs}*
H4 : is_tm_list FVs
H5 : tm_subset FVs1 FVs
H6 : tm_subset Vs2 FVs
============================
tm_subset Vs2 (scons X FVs)
combine_subset < backchain tm_subset_add.
Proof completed.
Abella < Theorem combine_sub1 :
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs1 Vs.
============================
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs1 Vs
combine_sub1 < intros.
Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
============================
tm_subset Vs1 Vs
combine_sub1 < apply combine_subset to _ H2.
Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
H3 : tm_subset Vs1 Vs
H4 : tm_subset Vs2 Vs
============================
tm_subset Vs1 Vs
combine_sub1 < search.
Proof completed.
Abella < Theorem combine_sub2 :
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs2 Vs.
============================
forall Vs1 Vs2 Vs, is_tm_list Vs -> {combine Vs1 Vs2 Vs} -> tm_subset Vs2 Vs
combine_sub2 < intros.
Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
============================
tm_subset Vs2 Vs
combine_sub2 < apply combine_subset to _ H2.
Variables: Vs1 Vs2 Vs
H1 : is_tm_list Vs
H2 : {combine Vs1 Vs2 Vs}
H3 : tm_subset Vs1 Vs
H4 : tm_subset Vs2 Vs
============================
tm_subset Vs2 Vs
combine_sub2 < search.
Proof completed.
Abella < Kind smap type.
Abella < Kind smap_list type.
Abella < Type smap tm -> tm -> smap.
Abella < Type smnil smap_list.
Abella < Type smcons smap -> smap_list -> smap_list.
Abella < Define smmember : smap -> smap_list -> prop by
smmember X (smcons X L);
smmember X (smcons Y L) := smmember X L.
Abella < Kind cmap type.
Abella < Kind cmap_list type.
Abella < Type cmap tm' -> tm' -> cmap.
Abella < Type cmnil cmap_list.
Abella < Type cmcons cmap -> cmap_list -> cmap_list.
Abella < Define cmmember : cmap -> cmap_list -> prop by
cmmember X (cmcons X L);
cmmember X (cmcons Y L) := cmmember X L.
Abella < Theorem smmember_prune_tm :
forall M L, nabla x, smmember (M x) L -> (exists M', M = y\M').
============================
forall M L, nabla x, smmember (M x) L -> (exists M', M = y\M')
smmember_prune_tm < induction on 1.
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
============================
forall M L, nabla x, smmember (M x) L @ -> (exists M', M = y\M')
smmember_prune_tm < intros.
Variables: M L
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
H1 : smmember (M n1) L @
============================
exists M', M = y\M'
smmember_prune_tm < case H1.
Subgoal 1:
Variables: L3 L2
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
============================
exists M', z1\L2 = y\M'
Subgoal 2 is:
exists M', M = y\M'
smmember_prune_tm < search.
Subgoal 2:
Variables: M L3 L2
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
H2 : smmember (M n1) L3 *
============================
exists M', M = y\M'
smmember_prune_tm < apply IH to H2.
Subgoal 2:
Variables: L3 L2 M'
IH : forall M L, nabla x, smmember (M x) L * -> (exists M', M = y\M')
H2 : smmember M' L3 *
============================
exists M'1, z1\M' = y\M'1
smmember_prune_tm < search.
Proof completed.
Abella < Theorem cmmember_prune_tm' :
forall M L, nabla x, cmmember (M x) L -> (exists M', M = y\M').
============================
forall M L, nabla x, cmmember (M x) L -> (exists M', M = y\M')
cmmember_prune_tm' < induction on 1.
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
============================
forall M L, nabla x, cmmember (M x) L @ -> (exists M', M = y\M')
cmmember_prune_tm' < intros.
Variables: M L
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
H1 : cmmember (M n1) L @
============================
exists M', M = y\M'
cmmember_prune_tm' < case H1.
Subgoal 1:
Variables: L3 L2
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
============================
exists M', z1\L2 = y\M'
Subgoal 2 is:
exists M', M = y\M'
cmmember_prune_tm' < search.
Subgoal 2:
Variables: M L3 L2
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
H2 : cmmember (M n1) L3 *
============================
exists M', M = y\M'
cmmember_prune_tm' < apply IH to H2.
Subgoal 2:
Variables: L3 L2 M'
IH : forall M L, nabla x, cmmember (M x) L * -> (exists M', M = y\M')
H2 : cmmember M' L3 *
============================
exists M'1, z1\M' = y\M'1
cmmember_prune_tm' < search.
Proof completed.
Abella < Theorem crev_det :
forall L1 L2 L3 L3', {crev L1 L2 L3} -> {crev L1 L2 L3'} -> L3 = L3'.
============================
forall L1 L2 L3 L3', {crev L1 L2 L3} -> {crev L1 L2 L3'} -> L3 = L3'
crev_det < induction on 1.
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
============================
forall L1 L2 L3 L3', {crev L1 L2 L3}@ -> {crev L1 L2 L3'} -> L3 = L3'
crev_det < intros.
Variables: L1 L2 L3 L3'
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H1 : {crev L1 L2 L3}@
H2 : {crev L1 L2 L3'}
============================
L3 = L3'
crev_det < case H1.
Subgoal 1:
Variables: L3 L3'
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H2 : {crev cnil L3 L3'}
============================
L3 = L3'
Subgoal 2 is:
L3 = L3'
crev_det < case H2.
Subgoal 1:
Variables: L3'
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
============================
L3' = L3'
Subgoal 2 is:
L3 = L3'
crev_det < search.
Subgoal 2:
Variables: L2 L3 L3' X L5
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H2 : {crev (ccons X L5) L2 L3'}
H3 : {crev L5 (ccons X L2) L3}*
============================
L3 = L3'
crev_det < case H2.
Subgoal 2:
Variables: L2 L3 L3' X L5
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H3 : {crev L5 (ccons X L2) L3}*
H4 : {crev L5 (ccons X L2) L3'}
============================
L3 = L3'
crev_det < apply IH to H3 H4.
Subgoal 2:
Variables: L2 L3' X L5
IH : forall L1 L2 L3 L3', {crev L1 L2 L3}* -> {crev L1 L2 L3'} -> L3 = L3'
H3 : {crev L5 (ccons X L2) L3'}*
H4 : {crev L5 (ccons X L2) L3'}
============================
L3' = L3'
crev_det < search.
Proof completed.
Abella < Theorem crev_prune :
forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)} -> (exists L3', L3 = x\L3').
============================
forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)} -> (exists L3', L3 = x\L3')
crev_prune < induction on 1.
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
(exists L3', L3 = x\L3')
============================
forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}@ -> (exists L3', L3 = x\L3')
crev_prune < intros.
Variables: L1 L2 L3
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
(exists L3', L3 = x\L3')
H1 : {crev L1 L2 (L3 n1)}@
============================
exists L3', L3 = x\L3'
crev_prune < case H1.
Subgoal 1:
Variables: L2
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
(exists L3', L3 = x\L3')
============================
exists L3', z1\L2 = x\L3'
Subgoal 2 is:
exists L3', L3 = x\L3'
crev_prune < search.
Subgoal 2:
Variables: L2 L3 L6 L7
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
(exists L3', L3 = x\L3')
H2 : {crev L7 (ccons L6 L2) (L3 n1)}*
============================
exists L3', L3 = x\L3'
crev_prune < apply IH to H2.
Subgoal 2:
Variables: L2 L6 L7 L3'
IH : forall L1 L2 L3, nabla x, {crev L1 L2 (L3 x)}* ->
(exists L3', L3 = x\L3')
H2 : {crev L7 (ccons L6 L2) L3'}*
============================
exists L3'1, z1\L3' = x\L3'1
crev_prune < search.
Proof completed.
Abella < Theorem tm'_list_to_tuple_det :
forall FE E E', {tm'_list_to_tuple FE E} -> {tm'_list_to_tuple FE E'} -> E =
E'.
============================
forall FE E E', {tm'_list_to_tuple FE E} -> {tm'_list_to_tuple FE E'} -> E =
E'
tm'_list_to_tuple_det < induction on 1.
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
{tm'_list_to_tuple FE E'} -> E =
E'
============================
forall FE E E', {tm'_list_to_tuple FE E}@ -> {tm'_list_to_tuple FE E'} ->
E =
E'
tm'_list_to_tuple_det < intros.
Variables: FE E E'
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
{tm'_list_to_tuple FE E'} -> E =
E'
H1 : {tm'_list_to_tuple FE E}@
H2 : {tm'_list_to_tuple FE E'}
============================
E = E'
tm'_list_to_tuple_det < case H1.
Subgoal 1:
Variables: E'
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
{tm'_list_to_tuple FE E'} -> E =
E'
H2 : {tm'_list_to_tuple cnil E'}
============================
unit' = E'
Subgoal 2 is:
pair' M ML' = E'
tm'_list_to_tuple_det < case H2.
Subgoal 1:
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
{tm'_list_to_tuple FE E'} -> E =
E'
============================
unit' = unit'
Subgoal 2 is:
pair' M ML' = E'
tm'_list_to_tuple_det < search.
Subgoal 2:
Variables: E' ML' ML M
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
{tm'_list_to_tuple FE E'} -> E =
E'
H2 : {tm'_list_to_tuple (ccons M ML) E'}
H3 : {tm'_list_to_tuple ML ML'}*
============================
pair' M ML' = E'
tm'_list_to_tuple_det < case H2.
Subgoal 2:
Variables: ML' ML M ML'1
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
{tm'_list_to_tuple FE E'} -> E =
E'
H3 : {tm'_list_to_tuple ML ML'}*
H4 : {tm'_list_to_tuple ML ML'1}
============================
pair' M ML' = pair' M ML'1
tm'_list_to_tuple_det < apply IH to H3 H4.
Subgoal 2:
Variables: ML M ML'1
IH : forall FE E E', {tm'_list_to_tuple FE E}* ->
{tm'_list_to_tuple FE E'} -> E =
E'
H3 : {tm'_list_to_tuple ML ML'1}*
H4 : {tm'_list_to_tuple ML ML'1}
============================
pair' M ML'1 = pair' M ML'1
tm'_list_to_tuple_det < search.
Proof completed.
Abella < Theorem tm'_list_to_tuple_exists :
forall L, is_tm'_list L -> (exists E, {tm'_list_to_tuple L E}).
============================
forall L, is_tm'_list L -> (exists E, {tm'_list_to_tuple L E})
tm'_list_to_tuple_exists < induction on 1.
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
============================
forall L, is_tm'_list L @ -> (exists E, {tm'_list_to_tuple L E})
tm'_list_to_tuple_exists < intros.
Variables: L
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
H1 : is_tm'_list L @
============================
exists E, {tm'_list_to_tuple L E}
tm'_list_to_tuple_exists < case H1.
Subgoal 1:
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
============================
exists E, {tm'_list_to_tuple cnil E}
Subgoal 2 is:
exists E, {tm'_list_to_tuple (ccons X L1) E}
tm'_list_to_tuple_exists < search.
Subgoal 2:
Variables: L1 X
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
H2 : is_tm'_list L1 *
============================
exists E, {tm'_list_to_tuple (ccons X L1) E}
tm'_list_to_tuple_exists < apply IH to H2.
Subgoal 2:
Variables: L1 X E
IH : forall L, is_tm'_list L * -> (exists E, {tm'_list_to_tuple L E})
H2 : is_tm'_list L1 *
H3 : {tm'_list_to_tuple L1 E}
============================
exists E, {tm'_list_to_tuple (ccons X L1) E}
tm'_list_to_tuple_exists < search.
Proof completed.
Abella < Theorem tm'_list_to_tuple_prune :
forall L E, nabla x, {tm'_list_to_tuple L (E x)} -> (exists E', E = y\E').
============================
forall L E, nabla x, {tm'_list_to_tuple L (E x)} -> (exists E', E = y\E')
tm'_list_to_tuple_prune < induction on 1.
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
(exists E', E = y\E')
============================
forall L E, nabla x, {tm'_list_to_tuple L (E x)}@ -> (exists E', E = y\E')
tm'_list_to_tuple_prune < intros.
Variables: L E
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
(exists E', E = y\E')
H1 : {tm'_list_to_tuple L (E n1)}@
============================
exists E', E = y\E'
tm'_list_to_tuple_prune < case H1.
Subgoal 1:
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
(exists E', E = y\E')
============================
exists E', z1\unit' = y\E'
Subgoal 2 is:
exists E', z1\pair' L1 (ML' z1) = y\E'
tm'_list_to_tuple_prune < search.
Subgoal 2:
Variables: ML' L2 L1
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
(exists E', E = y\E')
H2 : {tm'_list_to_tuple L2 (ML' n1)}*
============================
exists E', z1\pair' L1 (ML' z1) = y\E'
tm'_list_to_tuple_prune < apply IH to H2.
Subgoal 2:
Variables: L2 L1 E'
IH : forall L E, nabla x, {tm'_list_to_tuple L (E x)}* ->
(exists E', E = y\E')
H2 : {tm'_list_to_tuple L2 E'}*
============================
exists E'1, z1\pair' L1 E' = y\E'1
tm'_list_to_tuple_prune < search.
Proof completed.
Abella <