proposition: Lemma transitive_lt_mpo : forall u t s : term, lt_mpo u t -> lt_mpo t s -> lt_mpo u s.
proof: Proof. intro u; induction u as [x | h us HInd1] using term_ind_forall2. intros t s H1 H2. inversion H1 as [ | |x' g ts H eq1 eq2]; subst. elim H; clear H; intros t Ht; elim Ht; clear Ht; intros t_in_ts Ht. cut (le_mpo (Var x) s); [intro H ; elim H; clear H; intro H; trivial | idtac]. subst; inversion H2. apply in_var. apply (var_in_s_in_terms_greater_than_s (Fun g ts) s); try right; trivial. exists t; split; trivial. elim Ht; clear Ht; intro Ht; [subst; constructor | apply var_in; trivial]. intro t; induction t as [x | g ts HInd2] using term_ind_forall2. intros t H1; inversion H1. intro s; induction s as [x | f ss HInd3] using term_ind_forall2. intros H1 H2; inversion H2. intros H1 H2. inversion H1 as [f' g' ss' ts' ltFfg Hsi | f' ss' ts' Hss'ts' Hsi | f' ss' t' Hex]; subst. inversion H2 as [g' h' ts' us' ltFgh Hti | g' ts' us' Hts'us' Hti | g' ts' u' Hex]; subst. apply mpo1. apply ltF_trans with g; hyp. intros u u_in_us. apply (HInd1 u u_in_us (Fun g ts)). apply (Hsi u u_in_us). hyp. apply mpo1. hyp. intros u u_in_us. apply (HInd1 u u_in_us (Fun f ts)). apply (Hsi u u_in_us). hyp. elim Hex; intros s Hs2; elim Hs2; clear Hs2; intros s_in_ss Hs2. gen (HInd3 s s_in_ss); intro HInd3'. apply (mpo3 (Fun h us) f ss). exists s. split; trivial. right. elim Hs2; clear Hs2; intro Hs2. subst s; hyp. apply HInd3'; hyp. gen (mult2element (transp lt_mpo) IN_eqA_compat us ts Hss'ts'); intro Hss. inversion H2 as [g' h' ts' us' ltFgh Hti | g' ts' us' Hts'us' Hti | g' ts' us' Hex]; subst. apply mpo1. hyp. intros u u_in_us. apply (HInd1 u u_in_us (Fun g ts)); trivial. elim (Hss u u_in_us). intros t Ht; elim Ht; clear Ht; intros t_in_ts Ht. apply mpo3. exists t. split; trivial. apply mpo2. apply transp_trans_to_mult_trans with ts; trivial. apply tlt_mpo_eqA_compat. elim Hex; clear Hex; intros s Hs2; elim Hs2; clear Hs2; intros s_in_ss Hs2. gen (HInd3 s s_in_ss H1); intro HInd3'. apply (mpo3 (Fun g us) f ss). exists s. split; trivial. right. elim Hs2; clear Hs2; intro Hs2. subst s; hyp. apply HInd3'; hyp. elim Hex; clear Hex; intros ti Hti; elim Hti; clear Hti; intros ti_in_ts Hti. inversion H2 as [g' h' ts' us' ltFgh Hti' | g' ts' us' Hts'us' Hti' | g' ts' us' Hex]; subst. elim Hti; clear Hti; intro Hti. rewrite <- Hti; apply (Hti' ti ti_in_ts). apply (HInd2 ti ti_in_ts (Fun f ss) Hti). apply (Hti' ti ti_in_ts). elim Hti; clear Hti; intro Hti. rewrite <- Hti; elim (mult2element (transp lt_mpo) IN_eqA_compat ts ss Hts'us' ti ti_in_ts). intros x Hx; elim Hx; clear Hx; intros x_in_ss Hx. apply mpo3. exists x; split; trivial. apply (HInd2 ti ti_in_ts (Fun f ss)); trivial. elim (mult2element (transp lt_mpo) IN_eqA_compat ts ss Hts'us' ti ti_in_ts). intros x Hx; elim Hx; clear Hx; intros x_in_ss Hx. apply mpo3. exists x; split; trivial. elim Hex; clear Hex; intros s Hs2; elim Hs2; clear Hs2; intros s_in_ss Hs2. apply mpo3. exists s. split; trivial. elim Hs2; clear Hs2; intro Hs2. subst s; right; hyp. right; apply (HInd3 s s_in_ss); trivial. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)