22-words-theorems.mm1

import "13-fixedpoints.mm1";
import "21-words-helpers.mm1";

--- Lift axioms to higher level constructs
------------------------------------------

theorem def_a: $|^ a ^|$ =
  (named @ func_subst_thm 'functional_a 'x 'definedness);
theorem def_b: $|^ b ^|$ =
  (named @ func_subst_thm 'functional_b 'x 'definedness);

theorem a_in_top_letter: $|^ a /\ top_letter ^|$ =
  '(framing_def (iand id orl) def_a);
theorem b_in_top_letter: $|^ b /\ top_letter ^|$ =
  '(framing_def (iand id orr) def_b);

--- Lift functional axioms to $ a . [] $ and $ b . [] $.
theorem functional_l_concat {.w x y v: EVar} (l: Pattern v)
  (func_l: $ exists x (eVar x == l) $):
  $ exists y (eVar y == l . eVar v) $ =
  (func_subst_thm 'func_l 'w 'functional_concat);
theorem functional_a_concat {.w x v: EVar} :
  $ exists x (eVar x == a . eVar v) $ =
  (named '(functional_l_concat functional_a));
theorem functional_b_concat {.w x v: EVar} :
  $ exists x (eVar x == b . eVar v) $ =
  (named '(functional_l_concat functional_b));

theorem regex_eq_ewp_ab
  (h: $ letter -> top_letter $):
  $ epsilon /\ letter <-> bot $
  = '(ibii
    (exists_generalization_disjoint
      (com12
        (eq_to_imp (eq_to_def @ eq_to_and_l eq_to_intro) (eq_to_not @ eq_to_and_l eq_to_intro))
        (con2 (dne @ singleton_norm (! appCtxVar box1) (! defNorm box2))) -- |^ x /\ ~a ^| <-> ~(x /\ a)
      ) (exists_framing eq_sym (! functional_epsilon x))
      (framing_def (con3 @ imim2i @ syl h dne) @ dne no_confusion_ae_e))
    absurdum);

theorem no_confusion_cc_e_epsilon {u x y: EVar} : $(x in top_letter) -> (y in top_letter)
                            -> (eVar x . eVar u == eVar y) -> (eVar x == eVar y) /\ (eVar u == epsilon)$ =
  '(syl (imim2i @ imim1i @ com12 eq_trans @ eq_sym identity_right_e)
    ,(func_subst 'v $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y . eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$ 'no_confusion_cc_e '(! functional_epsilon w))
  );

theorem assoc_concat (Alpha Beta Gamma: Pattern): $ ((Alpha . Beta) . Gamma) <-> (Alpha . (Beta . Gamma)) $ =
  (named '(
    --- Alpha
    norm (norm_equiv appctx_concat_l_l appctx_concat_l) @
    bitr appCtx_pointwise @ bitr2 appCtx_pointwise @ bicom @
    cong_of_equiv_exists @ cong_of_equiv_and_l @
    norm (norm_sym @ norm_equiv appctx_concat_l_l appctx_concat_l) @
    --- Beta
    norm (norm_equiv appctx_concat_l_r appctx_concat_r_l) @
    bitr appCtx_pointwise @ bitr2 appCtx_pointwise @ bicom @
    cong_of_equiv_exists @ cong_of_equiv_and_l @
    norm (norm_sym @ norm_equiv appctx_concat_l_r appctx_concat_r_l) @
    --- Gamma
    norm (norm_equiv appctx_concat_r appctx_concat_r_r) @
    bitr appCtx_pointwise @ bitr2 appCtx_pointwise @ bicom @
    cong_of_equiv_exists @ cong_of_equiv_and_l @
    norm (norm_sym @ norm_equiv appctx_concat_r appctx_concat_r_r) @
    --- associativity axiom on eVars
    eq_to_intro_bi assoc_concat_e
  ));

theorem id_concat_l: $ epsilon . Alpha <-> Alpha $ =
  (named '(
    norm (norm_equiv appctx_concat_r appCtxVar) @
    bitr appCtx_pointwise @ bitr2 appCtx_pointwise @ bicom @
    cong_of_equiv_exists @ cong_of_equiv_and_l @
    norm (norm_sym @ norm_equiv appctx_concat_r appCtxVar) @
    eq_to_intro_bi identity_left_e
  ));

theorem id_concat_r: $ Alpha . epsilon <-> Alpha $ =
  (named '(
    norm (norm_equiv appctx_concat_l appCtxVar) @
    bitr appCtx_pointwise @ bitr2 appCtx_pointwise @ bicom @
    cong_of_equiv_exists @ cong_of_equiv_and_l @
    norm (norm_sym @ norm_equiv appctx_concat_l appCtxVar) @
    eq_to_intro_bi identity_right_e
  ));

theorem regex_eq_eps_concat_l: $ epsilon . Alpha <-> Alpha $ = 'id_concat_l;
theorem regex_eq_eps_concat_r: $ Alpha . epsilon <-> Alpha $ = 'id_concat_r;

--- Useful Theorems
-------------------

theorem concat_subset:
$ (phi1 C= psi1) -> (phi2 C= psi2) -> (phi1 . phi2 C= psi1 . psi2) $ =
  (named '(Fprop
    ,(subset_imp_subset_framing_subst 'appCtxLRVar)
    ,(subset_imp_subset_framing_subst 'appCtxRVar)
    subset_trans));

theorem epsilon_and_concat: $ ((epsilon /\ phi) . psi) <-> |^ epsilon /\ phi ^| /\ psi $ =
  (named '(membership_elim_implicit @ mp (anr ,(propag_mem 'x $((epsilon /\ phi) . psi) <-> |^ epsilon /\ phi ^| /\ psi$)) @
    bitr (cong_of_equiv_exists @ cong_of_equiv_and_r @ bicom membership_app) @ ibii
      (exists_generalization_disjoint @ rsyl (anl anass) @ rsyl (curry @ syl anl
        ,(func_subst_explicit_helper 'x $x in phi /\ z in (eVar x . psi)$)) @
        anim2 @ framing_in @ anl id_concat_l)
      (exists_generalization (eFresh_imp eFresh_disjoint eFresh_exists_same_var) (
          exp @ syl exists_intro_same_var @ syl (anr anass) @ iand anl @ syl (curry @ syl anr
            ,(func_subst_explicit_helper 'x $x in phi /\ z in (eVar x . psi)$)) @
            anim2 @ anim2 @ framing_in @ anr id_concat_l) functional_epsilon)));

theorem kleene_l_monotone {X : SVar} (phi: Pattern X)
  (X_fresh: $ _sFresh X phi $):
  $ phi -> kleene_l X phi $ =
  (named '(syl (anr @ unfold_kleene_l X_fresh) @ orrd @ syl
    (framing_concat_l @ anr @ unfold_kleene_l X_fresh) @
    rsyl (anr regex_eq_eps_concat_l) @ rsyl orl @ anr ,(or_appCtx_subst 'appctx_concat_l)));
theorem kleene_monotone {X : SVar} (phi: Pattern X)
  (X_fresh: $ _sFresh X phi $):
  $ phi -> kleene X phi $ =
  (named '(syl (anr @ unfold_kleene X_fresh) @ orrd @ syl
    (framing_concat_r @ anr @ unfold_kleene X_fresh) @
    rsyl (anr regex_eq_eps_concat_r) @ rsyl orl @ anr ,(or_appCtx_subst 'appctx_concat_r)));

theorem epsilon_in_concat_eVar {x: EVar} (phi: Pattern x):
  $ |^ epsilon /\ (eVar x . phi) ^| -> (eVar x == epsilon) $ =
  (named '(rsyl (anl ,(func_subst_eps 'x 'membership_app)) @ rsyl (exists_framing @ anim2
      @ rsyl ,(func_subst 't $(t in (eVar y . eVar z)) -> (eVar t == (eVar y . eVar z))$ (func_subst_concat 'y 'membership_var_forward) 'functional_epsilon)
      no_confusion_ec_e)
    @ rsyl (exists_framing @ anl anlass)
    @ rsyl and_exists_disjoint_forwards
    @ rsyl anl
    eq_sym));

--- Proving the Empty Word Property
-----------------------------------

theorem epsilon_implies_top :
  $ epsilon -> top $
= '(con2 absurdum);

theorem epsilon_implies_kleene {X: SVar} (phi: Pattern X)
  (h: $ _Positive X phi $):
  $ epsilon -> kleene X phi $ =
  '(rsyl orl (norm (norm_imp_l
    ,(propag_s_subst 'X $epsilon \/ phi . sVar X$)
    ) @ pre_fixpoint @ positive_in_kleene_r_body h));

theorem epsilon_implies_concat (phi psi : Pattern)
    (h1: $epsilon -> phi$)
    (h2: $epsilon -> psi$)
  : $epsilon -> (phi . psi)$
= '( rsyl (bi1i @ bicom id_concat_r)
   @ rsyl (framing_concat_l h1)
   @ rsyl (framing_concat_r h2)
     id);

theorem epsilon_implies_not_letter (letter : Pattern)
    (h: $letter -> top_letter$)
  : $epsilon -> ~ letter$
= '(exp (bi1i @ regex_eq_ewp_ab h))
  ;

theorem epsilon_implies_not_and_l (phi psi : Pattern)
    (h: $epsilon -> ~ phi$)
  : $epsilon -> ~ (phi /\ psi)$
= '(rsyl (orld h) (bi1i @ bicom notan));
theorem  epsilon_implies_not_and_r (phi psi : Pattern)
    (h: $epsilon -> ~ psi$)
  : $epsilon -> ~ (phi /\ psi)$
= '(rsyl (orrd h) (bi1i @ bicom notan));

theorem epsilon_implies_not_or (phi psi : Pattern)
    (h1: $epsilon -> ~ phi$)
    (h2: $epsilon -> ~ psi$)
  : $epsilon -> ~ (phi \/ psi)$
= '(rsyl (iand h1 h2) (bi1i @ bicom notor));


theorem regex_eq_ewp_bot:
  $ (epsilon /\ bot) <-> bot $ = '(ibii anr absurdum);
theorem regex_eq_ewp_epsilon:
  $ epsilon /\ epsilon <-> epsilon $ = 'anidm;
theorem regex_eq_ewp_a:
  $ epsilon /\ a <-> bot $ = '(regex_eq_ewp_ab orl);
theorem regex_eq_ewp_b:
  $ epsilon /\ b <-> bot $ = '(regex_eq_ewp_ab orr);
theorem regex_eq_ewp_and:
  $ epsilon /\ (Alpha /\ Beta) <-> (epsilon /\ Alpha) /\ (epsilon /\ Beta) $ = 'anandi;
theorem regex_eq_ewp_choice:
  $ epsilon /\ (Alpha \/ Beta) <-> (epsilon /\ Alpha) \/ (epsilon /\ Beta) $ = 'andi;
theorem regex_eq_ewp_kleene {X: SVar} (Alpha: Pattern X)
  (h: $ _Positive X Alpha $):
  $ epsilon /\ (kleene X Alpha) <-> epsilon $ =
  '(ibii anl @ iand id @ epsilon_implies_kleene h);

theorem regex_eq_ewp_not_bot: $ (epsilon /\ ~bot) <-> epsilon $ =
  '(ibii anl @ syl ancom top_and);
theorem regex_eq_ewp_not_eps: $ (epsilon /\ ~epsilon) <-> bot $ =
  '(ibii (notnot1 notnot1) absurdum);
theorem regex_eq_ewp_not_a: $ (epsilon /\ ~a) <-> epsilon $ =
  '(ibii anl @ iand id @ dne @ anl regex_eq_ewp_a);
theorem regex_eq_ewp_not_b: $ (epsilon /\ ~b) <-> epsilon $ =
  '(ibii anl @ iand id @ dne @ anl regex_eq_ewp_b);
theorem regex_eq_ewp_not_and: $ (epsilon /\ ~(Alpha /\ Beta)) <-> ((epsilon /\ ~ Alpha) \/ (epsilon /\ ~ Beta)) $ =
  '(bitr (cong_of_equiv_and_r notan) andi);
theorem regex_eq_ewp_not_choice: $ (epsilon /\ ~(Alpha \/ Beta)) <-> ((epsilon /\ ~ Alpha) /\ (epsilon /\ ~ Beta)) $ =
  '(bitr (cong_of_equiv_and_r not_distr_or) and_distr);
theorem regex_eq_ewp_not_kleene {X: SVar} (Alpha: Pattern X)
  (h: $ _Positive X Alpha $):
  $ (epsilon /\ ~(kleene X Alpha)) <-> bot $ =
  '(ibii (notnot1 @ syl notnot1 @ epsilon_implies_kleene h) absurdum);
theorem regex_eq_ewp_not_not: $ (epsilon /\ ~(~ Alpha)) <-> (epsilon /\ Alpha) $ =
  '(cong_of_equiv_and_r @ bicom notnot);

--- EWP related simplifications
theorem regex_eq_ewp_concat (Alpha Beta: Pattern):
  $ epsilon /\ (Alpha . Beta) <-> (epsilon /\ Alpha) /\ (epsilon /\ Beta) $ =
  (named '(membership_elim_implicit @ mp (anr
      ,(propag_mem 'x $epsilon /\ (Alpha . Beta) <-> (epsilon /\ Alpha) /\ (epsilon /\ Beta)$)
    ) @ ibii
      (curry @ mp
        ,(func_subst_imp_to_var 'x $(exists y (y in Alpha /\ exists z (z in Beta /\ x in (eVar y . eVar z)))) -> ((eVar x == epsilon) /\ (x in Alpha)) /\ ((eVar x == epsilon) /\ (x in Beta))$)
        @ rsyl (exists_framing @ anim2 @ syl (anim2 @ anr ,(func_subst_eps 'x 'membership_expand)) @ syl and_exists_disjoint_forwards @ exists_framing @ syl (anl anlass) @ anim2 @
            rsyl (anl ,(membership_var_func_subst 'functional_epsilon 'functional_concat)) no_confusion_ec_e)
        @ rsyl (exists_framing @ anr anass)
        @ rsyl (anl and_exists_disjoint_r)
        @ rsyl (anim1 @ anr ,(func_subst_eps 'x 'membership_expand))
        @ anim (iand (a1i eq_refl) id) (iand (a1i eq_refl) id))
      (rsyl (anl anass) @ curry @ mp
        ,(func_subst_imp_to_var 'x $(x in Alpha) /\ ((eVar x == epsilon) /\ (x in Beta)) -> (eVar x == epsilon) /\ (exists y (y in Alpha /\ exists z (z in Beta /\ x in (eVar y . eVar z))))$)
        @ rsyl (anim2 anr)
        @ iand (a1i eq_refl)
        @ syl (anl ,(func_subst_eps 'x 'membership_app2))
        @ rsyl (anim ,(func_subst_eps 'x 'eVar_in_subset_forward) ,(func_subst_eps 'x 'eVar_in_subset_forward))
        @ rsyl (curry concat_subset)
        @ rsyl (framing_subset (anr id_concat_l) id)
        ,(func_subst_eps 'x 'eVar_in_subset_reverse))));
theorem regex_eq_ewp_not_concat (Alpha Beta: Pattern):
  $ (epsilon /\ ~(Alpha . Beta)) <-> ((epsilon /\ ~ Alpha) \/ (epsilon /\ ~ Beta)) $ =
  (named '(membership_elim_implicit @ mp (anr
      ,(propag_mem 'x $epsilon /\ ~(Alpha . Beta) <-> (epsilon /\ ~ Alpha) \/ (epsilon /\ ~ Beta)$)
    ) @ ibii
      (curry @ mp
        ,(func_subst_imp_to_var 'x $(~ (exists y (y in Alpha /\ exists z (z in Beta /\ x in (eVar y . eVar z))))) -> ((eVar x == epsilon) /\ (~ (x in Alpha))) \/ ((eVar x == epsilon) /\ (~ (x in Beta)))$)
        @ con1
        @ rsyl (anl notor)
        @ rsyl (anim
          (rsyl (anl notan) @ eori (syl absurdum @ notnot1 eq_refl) dne)
          (rsyl (anl notan) @ eori (syl absurdum @ notnot1 eq_refl) dne))
        @ syl (anl ,(func_subst_eps 'x 'membership_app2))
        @ rsyl (anim ,(func_subst_eps 'x 'eVar_in_subset_forward) ,(func_subst_eps 'x 'eVar_in_subset_forward))
        @ rsyl (curry concat_subset)
        @ rsyl (framing_subset (anr id_concat_l) id)
        ,(func_subst_eps 'x 'eVar_in_subset_reverse))
      (rsyl (anr andi) @ curry @ mp
        ,(func_subst_imp_to_var 'x $(~ (x in Alpha)) \/ (~ (x in Beta)) -> (eVar x == epsilon) /\ ~(exists y (y in Alpha /\ exists z (z in Beta /\ x in (eVar y . eVar z))))$)
        @ rsyl (anr notan)
        @ con1
        @ rsyl (anl notan)
        @ eori (syl absurdum @ notnot1 eq_refl)
        @ rsyl dne
        @ rsyl (exists_framing @ anim2 @ syl (anim2 @ anr ,(func_subst_eps 'x 'membership_expand)) @ syl and_exists_disjoint_forwards @ exists_framing @ syl (anl anlass) @ anim2 @
            rsyl (anl ,(membership_var_func_subst 'functional_epsilon 'functional_concat)) no_confusion_ec_e)
        @ rsyl (exists_framing @ anr anass)
        @ rsyl (anl and_exists_disjoint_r)
        @ rsyl (anim1 @ anr ,(func_subst_eps 'x 'membership_expand))
        @ anim id id)));



theorem epsilon_implies_not_concat_l (phi psi : Pattern)
    (h: $epsilon -> ~ phi$)
  : $epsilon -> ~ (phi . psi)$
= '( exp
   @ rsyl (bi1i @ regex_eq_ewp_concat)
   @ anwl
   @ curry h );
theorem epsilon_implies_not_concat_r (phi psi : Pattern)
    (h: $epsilon -> ~ psi$)
  : $epsilon -> ~ (phi . psi)$
= '( exp
   @ rsyl (bi1i @ regex_eq_ewp_concat)
   @ anwr
   @ curry h );

--- Simplifications used in generated proofs
--------------------------------------------

--- Identity and idemoptency of \/
theorem regex_eq_or_choice_abs: $ top \/ Alpha <-> top $ = '(ibii imp_top @ a1i top_or);
theorem regex_eq_or_choice_unit: $ bot \/ Alpha <-> Alpha $ = '(ibii bot_or prop_1);
theorem regex_eq_or_choice_idem_node: $ Alpha \/ (Alpha \/ Beta) <-> Alpha \/ Beta$ = '(ibii (eori orl id) orr);
theorem regex_eq_or_choice_idem_leaf: $ Alpha \/ Alpha <-> Alpha $ = 'oridm;
theorem regex_eq_or_choice_assoc: $ (Alpha \/ Beta) \/ Gamma <-> Alpha \/ (Beta \/ Gamma) $ = 'orass;
theorem regex_eq_or_choice_comm_node: $ Alpha \/ (Beta \/ Gamma) <-> Beta \/ (Alpha \/ Gamma) $ = 'or12;
theorem regex_eq_or_choice_comm_leaf: $ Alpha \/ Beta <-> Beta \/ Alpha $ = 'orcomb;

--- Identity and idemoptency of /\
theorem regex_eq_and_choice_abs: $ bot /\ Alpha <-> bot $ = '(ibii anl absurdum);
theorem regex_eq_and_choice_unit: $ top /\ Alpha <-> Alpha $ = '(ibii anr top_and);
theorem regex_eq_and_choice_idem_node: $ Alpha /\ (Alpha /\ Beta) <-> Alpha /\ Beta$ = '(bicom @ bian11i @ bicom anidm);
theorem regex_eq_and_choice_idem_leaf: $ Alpha /\ Alpha <-> Alpha $ = 'anidm;
theorem regex_eq_and_choice_assoc: $ (Alpha /\ Beta) /\ Gamma <-> Alpha /\ (Beta /\ Gamma) $ = 'anass;
theorem regex_eq_and_choice_comm_node: $ Alpha /\ (Beta /\ Gamma) <-> Beta /\ (Alpha /\ Gamma) $ = 'anlass;
theorem regex_eq_and_choice_comm_leaf: $ Alpha /\ Beta <-> Beta /\ Alpha $ = 'ancomb;

theorem regex_eq_bot_concat_l: $ bot . Alpha <-> bot $ =
  '(ibii (norm (norm_not appCtxLRVar) (! propag_bot box)) absurdum);
theorem regex_eq_bot_concat_r: $ Alpha . bot <-> bot $ =
  '(ibii (norm (norm_not appCtxRVar) (! propag_bot box)) absurdum);
theorem regex_eq_double_neg: $ ~ (~ Alpha) <-> Alpha $ = '(bicom notnot);
theorem regex_eq_bot_kleene: $ (kleene X bot) <-> epsilon $ = '(ibii
  (rsyl (mu_framing (positive_in_or positive_disjoint @ positive_in_concat positive_disjoint positive_in_same_sVar) positive_disjoint (rsyl (orim2 @ norm (norm_imp_l appCtxLRVar) (! propag_bot box)) dne)) (KT positive_disjoint @ norm (norm_sym @ norm_imp_l sSubstitution_disjoint) id))
  (epsilon_implies_kleene positive_disjoint));

theorem regex_eq_eps_kleene {X: SVar}: $ (kleene X epsilon) <-> epsilon $ =
  '(ibii
    (KT (positive_in_kleene_r_body positive_disjoint) @ norm (norm_sym @ norm_imp_l ,(propag_s_subst 'Y $epsilon \/ (epsilon . sVar Y)$)) @ eori id @ eq_to_intro ,(func_subst 'u $(eVar u) . epsilon == (eVar u)$ 'identity_right_e '(! functional_epsilon w)))
    (imim1i orl @ norm (norm_imp_l ,(propag_s_subst 'Y $epsilon \/ (epsilon . sVar Y)$)) @ pre_fixpoint (positive_in_kleene_r_body positive_disjoint))
  );

theorem regex_eq_double_kleene_l_lemma {X: SVar} (Alpha: Pattern X) (h: $ _sFresh X Alpha $):
  $ (kleene_l X Alpha) . (kleene_l X Alpha) -> (kleene_l X Alpha) $ =
  (named '(norm (norm_imp_l appctx_concat_r)
                @ unwrap
                @ KT (positive_in_kleene_l_body @ positive_fresh h)
                @ norm (norm_imp_l @ norm_sym @ _sSubst_or sSubstitution_disjoint (sSubst_concat sSubstitution_in_same_sVar (sSubstitution_fresh h)))
                @ eori (wrap @ norm (norm_imp_l @ norm_sym appctx_concat_r ) @ bi1i id_concat_r)
                       ( wrap
                       @ norm (norm_imp_l @ norm_sym @ appctx_concat_r)
                       @ rsyl (anr assoc_concat)
                       @ norm (norm_imp_l @ norm_concat_l appctx_concat_r)
                       @ rsyl (framing_concat_l ctximp_in_ctx_forward)
                       @ unfold_r (positive_in_kleene_l_body @ positive_fresh h)
                       @ norm (norm_sym @ norm_imp_r @ _sSubst_or sSubstitution_disjoint @ sSubst_concat sSubstitution_in_same_sVar (sSubstitution_fresh h))
                       orr)));

theorem regex_eq_double_kleene_lemma {X: SVar} (Alpha: Pattern X) (h: $ _sFresh X Alpha $):
  $ (kleene X Alpha) . (kleene X Alpha) -> (kleene X Alpha) $ =
  (named '(norm (norm_imp_l appctx_concat_l)
                @ unwrap
                @ KT (positive_in_kleene_r_body @ positive_fresh h)
                @ norm (norm_imp_l @ norm_sym @ _sSubst_or sSubstitution_disjoint (sSubst_concat (sSubstitution_fresh h) sSubstitution_in_same_sVar) )
                @ eori (wrap @ norm (norm_imp_l @ norm_sym appctx_concat_l ) @ bi1i id_concat_l)
                       ( wrap
                       @ norm (norm_imp_l @ norm_sym @ appctx_concat_l)
                       @ rsyl (bi1i assoc_concat)
                       @ norm (norm_imp_l @ norm_concat_r appctx_concat_l)
                       @ rsyl (framing_concat_r ctximp_in_ctx_forward)
                       @ unfold_r (positive_in_kleene_r_body @ positive_fresh h)
                       @ norm (norm_imp_r @ norm_sym @ _sSubst_or sSubstitution_disjoint @ sSubst_concat (sSubstitution_fresh h) sSubstitution_in_same_sVar)
                       orr)));

theorem regex_eq_double_kleene {X: SVar} (Alpha: Pattern X) (h: $ _sFresh X Alpha $):
  $ (kleene X (kleene X Alpha)) <-> (kleene X Alpha) $ =
  '(ibii
    (KT (positive_in_kleene_r_body @ positive_fresh sFresh_mu_same_var)
      @ norm (norm_sym @ norm_imp_l ,(propag_s_subst 'X $epsilon \/ kleene X Alpha . sVar X$))
      @ eori (epsilon_implies_kleene @ positive_fresh h) @ regex_eq_double_kleene_lemma h)
    @ kleene_monotone sFresh_mu_same_var);

theorem kleene_r_to_kleene_l {X: SVar} (phi: Pattern X)
  (X_fresh: $ _sFresh X phi $):
  $ kleene_r X phi -> kleene_l X phi $ =
  '(KT (positive_in_kleene_r_body @ positive_fresh X_fresh) @ norm (norm_sym @ norm_imp_l @ _sSubst_or sSubstitution_disjoint @ _sSubst_concat (sSubstitution_fresh X_fresh) sSubstitution_in_same_sVar) @
    eori
      (rsyl orl @ norm (norm_imp_l ,(propag_s_subst 'X $epsilon \/ sVar X . phi$)) @ pre_fixpoint @ positive_in_kleene_l_body @ positive_fresh X_fresh)
      (rsyl (framing_concat_l @ kleene_l_monotone X_fresh) @ regex_eq_double_kleene_l_lemma X_fresh));

--- Derivatives: "Semantic" theorems
------------------------------------

theorem der_expand (l: Pattern) (phi: Pattern):
  $ (derivative l phi) <-> exists d (eVar d /\ ((l . eVar d) C= phi)) $ =
  '(norm (norm_equiv_r @ norm_exists @ norm_and_r @ norm_floor @ norm_imp_l (! appCtxRVar box _ _)) biid);

theorem l_der_phi_imp_phi (l phi: Pattern):
  $ (l . derivative l phi) -> phi $ =
  (named '(unwrap_subst appctx_concat_r id));

theorem der_equality_forward_lemma {x: EVar} (phi psi: Pattern x) (l: Pattern) (h: $ exists x (eVar x == l) $): $(l . psi) /\ phi -> l . derivative l phi$ =
  (named '(syl ,(framing_subst '(anr der_expand) 'appctx_concat_r) @ syl (anr ,(ex_appCtx_subst 'appctx_concat_r)) @
    rsyl (anim1 @ syl (anl ,(ex_appCtx_subst 'appctx_concat_r)) ,(framing_subst '(anl lemma_exists_and) 'appctx_concat_r)) @
    rsyl (anr and_exists_disjoint_r) @ exists_framing @ rsyl (anim1 ,(framing_subst 'anl 'appctx_concat_r)) @
    syl ,(func_subst 'd $(l . eVar y) /\ (d in phi) -> (l . (eVar y /\ (eVar d C= phi)))$ '(rsyl (anim2 eVar_in_subset_forward) @ anr ,(lemma_60_subset_subst 'appctx_concat_r)) '(functional_l_concat h)) @
    iand anl corollary_57_ceil));

theorem der_equality_forward {l: EVar} (phi: Pattern):
  $phi -> (epsilon /\ phi) \/ exists l ((eVar l . (derivative (eVar l) phi)) /\ l in top_letter)$
  = (named
    '(mpcom (! domain_words X)
    @ unfold_l_top_word_r
    @ expcom
    @ rsyl (bi1i andi)
    @ eori (orld ancom)
    @ orrd
    @ rsyl ancom
    @ rsyl (anim1 @ anl ,(appCtx_pointwise_subst 'appctx_concat_l))
    @ rsyl and_exists_disjoint_r_reverse
    @ exists_framing
    @ rsyl (anl anrass)
    @ anim1
    @ der_equality_forward_lemma functional_var
  ));
theorem der_equality_reverse:
    $(epsilon /\ phi) \/ exists l ((eVar l . (derivative (eVar l) phi)) /\ l in top_letter) -> phi$
  = '(eori anr
    @ exists_generalization_disjoint
    @ anwl l_der_phi_imp_phi);

--- main theorem for deriviatives
theorem der_equality_bi: $phi <-> (epsilon /\ phi) \/ exists l ((eVar l . (derivative (eVar l) phi)) /\ l in top_letter)$ =
  '(ibii der_equality_forward der_equality_reverse);
theorem der_equality: $phi == (epsilon /\ phi) \/ exists l ((eVar l . (derivative (eVar l) phi)) /\ l in top_letter)$ =
  '(equiv_to_eq der_equality_bi);

theorem der_equality_bi_concrete: $phi <-> (epsilon /\ phi) \/ ((a . (derivative a phi)) \/ (b . (derivative b phi)))$ =
  (named
  '(bitr der_equality_bi
  @ oreq2i
  -- @ exists_intro_l_bi_disjoint
  @ bitr (cong_of_equiv_exists @ aneq2i ,(propag_mem 'x $a \/ b$))
  @ bitr (cong_of_equiv_exists @ bitr ancomb andir)
  @ bitr or_exists_bi
  @ oreqi
    (mp ,(func_to_and_ctx_bi 'x $eVar x . derivative (eVar x) phi$) functional_a)
    (mp ,(func_to_and_ctx_bi 'x $eVar x . derivative (eVar x) phi$) functional_b)));

--- Derivatives: Syntactic Simplifications
------------------------------------------

theorem cong_of_equiv_der
  (h1: $ phi1 <-> phi2 $)
  (h2: $ psi1 <-> psi2 $):
  $ (derivative phi1 psi1) <-> (derivative phi2 psi2) $ =
  (named '(bisquare der_expand der_expand @ cong_of_equiv_exists @ cong_of_equiv_and_r @ cong_of_equiv_subset (cong_of_equiv_concat_l h1) h2));
theorem cong_of_equiv_der_l
  (h: $ phi1 <-> phi2 $):
  $ (derivative phi1 psi) <-> (derivative phi2 psi) $ =
  '(cong_of_equiv_der h biid);
theorem cong_of_equiv_der_r
  (h: $ psi1 <-> psi2 $):
  $ (derivative phi psi1) <-> (derivative phi psi2) $ =
  '(cong_of_equiv_der biid h);

theorem der_l1_l2_phi (l1 l2 phi: Pattern)
  (l1_func: $ exists x (eVar x == l1) $)
  (l2_func: $ exists y (eVar y == l2) $)
  (h1: $ |^ l1 /\ top_letter ^| $)
  (h2: $ |^ l2 /\ top_letter ^| $):
  $ (derivative l1 (l2 . phi)) <-> (l1 == l2) /\ phi $ =
  (named '(bitr der_expand @
    bitr (cong_of_equiv_exists @ cong_of_equiv_and_r @
      bitr
        ,(func_subst 'x $(eVar x C= (l2 . phi)) <-> exists z ((z in phi) /\ (eVar x == (l2 . eVar z)))$ '(bitr (bitr eVar_in_subset_rev membership_app) @ cong_of_equiv_exists @ cong_of_equiv_and_r
        ,(func_subst 'y $(x in eVar y) <-> (eVar x == eVar y)$ 'membership_var_bi '(functional_l_concat l2_func)))
        '(functional_l_concat l1_func)) @
      bitr (cong_of_equiv_exists @
        bitr (cong_of_equiv_and_r @ bitr (ibii (
              mp (mp ,(func_subst 'x $(x in top_letter) -> |^ l2 /\ top_letter ^| -> (eVar x . eVar u == l2 . eVar v) -> (eVar x == l2) /\ (eVar u == eVar v)$
                (func_subst 'y $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y . eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$ 'no_confusion_cc_e 'l2_func)
                'l1_func) h1) h2
            ) (rsyl (anim ,(eq_imp_eq_framing_subst 'appctx_concat_l) ,(eq_imp_eq_framing_subst 'appctx_concat_r)) @ curry eq_trans))
          (cong_of_equiv_and_r @ bicom membership_var_bi)) anlass) @
      bitr and_exists_disjoint @
      bicom @ cong_of_equiv_and_r ,(membership_appCtx_subst 'appCtxVar)
    ) @
    bitr (cong_of_equiv_exists anlass) @
    bitr and_exists_disjoint @
    cong_of_equiv_and_r lemma_62_b));

do {
  (def (der_transformer x y l phi) '(ibii
    (exists_generalization_disjoint @ curry @ syl anr ,(func_subst_explicit_helper 'y $(l . eVar y) C= phi$))
    (rsyl (ian eq_refl) @ norm (norm_imp_l ,(propag_e_subst_adv 'x $(eVar y == eVar x) /\ ((l . eVar x) C= phi)$ (atom-map! '[l #t] '[phi #t]))) exists_intro)
  ))
};
theorem der_transformer_test_1 {x y: EVar} (phi: Pattern):
  $ (exists x ((eVar y == eVar x) /\ ((a . eVar x) C= (~ phi)))) <-> ((a . eVar y) C= (~ phi)) $ =
  (der_transformer 'x 'y 'a $~ phi$);


theorem regex_eq_der_bot
  (h: $ exists x (eVar x == A) $):
  $ (derivative A bot) -> bot $
  = '(exists_generalization_disjoint @ con3 anr @ notnot1 @ framing_def notnot1 @
    exists_generalization_disjoint (com12
      (eq_to_def @ norm (norm_imp_r @ norm_imp_r @ norm_sym @ norm_trans appCtxR_disjoint @ norm_app norm_refl (! appCtxVar box)) @ eq_to_app_l @ eq_to_app_r eq_to_intro)
      (exists_generalization_disjoint (com12 (eq_to_def eq_to_intro) definedness)
          (! functional_concat x v1 x1))
        ) h
  );
theorem regex_eq_der_bot_wrt_a:
  $ (derivative a bot) <-> bot $ = '(ibii (regex_eq_der_bot (! functional_a x)) absurdum);
theorem regex_eq_der_bot_wrt_b:
  $ (derivative b bot) <-> bot $ = '(ibii (regex_eq_der_bot (! functional_b x)) absurdum);

theorem regex_eq_der_epsilon_wrt_a:
  $ (derivative a epsilon) <-> bot $ =
  '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @
    rsyl ,(func_subst 'x $((a . eVar d) C= eVar x) -> ((a . eVar d) == eVar x)$ (
        func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ (
          func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k)
        ) '(! functional_a w1)
      ) '(! functional_epsilon w2)) @
    rsyl eq_sym @
    rsyl ,(func_subst 'x $(epsilon == eVar x . eVar d) -> ((epsilon == eVar x) /\ (epsilon == eVar d))$ '(! no_confusion_ec_e _ d) '(! functional_a w3)) @
      con3 anl @ con3 (rsyl eq_imp_subset subset_imp_subset_or_l) no_confusion_ae_e
  ) absurdum);
theorem regex_eq_der_epsilon_wrt_b:
  $ (derivative b epsilon) <-> bot $ =
  '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @
    rsyl ,(func_subst 'x $((b . eVar d) C= eVar x) -> ((b . eVar d) == eVar x)$ (
        func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ (
          func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k)
        ) '(! functional_b w1)
      ) '(! functional_epsilon w2)) @
    rsyl eq_sym @
    rsyl ,(func_subst 'x $(epsilon == eVar x . eVar d) -> ((epsilon == eVar x) /\ (epsilon == eVar d))$ '(! no_confusion_ec_e _ d) '(! functional_b w3)) @
      con3 anl @ con3 (rsyl eq_imp_subset subset_imp_subset_or_r) no_confusion_ae_e
  ) absurdum);
theorem regex_eq_der_diff_a_wrt_a:
  $ (derivative a b) <-> bot $ =
  '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @
    rsyl ,(func_subst 'x $((a . eVar d) C= eVar x) -> ((a . eVar d) == eVar x)$ (
        func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ (
          func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k)
        ) '(! functional_a w1)
      ) '(! functional_b w2)) @
      syl no_confusion_ab_e @ syl anl @ mp
      ,(func_subst 'y $|^ a /\ top_letter ^| -> (y in top_letter) -> (a . eVar u == eVar y) -> (a == eVar y) /\ (eVar u == epsilon)$
        (func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y) -> (eVar x == eVar y) /\ (eVar u == epsilon)$ '(! no_confusion_cc_e_epsilon w3) '(! functional_a w5))
        '(! functional_b w4)) a_in_top_letter b_in_top_letter
  ) absurdum);
theorem regex_eq_der_diff_a_wrt_b:
  $ (derivative b a) <-> bot $ =
  '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @
    rsyl ,(func_subst 'x $((b . eVar d) C= eVar x) -> ((b . eVar d) == eVar x)$ (
        func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ (
          func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k)
        ) '(! functional_b w1)
      ) '(! functional_a w2)) @
      syl no_confusion_ab_e @ syl eq_sym @ syl anl @ mp
      ,(func_subst 'y $|^ b /\ top_letter ^| -> (y in top_letter) -> (b . eVar u == eVar y) -> (b == eVar y) /\ (eVar u == epsilon)$
        (func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y) -> (eVar x == eVar y) /\ (eVar u == epsilon)$ '(! no_confusion_cc_e_epsilon w3) '(! functional_b w5))
        '(! functional_a w4)) b_in_top_letter a_in_top_letter
  ) absurdum);
theorem regex_eq_der_same_a_wrt_a:
  $ (derivative a a) <-> epsilon $ =
  (named '(ibii
    (rsyl (anl der_expand) @ exists_generalization_disjoint @ syl simple_eq_subst @ anim2 @ syl
      (syl anr @ mp
        ,(func_subst 'y $(y in top_letter) -> (a . eVar d == eVar y) -> (a == eVar y) /\ (eVar d == epsilon)$
          '(mp
            ,(func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar d == eVar y) -> (eVar x == eVar y) /\ (eVar d == epsilon)$ 'no_confusion_cc_e_epsilon 'functional_a)
            a_in_top_letter)
          'functional_a)
        a_in_top_letter)
      ,(func_subst 'y $((a . eVar d) C= eVar y) -> ((a . eVar d) == eVar y)$ (func_subst 'v $((eVar v . eVar d) C= eVar y) -> ((eVar v . eVar d) == eVar y)$ (func_subst 'x $(eVar x C= eVar y) -> (eVar x == eVar y)$ 'eVars_subset_eq_forward 'functional_concat) 'functional_a) 'functional_a)
      )
    (syl (anr der_expand) @
      syl ,(func_subst_fresh '(eFresh_imp eFresh_disjoint eFresh_exists_same_var) 'd $(eVar d /\ ((a . eVar d) C= a)) -> exists d (eVar d /\ ((a . eVar d) C= a))$ 'exists_intro_same_var 'functional_epsilon) @
      iand id @ a1i @ imp_to_subset @ anl id_concat_r
    )
  ));
theorem regex_eq_der_same_a_wrt_b:
  $ (derivative b b) <-> epsilon $ =
  (named '(ibii
    (rsyl (anl der_expand) @ exists_generalization_disjoint @ syl simple_eq_subst @ anim2 @ syl
      (syl anr @ mp
        ,(func_subst 'y $(y in top_letter) -> (b . eVar d == eVar y) -> (b == eVar y) /\ (eVar d == epsilon)$
          '(mp
            ,(func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar d == eVar y) -> (eVar x == eVar y) /\ (eVar d == epsilon)$ 'no_confusion_cc_e_epsilon 'functional_b)
            b_in_top_letter)
          'functional_b)
        b_in_top_letter)
      ,(func_subst 'y $((b . eVar d) C= eVar y) -> ((b . eVar d) == eVar y)$ (func_subst 'v $((eVar v . eVar d) C= eVar y) -> ((eVar v . eVar d) == eVar y)$ (func_subst 'x $(eVar x C= eVar y) -> (eVar x == eVar y)$ 'eVars_subset_eq_forward 'functional_concat) 'functional_b) 'functional_b)
      )
    (syl (anr der_expand) @
      syl ,(func_subst_fresh '(eFresh_imp eFresh_disjoint eFresh_exists_same_var) 'd $(eVar d /\ ((b . eVar d) C= b)) -> exists d (eVar d /\ ((b . eVar d) C= b))$ 'exists_intro_same_var 'functional_epsilon) @
      iand id @ a1i @ imp_to_subset @ anl id_concat_r
    )
  ));

theorem regex_eq_der_choice_wrt_a: $ (derivative a (Alpha \/ Beta)) <-> (derivative a Alpha) \/ (derivative a Beta) $ =
  '(bitr (! der_expand d1) @
    bitr (
      membership_elim_implicit @ anr
        ,(propag_mem 'y $(exists x (eVar x /\ ((a . eVar x) C= (Alpha \/ Beta)))) <-> ((exists x (eVar x /\ ((a . eVar x) C= Alpha))) \/ (exists x (eVar x /\ ((a . eVar x) C= Beta))))$) @
          bitr ,(der_transformer 'x 'y 'a $Alpha \/ Beta$) @
          bitr ,(func_subst 'x $(eVar x C= Alpha \/ Beta) <-> (eVar x C= Alpha) \/ (eVar x C= Beta)$ '(
            bitr eVar_in_subset_rev @ bitr membership_or_bi (cong_of_equiv_or eVar_in_subset eVar_in_subset)
          ) '(! functional_a_concat d2 x)) @
          bicom @ cong_of_equiv_or ,(der_transformer 'x 'y 'a $Alpha$) ,(der_transformer 'x 'y 'a $Beta$)) @
    bicom @ cong_of_equiv_or (! der_expand d1) (! der_expand d1));
theorem regex_eq_der_choice_wrt_b: $ (derivative b (Alpha \/ Beta)) <-> (derivative b Alpha) \/ (derivative b Beta) $ =
  '(bitr (! der_expand d1) @
    bitr (
      membership_elim_implicit @ anr
        ,(propag_mem 'y $(exists x (eVar x /\ ((b . eVar x) C= (Alpha \/ Beta)))) <-> ((exists x (eVar x /\ ((b . eVar x) C= Alpha))) \/ (exists x (eVar x /\ ((b . eVar x) C= Beta))))$) @
          bitr ,(der_transformer 'x 'y 'b $Alpha \/ Beta$) @
          bitr ,(func_subst 'x $(eVar x C= Alpha \/ Beta) <-> (eVar x C= Alpha) \/ (eVar x C= Beta)$ '(
            bitr eVar_in_subset_rev @ bitr membership_or_bi (cong_of_equiv_or eVar_in_subset eVar_in_subset)
          ) '(! functional_b_concat d2 x)) @
          bicom @ cong_of_equiv_or ,(der_transformer 'x 'y 'b $Alpha$) ,(der_transformer 'x 'y 'b $Beta$)) @
    bicom @ cong_of_equiv_or (! der_expand d1) (! der_expand d1));
theorem regex_eq_der_conj_wrt_a: $ (derivative a (Alpha /\ Beta)) <-> (derivative a Alpha) /\ (derivative a Beta) $ =
  '(bitr (! der_expand d1) @
    bitr (
      membership_elim_implicit @ anr
        ,(propag_mem 'y $(exists x (eVar x /\ ((a . eVar x) C= (Alpha /\ Beta)))) <-> ((exists x (eVar x /\ ((a . eVar x) C= Alpha))) /\ (exists x (eVar x /\ ((a . eVar x) C= Beta))))$) @
          bitr ,(der_transformer 'x 'y 'a $Alpha /\ Beta$) @
          bitr ,(func_subst 'x $(eVar x C= Alpha /\ Beta) <-> (eVar x C= Alpha) /\ (eVar x C= Beta)$ '(
            bitr eVar_in_subset_rev @ bitr membership_and_bi (cong_of_equiv_and eVar_in_subset eVar_in_subset)
          ) '(! functional_a_concat d2 x)) @
          bicom @ cong_of_equiv_and ,(der_transformer 'x 'y 'a $Alpha$) ,(der_transformer 'x 'y 'a $Beta$)) @
    bicom @ cong_of_equiv_and (! der_expand d1) (! der_expand d1));
theorem regex_eq_der_conj_wrt_b: $ (derivative b (Alpha /\ Beta)) <-> (derivative b Alpha) /\ (derivative b Beta) $ =
  '(bitr (! der_expand d1) @
    bitr (
      membership_elim_implicit @ anr
        ,(propag_mem 'y $(exists x (eVar x /\ ((b . eVar x) C= (Alpha /\ Beta)))) <-> ((exists x (eVar x /\ ((b . eVar x) C= Alpha))) /\ (exists x (eVar x /\ ((b . eVar x) C= Beta))))$) @
          bitr ,(der_transformer 'x 'y 'b $Alpha /\ Beta$) @
          bitr ,(func_subst 'x $(eVar x C= Alpha /\ Beta) <-> (eVar x C= Alpha) /\ (eVar x C= Beta)$ '(
            bitr eVar_in_subset_rev @ bitr membership_and_bi (cong_of_equiv_and eVar_in_subset eVar_in_subset)
          ) '(! functional_b_concat d2 x)) @
          bicom @ cong_of_equiv_and ,(der_transformer 'x 'y 'b $Alpha$) ,(der_transformer 'x 'y 'b $Beta$)) @
    bicom @ cong_of_equiv_and (! der_expand d1) (! der_expand d1));
theorem regex_eq_der_neg_wrt_a: $ (derivative a (~ Alpha)) <-> ~ (derivative a Alpha) $ =
  '(bitr (! der_expand d1) @
    bitr (
      membership_elim_implicit @ anr
        ,(propag_mem 'y $(exists x (eVar x /\ ((a . eVar x) C= ~ Alpha))) <-> ~ (exists x (eVar x /\ ((a . eVar x) C= Alpha)))$) @
          bitr ,(der_transformer 'x 'y 'a $~ Alpha$) @
          bitr (cong_of_equiv_not ,(func_subst 'x $(x in Alpha) <-> (eVar x C= Alpha)$ 'eVar_in_subset '(! functional_a_concat d2 x))) @
          bicom @ cong_of_equiv_not ,(der_transformer 'x 'y 'b $Alpha$)) @
    bicom @ cong_of_equiv_not (! der_expand d1));
theorem regex_eq_der_neg_wrt_b: $ (derivative b (~ Alpha)) <-> ~ (derivative b Alpha) $ =
  '(bitr (! der_expand d1) @
    bitr (
      membership_elim_implicit @ anr
        ,(propag_mem 'y $(exists x (eVar x /\ ((b . eVar x) C= ~ Alpha))) <-> ~ (exists x (eVar x /\ ((b . eVar x) C= Alpha)))$) @
          bitr ,(der_transformer 'x 'y 'b $~ Alpha$) @
          bitr (cong_of_equiv_not ,(func_subst 'x $(x in Alpha) <-> (eVar x C= Alpha)$ 'eVar_in_subset '(! functional_b_concat d2 x))) @
          bicom @ cong_of_equiv_not ,(der_transformer 'x 'y 'b $Alpha$)) @
    bicom @ cong_of_equiv_not (! der_expand d1));
theorem regex_eq_der_concat_wrt_a (Alpha Beta: Pattern) :
  $ (derivative a (Alpha . Beta)) <-> ((derivative a Alpha) . Beta) \/ ((epsilon /\ Alpha) . (derivative a Beta)) $ =
  (named '(ibii
    (rsyl (anl @
      bitr (cong_of_equiv_der_r @ cong_of_equiv_concat_l der_equality_bi_concrete) @
      bitr (cong_of_equiv_der_r ,(or_appCtx2_r_subst 'appctx_concat_l)) @
      bitr regex_eq_der_choice_wrt_a @
      bitr (cong_of_equiv_or_r regex_eq_der_choice_wrt_a) @
      bitr (cong_of_equiv_or
          ( bitr (cong_of_equiv_der_r epsilon_and_concat)
            der_expand)
        @ cong_of_equiv_or
          ( bitr (cong_of_equiv_der_r assoc_concat) @
            bitr (der_l1_l2_phi functional_a functional_a a_in_top_letter a_in_top_letter) @
            taut_and_equiv eq_refl)
          ( bitr (cong_of_equiv_der_r assoc_concat) @
            bitr (der_l1_l2_phi functional_a functional_b a_in_top_letter b_in_top_letter) @
            absurd_and_equiv_bot no_confusion_ab_e)
      ) @
      bitr (cong_of_equiv_or_r or_bot_bi_l) @
      orcomb) @
    orim2 @ syl (anr epsilon_and_concat) @ syl (anim2 @ anr der_expand) @ rsyl
      (exists_framing @ syl (anr anlass) @ anim2 @ rsyl subset_and @ anim1
        ,(func_subst 'x $(eVar x C= |^ phi ^|) -> |^ phi ^|$ '(rsyl eVar_in_subset_reverse mem_def_forward) 'functional_a_concat))
      and_exists_disjoint_forwards
    )
    (rsyl (anl @ cong_of_equiv_or (cong_of_equiv_concat_l der_expand) (cong_of_equiv_concat_r der_expand)) @ syl (anr der_expand) @ eori
      (rsyl (norm (norm_imp appCtxLRVar @ norm_exists appCtxLRVar) propag_exists_disjoint) @ exists_generalization_disjoint @
        rsyl (anl ,(appCtx_pointwise_subst 'appCtxRVar)) @ exists_generalization_disjoint @ rsyl (anim1
          ,(func_subst 'x $((eVar d /\ (eVar x C= Alpha)) . eVar beta) -> (eVar d . eVar beta /\ (eVar x C= Alpha))$ '(anl ,(lemma_60_subset_subst 'appCtxLRVar)) 'functional_a_concat)) @
        rsyl (anl anass) @ rsyl (anim2 @ syl (framing_subset (anr assoc_concat) id) @ rsyl (anim
          ,(subset_imp_subset_framing_subst 'appCtxLRVar)
          (rsyl eVar_in_subset_forward ,(subset_imp_subset_framing_subst 'appCtxRVar))) @
        curry subset_trans) @ anr imp_exists_disjoint @ exists_framing (
          syl anr ,(func_subst_explicit_helper 'x $eVar x /\ ((a . eVar x) C= Alpha . Beta)$)
        ) functional_concat)
      (rsyl (anl ,(ex_appCtx_subst 'appCtxRVar)) @ exists_framing @ iand
        (rsyl ,(framing_subst 'anl 'appCtxLRVar) @ syl anl @ anl id_concat_l)
        (rsyl (iand (norm (norm_imp_l appCtxLRVar) lemma_56) (syl anr @ syl (anl id_concat_l) ,(framing_subst 'anl 'appCtxLRVar))) @
          rsyl (anim1 ,(func_subst 'x $(x in Alpha) -> (eVar x C= Alpha)$ 'eVar_in_subset_forward 'functional_epsilon)) @
          rsyl (curry concat_subset) @ framing_subset (anr id_concat_l) id))
    )));
theorem regex_eq_der_concat_wrt_b (Alpha Beta: Pattern) :
  $ (derivative b (Alpha . Beta)) <-> ((derivative b Alpha) . Beta) \/ ((epsilon /\ Alpha) . (derivative b Beta)) $ =
  (named '(ibii
    (rsyl (anl @
      bitr (cong_of_equiv_der_r @ cong_of_equiv_concat_l der_equality_bi_concrete) @
      bitr (cong_of_equiv_der_r ,(or_appCtx2_r_subst 'appctx_concat_l)) @
      bitr regex_eq_der_choice_wrt_b @
      bitr (cong_of_equiv_or_r regex_eq_der_choice_wrt_b) @
      bitr (cong_of_equiv_or
          ( bitr (cong_of_equiv_der_r epsilon_and_concat)
            der_expand)
        @ cong_of_equiv_or
          ( bitr (cong_of_equiv_der_r assoc_concat) @
            bitr (der_l1_l2_phi functional_b functional_a b_in_top_letter a_in_top_letter) @
            absurd_and_equiv_bot @ rsyl eq_sym no_confusion_ab_e)
          ( bitr (cong_of_equiv_der_r assoc_concat) @
            bitr (der_l1_l2_phi functional_b functional_b b_in_top_letter b_in_top_letter) @
            taut_and_equiv eq_refl)
      ) @
      bitr (cong_of_equiv_or_r or_bot_bi_r) @
      orcomb) @
    orim2 @ syl (anr epsilon_and_concat) @ syl (anim2 @ anr der_expand) @ rsyl
      (exists_framing @ syl (anr anlass) @ anim2 @ rsyl subset_and @ anim1
        ,(func_subst 'x $(eVar x C= |^ phi ^|) -> |^ phi ^|$ '(rsyl eVar_in_subset_reverse mem_def_forward) 'functional_b_concat))
      and_exists_disjoint_forwards
    )
    (rsyl (anl @ cong_of_equiv_or (cong_of_equiv_concat_l der_expand) (cong_of_equiv_concat_r der_expand)) @ syl (anr der_expand) @ eori
      (rsyl (norm (norm_imp appCtxLRVar @ norm_exists appCtxLRVar) propag_exists_disjoint) @ exists_generalization_disjoint @
        rsyl (anl ,(appCtx_pointwise_subst 'appCtxRVar)) @ exists_generalization_disjoint @ rsyl (anim1
          ,(func_subst 'x $((eVar d /\ (eVar x C= Alpha)) . eVar beta) -> (eVar d . eVar beta /\ (eVar x C= Alpha))$ '(anl ,(lemma_60_subset_subst 'appCtxLRVar)) 'functional_b_concat)) @
        rsyl (anl anass) @ rsyl (anim2 @ syl (framing_subset (anr assoc_concat) id) @ rsyl (anim
          ,(subset_imp_subset_framing_subst 'appCtxLRVar)
          (rsyl eVar_in_subset_forward ,(subset_imp_subset_framing_subst 'appCtxRVar))) @
        curry subset_trans) @ anr imp_exists_disjoint @ exists_framing (
          syl anr ,(func_subst_explicit_helper 'x $eVar x /\ ((b . eVar x) C= Alpha . Beta)$)
        ) functional_concat)
      (rsyl (anl ,(ex_appCtx_subst 'appCtxRVar)) @ exists_framing @ iand
        (rsyl ,(framing_subst 'anl 'appCtxLRVar) @ syl anl @ anl id_concat_l)
        (rsyl (iand (norm (norm_imp_l appCtxLRVar) lemma_56) (syl anr @ syl (anl id_concat_l) ,(framing_subst 'anl 'appCtxLRVar))) @
          rsyl (anim1 ,(func_subst 'x $(x in Alpha) -> (eVar x C= Alpha)$ 'eVar_in_subset_forward 'functional_epsilon)) @
          rsyl (curry concat_subset) @ framing_subset (anr id_concat_l) id))
    )));


theorem regex_eq_der_kleene_lemma {X: SVar} (Alpha: Pattern X)
  (h: $ _sFresh X Alpha $):
  $ ~epsilon /\ Alpha . kleene X Alpha <-> (~epsilon /\ Alpha) . kleene X Alpha $ =
  (named '(ibii
    ( rsyl ancom
    @ curry
    @ unwrap_subst appctx_concat_r
    @ rsyl (kleene_r_to_kleene_l h)
    @ KT (positive_in_kleene_l_body @ positive_fresh h)
    @ norm (norm_sym @ norm_imp_l ,(propag_s_subst 'X $epsilon \/ sVar X . Alpha$))
    @ eori
      ( wrap_subst appctx_concat_r
        @ rsyl (anl id_concat_r)
        @ expcom
        @ rsyl (anr id_concat_r)
        @ framing_concat_r @ epsilon_implies_kleene @ positive_fresh h)
      ( norm (norm_sym @ norm_imp_l @ norm_concat_r @ sSubstitution_fresh h)
        @ wrap
        @ norm (norm_sym @ norm_imp_l appctx_concat_r)
        @ rsyl (anr assoc_concat)
        @ norm (norm_imp_l @ norm_concat_l appctx_concat_r)
        @ rsyl (framing_concat_l ctximp_in_ctx_forward)
        @ rsyl (anl ,(or_appCtx_subst 'appctx_concat_l))
        @ eori
          ( rsyl (anl id_concat_l)
            @ expcom
            @ rsyl (anr id_concat_r)
            @ framing_concat_r @ epsilon_implies_kleene @ positive_fresh h)
            @ orrd
            @ rsyl (anl assoc_concat)
            @ framing_concat_r
            @ rsyl (framing_concat_r @ kleene_monotone h)
            @ regex_eq_double_kleene_lemma h)) 
    @ iand
      (con2 @ corollary_57_floor @ mp ,(func_subst_eps 'x 'eVar_in_subset_forward) @
        mp ,(func_subst 'x $~(exists y (~(eVar y == epsilon) /\ y in alpha /\ exists z ((z in alpha_k) /\ x in (eVar y . eVar z)))) -> x in ~(((~ epsilon) /\ alpha) . alpha_k)$ '(anr ,(propag_mem 'x $~(((~ epsilon) /\ alpha) . alpha_k)$)) 'functional_epsilon)
        (univ_gene @ rsyl ancom @ curry @ syl con3 @ a1i
          @ rsyl (exists_framing @ syl ancom @ anim2 epsilon_in_concat_eVar)
          @ rsyl and_exists_disjoint_forwards anl))
      @ framing_concat_l anr));

theorem regex_eq_der_kleene_wrt_a {X: SVar} (Alpha: Pattern X)
  (X_fresh: $ _sFresh X Alpha $):
  $ (derivative a (kleene X Alpha)) <-> ((derivative a Alpha) . (kleene X Alpha)) $ =
  (named '(bitr (cong_of_equiv_der_r @ bitr (unfold_kleene X_fresh) or_or_not_an) @
    bitr regex_eq_der_choice_wrt_a @
    bitr (cong_of_equiv_or_l regex_eq_der_epsilon_wrt_a) @
    bitr or_bot_bi_r @
    bitr (cong_of_equiv_der_r @ regex_eq_der_kleene_lemma X_fresh) @
    bitr regex_eq_der_concat_wrt_a @
    bitr (cong_of_equiv_or
      (cong_of_equiv_concat_l (bitr regex_eq_der_conj_wrt_a @ bitr (cong_of_equiv_and_l @ bitr regex_eq_der_neg_wrt_a @ cong_of_equiv_not regex_eq_der_epsilon_wrt_a) an_top_bi_r))
      (bitr (cong_of_equiv_concat_l @ bitr (bicom anass) @ bitr (cong_of_equiv_and_l absurd_an_r) an_bot_bi_r) (ibii (norm (norm_imp_l appctx_concat_l) propag_bot) absurdum))) @
    or_bot_bi_l));

theorem regex_eq_der_kleene_wrt_b {X: SVar} (Alpha: Pattern X)
  (X_fresh: $ _sFresh X Alpha $):
  $ (derivative b (kleene X Alpha)) <-> ((derivative b Alpha) . (kleene X Alpha)) $ =
  (named '(bitr (cong_of_equiv_der_r @ bitr (unfold_kleene X_fresh) or_or_not_an) @
    bitr regex_eq_der_choice_wrt_b @
    bitr (cong_of_equiv_or_l regex_eq_der_epsilon_wrt_b) @
    bitr or_bot_bi_r @
    bitr (cong_of_equiv_der_r @ regex_eq_der_kleene_lemma X_fresh) @
    bitr regex_eq_der_concat_wrt_b @
    bitr (cong_of_equiv_or
      (cong_of_equiv_concat_l (bitr regex_eq_der_conj_wrt_b @ bitr (cong_of_equiv_and_l @ bitr regex_eq_der_neg_wrt_b @ cong_of_equiv_not regex_eq_der_epsilon_wrt_b) an_top_bi_r))
      (bitr (cong_of_equiv_concat_l @ bitr (bicom anass) @ bitr (cong_of_equiv_and_l absurd_an_r) an_bot_bi_r) (ibii (norm (norm_imp_l appctx_concat_l) propag_bot) absurdum))) @
    or_bot_bi_l));

theorem inductive_domain_l_implies_r { X : SVar }
  : $(top_word_l X) -> (top_word_r X)$
  = (named '( kt_top_word_l
           ( unfold_r_top_word_r orl)
           ( norm (norm_imp (! appctx_concat_l _) norm_refl)
                  (unwrap @ kt_top_word_r
                    (wrap ( norm ( norm_sym  (norm_imp (! appctx_concat_l _) norm_refl) )
                            (sylbi id_concat_l
                            @ unfold_r_top_word_r @ orrd
                            @ sylbir id_concat_r
                            @ framing_concat_r
                            @ unfold_r_top_word_r orl)
                          )
                    )
                    @ wrap ( norm ( norm_sym  (norm_imp (! appctx_concat_l _) norm_refl) )
                           @ unfold_r_top_word_r @ orrd
                           @ sylbir (bicom assoc_concat) @ framing_concat_r
                           @ norm (norm_imp (norm_trans appctx_concat_l norm_refl) norm_refl)
                           @ ctximp_in_ctx_forward
                          )
                  ))
     ));
theorem inductive_domain_r_implies_l { X : SVar }
  : $(top_word_r X) -> (top_word_l X)$
  = (named '( kt_top_word_r
        ( unfold_r_top_word_l orl)
        ( norm (norm_imp appctx_concat_r norm_refl)
               (unwrap @ kt_top_word_l
                    (wrap @ norm ( norm_sym  (norm_imp appctx_concat_r norm_refl) )
                          @ sylbi id_concat_r
                          @ unfold_r_top_word_l @ orrd
                          @ sylbir id_concat_l
                          @ framing_concat_l
                          @ unfold_r_top_word_l orl
                    )
                    @ wrap @ norm ( norm_sym  (norm_imp appctx_concat_r norm_refl) )
                          @ unfold_r_top_word_l @ orrd
                          @ sylbir assoc_concat @ framing_concat_l
                          @ norm (norm_imp (norm_trans appctx_concat_r norm_refl) norm_refl)
                          @ ctximp_in_ctx_forward
               )
        )
     ));


--- Proof certificate implementation
------------------------------------

theorem top_implies_fp_init {X: SVar} (phi: Pattern)
    (he: $epsilon -> phi$)
    (hl:  $phi . top_letter -> phi$)
  : $top_word X -> phi$
= '( rsyl inductive_domain_r_implies_l @ kt_top_word_l he hl );

theorem top_implies_fp_leaf {box: SVar} (phi : Pattern box)
  : $( ctximp_app box (sVar box . top_letter) phi) . top_letter -> phi $
= '(norm (norm_imp appctx_concat_l norm_refl) ctximp_in_ctx_forward);

--- fp-implies-alpha
--------------------

theorem positive_in_fp_interior (phi_a phi_b: Pattern X)
  (p_a: $ _Positive X phi_a $)
  (p_b: $ _Positive X phi_b $):
  $ _Positive X (epsilon \/ (a . phi_a \/ b . phi_b )) $
  = '(positive_in_or positive_disjoint (positive_in_or (positive_in_concat positive_disjoint p_a)
                                                       (positive_in_concat positive_disjoint p_b)));

-- TODO(MirceaS): Can't this be relaxed to allow eBox to show up in some or all of the patterns?
theorem top_implies_fp_interior {X: SVar} {box: SVar} (fp_unf_a fp_unf_b fp_ctximp_a fp_ctximp_b: Pattern X box)
  (p_fp_unf_a: $ _Positive X fp_unf_a $)
  (p_fp_unf_b: $ _Positive X fp_unf_b $)
  (p_fp_ctximp_a: $ _Positive X fp_ctximp_a $)
  (p_fp_ctximp_b: $ _Positive X fp_ctximp_b $)

  (he_a: $epsilon -> s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_a$)
  (he_b: $epsilon -> s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_b$)
  (ha: $((s[ (ctximp_app box (sVar box . top_letter) (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b))))) / X ] fp_ctximp_a) . top_letter)
          -> (s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_a)$)
  (hb: $((s[ (ctximp_app box (sVar box . top_letter) (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b))))) / X ] fp_ctximp_b) . top_letter)
          -> (s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_b)$)
  : ------------------------
  $(mu X (epsilon \/ ((a . fp_ctximp_a) \/ (b . fp_ctximp_b)))) . top_letter -> (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b))))$
  = (id
    '(unwrap_subst appctx_concat_l
    @ KT_subst (positive_in_fp_interior p_fp_ctximp_a p_fp_ctximp_b) ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$)
    @ eori
      ( wrap_subst appctx_concat_l
        @ rsyl (anl regex_eq_eps_concat_l)
        @ unfold_r (positive_in_fp_interior p_fp_unf_a p_fp_unf_b)
        @ norm (norm_sym @ norm_imp_r ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$))
        @ orrd
        @ orim
          (rsyl (anr regex_eq_eps_concat_r) @ framing_concat_r he_a)
          (rsyl (anr regex_eq_eps_concat_r) @ framing_concat_r he_b))
    @ eori
      ( wrap_subst appctx_concat_l
        @ rsyl (bi1i @ assoc_concat)
        @ unfold_r (positive_in_fp_interior p_fp_unf_a p_fp_unf_b)
        @ norm (norm_sym @ norm_imp_r ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$))
        @ orrd @ orld
        @ framing_concat_r ha)
      ( wrap_subst appctx_concat_l
        @ rsyl (bi1i @ assoc_concat)
        @ unfold_r (positive_in_fp_interior p_fp_unf_a p_fp_unf_b)
        @ norm (norm_sym @ norm_imp_r ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$))
        @ orrd @ orrd
        @ framing_concat_r hb)
    ));



--- Apply equivalence left to right
theorem apply_equiv (eq: $phi <-> psi$) (cont: $rho -> psi$): $rho -> phi$
  = '(syl (bi2i eq) cont);

theorem fp_implies_regex_leaf :
    $rho -> rho$ = 'id;

theorem fp_implies_regex_interior {X: SVar} (phi_a phi_b: Pattern X)
    (posa: $ _Positive X phi_a $)
    (posb: $ _Positive X phi_b $)
    (he: $epsilon -> rho$)
    (ha: $s[ rho / X ] phi_a -> (derivative a rho)$)
    (hb: $s[ rho / X ] phi_b -> (derivative b rho)$):
    ----------------------------------------------
    $(mu X (epsilon \/ ((a . phi_a) \/ (b . phi_b)))) -> rho$ =
    '(KT
      (positive_in_or positive_disjoint @ positive_in_or (positive_in_concat positive_disjoint posa) (positive_in_concat positive_disjoint posb)) @
      apply_equiv der_equality_bi_concrete (norm
        (norm_imp_l @ norm_sym @ _sSubst_or sSubstitution_disjoint @ _sSubst_or (sSubst_concat_r norm_refl) (sSubst_concat_r norm_refl))
        (orim (iand id he) @ orim (framing_concat_r ha) (framing_concat_r hb))
      ));