sig mallq. kind term, atm, fm type. %% We reuse the o type to define LL formulas type atom, natom atm -> fm. type tens, par fm -> fm -> fm. type one, bot fm. type wth, plus fm -> fm -> fm. type top, zero fm. %% A quantifier on the object level is defined using the %% HOAS (or lambda-parse trees) approach, i.e., a binder %% on the object level is a binder on the meta-level %% (hence the first function argument). type all, exs (term -> fm) -> fm. type dual fm -> fm -> o.
module mallq. % By defining this predicate on the specification logic % we can instantiate its nominal constants and the abella % can identify that the IH applies. \o/ dual (atom A) (natom A). dual (tens A B) (par AA BB) :- dual A AA, dual B BB. dual one bot. dual (plus A B) (wth AA BB) :- dual A AA, dual B BB. dual zero top. dual (exs A) (all B) :- pi x\ dual (A x) (B x).
Click on a command or tactic to see a detailed view of its use.
Specification "mallq". Set witnesses on. Type form fm -> o. Define is_fm : o -> prop by ; is_fm (form (atom A)) ; is_fm (form (natom A)) ; is_fm (form (tens A B)) := is_fm (form A) /\ is_fm (form B) ; is_fm (form one) ; is_fm (form (par A B)) := is_fm (form A) /\ is_fm (form B) ; is_fm (form bot) ; is_fm (form (wth A B)) := is_fm (form A) /\ is_fm (form B) ; is_fm (form top) ; is_fm (form (plus A B)) := is_fm (form A) /\ is_fm (form B) ; is_fm (form zero) ; is_fm (form (all A)) := nabla x, is_fm (form (A x)) ; is_fm (form (exs A)) := nabla x, is_fm (form (A x)) . Theorem dual_is : forall A B, { dual A B } -> is_fm (form A) /\ is_fm (form B).induction on 1. intros. case H1. search. apply IH to *H2. apply IH to *H3. search. search. apply IH to *H2. apply IH to *H3. search. search. apply IH to *H2. search.%% FYI: Abella cannot infer the type of A Theorem is_fm_inst : forall (A : term -> o), nabla x, is_fm (A x) -> forall t, is_fm (A t).induction on 1. intros. case H1. search. search. apply IH to H2. apply H4 with t = t. apply IH to H3. apply H6 with t = t. search. search. apply IH to H2. apply H4 with t = t. apply IH to H3. apply H6 with t = t. search. search. apply IH to H2. apply H4 with t = t. apply IH to H3. apply H6 with t = t. search. search. apply IH to H2. apply H4 with t = t. apply IH to H3. apply H6 with t = t. search. search. apply IH to H2 with A = (X\ form (A1 X n2)). apply H3 with t = t. search. apply IH to H2 with A = (X\ form (A1 X n2)). apply H3 with t = t. search.% Theorem is_dual_inst : forall A B, % nabla (x : term), dual (A x) (B x) -> forall t, dual (A t) (B t). % induction on 1. intros. case H1. % search. % apply IH to H2. apply H4 with t = t. % apply IH to H3. apply H6 with t = t. search. % search. % apply IH to H2. apply H4 with t = t. % apply IH to H3. apply H6 with t = t. search. % search. % apply IH to H2 with A = (X\ A1 X n2), B = (X\ B1 X n2). % apply H3 with t = t. search. Import "../../lib/merge" with is_o := is_fm. [View ../../lib/merge] Theorem is_list_inst : forall (L : term -> olist), nabla x, is_list (L x) -> forall t, is_list (L t).induction on 1. intros. case H1. search. apply is_fm_inst to H2. apply H4 with t = t. apply IH to H3. apply H6 with t = t. search.Theorem adj_inst : forall K A L, nabla (x : term), adj (K x) (A x) (L x) -> forall t, adj (K t) (A t) (L t).induction on 1. intros. case H1. apply is_fm_inst to H2. apply H4 with t = t. apply is_list_inst to H3. apply H6 with t = t. search. apply is_fm_inst to H2. apply H4 with t = t. apply IH to H3. apply H6 with t = t. search.% Corollary: % adj J (A x) (K x) -> adj J (A t) (K t) Theorem merge_inst : forall J K L, nabla (x : term), merge (J x) (K x) (L x) -> forall t, merge (J t) (K t) (L t).induction on 1. intros. case H1. search. apply adj_inst to H2. apply *H5 with t = t. apply adj_inst to H3. apply *H7 with t = t. apply IH to H4. apply *H9 with t = t. search. apply adj_inst to H2. apply *H5 with t = t. apply adj_inst to H3. apply *H7 with t = t. apply IH to H4. apply *H9 with t = t. search.Define mall : olist -> prop by ; mall L := exists A, adj (form (natom A) :: nil) (form (atom A)) L ; mall L := exists A B LL JJ KK J K, adj LL (form (tens A B)) L /\ merge JJ KK LL /\ adj JJ (form A) J /\ mall J /\ adj KK (form B) K /\ mall K ; mall (form one :: nil) ; mall L := exists A B LL J K, adj LL (form (par A B)) L /\ adj LL (form A) J /\ adj J (form B) K /\ mall K ; mall L := exists LL, adj LL (form bot) L /\ mall LL ; mall L := exists A B LL J K, adj LL (form (wth A B)) L /\ adj LL (form A) J /\ mall J /\ adj LL (form B) K /\ mall K ; mall L := exists LL, adj LL (form top) L ; mall L := exists A B LL J, adj LL (form (plus A B)) L /\ adj LL (form A) J /\ mall J ; mall L := exists A B LL J, adj LL (form (plus A B)) L /\ adj LL (form B) J /\ mall J ; mall L := % Object-level exists is a meta-level exists exists x A LL J, adj LL (form (exs A)) L /\ adj LL (form (A x)) J /\ mall J ; mall L := % Object-level forall is meta-level nabla % x is free in J. exists A LL, adj LL (form (all A)) L /\ nabla x, exists J, adj LL (form (A x)) J /\ mall J . Theorem mall_inst : forall L, nabla (x : term), mall (L x) -> forall t, mall (L t).induction on 1. intros. case H1. apply adj_inst to *H2. apply *H3 with t = t. search. apply adj_inst to *H2. apply *H8 with t = t. apply merge_inst to *H3. apply *H10 with t = t. apply adj_inst to *H4. apply *H12 with t = t. apply IH to *H5. apply *H14 with t = t. apply adj_inst to *H6. apply *H16 with t = t. apply IH to H7. apply *H18 with t = t. search. search. apply adj_inst to *H2. apply *H6 with t = t. apply adj_inst to *H3. apply *H8 with t = t. apply adj_inst to *H4. apply *H10 with t = t. apply IH to H5. apply *H12 with t = t. search. apply adj_inst to *H2. apply *H4 with t = t. apply IH to *H3. apply *H6 with t = t. search. apply adj_inst to *H2. apply *H7 with t = t. apply adj_inst to *H3. apply *H9 with t = t. apply IH to *H4. apply *H11 with t = t. apply adj_inst to *H5. apply *H13 with t = t. apply IH to *H6. apply *H15 with t = t. search. apply adj_inst to *H2. apply *H3 with t = t. search. apply adj_inst to *H2. apply *H5 with t = t. apply adj_inst to *H3. apply *H7 with t = t. apply IH to *H4. apply *H9 with t = t. search. apply adj_inst to *H2. apply *H5 with t = t. apply adj_inst to *H3. apply *H7 with t = t. apply IH to *H4. apply *H9 with t = t. search. apply adj_inst to *H2. apply *H5 with t = t. apply adj_inst to *H3. apply *H7 with t = t. apply IH to *H4. apply *H9 with t = t. search. apply adj_inst to *H2. apply *H5 with t = t. apply adj_inst to *H3 with A = (X\ form (A X n2)). apply *H7 with t = t. apply IH to *H4 with L = (X\ J n2 X). apply *H9 with t = t. search.%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Theorem generalized_id : forall A B, { dual A B } -> mall ((form A) :: (form B) :: nil).induction on 1. intros. case H1. search. apply IH to H2. apply IH to H3. apply dual_is to H2. apply dual_is to H3. unfold 4. witness AA. witness BB. witness form (tens A1 B1) :: nil. witness form (tens A1 B1) :: form AA :: nil. witness form (tens A1 B1) :: form AA :: form BB :: nil. split. search. search. search. unfold 2. witness A1. witness B1. witness form AA :: form BB :: nil. witness form AA :: nil. witness form BB :: nil. witness form A1 :: form AA :: nil. witness form B1 :: form BB :: nil. search. search. apply IH to H2. apply IH to H3. apply dual_is to H2. apply dual_is to H3. search. search. apply IH to H2. apply dual_is to H2. search.%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Theorem mall_perm : forall K L, mall K -> perm K L -> mall L.induction on 1. intros. case H1. case H3. apply perm_cons_1 to *H2. apply perm_cons_1 to *H7. case H9. case H8. search. case H10. apply perm_cons_1 to *H2. apply adj_nil_1 to *H5. apply perm_cons_1 to *H7. apply adj_swap to *H8 *H6. apply perm_nil_1 to *H9. apply adj_nil_1 to *H10. unfold 1. search. apply adj_2_is_o to H5. apply adj_1_is_list to H5. apply adj_2_is_o to H7. apply adj_1_is_list to H7. assert perm J (form A :: JJ). apply perm_refl to H10. search. assert perm K1 (form B :: KK). apply perm_refl to H12. search. apply IH to *H6 *H13. apply IH to *H8 *H14. apply adj_perm_full to H2 H3. apply perm_merge_3 to *H4 *H18. unfold 2. search. case H2. case H3. apply perm_nil_1 to *H5. apply adj_nil_1 to *H4. search. case H7. apply adj_perm_full to *H2 *H3. assert perm J (form A :: KK). apply adj_1_is_list to H7. apply adj_2_is_o to H4. search. assert perm K1 (form B :: form A :: KK). apply adj_1_is_list to H7. apply adj_2_is_o to H4. apply adj_2_is_o to H5. search. apply IH to *H6 *H10. apply adj_1_is_list to H7. apply adj_2_is_o to H4. apply adj_2_is_o to H5. unfold 4. search. apply adj_perm_full to *H2 *H3. apply IH to *H4 *H6. unfold 5. search. apply adj_perm_full to *H2 *H3. assert perm J (form A :: KK). apply adj_1_is_list to H8. apply adj_2_is_o to H4. apply perm_refl to H10. search. assert perm K1 (form B :: KK). apply adj_1_is_list to H8. apply adj_2_is_o to H6. apply perm_refl to H11. search. apply IH to *H5 *H10. apply IH to *H7 *H11. apply adj_1_is_list to H8. apply adj_2_is_o to H8. case H15. unfold 6. search. apply adj_perm_full to *H2 *H3. unfold 7. search. apply adj_perm_full to *H2 *H3. assert perm J (form A :: KK). apply adj_1_is_list to H6. apply adj_2_is_o to H4. apply perm_refl to H8. search. apply IH to *H5 *H8. apply adj_1_is_list to H6. apply adj_2_is_o to H4. unfold 8. search. apply adj_perm_full to H2 H3. assert perm J (form B :: KK). apply adj_1_is_list to H6. apply adj_2_is_o to H4. apply perm_refl to H8. search. apply IH to H5 H8. apply adj_1_is_list to H6. apply adj_2_is_o to H4. unfold 9. search. apply adj_perm_full to H2 H3. assert perm J (form (A x) :: KK). apply adj_1_is_list to H6. apply adj_2_is_o to H4. apply perm_refl to H8. search. apply IH to H5 H8. apply adj_1_is_list to H6. apply adj_2_is_o to H4. unfold 10. search. apply adj_perm_full to H2 H3. assert perm (J n1) (form (A n1) :: KK). apply adj_1_is_list to H6. apply adj_2_is_o to H4. apply perm_refl to H8. search. apply IH to H5 H8. apply adj_1_is_list to H6. apply adj_2_is_o to H4. unfold 11. search.%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% Inversion theorems Theorem bot_inv : forall J L, mall L -> adj J (form bot) L -> mall J.induction on 1. intros. case H1. apply adj_same_result_diff to H2 H3. case H4. case H5. case H7. apply adj_same_result_diff to H2 H3. case H9. apply merge_unadj_3 to H4 H10. case H11. apply adj_swap to H12 H5. apply IH to *H6 H15. apply merge_unadj_1 to H4 H12. apply adj_swap to H17 H3. assert mall U1. apply adj_same_result to H20 H2. backchain mall_perm with K = U1. apply merge_unadj_2 to *H4 H12. apply adj_same_result to H14 H10. apply perm_merge_3 to *H15 *H16. apply adj_swap to H12 H7. apply IH to *H8 H19. apply adj_swap to H10 H3. assert mall U1. apply adj_same_result to H22 H2. backchain mall_perm with K = U1. case H2. case H4. apply adj_same_result_diff to H2 H3. case H7. apply adj_swap to H8 H4. apply adj_swap to H10 H5. apply IH to *H6 H12. apply adj_swap to H8 H3. assert mall U2. apply adj_same_result to H15 H2. backchain mall_perm with K = U2. apply adj_same_result to H3 H2. backchain mall_perm. apply adj_same_result_diff to H2 H3. case H8. apply adj_swap to H9 H4. apply IH to *H5 H11. apply adj_swap to H9 H6. apply IH to *H7 H14. apply adj_swap to H9 H3. apply adj_same_result to H17 H2. backchain mall_perm with K = U2. apply adj_same_result_diff to H2 H3. case H4. apply adj_swap to H5 H3. apply adj_same_result to H7 H2. backchain mall_perm with K = U. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to *H5 H9. apply adj_swap to *H7 *H3. apply adj_same_result to *H12 *H2. backchain mall_perm with K = U1. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to *H5 H9. apply adj_swap to *H7 *H3. apply adj_same_result to *H12 *H2. backchain mall_perm with K = U1. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to H5 H9. apply adj_swap to H7 H3. apply adj_same_result to H12 H2. backchain mall_perm with K = U1. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to H5 H9. apply adj_swap to H7 H3. apply adj_same_result to H12 H2. backchain mall_perm with K = U1.Theorem par_inv : forall L JJ A B, mall L -> adj JJ (form (par A B)) L -> exists KK LL, adj JJ (form A) KK /\ adj KK (form B) LL /\ mall LL.induction on 1. intros. case H1. apply adj_same_result_diff to H2 H3. case H4. case H5. case H7. apply adj_same_result_diff to H2 H3. case H9. apply merge_unadj_3 to *H4 H10. case H11. apply adj_swap to H12 *H5. apply IH to *H6 *H15. apply adj_swap to *H14 *H16. apply adj_swap to *H20 *H17. apply adj_1_is_list to H10. apply adj_2_is_o to H19. apply adj_2_is_o to H21. assert merge U2 KK (form A :: form B :: KK1). apply adj_2_is_o to H3. assert mall (form (tens A1 B1) :: form A :: form B :: KK1). apply adj_swap to *H10 *H3. apply adj_same_result to H30 H2. apply adj_perm_full to H31 H29. apply adj_1_is_list to *H2. assert perm (form (tens A1 B1) :: form A :: form B :: KK1) (form A :: form B :: JJ). apply mall_perm to *H28 *H35. assert adj JJ (form A) ((form A) :: JJ). assert adj (form A :: JJ) (form B) (form A :: form B :: JJ). search. %% symmetric case apply adj_swap to *H12 *H7. apply IH to *H8 *H15. apply adj_swap to *H14 *H16. apply adj_swap to *H20 *H17. apply adj_1_is_list to H10. apply adj_2_is_o to H19. apply adj_2_is_o to H21. assert merge JJ1 U2 (form A :: form B :: KK1). apply adj_2_is_o to H3. assert mall (form (tens A1 B1) :: form A :: form B :: KK1). apply adj_swap to *H10 *H3. apply adj_same_result to H30 H2. apply adj_perm_full to H31 H29. apply adj_1_is_list to *H2. assert perm (form (tens A1 B1) :: form A :: form B :: KK1) (form A :: form B :: JJ). apply mall_perm to *H28 *H35. assert adj JJ (form A) (form A :: JJ). assert adj (form A :: JJ) (form B) (form A :: form B :: JJ). search. case H2. case H4. apply adj_same_result_diff to H2 H3. apply adj_2_is_o to H4. apply adj_2_is_o to H5. apply adj_1_is_list to H2. case H7. assert perm (form A1 :: form B1 :: JJ) K. apply perm_sym to *H12. apply mall_perm to *H6 *H13. search. apply adj_swap to H11 *H4. apply adj_swap to *H13 *H5. apply IH to *H6 *H15. apply adj_swap to *H14 *H16. apply adj_swap to *H20 *H17. apply adj_swap to *H12 *H19. apply adj_swap to *H24 *H21. apply adj_1_is_list to H26. assert mall (form (par A1 B1) :: U5). apply adj_2_is_o to H23. apply adj_2_is_o to H25. assert perm (form (par A1 B1) :: U5) (form A :: form B :: JJ). unfold. witness (form B). witness form (par A1 B1) :: U4. witness form A :: JJ. split. search. search. unfold. witness (form A). witness form (par A1 B1) :: KK. witness JJ. split. search. search. apply adj_swap to *H11 *H3. apply adj_same_result to *H32 *H2. backchain perm_trans with K = U6. apply adj_1_is_list to H31. unfold. witness form (par A1 B1), KK, KK. split. search. search. backchain perm_refl. apply mall_perm to *H28 *H31. search. apply adj_same_result_diff to H2 H3. apply adj_2_is_o to H2. case H6. case H5. apply IH to *H4 H9. apply adj_3_is_list to H11. assert mall (form bot :: LL1). apply adj_1_is_list to H2. assert perm (form bot :: LL1) (form A :: form B :: JJ). unfold. witness form B. witness form bot :: KK1. witness form A :: JJ. split. search. search. unfold. witness form A. witness form bot :: KK. witness JJ. split. search. search. apply adj_swap to *H9 *H3. apply adj_same_result to *H17 H2. backchain perm_trans with K = U. apply adj_1_is_list to H16. apply perm_refl to H19. search. apply mall_perm to *H14 *H16. search. Ht : apply adj_2_is_o to H2. case Ht. Ht : apply adj_2_is_o to H3. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H13. apply adj_1_is_list to H14. apply adj_swap to H14 *H4. apply IH to *H5 *H17. apply adj_swap to H14 *H6. apply IH to *H7 *H22. apply perm_refl to H15. apply mall_perm to *H20 _ with L = (form A1 :: form A :: form B :: KK). apply mall_perm to *H25 _ with L = (form B1 :: form A :: form B :: KK). assert mall (form (wth A1 B1) :: form A :: form B :: KK). assert perm (form (wth A1 B1) :: form A :: form B :: KK) (form A :: form B :: JJ). unfold. witness form A, form (wth A1 B1) :: form B :: KK, form B :: JJ. split. search. search. unfold. witness form B, form (wth A1 B1) :: KK, JJ. split. search. search. apply adj_swap to *H14 *H3. apply adj_same_result to *H31 H2. backchain perm_trans with K = U2. apply mall_perm to *H29 *H30. search. Ht : apply adj_2_is_o to H2. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H7. apply adj_swap to *H8 *H3. apply adj_same_result to *H10 H2. apply adj_perm to *H11 *H9. apply adj_1_is_list to H12. apply perm_refl to H13. assert perm (form top :: form A :: form B :: KK1) (form A :: form B :: JJ). apply mall_perm to _ *H15. search. Ht : apply adj_2_is_o to H2. case Ht. Ht : apply adj_2_is_o to H3. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H11. apply adj_1_is_list to H12. apply adj_swap to H12 *H4. apply IH to *H5 *H15. apply perm_refl to H13. apply mall_perm to *H18 _ with L = (form A1 :: form A :: form B :: KK). assert mall (form (plus A1 B1) :: form A :: form B :: KK). assert perm (form (plus A1 B1) :: form A :: form B :: KK) (form A :: form B :: JJ). unfold. witness form A, form (plus A1 B1) :: form B :: KK, form B :: JJ. split. search. search. unfold. witness form B, form (plus A1 B1) :: KK, JJ. split. search. search. apply adj_swap to *H12 *H3. apply adj_same_result to *H23 H2. backchain perm_trans with K = U1. apply mall_perm to *H21 *H22. search. Ht : apply adj_2_is_o to H2. case Ht. Ht : apply adj_2_is_o to H3. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H11. apply adj_1_is_list to H12. apply adj_swap to H12 *H4. apply IH to *H5 *H15. apply perm_refl to H13. apply mall_perm to *H18 _ with L = (form B1 :: form A :: form B :: KK). assert mall (form (plus A1 B1) :: form A :: form B :: KK). assert perm (form (plus A1 B1) :: form A :: form B :: KK) (form A :: form B :: JJ). unfold. witness form A, form (plus A1 B1) :: form B :: KK, form B :: JJ. split. search. search. unfold. witness form B, form (plus A1 B1) :: KK, JJ. split. search. search. apply adj_swap to *H12 *H3. apply adj_same_result to *H23 H2. backchain perm_trans with K = U1. apply mall_perm to *H21 *H22. search. Ht : apply adj_2_is_o to H2. case Ht. apply adj_2_is_o to H3. apply adj_2_is_o to H4. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H11. apply adj_1_is_list to H12. apply adj_swap to H12 H4. apply IH to H5 H15. apply perm_refl to H13. apply mall_perm to H18 _ with L = (form (A1 x) :: form A :: form B :: KK). assert mall (form (exs A1) :: form A :: form B :: KK). assert perm (form (exs A1) :: form A :: form B :: KK) (form A :: form B :: JJ). unfold. witness form A, form (exs A1) :: form B :: KK, form B :: JJ. split. search. search. unfold. witness form B, form (exs A1) :: KK, JJ. split. search. search. apply adj_swap to *H12 *H3. apply adj_same_result to *H23 H2. backchain perm_trans with K = U1. apply mall_perm to *H21 *H22. search. Ht : apply adj_2_is_o to H2. case Ht. apply adj_2_is_o to H3. apply adj_2_is_o to H4. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H11. apply adj_1_is_list to H12. apply adj_swap to H12 H4. apply IH to H5 H15. apply perm_refl to H13. apply mall_perm to H18 _ with L = (form (A1 n1) :: form A :: form B :: KK). assert mall (form (all A1) :: form A :: form B :: KK). assert perm (form (all A1) :: form A :: form B :: KK) (form A :: form B :: JJ). unfold. witness form A, form (all A1) :: form B :: KK, form B :: JJ. split. search. search. unfold. witness form B, form (all A1) :: KK, JJ. split. search. search. apply adj_swap to *H12 *H3. apply adj_same_result to *H23 H2. backchain perm_trans with K = U1. apply mall_perm to *H21 *H22. search.Theorem wth_inv : forall L JJ A B, mall L -> adj JJ (form (wth A B)) L -> exists KK LL, adj JJ (form A) KK /\ mall KK /\ adj JJ (form B) LL /\ mall LL.induction on 1. intros. Ht : apply adj_2_is_o to H2. Hfm1 : case Ht. HJJ : apply adj_1_is_list to H2. case H1. apply adj_same_result_diff to H2 H3. case H4. case H5. case H7. rename A1 to C. rename B1 to D. Ht : apply adj_2_is_o to H3. Hfm1 : case Ht. apply adj_same_result_diff to H2 H3. case H9. apply merge_unadj_3 to H4 *H10. case H11. % with in left branch of tensor apply adj_swap to H12 H5. apply IH to *H6 *H15. apply adj_1_is_list to H14. apply perm_refl to H20. apply mall_perm to *H17 _ with L = (form C :: form A :: JJ2). apply mall_perm to *H19 _ with L = (form C :: form B :: JJ2). clear H14 H16 H18. apply merge_3_is_list to H13. assert mall (form (tens C D) :: form A :: KK1). assert mall (form (tens C D) :: form B :: KK1). apply merge_unadj_1 to H4 H12. apply adj_swap to H27 H3. apply adj_same_result to *H30 *H2. apply merge_perm_det to *H13 *H28. assert perm (form (tens C D) :: form A :: KK1) (form A :: JJ). unfold. witness form A, form (tens C D) :: KK1, JJ. split. search. search. backchain perm_trans with K = U1. apply mall_perm to *H25 *H33. assert perm (form (tens C D) :: form B :: KK1) (form B :: JJ). unfold. witness form B, form (tens C D) :: KK1, JJ. split. search. search. backchain perm_trans with K = U1. apply mall_perm to *H26 *H35. search. % with in left branch of tensor apply adj_swap to H12 H7. apply IH to *H8 *H15. apply adj_1_is_list to H14. apply perm_refl to H20. apply mall_perm to *H17 _ with L = (form D :: form A :: KK2). apply mall_perm to *H19 _ with L = (form D :: form B :: KK2). clear H14 H16 H18. apply merge_3_is_list to H13. assert merge JJ1 (form A :: KK2) (form A :: KK1). assert mall (form (tens C D) :: form A :: KK1). assert merge JJ1 (form B :: KK2) (form B :: KK1). assert mall (form (tens C D) :: form B :: KK1). apply merge_unadj_2 to H4 H12. apply adj_swap to H29 H3. apply adj_same_result to *H32 *H2. apply merge_perm_det to *H13 *H30. assert perm (form (tens C D) :: form A :: KK1) (form A :: JJ). unfold. witness form A, form (tens C D) :: KK1, JJ. split. search. search. backchain perm_trans with K = U1. apply mall_perm to *H26 *H35. assert perm (form (tens C D) :: form B :: KK1) (form B :: JJ). unfold. witness form B, form (tens C D) :: KK1, JJ. split. search. search. backchain perm_trans with K = U1. apply mall_perm to *H28 *H37. search. case H2. case H4. rename A1 to C. rename B1 to D. Ht : apply adj_2_is_o to H3. Hfm1 : case Ht. apply adj_same_result_diff to H2 H3. case H7. apply adj_swap to H8 *H4. apply adj_swap to *H10 *H5. apply IH to *H6 *H12. apply adj_1_is_list to H8. apply perm_refl to H17. apply mall_perm to *H14 _ with L = (form A :: form C :: form D :: KK). apply mall_perm to *H16 _ with L = (form B :: form C :: form D :: KK). assert mall (form A :: form (par C D) :: KK). clear H19. assert mall (form B :: form (par C D) :: KK). clear H20. apply adj_swap to H8 H3. apply adj_same_result to *H24 *H2. assert perm (form A :: form (par C D) :: KK) (form A :: JJ). unfold. witness form A, form (par C D) :: KK, JJ. split. search. search. backchain perm_trans with K = U2. apply mall_perm to *H21 *H26. assert perm (form B :: form (par C D) :: KK) (form B :: JJ). unfold. witness form B, form (par C D) :: KK, JJ. split. search. search. backchain perm_trans with K = U2. apply mall_perm to *H22 *H28. search. apply adj_same_result_diff to H2 H3. case H5. apply IH to *H4 H6. apply adj_1_is_list to H7. apply perm_refl to H11. apply mall_perm to *H8 _ with L = (form A :: KK). apply mall_perm to *H10 _ with L = (form B :: KK). apply adj_swap to H6 *H3. apply adj_same_result to *H16 *H2. assert perm (form A :: form bot :: KK) (form A :: JJ). unfold. witness form A, form bot :: KK, JJ. split. search. search. backchain perm_trans with K = U. apply mall_perm to _ *H18. clear H13. assert perm (form B :: form bot :: KK) (form B :: JJ). unfold. witness form B, form bot :: KK, JJ. split. search. search. backchain perm_trans with K = U. apply mall_perm to _ *H20. clear H14. search. rename A1 to C. rename B1 to D. Ht : apply adj_2_is_o to H3. Hfm1 : case Ht. apply adj_same_result_diff to H2 H3. case H8. % inverted formula is principal apply perm_1_is_list to H9. apply perm_refl to H10. apply perm_sym to *H9. apply mall_perm to *H5 _ with L = form C :: JJ. apply mall_perm to *H7 _ with L = form D :: JJ. search. % inverted formula is not principal apply adj_swap to H9 *H4. apply IH to *H5 *H11. apply adj_1_is_list to H9. apply perm_refl to H16. apply mall_perm to *H13 _ with L = (form C :: form A :: KK). apply mall_perm to *H15 _ with L = (form C :: form B :: KK). apply adj_swap to H9 *H6. apply IH to *H7 *H21. apply mall_perm to *H23 _ with L = (form D :: form A :: KK). apply mall_perm to *H25 _ with L = (form D :: form B :: KK). clear H10 H12 H14 H20 H22 H24. assert mall (form A :: form (wth C D) :: KK). assert mall (form B :: form (wth C D) :: KK). clear H18 H19 H26 H27. assert perm (form (wth C D) :: KK) JJ. apply adj_swap to *H9 *H3. apply adj_same_result to *H31 *H2. backchain perm_trans with K = U2. apply mall_perm to *H28 _ with L = form A :: JJ. apply mall_perm to *H29 _ with L = form B :: JJ. search. apply adj_same_result_diff to H2 H3. case H4. apply adj_swap to H5 H3. apply adj_same_result to *H7 *H2. apply adj_perm to *H8 *H6. search. rename A1 to C. rename B1 to D. Ht : apply adj_2_is_o to H3. Hfm1 : case Ht. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to *H5 *H9. apply adj_1_is_list to H7. apply perm_refl to H14. apply mall_perm to *H11 _ with L = (form A :: form C :: KK). apply mall_perm to *H13 _ with L = (form B :: form C :: KK). assert mall (form A :: form (plus C D) :: KK). clear H16. assert mall (form B :: form (plus C D) :: KK). clear H17. assert perm (form (plus C D) :: KK) JJ. apply adj_swap to *H7 *H3. apply adj_same_result to *H21 *H2. backchain perm_trans with K = U1. apply mall_perm to *H18 _ with L = form A :: JJ. apply mall_perm to *H19 _ with L = form B :: JJ. search. rename A1 to C. rename B1 to D. Ht : apply adj_2_is_o to H3. Hfm1 : case Ht. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to *H5 *H9. apply adj_1_is_list to H7. apply perm_refl to H14. apply mall_perm to *H11 _ with L = (form A :: form D :: KK). apply mall_perm to *H13 _ with L = (form B :: form D :: KK). assert mall (form A :: form (plus C D) :: KK). clear H16. assert mall (form B :: form (plus C D) :: KK). clear H17. assert perm (form (plus C D) :: KK) JJ. apply adj_swap to *H7 *H3. apply adj_same_result to *H21 *H2. backchain perm_trans with K = U1. apply mall_perm to *H18 _ with L = form A :: JJ. apply mall_perm to *H19 _ with L = form B :: JJ. search. rename A1 to C. Ht : apply adj_2_is_o to H3. Hfm1 : apply adj_2_is_o to H4. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to *H5 *H9. apply adj_1_is_list to H7. apply perm_refl to H14. apply mall_perm to *H11 _ with L = (form A :: form (C x) :: KK). apply mall_perm to *H13 _ with L = (form B :: form (C x) :: KK). assert mall (form A :: form (exs C) :: KK). clear H16. assert mall (form B :: form (exs C) :: KK). clear H17. assert perm (form (exs C) :: KK) JJ. apply adj_swap to *H7 *H3. apply adj_same_result to *H21 *H2. backchain perm_trans with K = U1. apply mall_perm to *H18 _ with L = form A :: JJ. apply mall_perm to *H19 _ with L = form B :: JJ. search. rename A1 to C. Ht : apply adj_2_is_o to H3. Hfm1 : apply adj_2_is_o to H4. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H4. apply IH to *H5 *H9. apply adj_1_is_list to H7. apply perm_refl to H14. apply mall_perm to *H11 _ with L = (form A :: form (C n1) :: KK). apply mall_perm to *H13 _ with L = (form B :: form (C n1) :: KK). assert mall (form A :: form (all C) :: KK). clear H16. assert mall (form B :: form (all C) :: KK). clear H17. assert perm (form (all C) :: KK) JJ. apply adj_swap to *H7 *H3. apply adj_same_result to *H21 *H2. backchain perm_trans with K = U1. apply mall_perm to *H18 _ with L = form A :: JJ. apply mall_perm to *H19 _ with L = form B :: JJ. search.Theorem all_inv : forall L JJ A, mall L -> adj JJ (form (all A)) L -> nabla x, exists J, adj JJ (form (A x)) J /\ mall J.induction on 1. intros. case H1. apply adj_same_result_diff to H2 H3. case H4. case H5. case H7. apply adj_same_result_diff to H2 H3. case H9. apply merge_unadj_3 to H4 H10. case H11. apply adj_swap to H12 H5. apply IH to H6 H15. apply adj_swap to H14 H16. apply adj_1_is_list to H10. apply adj_2_is_o to H16. assert merge (U1 n1) KK (form (A n1) :: KK1). apply adj_2_is_o to H3. assert mall (form (tens A1 B) :: form (A n1) :: KK1). apply adj_swap to H10 H3. apply adj_same_result to H26 H2. apply adj_perm_full to H27 H25. apply adj_1_is_list to H2. assert perm (form (tens A1 B) :: form (A n1) :: KK1) (form (A n1) :: JJ). apply mall_perm to H24 H31. search. apply adj_swap to H12 H7. apply IH to H8 H15. apply adj_swap to H14 H16. apply adj_1_is_list to H10. apply adj_2_is_o to H16. assert merge JJ1 (U1 n1) (form (A n1) :: KK1). apply adj_2_is_o to H3. assert mall (form (tens A1 B) :: form (A n1) :: KK1). apply adj_swap to H10 H3. apply adj_same_result to H26 H2. apply adj_perm_full to H27 H25. apply adj_1_is_list to H2. assert perm (form (tens A1 B) :: form (A n1) :: KK1) (form (A n1) :: JJ). apply mall_perm to H24 H31. search. case H2. case H4. apply adj_same_result_diff to H2 H3. case H7. apply adj_swap to H8 H4. apply adj_swap to H10 H5. apply IH to H6 H12. apply adj_swap to H11 H13. apply adj_swap to H9 H15. apply adj_1_is_list to H18. apply adj_2_is_o to H3. assert mall (form (par A1 B) :: U3 n1). apply adj_1_is_list to H2. apply adj_2_is_o to H13. assert perm (form (par A1 B) :: (U3 n1)) (form (A n1) :: JJ). unfold. witness (form (A n1)). witness form (par A1 B) :: KK. witness JJ. split. search. search. apply adj_swap to H8 H3. apply adj_same_result to H25 H2. backchain perm_trans with K = U4. apply adj_1_is_list to H24. unfold. witness form (par A1 B). witness KK. witness KK. split. search. search. backchain perm_refl. apply mall_perm to H21 H24. search. apply adj_same_result_diff to H2 H3. apply adj_2_is_o to H2. case H6. case H5. apply IH to H4 H8. apply adj_3_is_list to H9. assert mall (form bot :: (J n1)). apply adj_1_is_list to H2. assert perm (form bot :: (J n1)) (form (A n1) :: JJ). unfold. witness form (A n1). witness form bot :: KK. witness JJ. split. search. search. apply adj_swap to H8 H3. apply adj_same_result to H15 H2. backchain perm_trans with K = U. apply adj_1_is_list to H14. apply perm_refl to H17. search. apply mall_perm to H12 H14. search. Ht : apply adj_2_is_o to H2. case Ht. Ht : apply adj_2_is_o to H3. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H12. apply adj_1_is_list to H13. apply adj_swap to H13 H4. apply IH to H5 H16. apply adj_swap to H13 H6. apply IH to H7 H20. apply perm_refl to H14. apply mall_perm to H18 _ with L = (form A1 :: form (A n1) :: KK). apply mall_perm to H22 _ with L = (form B :: form (A n1) :: KK). assert mall (form (wth A1 B) :: form (A n1) :: KK). assert perm (form (wth A1 B) :: form (A n1) :: KK) (form (A n1) :: JJ). unfold. witness form (A n1). witness (form (wth A1 B) :: KK). witness JJ. split. search. search. apply adj_swap to H13 H3. apply adj_same_result to H28 H2. backchain perm_trans with K = U2. apply mall_perm to H26 H27. search. Ht : apply adj_2_is_o to H2. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H6. apply adj_swap to H7 H3. apply adj_same_result to H9 H2. apply adj_perm to H10 H8. apply adj_1_is_list to H11. apply perm_refl to H12. assert perm (form top :: form (A n1) :: KK1) (form (A n1) :: JJ). apply mall_perm to _ H14. search. Ht : apply adj_2_is_o to H2. case Ht. Ht : apply adj_2_is_o to H3. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H10. apply adj_1_is_list to H11. apply adj_swap to H11 H4. apply IH to H5 H14. apply perm_refl to H12. apply mall_perm to H16 _ with L = (form A1 :: form (A n1) :: KK). assert mall (form (plus A1 B) :: form (A n1) :: KK). assert perm (form (plus A1 B) :: form (A n1) :: KK) (form (A n1) :: JJ). unfold. witness form (A n1). witness (form (plus A1 B) :: KK). witness JJ. split. search. search. apply adj_swap to H11 H3. apply adj_same_result to H21 H2. backchain perm_trans with K = U1. apply mall_perm to H19 H20. search. Ht : apply adj_2_is_o to H2. case Ht. Ht : apply adj_2_is_o to H3. case Ht. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H10. apply adj_1_is_list to H11. apply adj_swap to H11 H4. apply IH to H5 H14. apply perm_refl to H12. apply mall_perm to H16 _ with L = (form B :: form (A n1) :: KK). assert mall (form (plus A1 B) :: form (A n1) :: KK). assert perm (form (plus A1 B) :: form (A n1) :: KK) (form (A n1) :: JJ). unfold. witness form (A n1). witness (form (plus A1 B) :: KK). witness JJ. split. search. search. apply adj_swap to H11 H3. apply adj_same_result to H21 H2. backchain perm_trans with K = U1. apply mall_perm to H19 H20. search. Ht : apply adj_2_is_o to H2. case Ht. apply adj_2_is_o to H3. apply adj_2_is_o to H4. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H10. apply adj_1_is_list to H11. apply adj_swap to H11 H4. apply IH to H5 H14. apply perm_refl to H12. apply mall_perm to H16 _ with L = (form (A1 x) :: form (A n1) :: KK). assert mall (form (exs A1) :: form (A n1) :: KK). assert perm (form (exs A1) :: form (A n1) :: KK) (form (A n1) :: JJ). unfold. witness form (A n1). witness form (exs A1) :: KK. witness JJ. split. search. search. apply adj_swap to H11 H3. apply adj_same_result to H21 H2. backchain perm_trans with K = U1. apply mall_perm to H19 H20. search. Ht : apply adj_2_is_o to H2. case Ht. apply adj_2_is_o to H3. apply adj_2_is_o to H4. apply adj_1_is_list to H2. apply adj_same_result_diff to H2 H3. case H10. apply perm_sym to H11. apply adj_perm_source to H12 H4. apply mall_perm to H5 H14. search. apply adj_1_is_list to H11. apply adj_swap to H11 H4. apply IH to H5 H14. apply perm_refl to H12. apply mall_perm to H16 _ with L = (form (A1 n1) :: form (A n2) :: KK). assert mall (form (all A1) :: form (A n2) :: KK). assert perm (form (all A1) :: form (A n2) :: KK) (form (A n2) :: JJ). unfold. witness form (A n2). witness form (all A1) :: KK. witness JJ. split. search. search. apply adj_swap to H11 H3. apply adj_same_result to H21 H2. backchain perm_trans with K = U1. apply mall_perm to H19 H20. search.%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Theorem mall_cut : forall A B JJ J KK K LL, { dual A B } -> adj JJ (form A) J -> mall J -> adj KK (form B) K -> mall K -> merge JJ KK LL -> mall LL.induction on 1. induction on 3. intros. case H3. %% identity apply adj_same_result_diff to H2 H7. case H8. %% Cut formula principal case H1. case H9. case H11. apply adj_same_result to H2 H7. case H15. case H12. case H10. apply merge_move_12 to _ H4 H6. apply merge_nil_perm to H21. backchain mall_perm. case H20. case H14. %% Cut formula is not principal -- impossible case H9. case H1. case H11. %% tensor apply adj_same_result_diff to H2 H7. case H13. %% cut formula is the tensor -- rank decreases case H1. apply par_inv to H5 H4. apply adj_1_is_list to H18. apply adj_1_is_list to H11. apply merge_exists to *H21 *H20. apply IH to H16 H11 H12 H18 H19 H22. apply merge_unadj_2 to H22 H17. apply adj_1_is_list to H24. apply adj_1_is_list to H9. apply merge_exists to *H27 *H26. apply IH to H15 H9 H10 H24 H23 H28. apply perm_sym to *H14. apply perm_merge_3 to *H8 *H30. apply merge_assoc to *H31 *H25 *H28 *H6. backchain mall_perm with K = L1. %% cut formula is some other formula -- height decreases apply merge_unadj_3 to H8 H14. case H15. %% cut formula goes to left operand apply adj_swap to H16 H9. apply add_to_merge_left to H18 H17. rename M to UKK1. Ht : assert 0 exists UKK, merge U KK UKK. apply adj_1_is_list to H19. apply adj_1_is_list to H4. apply merge_exists to H22 H23. search. case Ht. Hi : apply IH1 to H1 H19 H10 H4 H5 H22. apply merge_unadj_1 to H22 H18. Ht : assert 0 exists V, merge LL2 KK1 V. apply adj_1_is_list to H23. apply adj_1_is_list to H11. apply merge_exists to H25 H26. search. case Ht. Ht : assert 0 exists VT, adj V (form (tens A1 B1)) VT. apply merge_3_is_list to H25. apply adj_2_is_o to H7. apply adj_exists to H27 H26. search. case Ht. assert mall VT. apply adj_swap to H14 H7. apply adj_same_result to H2 *H29. apply perm_merge_1 to *H6 *H30. apply merge_unadj_1 to H31 H28. assert 0 perm VT LL. unfold. witness form (tens A1 B1). witness V. witness LL3. split. search. search. assert merge KK1 JJ2 KK2. backchain merge_sym. assert merge KK1 LL2 V. backchain merge_sym. backchain merge_assoc with J = KK1, K = JJ2, L = KK, JK = KK2, KL = LL2. backchain mall_perm with K = VT. %% cut formula goes to the right operand apply adj_swap to H16 H11. apply add_to_merge_right to H18 H17. rename M to UJJ1. Ht : assert 0 exists UKK, merge U KK UKK. apply adj_1_is_list to H19. apply adj_1_is_list to H4. apply merge_exists to H22 H23. search. case Ht. Hi : apply IH1 to H1 H19 H12 H4 H5 H22. apply merge_unadj_1 to H22 H18. Ht : assert 0 exists V, merge JJ1 LL2 V. apply adj_1_is_list to H9. apply adj_1_is_list to H23. apply merge_exists to H25 H26. search. case Ht. Ht : assert 0 exists VT, adj V (form (tens A1 B1)) VT. apply merge_3_is_list to H25. apply adj_2_is_o to H7. apply adj_exists to H27 H26. search. case Ht. assert mall VT. apply adj_swap to H14 H7. apply adj_same_result to H2 *H29. apply perm_merge_1 to *H6 *H30. apply merge_unadj_1 to H31 H28. assert 0 perm VT LL. unfold. witness form (tens A1 B1). witness V. witness LL3. split. search. search. backchain merge_assoc with J = JJ1, K = KK3, L = KK, JK = KK2, KL = LL2. backchain mall_perm with K = VT. %% one case H2. case H1. apply merge_nil_perm to H6. apply bot_inv to H5 H4. backchain mall_perm with K = KK. case H8. %% par apply adj_same_result_diff to H2 H7. case H11. %% left cut formula cannot be a par because it is positive case H1. %% cut formula goes up in left premise apply adj_swap to H12 *H8. apply adj_swap to *H14 *H9. Ht : assert 0 exists V, merge U1 KK V. apply adj_1_is_list to H16. apply adj_1_is_list to H4. apply merge_exists to H17 H18. search. case Ht. Hi : apply IH1 to H1 H16 H10 H4 H5 H17. apply merge_unadj_1 to *H17 *H15. apply merge_unadj_1 to *H19 *H13. Ht : assert 0 exists VV, adj LL3 (form (par A1 B1)) VV. apply adj_1_is_list to H20. apply adj_2_is_o to H7. apply adj_exists to H23 H22. search. case Ht. assert mall VV. assert 0 perm VV LL. apply adj_swap to *H12 *H7. apply adj_same_result to *H2 *H25. apply perm_merge_1 to *H6 *H26. apply merge_unadj_1 to H27 H24. unfold. witness form (par A1 B1). witness LL3. witness LL4. split. search. search. backchain merge_perm_det. backchain mall_perm with K = VV. %% bot apply adj_same_result_diff to H2 H7. case H9. %% left cut formula cannot be bot because it is positive. case H1. %% cut formula goes up in left premise Ht : assert 0 exists V, merge KK1 KK V. apply adj_1_is_list to H10. apply adj_1_is_list to H4. apply merge_exists to H11 H12. search. case Ht. Hi : apply IH1 to H1 H10 H8 H4 H5 H11. Ht : assert 0 exists VV, adj V (form bot) VV. apply merge_3_is_list to H11. apply adj_exists to _ H12 with A = form bot. search. case Ht. assert mall VV. assert 0 perm VV LL. apply adj_swap to *H10 *H7. apply adj_same_result to *H2 *H15. apply perm_merge_1 to *H6 *H16. apply merge_unadj_1 to H17 H14. unfold. witness form bot. witness V. witness LL2. split. search. search. backchain merge_perm_det. backchain mall_perm with K = VV. %% with apply adj_same_result_diff to H2 H7. case H12. %% left cut formula cannot be with case H1. %% cut formula goes up in left premise Ht : apply adj_2_is_o to H7. Hfm1 : case Ht. Hfm1 : apply adj_2_is_o to H2. Hfm1 : apply adj_2_is_o to H4. apply adj_1_is_list to H13. apply adj_1_is_list to H4. Ht : assert 0 exists V, merge KK1 KK V. apply merge_exists to H14 H15. search. case Ht. apply merge_3_is_list to H16. apply perm_refl to H17. assert 0 mall (form (wth A1 B1) :: V). apply adj_swap to H13 *H8. apply IH1 to H1 H20 *H9 H4 H5 _ with LL = form A1 :: V. apply adj_swap to H13 *H10. apply IH1 to H1 H23 *H11 H4 H5 _ with LL = form B1 :: V. search. assert perm (form (wth A1 B1) :: V) LL. apply adj_swap to H13 H7. apply adj_same_result to *H2 *H21. apply perm_merge_1 to *H6 *H22. apply merge_unadj_1 to H23 H20. unfold. witness form (wth A1 B1), V, LL2. split. search. search. backchain merge_perm_det. backchain mall_perm with K = form (wth A1 B1) :: V. %% top apply adj_same_result_diff to H2 H7. case H8. case H1. apply adj_swap to H9 H7. apply adj_same_result to H2 H11. apply perm_merge_1 to *H6 H12. apply merge_unadj_1 to *H13 *H10. search. %% plus_1 apply adj_same_result_diff to H2 H7. case H10. %% cut formula is A1 + B1 case H1. apply wth_inv to *H5 *H4. apply perm_merge_1 to *H6 *H11. backchain IH. %% left cut formula moves up apply adj_1_is_list to H11. apply adj_1_is_list to H4. Ht : assert 0 exists V, merge KK1 KK V. apply merge_exists to H12 H13. search. case Ht. apply merge_3_is_list to H14. apply perm_refl to H15. Ht : apply adj_2_is_o to H7. Hfm1 : case Ht. assert 0 mall (form (plus A1 B1) :: V). apply adj_swap to H11 *H8. apply IH1 to H1 H18 *H9 H4 H5 _ with LL = form A1 :: V. search. assert perm (form (plus A1 B1) :: V) LL. apply adj_swap to H11 H7. apply adj_same_result to *H2 *H19. apply perm_merge_1 to *H6 *H20. apply merge_unadj_1 to H21 H18. unfold. witness form (plus A1 B1), V, LL2. split. search. search. backchain merge_perm_det. backchain mall_perm with K = form (plus A1 B1) :: V. %% plus_2 apply adj_same_result_diff to H2 H7. case H10. %% cut formula is A1 + B1 case H1. apply wth_inv to *H5 *H4. apply perm_merge_1 to *H6 *H11. backchain IH with A = B1, B = BB. %% left cut formula moves up apply adj_1_is_list to H11. apply adj_1_is_list to H4. Ht : assert 0 exists V, merge KK1 KK V. apply merge_exists to H12 H13. search. case Ht. apply merge_3_is_list to H14. apply perm_refl to H15. Ht : apply adj_2_is_o to H7. Hfm1 : case Ht. assert 0 mall (form (plus A1 B1) :: V). apply adj_swap to H11 *H8. apply IH1 to H1 H18 *H9 H4 H5 _ with LL = form B1 :: V. search. assert perm (form (plus A1 B1) :: V) LL. apply adj_swap to H11 H7. apply adj_same_result to *H2 *H19. apply perm_merge_1 to *H6 *H20. apply merge_unadj_1 to H21 H18. unfold. witness form (plus A1 B1), V, LL2. split. search. search. backchain merge_perm_det. backchain mall_perm with K = form (plus A1 B1) :: V. %% exists apply adj_same_result_diff to H2 H7. case H10. %% cut formula is exs A1 case H1. apply all_inv to H5 H4. apply perm_merge_1 to H6 H11. inst H12 with n1 = x. %% THIS IS THE TRICK :) apply adj_inst to H13. apply *H17 with t = x. apply mall_inst to H14. apply *H19 with t = x. backchain IH with A = A1 x, B = B1 x. %% cut moves up the left branch apply adj_1_is_list to H11. apply adj_1_is_list to H4. Ht : assert 0 exists V, merge KK1 KK V. apply merge_exists to H12 H13. search. case Ht. apply merge_3_is_list to H14. apply perm_refl to H15. Ht : apply adj_2_is_o to H7. Hfm1 : case Ht. Hfm2 : apply is_fm_inst to Hfm1. Hfmx : apply *Hfm2 with t = x. assert 0 mall (form (exs A1) :: V). apply adj_swap to H11 H8. apply IH1 to H1 H18 H9 H4 H5 _ with LL = form (A1 x) :: V. search. assert perm (form (exs A1) :: V) LL. apply adj_swap to H11 H7. apply adj_same_result to *H2 *H19. apply perm_merge_1 to *H6 *H20. apply merge_unadj_1 to H21 H18. unfold. witness form (exs A1), V, LL2. split. search. search. backchain merge_perm_det. backchain mall_perm with K = form (exs A1) :: V. %% forall apply adj_same_result_diff to H2 H7. case H10. % left cut-formula cannot be forall case H1. % cut moves up the left branch apply adj_1_is_list to H11. apply adj_1_is_list to H4. Ht : assert 0 exists V, merge KK1 KK V. apply merge_exists to H12 H13. search. case Ht. apply merge_3_is_list to H14. apply perm_refl to H15. Ht : apply adj_2_is_o to H7. Hfm1 : case Ht. assert 0 mall (form (all A1) :: V). apply adj_swap to H11 H8. apply IH1 to H1 H18 H9 H4 H5 _ with LL = form (A1 n1) :: V. search. assert perm (form (all A1) :: V) LL. apply adj_swap to H11 H7. apply adj_same_result to *H2 *H19. apply perm_merge_1 to *H6 *H20. apply merge_unadj_1 to H21 H18. unfold. witness form (all A1), V, LL2. split. search. search. backchain merge_perm_det. backchain mall_perm with K = form (all A1) :: V.