proposition: Lemma horpo_conv_comp_aux : forall M N M' N' Q, (forall L L' R R' Q, (subterm L M \/ (L = M /\ subterm R N)) -> L ~(Q) L' -> R ~(Q) R' -> L >> R -> env L' = env R' -> L' >> R' ) -> M ~(Q) M' -> N ~(Q) N' -> M >> N -> env M' = env N' -> M' >> N'.
proof: Proof. intros M N M' N' Q IH MM' NN' MN M'N'. destruct MN as [M N MNtype MNenv Mnorm Nnorm M_N]. constructor; trivial. rewrite <- (terms_conv_eq_type (conv_by MM')), <- (terms_conv_eq_type (conv_by NN')). trivial. rewrite <- (conv_by MM'); trivial. rewrite <- (conv_by NN'); 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]. destruct (conv_arg Msub MM') as [Nsub [Nsub_arg MN]]; trivial. constructor 1. rewrite <- (conv_by MM'); trivial. exists Nsub; trivial. destruct Cond as [Msub N Msub_N | Msub]. constructor. apply (IH Msub Nsub N N' Q); trivial. left; apply arg_subterm; trivial. rewrite (appUnit_env Nsub M'); auto with terms. replace N' with Nsub. constructor 2. apply term_eq. rewrite (appUnit_env Nsub M'); auto with terms. apply conv_term_unique with (term Msub) Q; fo. constructor 2 with f g; trivial. destruct (appHead_conv MM'). rewrite Mf in H; inversion H; trivial. destruct (appHead_conv NN'). rewrite Ng in H; inversion H; trivial. apply horpo_args_conv with M (appArgs N) Q; trivial. intros; rewrite (appUnit_env MsX N); auto with terms. intros; rewrite (appUnit_env NsX N'); auto with terms. apply appArgs_conv; trivial. intros. apply IH with L R Q; trivial. destruct H; auto. right; destruct H; split; trivial. apply arg_subterm; trivial. constructor 3 with f. destruct (appHead_conv MM'). rewrite Mf in H; inversion H; trivial. destruct (appHead_conv NN'). rewrite Nf in H; inversion H; trivial. constructor. assert (arg_env: forall x y, isArg x M' -> isArg y N' -> env x = env y). intros. rewrite (@appUnit_env x M'), (@appUnit_env y N'); trivial. apply appArg_is_appUnit; trivial. apply appArg_is_appUnit; trivial. apply mord_list_sim with (fun L R => L ~(Q) R) (appArgs M) (appArgs N); auto. apply horpo_eq_compat'. unfold order_compatible. intros; split; intro. apply IH with x y Q; try_solve. left; apply arg_subterm; trivial. apply term_eq; try_solve. apply conv_term_unique with (term y) Q. unfold eqA in H5; unfold TermsEqset.eqA in H5; rewrite <- H5. destruct H1; trivial. destruct H4; trivial. unfold eq_compat; intros. apply term_eq. rewrite (appUnit_env y M'), (appUnit_env y' N'); trivial. apply appArg_is_appUnit; trivial. apply appArg_is_appUnit; trivial. apply conv_term_unique with (term x) Q; destruct H2; destruct H3; trivial. apply appArgs_conv; trivial. apply appArgs_conv; trivial. inversion MNargs; trivial. destruct (partialFlattening_conv Ns NN') as [Ns' [Ns'N' NsNs']]; trivial. constructor 4 with Ns'; trivial. rewrite <- (conv_by MM'); trivial. apply horpo_args_conv with M Ns Q; trivial. intros; rewrite (partialFlattening_env N Ns); auto. intros; rewrite (partialFlattening_env N' Ns'); auto. intros. apply IH with L R Q; trivial. destruct H; auto. right; destruct H; split; trivial. apply partialFlattening_subterm with Ns; trivial. assert (M'app: isApp M'). assert (MeqM' : M ~ M') by (exists Q; trivial). rewrite <- MeqM'; trivial. assert (N'app: isApp N'). assert (NeqN' : N ~ N') by (exists Q; trivial). rewrite <- NeqN'; trivial. assert (L_L: appBodyL Mapp >> appBodyL Napp -> appBodyL M'app >> appBodyL N'app). intro MN. apply IH with (appBodyL Mapp) (appBodyL Napp) Q; trivial. left; apply appBodyL_subterm. apply app_conv_app_left_aux; trivial. apply app_conv_app_left_aux; trivial. autorewrite with terms using trivial. assert (R_R: appBodyR Mapp >> appBodyR Napp -> appBodyR M'app >> appBodyR N'app). intro MN. apply IH with (appBodyR Mapp) (appBodyR Napp) Q; trivial. left; apply appBodyR_subterm. apply app_conv_app_right_aux; trivial. apply app_conv_app_right_aux; trivial. autorewrite with terms using trivial. constructor 5 with M'app N'app. intro M'fapp. absurd (isFunApp M); trivial. assert (MeqM' : M ~ M') by (exists Q; trivial). rewrite MeqM'; trivial. intro N'fapp. absurd (isFunApp N); trivial. assert (NeqN' : N ~ N') by (exists Q; trivial). rewrite NeqN'; trivial. set (w := horpo_eq_compat). destruct (horpo_app M N Mapp Napp MNtype LL) as [left [right [Lred | Rred]]]. constructor; apply pair_mOrd_left; trivial. apply horpo_eq_compat'. apply L_L; trivial. apply horpo_RC. inversion right. left; apply R_R; trivial. replace (appBodyR N'app) with (appBodyR M'app). right. apply term_eq. autorewrite with terms using trivial. apply conv_term_unique with (term (appBodyR Mapp)) Q. destruct (app_conv_app_right_aux Mapp M'app MM'); trivial. rewrite H1. destruct (app_conv_app_right_aux Napp N'app NN'); trivial. constructor; apply pair_mOrd_right; trivial. apply horpo_eq_compat'. apply horpo_RC. inversion left. left; apply L_L; trivial. replace (appBodyL N'app) with (appBodyL M'app). right. apply term_eq. autorewrite with terms using trivial. apply conv_term_unique with (term (appBodyL Mapp)) Q. destruct (app_conv_app_left_aux Mapp M'app MM'); trivial. rewrite H1. destruct (app_conv_app_left_aux Napp N'app NN'); trivial. apply R_R; trivial. assert (M'abs: isAbs M'). assert (MeqM' : M ~ M') by (exists Q; trivial). rewrite <- MeqM'; trivial. assert (N'abs: isAbs N'). assert (NeqN' : N ~ N') by (exists Q; trivial). rewrite <- NeqN'; trivial. constructor 6 with M'abs N'abs. apply IH with (absBody Mabs) (absBody Nabs) (envSubst_lift1 Q); trivial. left; apply absBody_subterm. apply abs_conv_absBody_aux; trivial. apply abs_conv_absBody_aux; trivial. apply absBody_eq_env; trivial. rewrite <- (terms_conv_eq_type (conv_by MM')), <- (terms_conv_eq_type (conv_by NN')). trivial. apply HBeta. apply beta_conv_comp with M N Q; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)