proposition: Lemma argsComp_appComp_aux : forall Px: pair, (forall Py: pair, Py <lex Px -> forall M, algebraic M -> term (appHead M) = ^fst Py -> appArgs M = proj1_sig (snd Py) -> CompH M) -> forall M N, algebraic M -> term (appHead M) = ^fst Px -> appArgs M = proj1_sig (snd Px) -> (forall N', subterm N' N -> M >> N' -> CompH N') -> M >> N -> CompH N.
proof: Proof. intros Px IH_out M N Mnorm Mhead Margs IH_in MN. destruct Px as [f fArgs]; simpl in * . destruct MN as [M N eqTypeMN eqEnvMN _ Nnorm horpoMN]. destruct horpoMN as [ M N _ Msub | M N f' g Mhead' Nhead f'_gt_g Margs_gt_N | M N f' Mhead' Nhead argsM_mul_argsN | M N Ns Napp Ns_flat_N Margs_Ns | M N Mapp' Napp Mhead' Margs_mul_Nargs | M N Mabs Nabs _ | M N MNbeta ]. destruct Msub as [M' M'arg M'_ge_N]. assert (M'comp: CompH M'). apply (proj2_sig fArgs); rewrite <- Margs; exact M'arg. destruct M'_ge_N as [M' N M'_N | M']. unfold CompH; apply horpo_comp_step_comp with M'; auto with horpo. trivial. assert (argsNcomp: CompTerms (appArgs N)). apply compTerms with M N; trivial. rewrite Margs; exact (proj2_sig fArgs). intros; apply appUnit_subterm; auto with terms. term_inv N. set (Nmul := exist argsNcomp). apply IH_out with (Py := (g, Nmul)); auto with terms. assert (ff': f = f'); [congruence | idtac]. constructor 1; rewrite ff'; auto with terms. inversion argsM_mul_argsN as [aM aN argsM_horpo_argsN aMdef aNdef]. assert (argsNcomp: CompTerms (appArgs N)). unfold CompTerms; intros n n_arg_N. assert (n_in_N: n in (list2multiset (appArgs N))). apply member_list_multiset; trivial. destruct (mOrd_elts_ge argsM_horpo_argsN n_in_N) as [m m_in_M [m_gt_n | m_eq_n]]. apply horpo_comp_step_comp with m. apply (proj2_sig fArgs); rewrite <- Margs. apply arg_mul_arg; trivial. trivial. unfold eqA in m_eq_n; unfold TermsEqset.eqA in m_eq_n; rewrite <- m_eq_n. apply (proj2_sig fArgs); rewrite <- Margs. apply arg_mul_arg; trivial. set (Nmul := exist argsNcomp). assert (NfApp: isFunApp N). unfold isFunApp; apply funS_is_funS with f'; trivial. apply IH_out with (Py := (f', Nmul)); auto with terms. constructor 2. assert (ff': f = f'); [congruence | rewrite ff'; auto with sets]. unfold H_WFmul_ord.gtA, H_WFterms_lt, WFterms_to_mul, horpo_mul_lt, MultisetLT, transp. simpl; apply mOrd_inclusion with horpo. intros x y x_y; trivial. rewrite <- Margs; trivial. assert (Ns_comp: CompTerms Ns). apply compTerms with M N; trivial. rewrite Margs; exact (proj2_sig fArgs). intros; apply partialFlattening_subterm with Ns; trivial. unfold CompH; apply horpo_comp_pflat with Ns; trivial. absurd (isFunApp M); eauto with terms. rewrite appHead_notApp in Mhead; term_inv M. assert (Napp: isApp N). apply app_beta_isapp with M f; trivial. assert (Mapp: isApp M). term_inv M. apply beta_notFunS with Tr N; unfold Tr; auto with terms. assert (NargsComp: CompTerms (appArgs N)). unfold CompTerms; intros P P_arg_N. case (app_beta_args_eq P Mapp MNbeta Mhead P_arg_N). intro Parg. apply (proj2_sig fArgs P). rewrite <- Margs; exact Parg. destruct 1 as [Mb Mb_P M_Mb]. unfold CompH; apply horpo_comp_step_comp with Mb. apply (proj2_sig fArgs); rewrite <- Margs; trivial. apply beta_imp_horpo; trivial. apply algebraic_arg with M; trivial. set (Nmul := exist NargsComp). fold CompH; apply IH_out with (Py := (f, Nmul))(M := N); auto with terms. constructor 2. auto with sets. destruct (app_beta_args Mapp MNbeta Mhead) as [[al ar] [[tl tr] [tlM [trN [tltr [Mb_args Nb_args]]]]]]. unfold H_WFmul_ord.gtA, transp, H_WFterms_lt, horpo_mul_lt, MultisetLT, transp, WFterms_to_mul; simpl in * . rewrite <- Margs, Mb_args, Nb_args. apply mulOrd_oneElemDiff. apply horpo_eq_compat'. refl. apply beta_imp_horpo; trivial. apply algebraic_arg with M; trivial. apply app_beta_headSymbol with M; trivial. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)