proposition: Lemma argsComp_appComp_ind : forall (P: pair) M, algebraic M -> term (appHead M) = Fun (fst P) -> appArgs M = proj1_sig (snd P) -> CompH M.
proof: Proof. intro P. apply well_founded_ind with (R := LexProd_Lt) (P := fun (Px: pair) => forall M, algebraic M -> term (appHead M) = Fun (fst Px) -> appArgs M = proj1_sig (snd Px) -> CompH M). apply lexprod_wf. apply Prec.Ord_wf. apply wf_MulLt_WFterms. clear P. intros P IH_out M Mnorm Mhead Margs. assert (Mneutral: isNeutral M). term_inv M. rewrite_rl (horpo_neutral_comp_step Mnorm Mneutral). intros N; fold CompH. apply well_founded_ind with (R := subterm) (P := fun (N: Term) => M >> N -> CompH N). apply subterm_wf. clear N. intros N IH_in M_red_N. apply argsComp_appComp_aux with P M; trivial. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)