proposition: Lemma horpo_monotonous : algebraic_monotonicity horpo.
proof: Proof. apply algebraic_monotonicity_criterion; intros. unfold appMonCond; intros. destruct H1 as [P | [P | P]]. destruct P as [Mnfa [M'nfa [L_red R_eq]]]. constructor; trivial. apply app_type_eq with Mapp M'app; try_solve. apply horpo_type_preserving; trivial. rewrite <- (appBodyR_env M Mapp), <- (appBodyR_env M' M'app). try_solve. apply HApp with Mapp M'app; trivial. constructor; apply pair_mOrd_left; trivial. apply horpo_eq_compat'. right; trivial. destruct P as [Mnfa [M'nfa [L_eq R_red]]]. constructor; trivial. apply app_type_eq with Mapp M'app; try_solve. apply horpo_type_preserving; trivial. rewrite <- (appBodyR_env M Mapp), <- (appBodyR_env M' M'app). apply horpo_env_preserving; trivial. apply HApp with Mapp M'app; trivial. constructor; apply pair_mOrd_right; trivial. apply horpo_eq_compat'. right; trivial. destruct P as [Mfa [MM'head [l [m [m' [Margs [M'args mm']]]]]]]. constructor; trivial. apply eq_unitTypes_eq_types. rewrite (app_units_app M Mapp), (app_units_app M' M'app). simpl; rewrite Margs, M'args, !length_app; trivial. intros. rewrite (app_units_app M Mapp) in H1. rewrite (app_units_app M' M'app) in H2. destruct p. inversion H1; inversion H2. rewrite MM'head; trivial. simpl in H1; simpl in H2. rewrite Margs in H1. rewrite M'args in H2. destruct (Compare_dec.le_lt_dec (length (fst l)) p). rewrite nth_app_right in H1; trivial. rewrite nth_app_right in H2; trivial. destruct ((p - length (fst l))%nat). inversion H1; inversion H2. rewrite <- H4, <- H5. apply horpo_type_preserving; trivial. inversion H1; inversion H2; try_solve. rewrite nth_app_left in H1; trivial. rewrite nth_app_left in H2; trivial. inversion H1; inversion H2; try_solve. rewrite <- (@appUnit_env m M), <- (@appUnit_env m' M'). apply horpo_env_preserving; trivial. apply appArg_is_appUnit. unfold isArg; rewrite M'args; auto with datatypes. apply appArg_is_appUnit. unfold isArg; rewrite Margs; auto with datatypes. destruct (funApp_head M Mfa). apply HMul with x; trivial. rewrite <- MM'head; trivial. rewrite Margs, M'args. constructor; apply mulOrd_oneElemDiff; trivial. apply horpo_eq_compat'. unfold absMonCond; intros. constructor; trivial. apply abs_type_eq with Nabs N'abs; trivial. apply horpo_type_preserving; trivial. set (w := horpo_env_preserving H2). rewrite !absBody_env in w. inversion w; trivial. apply AlgAbs with Nabs; trivial. apply AlgAbs with N'abs; trivial. apply HAbs with Nabs N'abs; trivial. Qed.
imports: CoLoR(RelExtras ListExtras RelUtil Terms MultisetOrder PairLex MultisetList MultisetTheory AccUtil LogicUtil) Coq(Morphisms Basics)