Welcome to Abella 2.0.7-dev.
Abella < Type is_o o -> prop.
Abella < Import "perm" with is_o := is_o.
Importing from "perm".
Abella < Define merge : (list o) -> (list o) -> (list o) -> prop by
merge nil nil nil;
merge J K L := exists A JJ LL, adj JJ A J /\ adj LL A L /\ merge JJ K LL;
merge J K L := exists A KK LL, adj KK A K /\ adj LL A L /\ merge J KK LL.
Abella < Theorem merge_1_is_list :
forall J K L, merge J K L -> is_list J.
============================
forall J K L, merge J K L -> is_list J
merge_1_is_list < induction on 1.
IH : forall J K L, merge J K L * -> is_list J
============================
forall J K L, merge J K L @ -> is_list J
merge_1_is_list < intros.
Variables: J K L
IH : forall J K L, merge J K L * -> is_list J
H1 : merge J K L @
============================
is_list J
merge_1_is_list < case H1.
Subgoal 1:
IH : forall J K L, merge J K L * -> is_list J
============================
is_list nil
Subgoal 2 is:
is_list J
Subgoal 3 is:
is_list J
merge_1_is_list < search.
Subgoal 2:
Variables: J K L A JJ LL
IH : forall J K L, merge J K L * -> is_list J
H2 : adj JJ A J
H3 : adj LL A L
H4 : merge JJ K LL *
============================
is_list J
Subgoal 3 is:
is_list J
merge_1_is_list < backchain adj_3_is_list.
Subgoal 3:
Variables: J K L A KK LL
IH : forall J K L, merge J K L * -> is_list J
H2 : adj KK A K
H3 : adj LL A L
H4 : merge J KK LL *
============================
is_list J
merge_1_is_list < backchain IH.
Proof completed.
Abella < Theorem merge_2_is_list :
forall J K L, merge J K L -> is_list K.
============================
forall J K L, merge J K L -> is_list K
merge_2_is_list < induction on 1.
IH : forall J K L, merge J K L * -> is_list K
============================
forall J K L, merge J K L @ -> is_list K
merge_2_is_list < intros.
Variables: J K L
IH : forall J K L, merge J K L * -> is_list K
H1 : merge J K L @
============================
is_list K
merge_2_is_list < case H1.
Subgoal 1:
IH : forall J K L, merge J K L * -> is_list K
============================
is_list nil
Subgoal 2 is:
is_list K
Subgoal 3 is:
is_list K
merge_2_is_list < search.
Subgoal 2:
Variables: J K L A JJ LL
IH : forall J K L, merge J K L * -> is_list K
H2 : adj JJ A J
H3 : adj LL A L
H4 : merge JJ K LL *
============================
is_list K
Subgoal 3 is:
is_list K
merge_2_is_list < backchain IH.
Subgoal 3:
Variables: J K L A KK LL
IH : forall J K L, merge J K L * -> is_list K
H2 : adj KK A K
H3 : adj LL A L
H4 : merge J KK LL *
============================
is_list K
merge_2_is_list < backchain adj_3_is_list.
Proof completed.
Abella < Theorem merge_3_is_list :
forall J K L, merge J K L -> is_list L.
============================
forall J K L, merge J K L -> is_list L
merge_3_is_list < intros.
Variables: J K L
H1 : merge J K L
============================
is_list L
merge_3_is_list < case H1.
Subgoal 1:
============================
is_list nil
Subgoal 2 is:
is_list L
Subgoal 3 is:
is_list L
merge_3_is_list < search.
Subgoal 2:
Variables: J K L A JJ LL
H2 : adj JJ A J
H3 : adj LL A L
H4 : merge JJ K LL
============================
is_list L
Subgoal 3 is:
is_list L
merge_3_is_list < backchain adj_3_is_list.
Subgoal 3:
Variables: J K L A KK LL
H2 : adj KK A K
H3 : adj LL A L
H4 : merge J KK LL
============================
is_list L
merge_3_is_list < backchain adj_3_is_list.
Proof completed.
Abella < Theorem perm_merge_1 :
forall J K L JJ, merge J K L -> perm J JJ -> merge JJ K L.
============================
forall J K L JJ, merge J K L -> perm J JJ -> merge JJ K L
perm_merge_1 < induction on 1.
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
============================
forall J K L JJ, merge J K L @ -> perm J JJ -> merge JJ K L
perm_merge_1 < intros.
Variables: J K L JJ
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H1 : merge J K L @
H2 : perm J JJ
============================
merge JJ K L
perm_merge_1 < case H1.
Subgoal 1:
Variables: JJ
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H2 : perm nil JJ
============================
merge JJ nil nil
Subgoal 2 is:
merge JJ K L
Subgoal 3 is:
merge JJ K L
perm_merge_1 < case H2.
Subgoal 1.1:
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
============================
merge nil nil nil
Subgoal 1.2 is:
merge JJ nil nil
Subgoal 2 is:
merge JJ K L
Subgoal 3 is:
merge JJ K L
perm_merge_1 < search.
Subgoal 1.2:
Variables: JJ A KK LL
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H3 : adj KK A nil
H4 : adj LL A JJ
H5 : perm KK LL
============================
merge JJ nil nil
Subgoal 2 is:
merge JJ K L
Subgoal 3 is:
merge JJ K L
perm_merge_1 < case H3.
Subgoal 2:
Variables: J K L JJ A JJ1 LL
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H2 : perm J JJ
H3 : adj JJ1 A J
H4 : adj LL A L
H5 : merge JJ1 K LL *
============================
merge JJ K L
Subgoal 3 is:
merge JJ K L
perm_merge_1 < apply adj_perm to H2 H3.
Subgoal 2:
Variables: J K L JJ A JJ1 LL KK
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H2 : perm J JJ
H3 : adj JJ1 A J
H4 : adj LL A L
H5 : merge JJ1 K LL *
H6 : adj KK A JJ
============================
merge JJ K L
Subgoal 3 is:
merge JJ K L
perm_merge_1 < apply perm_invert to H2 H3 H6.
Subgoal 2:
Variables: J K L JJ A JJ1 LL KK
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H2 : perm J JJ
H3 : adj JJ1 A J
H4 : adj LL A L
H5 : merge JJ1 K LL *
H6 : adj KK A JJ
H7 : perm JJ1 KK
============================
merge JJ K L
Subgoal 3 is:
merge JJ K L
perm_merge_1 < apply IH to H5 H7.
Subgoal 2:
Variables: J K L JJ A JJ1 LL KK
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H2 : perm J JJ
H3 : adj JJ1 A J
H4 : adj LL A L
H5 : merge JJ1 K LL *
H6 : adj KK A JJ
H7 : perm JJ1 KK
H8 : merge KK K LL
============================
merge JJ K L
Subgoal 3 is:
merge JJ K L
perm_merge_1 < search.
Subgoal 3:
Variables: J K L JJ A KK LL
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H2 : perm J JJ
H3 : adj KK A K
H4 : adj LL A L
H5 : merge J KK LL *
============================
merge JJ K L
perm_merge_1 < apply IH to H5 H2.
Subgoal 3:
Variables: J K L JJ A KK LL
IH : forall J K L JJ, merge J K L * -> perm J JJ -> merge JJ K L
H2 : perm J JJ
H3 : adj KK A K
H4 : adj LL A L
H5 : merge J KK LL *
H6 : merge JJ KK LL
============================
merge JJ K L
perm_merge_1 < search.
Proof completed.
Abella < Theorem perm_merge_2 :
forall J K L KK, merge J K L -> perm K KK -> merge J KK L.
============================
forall J K L KK, merge J K L -> perm K KK -> merge J KK L
perm_merge_2 < induction on 1.
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
============================
forall J K L KK, merge J K L @ -> perm K KK -> merge J KK L
perm_merge_2 < intros.
Variables: J K L KK
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H1 : merge J K L @
H2 : perm K KK
============================
merge J KK L
perm_merge_2 < case H1.
Subgoal 1:
Variables: KK
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H2 : perm nil KK
============================
merge nil KK nil
Subgoal 2 is:
merge J KK L
Subgoal 3 is:
merge J KK L
perm_merge_2 < case H2.
Subgoal 1.1:
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
============================
merge nil nil nil
Subgoal 1.2 is:
merge nil KK nil
Subgoal 2 is:
merge J KK L
Subgoal 3 is:
merge J KK L
perm_merge_2 < search.
Subgoal 1.2:
Variables: KK A KK1 LL
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H3 : adj KK1 A nil
H4 : adj LL A KK
H5 : perm KK1 LL
============================
merge nil KK nil
Subgoal 2 is:
merge J KK L
Subgoal 3 is:
merge J KK L
perm_merge_2 < case H3.
Subgoal 2:
Variables: J K L KK A JJ LL
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H2 : perm K KK
H3 : adj JJ A J
H4 : adj LL A L
H5 : merge JJ K LL *
============================
merge J KK L
Subgoal 3 is:
merge J KK L
perm_merge_2 < apply IH to H5 H2.
Subgoal 2:
Variables: J K L KK A JJ LL
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H2 : perm K KK
H3 : adj JJ A J
H4 : adj LL A L
H5 : merge JJ K LL *
H6 : merge JJ KK LL
============================
merge J KK L
Subgoal 3 is:
merge J KK L
perm_merge_2 < search.
Subgoal 3:
Variables: J K L KK A KK1 LL
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H2 : perm K KK
H3 : adj KK1 A K
H4 : adj LL A L
H5 : merge J KK1 LL *
============================
merge J KK L
perm_merge_2 < apply adj_perm to H2 H3.
Subgoal 3:
Variables: J K L KK A KK1 LL KK2
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H2 : perm K KK
H3 : adj KK1 A K
H4 : adj LL A L
H5 : merge J KK1 LL *
H6 : adj KK2 A KK
============================
merge J KK L
perm_merge_2 < apply perm_invert to H2 H3 H6.
Subgoal 3:
Variables: J K L KK A KK1 LL KK2
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H2 : perm K KK
H3 : adj KK1 A K
H4 : adj LL A L
H5 : merge J KK1 LL *
H6 : adj KK2 A KK
H7 : perm KK1 KK2
============================
merge J KK L
perm_merge_2 < apply IH to H5 H7.
Subgoal 3:
Variables: J K L KK A KK1 LL KK2
IH : forall J K L KK, merge J K L * -> perm K KK -> merge J KK L
H2 : perm K KK
H3 : adj KK1 A K
H4 : adj LL A L
H5 : merge J KK1 LL *
H6 : adj KK2 A KK
H7 : perm KK1 KK2
H8 : merge J KK2 LL
============================
merge J KK L
perm_merge_2 < search.
Proof completed.
Abella < Theorem perm_merge_3 :
forall J K L LL, merge J K L -> perm L LL -> merge J K LL.
============================
forall J K L LL, merge J K L -> perm L LL -> merge J K LL
perm_merge_3 < induction on 1.
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
============================
forall J K L LL, merge J K L @ -> perm L LL -> merge J K LL
perm_merge_3 < intros.
Variables: J K L LL
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H1 : merge J K L @
H2 : perm L LL
============================
merge J K LL
perm_merge_3 < case H1.
Subgoal 1:
Variables: LL
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H2 : perm nil LL
============================
merge nil nil LL
Subgoal 2 is:
merge J K LL
Subgoal 3 is:
merge J K LL
perm_merge_3 < case H2.
Subgoal 1.1:
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
============================
merge nil nil nil
Subgoal 1.2 is:
merge nil nil LL
Subgoal 2 is:
merge J K LL
Subgoal 3 is:
merge J K LL
perm_merge_3 < search.
Subgoal 1.2:
Variables: LL A KK LL1
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H3 : adj KK A nil
H4 : adj LL1 A LL
H5 : perm KK LL1
============================
merge nil nil LL
Subgoal 2 is:
merge J K LL
Subgoal 3 is:
merge J K LL
perm_merge_3 < case H3.
Subgoal 2:
Variables: J K L LL A JJ LL1
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H2 : perm L LL
H3 : adj JJ A J
H4 : adj LL1 A L
H5 : merge JJ K LL1 *
============================
merge J K LL
Subgoal 3 is:
merge J K LL
perm_merge_3 < apply adj_perm_result to H2 H4.
Subgoal 2:
Variables: J K L LL A JJ LL1 KK
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H2 : perm L LL
H3 : adj JJ A J
H4 : adj LL1 A L
H5 : merge JJ K LL1 *
H6 : adj KK A LL
H7 : perm LL1 KK
============================
merge J K LL
Subgoal 3 is:
merge J K LL
perm_merge_3 < apply IH to H5 H7.
Subgoal 2:
Variables: J K L LL A JJ LL1 KK
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H2 : perm L LL
H3 : adj JJ A J
H4 : adj LL1 A L
H5 : merge JJ K LL1 *
H6 : adj KK A LL
H7 : perm LL1 KK
H8 : merge JJ K KK
============================
merge J K LL
Subgoal 3 is:
merge J K LL
perm_merge_3 < search.
Subgoal 3:
Variables: J K L LL A KK LL1
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H2 : perm L LL
H3 : adj KK A K
H4 : adj LL1 A L
H5 : merge J KK LL1 *
============================
merge J K LL
perm_merge_3 < apply adj_perm_result to H2 H4.
Subgoal 3:
Variables: J K L LL A KK LL1 KK1
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H2 : perm L LL
H3 : adj KK A K
H4 : adj LL1 A L
H5 : merge J KK LL1 *
H6 : adj KK1 A LL
H7 : perm LL1 KK1
============================
merge J K LL
perm_merge_3 < apply IH to H5 H7.
Subgoal 3:
Variables: J K L LL A KK LL1 KK1
IH : forall J K L LL, merge J K L * -> perm L LL -> merge J K LL
H2 : perm L LL
H3 : adj KK A K
H4 : adj LL1 A L
H5 : merge J KK LL1 *
H6 : adj KK1 A LL
H7 : perm LL1 KK1
H8 : merge J KK KK1
============================
merge J K LL
perm_merge_3 < search.
Proof completed.
Abella < Theorem merge_sym :
forall J K L, merge J K L -> merge K J L.
============================
forall J K L, merge J K L -> merge K J L
merge_sym < induction on 1.
IH : forall J K L, merge J K L * -> merge K J L
============================
forall J K L, merge J K L @ -> merge K J L
merge_sym < intros.
Variables: J K L
IH : forall J K L, merge J K L * -> merge K J L
H1 : merge J K L @
============================
merge K J L
merge_sym < case H1.
Subgoal 1:
IH : forall J K L, merge J K L * -> merge K J L
============================
merge nil nil nil
Subgoal 2 is:
merge K J L
Subgoal 3 is:
merge K J L
merge_sym < search.
Subgoal 2:
Variables: J K L A JJ LL
IH : forall J K L, merge J K L * -> merge K J L
H2 : adj JJ A J
H3 : adj LL A L
H4 : merge JJ K LL *
============================
merge K J L
Subgoal 3 is:
merge K J L
merge_sym < apply IH to H4.
Subgoal 2:
Variables: J K L A JJ LL
IH : forall J K L, merge J K L * -> merge K J L
H2 : adj JJ A J
H3 : adj LL A L
H4 : merge JJ K LL *
H5 : merge K JJ LL
============================
merge K J L
Subgoal 3 is:
merge K J L
merge_sym < search.
Subgoal 3:
Variables: J K L A KK LL
IH : forall J K L, merge J K L * -> merge K J L
H2 : adj KK A K
H3 : adj LL A L
H4 : merge J KK LL *
============================
merge K J L
merge_sym < apply IH to H4.
Subgoal 3:
Variables: J K L A KK LL
IH : forall J K L, merge J K L * -> merge K J L
H2 : adj KK A K
H3 : adj LL A L
H4 : merge J KK LL *
H5 : merge KK J LL
============================
merge K J L
merge_sym < search.
Proof completed.
Abella < Theorem merge_nil_perm :
forall K L, merge nil K L -> perm K L.
============================
forall K L, merge nil K L -> perm K L
merge_nil_perm < induction on 1.
IH : forall K L, merge nil K L * -> perm K L
============================
forall K L, merge nil K L @ -> perm K L
merge_nil_perm < intros.
Variables: K L
IH : forall K L, merge nil K L * -> perm K L
H1 : merge nil K L @
============================
perm K L
merge_nil_perm < case H1.
Subgoal 1:
IH : forall K L, merge nil K L * -> perm K L
============================
perm nil nil
Subgoal 2 is:
perm K L
Subgoal 3 is:
perm K L
merge_nil_perm < search.
Subgoal 2:
Variables: K L A JJ LL
IH : forall K L, merge nil K L * -> perm K L
H2 : adj JJ A nil
H3 : adj LL A L
H4 : merge JJ K LL *
============================
perm K L
Subgoal 3 is:
perm K L
merge_nil_perm < case H2.
Subgoal 3:
Variables: K L A KK LL
IH : forall K L, merge nil K L * -> perm K L
H2 : adj KK A K
H3 : adj LL A L
H4 : merge nil KK LL *
============================
perm K L
merge_nil_perm < apply IH to H4.
Subgoal 3:
Variables: K L A KK LL
IH : forall K L, merge nil K L * -> perm K L
H2 : adj KK A K
H3 : adj LL A L
H4 : merge nil KK LL *
H5 : perm KK LL
============================
perm K L
merge_nil_perm < search.
Proof completed.
Abella < Theorem merge_adj_1 :
forall A JJ J K LL, merge JJ K LL -> adj JJ A J ->
(exists L, adj LL A L /\ merge J K L).
============================
forall A JJ J K LL, merge JJ K LL -> adj JJ A J ->
(exists L, adj LL A L /\ merge J K L)
merge_adj_1 < intros.
Variables: A JJ J K LL
H1 : merge JJ K LL
H2 : adj JJ A J
============================
exists L, adj LL A L /\ merge J K L
merge_adj_1 < apply adj_2_is_o to H2.
Variables: A JJ J K LL
H1 : merge JJ K LL
H2 : adj JJ A J
H3 : is_o A
============================
exists L, adj LL A L /\ merge J K L
merge_adj_1 < apply merge_3_is_list to H1.
Variables: A JJ J K LL
H1 : merge JJ K LL
H2 : adj JJ A J
H3 : is_o A
H4 : is_list LL
============================
exists L, adj LL A L /\ merge J K L
merge_adj_1 < apply adj_exists to *H3 *H4.
Variables: A JJ J K LL M
H1 : merge JJ K LL
H2 : adj JJ A J
H5 : adj LL A M
============================
exists L, adj LL A L /\ merge J K L
merge_adj_1 < search.
Proof completed.
Abella < Theorem merge_unadj_1 :
forall J K L JJ A, merge J K L -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL).
============================
forall J K L JJ A, merge J K L -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
merge_unadj_1 < induction on 1.
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
============================
forall J K L JJ A, merge J K L @ -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
merge_unadj_1 < intros.
Variables: J K L JJ A
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H1 : merge J K L @
H2 : adj JJ A J
============================
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < case H1.
Subgoal 1:
Variables: JJ A
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A nil
============================
exists LL, adj LL A nil /\ merge JJ nil LL
Subgoal 2 is:
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < case H2.
Subgoal 2:
Variables: J K L JJ A A1 JJ1 LL
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H5 : merge JJ1 K LL *
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply adj_same_result_diff to H2 H3.
Subgoal 2:
Variables: J K L JJ A A1 JJ1 LL
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H5 : merge JJ1 K LL *
H6 : A = A1 /\ perm JJ JJ1 \/ (exists KK, adj KK A JJ1)
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < case H6.
Subgoal 2.1:
Variables: J K L JJ A1 JJ1 LL
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A1 J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H5 : merge JJ1 K LL *
H7 : perm JJ JJ1
============================
exists LL, adj LL A1 L /\ merge JJ K LL
Subgoal 2.2 is:
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply perm_sym to *H7.
Subgoal 2.1:
Variables: J K L JJ A1 JJ1 LL
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A1 J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H5 : merge JJ1 K LL *
H8 : perm JJ1 JJ
============================
exists LL, adj LL A1 L /\ merge JJ K LL
Subgoal 2.2 is:
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply perm_merge_1 to *H5 *H8.
Subgoal 2.1:
Variables: J K L JJ A1 JJ1 LL
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A1 J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H9 : merge JJ K LL
============================
exists LL, adj LL A1 L /\ merge JJ K LL
Subgoal 2.2 is:
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < search.
Subgoal 2.2:
Variables: J K L JJ A A1 JJ1 LL KK
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H5 : merge JJ1 K LL *
H7 : adj KK A JJ1
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply IH to *H5 H7.
Subgoal 2.2:
Variables: J K L JJ A A1 JJ1 LL KK LL1
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H7 : adj KK A JJ1
H8 : adj LL1 A LL
H9 : merge KK K LL1
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply adj_swap to H8 H4.
Subgoal 2.2:
Variables: J K L JJ A A1 JJ1 LL KK LL1 U
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H7 : adj KK A JJ1
H8 : adj LL1 A LL
H9 : merge KK K LL1
H10 : adj LL1 A1 U
H11 : adj U A L
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply adj_swap to H7 H3.
Subgoal 2.2:
Variables: J K L JJ A A1 JJ1 LL KK LL1 U U1
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H7 : adj KK A JJ1
H8 : adj LL1 A LL
H9 : merge KK K LL1
H10 : adj LL1 A1 U
H11 : adj U A L
H12 : adj KK A1 U1
H13 : adj U1 A J
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < assert merge U1 K U.
Subgoal 2.2:
Variables: J K L JJ A A1 JJ1 LL KK LL1 U U1
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H7 : adj KK A JJ1
H8 : adj LL1 A LL
H9 : merge KK K LL1
H10 : adj LL1 A1 U
H11 : adj U A L
H12 : adj KK A1 U1
H13 : adj U1 A J
H14 : merge U1 K U
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply adj_same_result to H13 H2.
Subgoal 2.2:
Variables: J K L JJ A A1 JJ1 LL KK LL1 U U1
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H7 : adj KK A JJ1
H8 : adj LL1 A LL
H9 : merge KK K LL1
H10 : adj LL1 A1 U
H11 : adj U A L
H12 : adj KK A1 U1
H13 : adj U1 A J
H14 : merge U1 K U
H15 : perm U1 JJ
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply perm_merge_1 to *H14 *H15.
Subgoal 2.2:
Variables: J K L JJ A A1 JJ1 LL KK LL1 U U1
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj JJ1 A1 J
H4 : adj LL A1 L
H7 : adj KK A JJ1
H8 : adj LL1 A LL
H9 : merge KK K LL1
H10 : adj LL1 A1 U
H11 : adj U A L
H12 : adj KK A1 U1
H13 : adj U1 A J
H16 : merge JJ K U
============================
exists LL, adj LL A L /\ merge JJ K LL
Subgoal 3 is:
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < search.
Subgoal 3:
Variables: J K L JJ A A1 KK LL
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj KK A1 K
H4 : adj LL A1 L
H5 : merge J KK LL *
============================
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply IH to H5 H2.
Subgoal 3:
Variables: J K L JJ A A1 KK LL LL1
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj KK A1 K
H4 : adj LL A1 L
H5 : merge J KK LL *
H6 : adj LL1 A LL
H7 : merge JJ KK LL1
============================
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < apply adj_swap to H6 H4.
Subgoal 3:
Variables: J K L JJ A A1 KK LL LL1 U
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj KK A1 K
H4 : adj LL A1 L
H5 : merge J KK LL *
H6 : adj LL1 A LL
H7 : merge JJ KK LL1
H8 : adj LL1 A1 U
H9 : adj U A L
============================
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < assert merge JJ K U.
Subgoal 3:
Variables: J K L JJ A A1 KK LL LL1 U
IH : forall J K L JJ A, merge J K L * -> adj JJ A J ->
(exists LL, adj LL A L /\ merge JJ K LL)
H2 : adj JJ A J
H3 : adj KK A1 K
H4 : adj LL A1 L
H5 : merge J KK LL *
H6 : adj LL1 A LL
H7 : merge JJ KK LL1
H8 : adj LL1 A1 U
H9 : adj U A L
H10 : merge JJ K U
============================
exists LL, adj LL A L /\ merge JJ K LL
merge_unadj_1 < search.
Proof completed.
Abella < Theorem merge_adj_2 :
forall A J KK K LL, merge J KK LL -> adj KK A K ->
(exists L, adj LL A L /\ merge J K L).
============================
forall A J KK K LL, merge J KK LL -> adj KK A K ->
(exists L, adj LL A L /\ merge J K L)
merge_adj_2 < intros.
Variables: A J KK K LL
H1 : merge J KK LL
H2 : adj KK A K
============================
exists L, adj LL A L /\ merge J K L
merge_adj_2 < apply adj_2_is_o to H2.
Variables: A J KK K LL
H1 : merge J KK LL
H2 : adj KK A K
H3 : is_o A
============================
exists L, adj LL A L /\ merge J K L
merge_adj_2 < apply merge_3_is_list to H1.
Variables: A J KK K LL
H1 : merge J KK LL
H2 : adj KK A K
H3 : is_o A
H4 : is_list LL
============================
exists L, adj LL A L /\ merge J K L
merge_adj_2 < apply adj_exists to *H3 *H4.
Variables: A J KK K LL M
H1 : merge J KK LL
H2 : adj KK A K
H5 : adj LL A M
============================
exists L, adj LL A L /\ merge J K L
merge_adj_2 < search.
Proof completed.
Abella < Theorem merge_unadj_2 :
forall J K L KK A, merge J K L -> adj KK A K ->
(exists LL, adj LL A L /\ merge J KK LL).
============================
forall J K L KK A, merge J K L -> adj KK A K ->
(exists LL, adj LL A L /\ merge J KK LL)
merge_unadj_2 < intros.
Variables: J K L KK A
H1 : merge J K L
H2 : adj KK A K
============================
exists LL, adj LL A L /\ merge J KK LL
merge_unadj_2 < apply merge_sym to *H1.
Variables: J K L KK A
H2 : adj KK A K
H3 : merge K J L
============================
exists LL, adj LL A L /\ merge J KK LL
merge_unadj_2 < apply merge_unadj_1 to *H3 *H2.
Variables: J K L KK A LL
H4 : adj LL A L
H5 : merge KK J LL
============================
exists LL, adj LL A L /\ merge J KK LL
merge_unadj_2 < apply merge_sym to *H5.
Variables: J K L KK A LL
H4 : adj LL A L
H6 : merge J KK LL
============================
exists LL, adj LL A L /\ merge J KK LL
merge_unadj_2 < search.
Proof completed.
Abella < Theorem merge_unadj_3 :
forall J K L LL A, merge J K L -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL).
============================
forall J K L LL A, merge J K L -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < induction on 1.
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
============================
forall J K L LL A, merge J K L @ -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < intros.
Variables: J K L LL A
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H1 : merge J K L @
H2 : adj LL A L
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < case H1.
Subgoal 1:
Variables: LL A
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A nil
============================
(exists JJ, adj JJ A nil /\ merge JJ nil LL) \/
(exists KK, adj KK A nil /\ merge nil KK LL)
Subgoal 2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < case H2.
Subgoal 2:
Variables: J K L LL A A1 JJ LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result_diff to H4 H2.
Subgoal 2:
Variables: J K L LL A A1 JJ LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H6 : A1 = A /\ perm LL1 LL \/ (exists KK, adj KK A1 LL)
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < case H6.
Subgoal 2.1:
Variables: J K L LL A JJ LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A J
H4 : adj LL1 A L
H5 : merge JJ K LL1 *
H7 : perm LL1 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply perm_merge_3 to *H5 *H7.
Subgoal 2.1:
Variables: J K L LL A JJ LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A J
H4 : adj LL1 A L
H8 : merge JJ K LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < search.
Subgoal 2.2:
Variables: J K L LL A A1 JJ LL1 KK
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H7 H2.
Subgoal 2.2:
Variables: J K L LL A A1 JJ LL1 KK U
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result to H9 H4.
Subgoal 2.2:
Variables: J K L LL A A1 JJ LL1 KK U
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_perm to H10 H8.
Subgoal 2.2:
Variables: J K L LL A A1 JJ LL1 KK U KK1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply IH to H5 H11.
Subgoal 2.2:
Variables: J K L LL A A1 JJ LL1 KK U KK1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H12 : (exists JJ1, adj JJ1 A JJ /\ merge JJ1 K KK1) \/
(exists KK, adj KK A K /\ merge JJ KK KK1)
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < case H12.
Subgoal 2.2.1:
Variables: J K L LL A A1 JJ LL1 KK U KK1 JJ1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj JJ1 A JJ
H14 : merge JJ1 K KK1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H13 H3.
Subgoal 2.2.1:
Variables: J K L LL A A1 JJ LL1 KK U KK1 JJ1 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj JJ1 A JJ
H14 : merge JJ1 K KK1
H15 : adj JJ1 A1 U1
H16 : adj U1 A J
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < assert merge U1 K LL.
Subgoal 2.2.1.1:
Variables: J K L LL A A1 JJ LL1 KK U KK1 JJ1 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj JJ1 A JJ
H14 : merge JJ1 K KK1
H15 : adj JJ1 A1 U1
H16 : adj U1 A J
============================
merge U1 K LL
Subgoal 2.2.1 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H11 H4.
Subgoal 2.2.1.1:
Variables: J K L LL A A1 JJ LL1 KK U KK1 JJ1 U1 U2
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj JJ1 A JJ
H14 : merge JJ1 K KK1
H15 : adj JJ1 A1 U1
H16 : adj U1 A J
H17 : adj KK1 A1 U2
H18 : adj U2 A L
============================
merge U1 K LL
Subgoal 2.2.1 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result to H18 H2.
Subgoal 2.2.1.1:
Variables: J K L LL A A1 JJ LL1 KK U KK1 JJ1 U1 U2
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj JJ1 A JJ
H14 : merge JJ1 K KK1
H15 : adj JJ1 A1 U1
H16 : adj U1 A J
H17 : adj KK1 A1 U2
H18 : adj U2 A L
H19 : perm U2 LL
============================
merge U1 K LL
Subgoal 2.2.1 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < backchain perm_merge_3.
Subgoal 2.2.1:
Variables: J K L LL A A1 JJ LL1 KK U KK1 JJ1 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj JJ1 A JJ
H14 : merge JJ1 K KK1
H15 : adj JJ1 A1 U1
H16 : adj U1 A J
H17 : merge U1 K LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 2.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < search.
Subgoal 2.2.2:
Variables: J K L LL A A1 JJ LL1 KK U KK1 KK2
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj KK2 A K
H14 : merge JJ KK2 KK1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H11 H4.
Subgoal 2.2.2:
Variables: J K L LL A A1 JJ LL1 KK U KK1 KK2 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj KK2 A K
H14 : merge JJ KK2 KK1
H15 : adj KK1 A1 U1
H16 : adj U1 A L
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < assert merge J KK2 U1.
Subgoal 2.2.2:
Variables: J K L LL A A1 JJ LL1 KK U KK1 KK2 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj KK2 A K
H14 : merge JJ KK2 KK1
H15 : adj KK1 A1 U1
H16 : adj U1 A L
H17 : merge J KK2 U1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result to H16 H2.
Subgoal 2.2.2:
Variables: J K L LL A A1 JJ LL1 KK U KK1 KK2 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj KK2 A K
H14 : merge JJ KK2 KK1
H15 : adj KK1 A1 U1
H16 : adj U1 A L
H17 : merge J KK2 U1
H18 : perm U1 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply perm_merge_3 to *H17 *H18.
Subgoal 2.2.2:
Variables: J K L LL A A1 JJ LL1 KK U KK1 KK2 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj JJ A1 J
H4 : adj LL1 A1 L
H5 : merge JJ K LL1 *
H7 : adj KK A1 LL
H8 : adj KK A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK1 A LL1
H13 : adj KK2 A K
H14 : merge JJ KK2 KK1
H15 : adj KK1 A1 U1
H16 : adj U1 A L
H19 : merge J KK2 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < search.
Subgoal 3:
Variables: J K L LL A A1 KK LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result_diff to H4 H2.
Subgoal 3:
Variables: J K L LL A A1 KK LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H6 : A1 = A /\ perm LL1 LL \/ (exists KK, adj KK A1 LL)
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < case H6.
Subgoal 3.1:
Variables: J K L LL A KK LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A K
H4 : adj LL1 A L
H5 : merge J KK LL1 *
H7 : perm LL1 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply perm_merge_3 to *H5 *H7.
Subgoal 3.1:
Variables: J K L LL A KK LL1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A K
H4 : adj LL1 A L
H8 : merge J KK LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < search.
Subgoal 3.2:
Variables: J K L LL A A1 KK LL1 KK1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H7 H2.
Subgoal 3.2:
Variables: J K L LL A A1 KK LL1 KK1 U
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result to H9 H4.
Subgoal 3.2:
Variables: J K L LL A A1 KK LL1 KK1 U
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_perm to H10 H8.
Subgoal 3.2:
Variables: J K L LL A A1 KK LL1 KK1 U KK2
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply IH to H5 H11.
Subgoal 3.2:
Variables: J K L LL A A1 KK LL1 KK1 U KK2
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H12 : (exists JJ, adj JJ A J /\ merge JJ KK KK2) \/
(exists KK1, adj KK1 A KK /\ merge J KK1 KK2)
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < case H12.
Subgoal 3.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 JJ
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj JJ A J
H14 : merge JJ KK KK2
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H11 H4.
Subgoal 3.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 JJ U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj JJ A J
H14 : merge JJ KK KK2
H15 : adj KK2 A1 U1
H16 : adj U1 A L
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < assert merge JJ K U1.
Subgoal 3.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 JJ U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj JJ A J
H14 : merge JJ KK KK2
H15 : adj KK2 A1 U1
H16 : adj U1 A L
H17 : merge JJ K U1
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result to H16 H2.
Subgoal 3.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 JJ U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj JJ A J
H14 : merge JJ KK KK2
H15 : adj KK2 A1 U1
H16 : adj U1 A L
H17 : merge JJ K U1
H18 : perm U1 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply perm_merge_3 to *H17 *H18.
Subgoal 3.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 JJ U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj JJ A J
H14 : merge JJ KK KK2
H15 : adj KK2 A1 U1
H16 : adj U1 A L
H19 : merge JJ K LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < search.
Subgoal 3.2.2:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 KK3
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj KK3 A KK
H14 : merge J KK3 KK2
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H13 H3.
Subgoal 3.2.2:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 KK3 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj KK3 A KK
H14 : merge J KK3 KK2
H15 : adj KK3 A1 U1
H16 : adj U1 A K
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < assert merge J U1 LL.
Subgoal 3.2.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 KK3 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj KK3 A KK
H14 : merge J KK3 KK2
H15 : adj KK3 A1 U1
H16 : adj U1 A K
============================
merge J U1 LL
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_swap to H11 H4.
Subgoal 3.2.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 KK3 U1 U2
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj KK3 A KK
H14 : merge J KK3 KK2
H15 : adj KK3 A1 U1
H16 : adj U1 A K
H17 : adj KK2 A1 U2
H18 : adj U2 A L
============================
merge J U1 LL
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < apply adj_same_result to H18 H2.
Subgoal 3.2.2.1:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 KK3 U1 U2
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj KK3 A KK
H14 : merge J KK3 KK2
H15 : adj KK3 A1 U1
H16 : adj U1 A K
H17 : adj KK2 A1 U2
H18 : adj U2 A L
H19 : perm U2 LL
============================
merge J U1 LL
Subgoal 3.2.2 is:
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < backchain perm_merge_3.
Subgoal 3.2.2:
Variables: J K L LL A A1 KK LL1 KK1 U KK2 KK3 U1
IH : forall J K L LL A, merge J K L * -> adj LL A L ->
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
H2 : adj LL A L
H3 : adj KK A1 K
H4 : adj LL1 A1 L
H5 : merge J KK LL1 *
H7 : adj KK1 A1 LL
H8 : adj KK1 A U
H9 : adj U A1 L
H10 : perm U LL1
H11 : adj KK2 A LL1
H13 : adj KK3 A KK
H14 : merge J KK3 KK2
H15 : adj KK3 A1 U1
H16 : adj U1 A K
H17 : merge J U1 LL
============================
(exists JJ, adj JJ A J /\ merge JJ K LL) \/
(exists KK, adj KK A K /\ merge J KK LL)
merge_unadj_3 < search.
Proof completed.
Abella < Theorem merge_invert_1 :
forall A JJ J K LL L, merge J K L -> adj JJ A J -> adj LL A L ->
merge JJ K LL.
============================
forall A JJ J K LL L, merge J K L -> adj JJ A J -> adj LL A L ->
merge JJ K LL
merge_invert_1 < intros.
Variables: A JJ J K LL L
H1 : merge J K L
H2 : adj JJ A J
H3 : adj LL A L
============================
merge JJ K LL
merge_invert_1 < apply merge_unadj_1 to H1 H2.
Variables: A JJ J K LL L LL1
H1 : merge J K L
H2 : adj JJ A J
H3 : adj LL A L
H4 : adj LL1 A L
H5 : merge JJ K LL1
============================
merge JJ K LL
merge_invert_1 < apply adj_same_result to *H4 *H3.
Variables: A JJ J K LL L LL1
H1 : merge J K L
H2 : adj JJ A J
H5 : merge JJ K LL1
H6 : perm LL1 LL
============================
merge JJ K LL
merge_invert_1 < backchain perm_merge_3.
Proof completed.
Abella < Theorem merge_invert_2 :
forall A J KK K LL L, merge J K L -> adj KK A K -> adj LL A L ->
merge J KK LL.
============================
forall A J KK K LL L, merge J K L -> adj KK A K -> adj LL A L ->
merge J KK LL
merge_invert_2 < intros.
Variables: A J KK K LL L
H1 : merge J K L
H2 : adj KK A K
H3 : adj LL A L
============================
merge J KK LL
merge_invert_2 < apply merge_sym to *H1.
Variables: A J KK K LL L
H2 : adj KK A K
H3 : adj LL A L
H4 : merge K J L
============================
merge J KK LL
merge_invert_2 < apply merge_invert_1 to *H4 *H2 *H3.
Variables: A J KK K LL L
H5 : merge KK J LL
============================
merge J KK LL
merge_invert_2 < backchain merge_sym.
Proof completed.
Abella < Theorem merge_move_12 :
forall A JJ J KK K L, adj JJ A J -> adj KK A K -> merge J KK L ->
merge JJ K L.
============================
forall A JJ J KK K L, adj JJ A J -> adj KK A K -> merge J KK L ->
merge JJ K L
merge_move_12 < intros.
Variables: A JJ J KK K L
H1 : adj JJ A J
H2 : adj KK A K
H3 : merge J KK L
============================
merge JJ K L
merge_move_12 < apply merge_unadj_1 to H3 H1.
Variables: A JJ J KK K L LL
H1 : adj JJ A J
H2 : adj KK A K
H3 : merge J KK L
H4 : adj LL A L
H5 : merge JJ KK LL
============================
merge JJ K L
merge_move_12 < search.
Proof completed.
Abella < Theorem merge_move_21 :
forall A JJ J KK K L, adj JJ A J -> adj KK A K -> merge JJ K L ->
merge J KK L.
============================
forall A JJ J KK K L, adj JJ A J -> adj KK A K -> merge JJ K L ->
merge J KK L
merge_move_21 < intros.
Variables: A JJ J KK K L
H1 : adj JJ A J
H2 : adj KK A K
H3 : merge JJ K L
============================
merge J KK L
merge_move_21 < apply merge_unadj_2 to H3 H2.
Variables: A JJ J KK K L LL
H1 : adj JJ A J
H2 : adj KK A K
H3 : merge JJ K L
H4 : adj LL A L
H5 : merge JJ KK LL
============================
merge J KK L
merge_move_21 < search.
Proof completed.
Abella < Theorem add_to_merge_right :
forall A J K KK L, adj KK A K -> merge J KK L ->
(exists M, merge J K M /\ adj L A M).
============================
forall A J K KK L, adj KK A K -> merge J KK L ->
(exists M, merge J K M /\ adj L A M)
add_to_merge_right < intros.
Variables: A J K KK L
H1 : adj KK A K
H2 : merge J KK L
============================
exists M, merge J K M /\ adj L A M
add_to_merge_right < apply adj_2_is_o to H1.
Variables: A J K KK L
H1 : adj KK A K
H2 : merge J KK L
H3 : is_o A
============================
exists M, merge J K M /\ adj L A M
add_to_merge_right < apply merge_3_is_list to H2.
Variables: A J K KK L
H1 : adj KK A K
H2 : merge J KK L
H3 : is_o A
H4 : is_list L
============================
exists M, merge J K M /\ adj L A M
add_to_merge_right < apply adj_exists to H3 H4.
Variables: A J K KK L M
H1 : adj KK A K
H2 : merge J KK L
H3 : is_o A
H4 : is_list L
H5 : adj L A M
============================
exists M, merge J K M /\ adj L A M
add_to_merge_right < search.
Proof completed.
Abella < Theorem add_to_merge_left :
forall A J JJ K L, adj JJ A J -> merge JJ K L ->
(exists M, merge J K M /\ adj L A M).
============================
forall A J JJ K L, adj JJ A J -> merge JJ K L ->
(exists M, merge J K M /\ adj L A M)
add_to_merge_left < intros.
Variables: A J JJ K L
H1 : adj JJ A J
H2 : merge JJ K L
============================
exists M, merge J K M /\ adj L A M
add_to_merge_left < apply adj_2_is_o to H1.
Variables: A J JJ K L
H1 : adj JJ A J
H2 : merge JJ K L
H3 : is_o A
============================
exists M, merge J K M /\ adj L A M
add_to_merge_left < apply merge_3_is_list to H2.
Variables: A J JJ K L
H1 : adj JJ A J
H2 : merge JJ K L
H3 : is_o A
H4 : is_list L
============================
exists M, merge J K M /\ adj L A M
add_to_merge_left < apply adj_exists to H3 H4.
Variables: A J JJ K L M
H1 : adj JJ A J
H2 : merge JJ K L
H3 : is_o A
H4 : is_list L
H5 : adj L A M
============================
exists M, merge J K M /\ adj L A M
add_to_merge_left < search.
Proof completed.
Abella < Theorem merge_nil_equal :
forall L, is_list L -> merge nil L L.
============================
forall L, is_list L -> merge nil L L
merge_nil_equal < induction on 1.
IH : forall L, is_list L * -> merge nil L L
============================
forall L, is_list L @ -> merge nil L L
merge_nil_equal < intros.
Variables: L
IH : forall L, is_list L * -> merge nil L L
H1 : is_list L @
============================
merge nil L L
merge_nil_equal < case H1.
Subgoal 1:
IH : forall L, is_list L * -> merge nil L L
============================
merge nil nil nil
Subgoal 2 is:
merge nil (A :: L1) (A :: L1)
merge_nil_equal < search.
Subgoal 2:
Variables: L1 A
IH : forall L, is_list L * -> merge nil L L
H2 : is_o A
H3 : is_list L1 *
============================
merge nil (A :: L1) (A :: L1)
merge_nil_equal < apply IH to H3.
Subgoal 2:
Variables: L1 A
IH : forall L, is_list L * -> merge nil L L
H2 : is_o A
H3 : is_list L1 *
H4 : merge nil L1 L1
============================
merge nil (A :: L1) (A :: L1)
merge_nil_equal < search.
Proof completed.
Abella < Theorem merge_exists :
forall J K, is_list J -> is_list K -> (exists L, merge J K L).
============================
forall J K, is_list J -> is_list K -> (exists L, merge J K L)
merge_exists < induction on 1.
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
============================
forall J K, is_list J @ -> is_list K -> (exists L, merge J K L)
merge_exists < intros.
Variables: J K
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
H1 : is_list J @
H2 : is_list K
============================
exists L, merge J K L
merge_exists < case H1.
Subgoal 1:
Variables: K
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
H2 : is_list K
============================
exists L, merge nil K L
Subgoal 2 is:
exists L1, merge (A :: L) K L1
merge_exists < apply merge_nil_equal to H2.
Subgoal 1:
Variables: K
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
H2 : is_list K
H3 : merge nil K K
============================
exists L, merge nil K L
Subgoal 2 is:
exists L1, merge (A :: L) K L1
merge_exists < search.
Subgoal 2:
Variables: K L A
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
H2 : is_list K
H3 : is_o A
H4 : is_list L *
============================
exists L1, merge (A :: L) K L1
merge_exists < apply IH to H4 H2.
Subgoal 2:
Variables: K L A L1
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
H2 : is_list K
H3 : is_o A
H4 : is_list L *
H5 : merge L K L1
============================
exists L1, merge (A :: L) K L1
merge_exists < assert adj L A (A :: L).
Subgoal 2:
Variables: K L A L1
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
H2 : is_list K
H3 : is_o A
H4 : is_list L *
H5 : merge L K L1
H6 : adj L A (A :: L)
============================
exists L1, merge (A :: L) K L1
merge_exists < apply add_to_merge_left to H6 H5.
Subgoal 2:
Variables: K L A L1 M
IH : forall J K, is_list J * -> is_list K -> (exists L, merge J K L)
H2 : is_list K
H3 : is_o A
H4 : is_list L *
H5 : merge L K L1
H6 : adj L A (A :: L)
H7 : merge (A :: L) K M
H8 : adj L1 A M
============================
exists L1, merge (A :: L) K L1
merge_exists < search.
Proof completed.
Abella < Theorem merge_head_lemma :
forall L A, is_o A -> is_list L -> merge L (A :: nil) (A :: L).
============================
forall L A, is_o A -> is_list L -> merge L (A :: nil) (A :: L)
merge_head_lemma < induction on 2.
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
============================
forall L A, is_o A -> is_list L @ -> merge L (A :: nil) (A :: L)
merge_head_lemma < intros.
Variables: L A
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list L @
============================
merge L (A :: nil) (A :: L)
merge_head_lemma < case H2 (keep).
Subgoal 1:
Variables: A
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list nil @
============================
merge nil (A :: nil) (A :: nil)
Subgoal 2 is:
merge (A1 :: L1) (A :: nil) (A :: A1 :: L1)
merge_head_lemma < assert is_list (A :: nil).
Subgoal 1:
Variables: A
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list nil @
H3 : is_list (A :: nil)
============================
merge nil (A :: nil) (A :: nil)
Subgoal 2 is:
merge (A1 :: L1) (A :: nil) (A :: A1 :: L1)
merge_head_lemma < apply merge_nil_equal to H3.
Subgoal 1:
Variables: A
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list nil @
H3 : is_list (A :: nil)
H4 : merge nil (A :: nil) (A :: nil)
============================
merge nil (A :: nil) (A :: nil)
Subgoal 2 is:
merge (A1 :: L1) (A :: nil) (A :: A1 :: L1)
merge_head_lemma < search.
Subgoal 2:
Variables: A L1 A1
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list (A1 :: L1) @
H3 : is_o A1
H4 : is_list L1 *
============================
merge (A1 :: L1) (A :: nil) (A :: A1 :: L1)
merge_head_lemma < assert adj L1 A1 (A1 :: L1).
Subgoal 2:
Variables: A L1 A1
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list (A1 :: L1) @
H3 : is_o A1
H4 : is_list L1 *
H5 : adj L1 A1 (A1 :: L1)
============================
merge (A1 :: L1) (A :: nil) (A :: A1 :: L1)
merge_head_lemma < apply IH to H1 H4.
Subgoal 2:
Variables: A L1 A1
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list (A1 :: L1) @
H3 : is_o A1
H4 : is_list L1 *
H5 : adj L1 A1 (A1 :: L1)
H6 : merge L1 (A :: nil) (A :: L1)
============================
merge (A1 :: L1) (A :: nil) (A :: A1 :: L1)
merge_head_lemma < apply add_to_merge_left to H5 H6.
Subgoal 2:
Variables: A L1 A1 M
IH : forall L A, is_o A -> is_list L * -> merge L (A :: nil) (A :: L)
H1 : is_o A
H2 : is_list (A1 :: L1) @
H3 : is_o A1
H4 : is_list L1 *
H5 : adj L1 A1 (A1 :: L1)
H6 : merge L1 (A :: nil) (A :: L1)
H7 : merge (A1 :: L1) (A :: nil) M
H8 : adj (A :: L1) A1 M
============================
merge (A1 :: L1) (A :: nil) (A :: A1 :: L1)
merge_head_lemma < search.
Proof completed.
Abella < Theorem adj_implies_merge :
forall L J A, adj L A J -> merge L (A :: nil) J.
============================
forall L J A, adj L A J -> merge L (A :: nil) J
adj_implies_merge < induction on 1.
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
============================
forall L J A, adj L A J @ -> merge L (A :: nil) J
adj_implies_merge < intros.
Variables: L J A
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H1 : adj L A J @
============================
merge L (A :: nil) J
adj_implies_merge < case H1.
Subgoal 1:
Variables: L A
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o A
H3 : is_list L
============================
merge L (A :: nil) (A :: L)
Subgoal 2 is:
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < apply merge_head_lemma to H2 H3.
Subgoal 1:
Variables: L A
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o A
H3 : is_list L
H4 : merge L (A :: nil) (A :: L)
============================
merge L (A :: nil) (A :: L)
Subgoal 2 is:
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < search.
Subgoal 2:
Variables: A L1 B K
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o B
H3 : adj K A L1 *
============================
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < apply IH to H3.
Subgoal 2:
Variables: A L1 B K
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o B
H3 : adj K A L1 *
H4 : merge K (A :: nil) L1
============================
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < apply adj_1_is_list to H3.
Subgoal 2:
Variables: A L1 B K
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o B
H3 : adj K A L1 *
H4 : merge K (A :: nil) L1
H5 : is_list K
============================
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < assert adj K B (B :: K).
Subgoal 2:
Variables: A L1 B K
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o B
H3 : adj K A L1 *
H4 : merge K (A :: nil) L1
H5 : is_list K
H6 : adj K B (B :: K)
============================
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < apply add_to_merge_left to H6 H4.
Subgoal 2:
Variables: A L1 B K M
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o B
H3 : adj K A L1 *
H4 : merge K (A :: nil) L1
H5 : is_list K
H6 : adj K B (B :: K)
H7 : merge (B :: K) (A :: nil) M
H8 : adj L1 B M
============================
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < apply adj_3_is_list to H3.
Subgoal 2:
Variables: A L1 B K M
IH : forall L J A, adj L A J * -> merge L (A :: nil) J
H2 : is_o B
H3 : adj K A L1 *
H4 : merge K (A :: nil) L1
H5 : is_list K
H6 : adj K B (B :: K)
H7 : merge (B :: K) (A :: nil) M
H8 : adj L1 B M
H9 : is_list L1
============================
merge (B :: K) (A :: nil) (B :: L1)
adj_implies_merge < search.
Proof completed.
Abella < Theorem merge_assoc :
forall J K L JK KL JKL1 JKL2, merge J K JK -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2.
============================
forall J K L JK KL JKL1 JKL2, merge J K JK -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
merge_assoc < induction on 1.
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
============================
forall J K L JK KL JKL1 JKL2, merge J K JK @ -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
merge_assoc < intros.
Variables: J K L JK KL JKL1 JKL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H1 : merge J K JK @
H2 : merge K L KL
H3 : merge J KL JKL1
H4 : merge JK L JKL2
============================
perm JKL1 JKL2
merge_assoc < case H1.
Subgoal 1:
Variables: L KL JKL1 JKL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H2 : merge nil L KL
H3 : merge nil KL JKL1
H4 : merge nil L JKL2
============================
perm JKL1 JKL2
Subgoal 2 is:
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < apply merge_nil_perm to *H2.
Subgoal 1:
Variables: L KL JKL1 JKL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H3 : merge nil KL JKL1
H4 : merge nil L JKL2
H5 : perm L KL
============================
perm JKL1 JKL2
Subgoal 2 is:
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < apply merge_nil_perm to *H3.
Subgoal 1:
Variables: L KL JKL1 JKL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H4 : merge nil L JKL2
H5 : perm L KL
H6 : perm KL JKL1
============================
perm JKL1 JKL2
Subgoal 2 is:
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < apply merge_nil_perm to *H4.
Subgoal 1:
Variables: L KL JKL1 JKL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H5 : perm L KL
H6 : perm KL JKL1
H7 : perm L JKL2
============================
perm JKL1 JKL2
Subgoal 2 is:
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < backchain perm_trans with K = L.
Subgoal 1:
Variables: L KL JKL1 JKL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H5 : perm L KL
H6 : perm KL JKL1
H7 : perm L JKL2
============================
perm JKL1 L
Subgoal 2 is:
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < backchain perm_sym.
Subgoal 1:
Variables: L KL JKL1 JKL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H5 : perm L KL
H6 : perm KL JKL1
H7 : perm L JKL2
============================
perm L JKL1
Subgoal 2 is:
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < backchain perm_trans.
Subgoal 2:
Variables: J K L JK KL JKL1 JKL2 A JJ LL
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H2 : merge K L KL
H3 : merge J KL JKL1
H4 : merge JK L JKL2
H5 : adj JJ A J
H6 : adj LL A JK
H7 : merge JJ K LL *
============================
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < apply merge_unadj_1 to *H4 H6.
Subgoal 2:
Variables: J K L JK KL JKL1 JKL2 A JJ LL LL1
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H2 : merge K L KL
H3 : merge J KL JKL1
H5 : adj JJ A J
H6 : adj LL A JK
H7 : merge JJ K LL *
H8 : adj LL1 A JKL2
H9 : merge LL L LL1
============================
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < apply merge_unadj_1 to *H3 H5.
Subgoal 2:
Variables: J K L JK KL JKL1 JKL2 A JJ LL LL1 LL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H2 : merge K L KL
H5 : adj JJ A J
H6 : adj LL A JK
H7 : merge JJ K LL *
H8 : adj LL1 A JKL2
H9 : merge LL L LL1
H10 : adj LL2 A JKL1
H11 : merge JJ KL LL2
============================
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < apply IH to *H7 *H2 *H11 *H9.
Subgoal 2:
Variables: J K L JK KL JKL1 JKL2 A JJ LL LL1 LL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H5 : adj JJ A J
H6 : adj LL A JK
H8 : adj LL1 A JKL2
H10 : adj LL2 A JKL1
H12 : perm LL2 LL1
============================
perm JKL1 JKL2
Subgoal 3 is:
perm JKL1 JKL2
merge_assoc < search.
Subgoal 3:
Variables: J K L JK KL JKL1 JKL2 A KK LL
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H2 : merge K L KL
H3 : merge J KL JKL1
H4 : merge JK L JKL2
H5 : adj KK A K
H6 : adj LL A JK
H7 : merge J KK LL *
============================
perm JKL1 JKL2
merge_assoc < apply merge_unadj_1 to *H2 H5.
Subgoal 3:
Variables: J K L JK KL JKL1 JKL2 A KK LL LL1
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H3 : merge J KL JKL1
H4 : merge JK L JKL2
H5 : adj KK A K
H6 : adj LL A JK
H7 : merge J KK LL *
H8 : adj LL1 A KL
H9 : merge KK L LL1
============================
perm JKL1 JKL2
merge_assoc < apply merge_unadj_1 to *H4 H6.
Subgoal 3:
Variables: J K L JK KL JKL1 JKL2 A KK LL LL1 LL2
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H3 : merge J KL JKL1
H5 : adj KK A K
H6 : adj LL A JK
H7 : merge J KK LL *
H8 : adj LL1 A KL
H9 : merge KK L LL1
H10 : adj LL2 A JKL2
H11 : merge LL L LL2
============================
perm JKL1 JKL2
merge_assoc < apply merge_unadj_2 to *H3 H8.
Subgoal 3:
Variables: J K L JK KL JKL1 JKL2 A KK LL LL1 LL2 LL3
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H5 : adj KK A K
H6 : adj LL A JK
H7 : merge J KK LL *
H8 : adj LL1 A KL
H9 : merge KK L LL1
H10 : adj LL2 A JKL2
H11 : merge LL L LL2
H12 : adj LL3 A JKL1
H13 : merge J LL1 LL3
============================
perm JKL1 JKL2
merge_assoc < apply IH to *H7 *H9 *H13 *H11.
Subgoal 3:
Variables: J K L JK KL JKL1 JKL2 A KK LL LL1 LL2 LL3
IH : forall J K L JK KL JKL1 JKL2, merge J K JK * -> merge K L KL ->
merge J KL JKL1 -> merge JK L JKL2 -> perm JKL1 JKL2
H5 : adj KK A K
H6 : adj LL A JK
H8 : adj LL1 A KL
H10 : adj LL2 A JKL2
H12 : adj LL3 A JKL1
H14 : perm LL3 LL2
============================
perm JKL1 JKL2
merge_assoc < search.
Proof completed.
Abella < Theorem change_merge_order :
forall J K L JK KL JKL, merge JK L JKL -> merge J K JK -> merge K L KL ->
merge J KL JKL.
============================
forall J K L JK KL JKL, merge JK L JKL -> merge J K JK -> merge K L KL ->
merge J KL JKL
change_merge_order < intros.
Variables: J K L JK KL JKL
H1 : merge JK L JKL
H2 : merge J K JK
H3 : merge K L KL
============================
merge J KL JKL
change_merge_order < apply merge_1_is_list to H2.
Variables: J K L JK KL JKL
H1 : merge JK L JKL
H2 : merge J K JK
H3 : merge K L KL
H4 : is_list J
============================
merge J KL JKL
change_merge_order < apply merge_3_is_list to H3.
Variables: J K L JK KL JKL
H1 : merge JK L JKL
H2 : merge J K JK
H3 : merge K L KL
H4 : is_list J
H5 : is_list KL
============================
merge J KL JKL
change_merge_order < apply merge_exists to H4 H5.
Variables: J K L JK KL JKL L1
H1 : merge JK L JKL
H2 : merge J K JK
H3 : merge K L KL
H4 : is_list J
H5 : is_list KL
H6 : merge J KL L1
============================
merge J KL JKL
change_merge_order < apply merge_assoc to H2 H3 H6 H1.
Variables: J K L JK KL JKL L1
H1 : merge JK L JKL
H2 : merge J K JK
H3 : merge K L KL
H4 : is_list J
H5 : is_list KL
H6 : merge J KL L1
H7 : perm L1 JKL
============================
merge J KL JKL
change_merge_order < apply perm_merge_3 to H6 H7.
Variables: J K L JK KL JKL L1
H1 : merge JK L JKL
H2 : merge J K JK
H3 : merge K L KL
H4 : is_list J
H5 : is_list KL
H6 : merge J KL L1
H7 : perm L1 JKL
H8 : merge J KL JKL
============================
merge J KL JKL
change_merge_order < search.
Proof completed.
Abella < Theorem change_merge_order2 :
forall J K JK L KL JKL, merge J K JK -> merge K L KL -> merge J KL JKL ->
merge JK L JKL.
============================
forall J K JK L KL JKL, merge J K JK -> merge K L KL -> merge J KL JKL ->
merge JK L JKL
change_merge_order2 < intros.
Variables: J K JK L KL JKL
H1 : merge J K JK
H2 : merge K L KL
H3 : merge J KL JKL
============================
merge JK L JKL
change_merge_order2 < apply merge_3_is_list to H1.
Variables: J K JK L KL JKL
H1 : merge J K JK
H2 : merge K L KL
H3 : merge J KL JKL
H4 : is_list JK
============================
merge JK L JKL
change_merge_order2 < apply merge_2_is_list to H2.
Variables: J K JK L KL JKL
H1 : merge J K JK
H2 : merge K L KL
H3 : merge J KL JKL
H4 : is_list JK
H5 : is_list L
============================
merge JK L JKL
change_merge_order2 < apply merge_exists to *H4 *H5.
Variables: J K JK L KL JKL L1
H1 : merge J K JK
H2 : merge K L KL
H3 : merge J KL JKL
H6 : merge JK L L1
============================
merge JK L JKL
change_merge_order2 < apply merge_assoc to *H1 *H2 *H3 H6.
Variables: J K JK L KL JKL L1
H6 : merge JK L L1
H7 : perm JKL L1
============================
merge JK L JKL
change_merge_order2 < apply perm_sym to *H7.
Variables: J K JK L KL JKL L1
H6 : merge JK L L1
H8 : perm L1 JKL
============================
merge JK L JKL
change_merge_order2 < backchain perm_merge_3.
Proof completed.
Abella < Theorem merge_perm_det :
forall J K L1 L2, merge J K L1 -> merge J K L2 -> perm L1 L2.
============================
forall J K L1 L2, merge J K L1 -> merge J K L2 -> perm L1 L2
merge_perm_det < induction on 1.
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
============================
forall J K L1 L2, merge J K L1 @ -> merge J K L2 -> perm L1 L2
merge_perm_det < intros.
Variables: J K L1 L2
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H1 : merge J K L1 @
H2 : merge J K L2
============================
perm L1 L2
merge_perm_det < case H1.
Subgoal 1:
Variables: L2
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H2 : merge nil nil L2
============================
perm nil L2
Subgoal 2 is:
perm L1 L2
Subgoal 3 is:
perm L1 L2
merge_perm_det < backchain merge_nil_perm.
Subgoal 2:
Variables: J K L1 L2 A JJ LL
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H2 : merge J K L2
H3 : adj JJ A J
H4 : adj LL A L1
H5 : merge JJ K LL *
============================
perm L1 L2
Subgoal 3 is:
perm L1 L2
merge_perm_det < apply merge_unadj_1 to H2 H3.
Subgoal 2:
Variables: J K L1 L2 A JJ LL LL1
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H2 : merge J K L2
H3 : adj JJ A J
H4 : adj LL A L1
H5 : merge JJ K LL *
H6 : adj LL1 A L2
H7 : merge JJ K LL1
============================
perm L1 L2
Subgoal 3 is:
perm L1 L2
merge_perm_det < apply IH to H5 H7.
Subgoal 2:
Variables: J K L1 L2 A JJ LL LL1
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H2 : merge J K L2
H3 : adj JJ A J
H4 : adj LL A L1
H5 : merge JJ K LL *
H6 : adj LL1 A L2
H7 : merge JJ K LL1
H8 : perm LL LL1
============================
perm L1 L2
Subgoal 3 is:
perm L1 L2
merge_perm_det < search.
Subgoal 3:
Variables: J K L1 L2 A KK LL
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H2 : merge J K L2
H3 : adj KK A K
H4 : adj LL A L1
H5 : merge J KK LL *
============================
perm L1 L2
merge_perm_det < apply merge_unadj_2 to H2 H3.
Subgoal 3:
Variables: J K L1 L2 A KK LL LL1
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H2 : merge J K L2
H3 : adj KK A K
H4 : adj LL A L1
H5 : merge J KK LL *
H6 : adj LL1 A L2
H7 : merge J KK LL1
============================
perm L1 L2
merge_perm_det < apply IH to H5 H7.
Subgoal 3:
Variables: J K L1 L2 A KK LL LL1
IH : forall J K L1 L2, merge J K L1 * -> merge J K L2 -> perm L1 L2
H2 : merge J K L2
H3 : adj KK A K
H4 : adj LL A L1
H5 : merge J KK LL *
H6 : adj LL1 A L2
H7 : merge J KK LL1
H8 : perm LL LL1
============================
perm L1 L2
merge_perm_det < search.
Proof completed.
Abella < Theorem merge_preserves_perm_lem :
forall L LL J K, is_list J -> merge L J K -> merge LL J K -> perm L LL.
============================
forall L LL J K, is_list J -> merge L J K -> merge LL J K -> perm L LL
merge_preserves_perm_lem < induction on 1.
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
============================
forall L LL J K, is_list J @ -> merge L J K -> merge LL J K -> perm L LL
merge_preserves_perm_lem < intros.
Variables: L LL J K
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H1 : is_list J @
H2 : merge L J K
H3 : merge LL J K
============================
perm L LL
merge_preserves_perm_lem < case H1.
Subgoal 1:
Variables: L LL K
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L nil K
H3 : merge LL nil K
============================
perm L LL
Subgoal 2 is:
perm L LL
merge_preserves_perm_lem < apply merge_sym to H2.
Subgoal 1:
Variables: L LL K
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L nil K
H3 : merge LL nil K
H4 : merge nil L K
============================
perm L LL
Subgoal 2 is:
perm L LL
merge_preserves_perm_lem < apply merge_nil_perm to *H4.
Subgoal 1:
Variables: L LL K
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L nil K
H3 : merge LL nil K
H5 : perm L K
============================
perm L LL
Subgoal 2 is:
perm L LL
merge_preserves_perm_lem < apply merge_sym to H3.
Subgoal 1:
Variables: L LL K
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L nil K
H3 : merge LL nil K
H5 : perm L K
H6 : merge nil LL K
============================
perm L LL
Subgoal 2 is:
perm L LL
merge_preserves_perm_lem < apply merge_nil_perm to *H6.
Subgoal 1:
Variables: L LL K
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L nil K
H3 : merge LL nil K
H5 : perm L K
H7 : perm LL K
============================
perm L LL
Subgoal 2 is:
perm L LL
merge_preserves_perm_lem < apply perm_sym to *H7.
Subgoal 1:
Variables: L LL K
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L nil K
H3 : merge LL nil K
H5 : perm L K
H8 : perm K LL
============================
perm L LL
Subgoal 2 is:
perm L LL
merge_preserves_perm_lem < backchain perm_trans.
Subgoal 2:
Variables: L LL K L1 A
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L (A :: L1) K
H3 : merge LL (A :: L1) K
H4 : is_o A
H5 : is_list L1 *
============================
perm L LL
merge_preserves_perm_lem < apply merge_unadj_2 to H2 _.
Subgoal 2:
Variables: L LL K L1 A LL1
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L (A :: L1) K
H3 : merge LL (A :: L1) K
H4 : is_o A
H5 : is_list L1 *
H6 : adj LL1 A K
H7 : merge L L1 LL1
============================
perm L LL
merge_preserves_perm_lem < apply merge_unadj_2 to H3 _.
Subgoal 2:
Variables: L LL K L1 A LL1 LL2
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L (A :: L1) K
H3 : merge LL (A :: L1) K
H4 : is_o A
H5 : is_list L1 *
H6 : adj LL1 A K
H7 : merge L L1 LL1
H8 : adj LL2 A K
H9 : merge LL L1 LL2
============================
perm L LL
merge_preserves_perm_lem < apply adj_same_result to H8 H6.
Subgoal 2:
Variables: L LL K L1 A LL1 LL2
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L (A :: L1) K
H3 : merge LL (A :: L1) K
H4 : is_o A
H5 : is_list L1 *
H6 : adj LL1 A K
H7 : merge L L1 LL1
H8 : adj LL2 A K
H9 : merge LL L1 LL2
H10 : perm LL2 LL1
============================
perm L LL
merge_preserves_perm_lem < apply perm_merge_3 to *H9 *H10.
Subgoal 2:
Variables: L LL K L1 A LL1 LL2
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L (A :: L1) K
H3 : merge LL (A :: L1) K
H4 : is_o A
H5 : is_list L1 *
H6 : adj LL1 A K
H7 : merge L L1 LL1
H8 : adj LL2 A K
H11 : merge LL L1 LL1
============================
perm L LL
merge_preserves_perm_lem < apply IH to *H5 *H7 *H11.
Subgoal 2:
Variables: L LL K L1 A LL1 LL2
IH : forall L LL J K, is_list J * -> merge L J K -> merge LL J K -> perm L LL
H2 : merge L (A :: L1) K
H3 : merge LL (A :: L1) K
H4 : is_o A
H6 : adj LL1 A K
H8 : adj LL2 A K
H12 : perm L LL
============================
perm L LL
merge_preserves_perm_lem < search.
Proof completed.
Abella < Theorem merge_preserves_perm :
forall L LL J K, merge L J K -> merge LL J K -> perm L LL.
============================
forall L LL J K, merge L J K -> merge LL J K -> perm L LL
merge_preserves_perm < intros.
Variables: L LL J K
H1 : merge L J K
H2 : merge LL J K
============================
perm L LL
merge_preserves_perm < apply merge_2_is_list to H1.
Variables: L LL J K
H1 : merge L J K
H2 : merge LL J K
H3 : is_list J
============================
perm L LL
merge_preserves_perm < backchain merge_preserves_perm_lem.
Proof completed.
Abella < Theorem merge_sub :
forall J K L JK JL JKL, merge J K JK -> merge JK L JKL -> merge JL K JKL ->
merge J L JL.
============================
forall J K L JK JL JKL, merge J K JK -> merge JK L JKL -> merge JL K JKL ->
merge J L JL
merge_sub < intros.
Variables: J K L JK JL JKL
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
============================
merge J L JL
merge_sub < apply merge_1_is_list to H1.
Variables: J K L JK JL JKL
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
============================
merge J L JL
merge_sub < apply merge_2_is_list to H2.
Variables: J K L JK JL JKL
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
============================
merge J L JL
merge_sub < apply merge_exists to H4 H5.
Variables: J K L JK JL JKL L1
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
============================
merge J L JL
merge_sub < apply merge_sym to H1.
Variables: J K L JK JL JKL L1
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
============================
merge J L JL
merge_sub < apply merge_2_is_list to H1.
Variables: J K L JK JL JKL L1
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
============================
merge J L JL
merge_sub < apply merge_3_is_list to H6.
Variables: J K L JK JL JKL L1
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
H9 : is_list L1
============================
merge J L JL
merge_sub < apply merge_exists to H8 H9.
Variables: J K L JK JL JKL L1 L2
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
H9 : is_list L1
H10 : merge K L1 L2
============================
merge J L JL
merge_sub < apply merge_assoc to H7 H6 H10 H2.
Variables: J K L JK JL JKL L1 L2
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
H9 : is_list L1
H10 : merge K L1 L2
H11 : perm L2 JKL
============================
merge J L JL
merge_sub < apply merge_sym to H10.
Variables: J K L JK JL JKL L1 L2
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
H9 : is_list L1
H10 : merge K L1 L2
H11 : perm L2 JKL
H12 : merge L1 K L2
============================
merge J L JL
merge_sub < apply perm_merge_3 to H12 H11.
Variables: J K L JK JL JKL L1 L2
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
H9 : is_list L1
H10 : merge K L1 L2
H11 : perm L2 JKL
H12 : merge L1 K L2
H13 : merge L1 K JKL
============================
merge J L JL
merge_sub < apply merge_preserves_perm to H13 H3.
Variables: J K L JK JL JKL L1 L2
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
H9 : is_list L1
H10 : merge K L1 L2
H11 : perm L2 JKL
H12 : merge L1 K L2
H13 : merge L1 K JKL
H14 : perm L1 JL
============================
merge J L JL
merge_sub < apply perm_merge_3 to H6 H14.
Variables: J K L JK JL JKL L1 L2
H1 : merge J K JK
H2 : merge JK L JKL
H3 : merge JL K JKL
H4 : is_list J
H5 : is_list L
H6 : merge J L L1
H7 : merge K J JK
H8 : is_list K
H9 : is_list L1
H10 : merge K L1 L2
H11 : perm L2 JKL
H12 : merge L1 K L2
H13 : merge L1 K JKL
H14 : perm L1 JL
H15 : merge J L JL
============================
merge J L JL
merge_sub < search.
Proof completed.
Abella < Theorem merge_to_adj :
forall J L A, merge J (A :: nil) L -> (exists JJ, perm J JJ /\ adj JJ A L).
============================
forall J L A, merge J (A :: nil) L -> (exists JJ, perm J JJ /\ adj JJ A L)
merge_to_adj < induction on 1.
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
============================
forall J L A, merge J (A :: nil) L @ -> (exists JJ, perm J JJ /\ adj JJ A L)
merge_to_adj < intros.
Variables: J L A
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H1 : merge J (A :: nil) L @
============================
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < case H1.
Subgoal 1:
Variables: J L A A1 JJ LL
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H2 : adj JJ A1 J
H3 : adj LL A1 L
H4 : merge JJ (A :: nil) LL *
============================
exists JJ, perm J JJ /\ adj JJ A L
Subgoal 2 is:
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < apply IH to H4.
Subgoal 1:
Variables: J L A A1 JJ LL JJ1
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H2 : adj JJ A1 J
H3 : adj LL A1 L
H4 : merge JJ (A :: nil) LL *
H5 : perm JJ JJ1
H6 : adj JJ1 A LL
============================
exists JJ, perm J JJ /\ adj JJ A L
Subgoal 2 is:
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < apply adj_swap to H6 H3.
Subgoal 1:
Variables: J L A A1 JJ LL JJ1 U
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H2 : adj JJ A1 J
H3 : adj LL A1 L
H4 : merge JJ (A :: nil) LL *
H5 : perm JJ JJ1
H6 : adj JJ1 A LL
H7 : adj JJ1 A1 U
H8 : adj U A L
============================
exists JJ, perm J JJ /\ adj JJ A L
Subgoal 2 is:
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < search.
Subgoal 2:
Variables: J L A A1 KK LL
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H2 : adj KK A1 (A :: nil)
H3 : adj LL A1 L
H4 : merge J KK LL *
============================
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < apply adj_det to H2.
Subgoal 2:
Variables: J L A LL
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H2 : adj nil A (A :: nil)
H3 : adj LL A L
H4 : merge J nil LL *
============================
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < apply merge_sym to H4.
Subgoal 2:
Variables: J L A LL
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H2 : adj nil A (A :: nil)
H3 : adj LL A L
H4 : merge J nil LL *
H5 : merge nil J LL
============================
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < apply merge_nil_perm to H5.
Subgoal 2:
Variables: J L A LL
IH : forall J L A, merge J (A :: nil) L * ->
(exists JJ, perm J JJ /\ adj JJ A L)
H2 : adj nil A (A :: nil)
H3 : adj LL A L
H4 : merge J nil LL *
H5 : merge nil J LL
H6 : perm J LL
============================
exists JJ, perm J JJ /\ adj JJ A L
merge_to_adj < search.
Proof completed.
Abella < Theorem merge_same_result_diff :
forall J A K B L, merge J (A :: nil) L -> merge K (B :: nil) L -> A = B /\
perm J K \/ (exists KK, merge KK (A :: nil) K).
============================
forall J A K B L, merge J (A :: nil) L -> merge K (B :: nil) L -> A = B /\
perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < intros.
Variables: J A K B L
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply merge_to_adj to H1.
Variables: J A K B L JJ
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ A L
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply merge_to_adj to H2.
Variables: J A K B L JJ JJ1
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ A L
H5 : perm K JJ1
H6 : adj JJ1 B L
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply adj_same_result_diff to H4 H6.
Variables: J A K B L JJ JJ1
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ A L
H5 : perm K JJ1
H6 : adj JJ1 B L
H7 : A = B /\ perm JJ JJ1 \/ (exists KK, adj KK A JJ1)
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < case H7.
Subgoal 1:
Variables: J K B L JJ JJ1
H1 : merge J (B :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ B L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : perm JJ JJ1
============================
B = B /\ perm J K \/ (exists KK, merge KK (B :: nil) K)
Subgoal 2 is:
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply perm_trans to H3 H8.
Subgoal 1:
Variables: J K B L JJ JJ1
H1 : merge J (B :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ B L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : perm JJ JJ1
H9 : perm J JJ1
============================
B = B /\ perm J K \/ (exists KK, merge KK (B :: nil) K)
Subgoal 2 is:
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply perm_sym to H5.
Subgoal 1:
Variables: J K B L JJ JJ1
H1 : merge J (B :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ B L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : perm JJ JJ1
H9 : perm J JJ1
H10 : perm JJ1 K
============================
B = B /\ perm J K \/ (exists KK, merge KK (B :: nil) K)
Subgoal 2 is:
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply perm_trans to H9 H10.
Subgoal 1:
Variables: J K B L JJ JJ1
H1 : merge J (B :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ B L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : perm JJ JJ1
H9 : perm J JJ1
H10 : perm JJ1 K
H11 : perm J K
============================
B = B /\ perm J K \/ (exists KK, merge KK (B :: nil) K)
Subgoal 2 is:
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < search.
Subgoal 2:
Variables: J A K B L JJ JJ1 KK
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ A L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : adj KK A JJ1
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply adj_implies_merge to H8.
Subgoal 2:
Variables: J A K B L JJ JJ1 KK
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ A L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : adj KK A JJ1
H9 : merge KK (A :: nil) JJ1
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply perm_sym to H5.
Subgoal 2:
Variables: J A K B L JJ JJ1 KK
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ A L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : adj KK A JJ1
H9 : merge KK (A :: nil) JJ1
H10 : perm JJ1 K
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < apply perm_merge_3 to H9 H10.
Subgoal 2:
Variables: J A K B L JJ JJ1 KK
H1 : merge J (A :: nil) L
H2 : merge K (B :: nil) L
H3 : perm J JJ
H4 : adj JJ A L
H5 : perm K JJ1
H6 : adj JJ1 B L
H8 : adj KK A JJ1
H9 : merge KK (A :: nil) JJ1
H10 : perm JJ1 K
H11 : merge KK (A :: nil) K
============================
A = B /\ perm J K \/ (exists KK, merge KK (A :: nil) K)
merge_same_result_diff < search.
Proof completed.
Abella < Define subset : (list o) -> (list o) -> prop by
subset J L := exists K, merge J K L.
Abella < Theorem subset_1_is_list :
forall J K, subset J K -> is_list J.
============================
forall J K, subset J K -> is_list J
subset_1_is_list < intros.
Variables: J K
H1 : subset J K
============================
is_list J
subset_1_is_list < case H1.
Variables: J K K1
H2 : merge J K1 K
============================
is_list J
subset_1_is_list < backchain merge_1_is_list.
Proof completed.
Abella < Theorem subset_2_is_list :
forall J K, subset J K -> is_list K.
============================
forall J K, subset J K -> is_list K
subset_2_is_list < intros.
Variables: J K
H1 : subset J K
============================
is_list K
subset_2_is_list < case H1.
Variables: J K K1
H2 : merge J K1 K
============================
is_list K
subset_2_is_list < backchain merge_3_is_list.
Proof completed.
Abella <
