proposition: Lemma horpo_subst_stable_aux : forall M N G (MG: correct_subst M G) (NG: correct_subst N G), algebraicSubstitution G -> (forall L R G (LG: correct_subst L G) (RG: correct_subst R G), algebraicSubstitution G -> (subterm L M \/ (L = M /\ subterm R N)) -> L >> R -> subst LG >> subst RG) -> M >> N -> subst MG >> subst NG.
proof: Proof. intros M N G MG NG Gnorm IH MN. destruct MN as [M N MNtype MNenv Mnorm Nnorm M_N]. constructor; trivial. autorewrite with terms; trivial. autorewrite with terms; congruence. apply algebraic_subst; trivial. apply algebraic_subst; trivial. destruct M_N as [ M N MFapp Cond | M N f g Mf Ng f_g M_Nargs | M N f Mf Nf MNargs | M N Ns Mfapp NsN MNs | M N Mapp Napp Mnfapp Nnfapp LL | M N Mabs Nabs MN | M N MNbeta]. destruct Cond as [Msub Msub_arg Cond]. constructor 1. apply funApp_subst_funApp; trivial. destruct (subst_arg Msub MG Msub_arg) as [M'sub [M'sub_arg [M'subG M'sub_def]]]. exists M'sub; trivial. destruct Cond as [Msub N Msub_N | Msub]. constructor. rewrite M'sub_def. apply IH; trivial. left; apply arg_subterm; trivial. replace (subst NG) with M'sub. constructor 2. rewrite M'sub_def. apply term_eq. autorewrite with terms; congruence. autorewrite with terms; trivial. constructor 2 with f g; trivial. apply funS_headS_subst; trivial. apply funS_headS_subst; trivial. apply horpo_args_subst with (appArgs N); trivial. apply subst_list_args. apply funS_is_funS with g; trivial. intros. apply IH; trivial. destruct H; auto. right; destruct H; split; trivial. apply arg_subterm; trivial. constructor 3 with f. apply funS_headS_subst; trivial. apply funS_headS_subst; trivial. constructor. set (P := fun L R => exists LG: correct_subst L G, R = subst LG). apply mord_list_sim with P (appArgs M) (appArgs N); auto. apply horpo_eq_compat'. unfold order_compatible; intros. inversion H1; inversion H4. rewrite H5, H6. split; intros. apply IH; trivial. left; apply arg_subterm; trivial. unfold eqA in H7; unfold TermsEqset.eqA in H7. apply term_eq; autorewrite with terms using try rewrite H7; trivial. unfold eq_compat; intros. destruct H2; rewrite H2. destruct H3; rewrite H3. apply term_eq; autorewrite with terms using trivial. unfold P; apply subst_list_args. apply funS_is_funS with f; trivial. unfold P; apply subst_list_args. apply funS_is_funS with f; trivial. inversion MNargs; trivial. destruct (subst_list_partialFlattening Ns NG NsN) as [Ns' [Ns'N' NsNs']]. constructor 4 with Ns'; trivial. apply funApp_subst_funApp; trivial. apply horpo_args_subst with Ns; trivial. intros. apply IH; trivial. destruct H; auto. right; destruct H; split; trivial. apply partialFlattening_subterm with Ns; trivial. set (M'app := app_subst_app Mapp MG). set (N'app := app_subst_app Napp NG). destruct (app_subst Mapp MG) as [ML MR]. destruct (app_subst Napp NG) as [NL NR]. assert (L_L: appBodyL Mapp >> appBodyL Napp -> appBodyL M'app >> appBodyL N'app). intro MN. unfold M'app; rewrite ML. unfold N'app; rewrite NL. apply IH; trivial. left; apply appBodyL_subterm. assert (R_R: appBodyR Mapp >> appBodyR Napp -> appBodyR M'app >> appBodyR N'app). intro MN. unfold M'app; rewrite MR. unfold N'app; rewrite NR. apply IH; trivial. left; apply appBodyR_subterm. constructor 5 with M'app N'app. apply notFunApp_subst; trivial. apply notFunApp_subst; trivial. set (w := horpo_eq_compat). destruct (horpo_app M N Mapp Napp MNtype LL) as [LrL [RrR [Ls | Rs]]]. constructor; apply pair_mOrd_left; trivial. apply horpo_eq_compat'. apply L_L; trivial. inversion RrR. left; trivial. apply R_R; trivial. right; apply term_eq. autorewrite with terms; rewrite MNenv; trivial. destruct (app_subst Mapp MG). rewrite (app_proof_irr (subst MG) M'app (app_subst_app Mapp MG)), H2. destruct (app_subst Napp NG). rewrite (app_proof_irr (subst NG) N'app (app_subst_app Napp NG)), H4. autorewrite with terms; rewrite H1; trivial. constructor; apply pair_mOrd_right; trivial. apply horpo_eq_compat'. inversion LrL. left; trivial. apply L_L; trivial. right; apply term_eq. autorewrite with terms; rewrite MNenv; trivial. destruct (app_subst Mapp MG). rewrite (app_proof_irr (subst MG) M'app (app_subst_app Mapp MG)), H0. destruct (app_subst Napp NG). rewrite (app_proof_irr (subst NG) N'app (app_subst_app Napp NG)), H3. autorewrite with terms; rewrite H1; trivial. apply R_R; trivial. constructor 6 with (abs_subst_abs Mabs MG) (abs_subst_abs Nabs NG). destruct (abs_subst Mabs MG) as [M'type M'body]. destruct (abs_subst Nabs NG) as [N'type N'body]. rewrite M'body, N'body. apply IH; trivial. apply algebraicSubstitution_cons_none. apply algebraicSubstitution_lifted; trivial. left; apply absBody_subterm. apply HBeta. apply beta_subst_stable. hyp. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)