proposition: Lemma lt_decomp : forall s t, lt s t -> ((ex (fun f => ex (fun g => ex (fun ss => ex (fun ts => ltF f g /\ (forall s, In s ss -> lt s (Fun g ts)) /\ s = Fun f ss /\ t = Fun g ts ))))) \/ ex (fun f => ex (fun g => ex (fun ss => ex (fun ts => f =F= g /\ (forall s, In s ss -> lt s (Fun g ts)) /\ tau f lt ss ts /\ s = Fun f ss /\ t = Fun g ts))))) \/ ex (fun f => ex (fun ts => ex (fun t' => In t' ts /\ (s = t' \/ lt s t')) /\ t = Fun f ts)).
proof: Proof. intros s t Hst. unfold lt in Hst; inversion Hst as [f'' g'' ss' ts'' ltFfg Hsi' | f'' g'' feq ss' ts'' Hss'ts' Hsi' | f'' s' ts'' Hex]; subst. left; left. exists g''; exists f''; exists ts''; exists ss'. split; trivial; repeat split; trivial. left; right. exists g''; exists f''; exists ts''; exists ss'. split; elim feq; trivial; repeat split; trivial. intros t t_in_ts''. assert (IN_compat : forall ss x x', In x' ss -> x =A= x' -> In x ss). unfold eqA; intros; subst; trivial. elim (mult2element (transp lt_mpo) IN_compat ts'' ss' Hss'ts' t t_in_ts''). intros s Hs; elim Hs; clear Hs; intros s_in_ss Hs. apply mpo3; exists s; split; trivial. right. exists s'; exists ts''. split; trivial; elim Hex; clear Hex; intros t Ht. elim Ht; clear Ht; intros t_in_ts Ht. exists t; split; trivial. elim Ht; [left; subst | right]; trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations) CoLoR(VRPO_Type)