proposition: Lemma transp_SPO_to_mult_SPO : forall us, (forall u, In u us -> ((forall t s, transp r u t -> transp r t s -> transp r u s) /\ (transp r u u -> False))) -> (forall ts ss, mult us ts -> mult ts ss -> mult us ss) /\ (mult us us -> False).
proof: Proof. intros us Hsub; unfold mult, MultisetLT, transp; split. intros ts ss. assert (Hsub' : forall p, p in (list2multiset us) -> forall x y, r x p -> r y x -> r y p). intros p p_in_us x y H H'. elim (member_multiset_list us p_in_us); intros p' p'_in_us p'eq. apply r_eqA_compat with y p'; auto with multisets. auto with sets. auto with sets. elim (Hsub p' p'_in_us); intros Hsub' Hsub''; gen (Hsub' x y); unfold transp; simpl; clear Hsub'; intro Hsub'; apply Hsub'; trivial. apply r_eqA_compat with x p; auto with multisets. auto with sets. intros; apply (sub_transp_trans_2_mOrd_trans Hsub') with (list2multiset ts); trivial. intro HM; inversion HM. assert (H' : X =mul= Y). apply meq_union_meq with Z. rewrite (union_comm X Z), (union_comm Y Z), <- H1, <- H0. auto with multisets. assert (H'' : forall (x : A), x in X -> ex (fun (x' : A) => x' in X /\ r x' x)). intros x x_in_X; assert (x_in_Y : x in Y). rewrite <- H'; trivial. elim (H2 x x_in_Y); intros x' Hx'1 Hx'2. exists x'; split; trivial. assert (Htrans : forall x, x in X -> forall y z, r y x -> r z y -> r z x). intros x x_in_X; assert (x_in_us : In x us). assert (x_in_usM : x in (list2multiset us)). rewrite H0, (union_comm Z X); apply member_member_union; trivial. elim (member_multiset_list us x_in_usM); intros; apply In_eqA_compat with x0; trivial. elim (Hsub x x_in_us); intros H3 H4; unfold transp in H3; simpl in H3; apply H3. elim (self_dom2 X H Htrans H''); intros x Hx. elim Hx; clear Hx; intros Hx1 Hx2. assert (x_in_us : In x us). assert (x_in_usM : x in (list2multiset us)). rewrite H0, (union_comm Z X); apply member_member_union; trivial. elim (member_multiset_list us x_in_usM); intros; apply In_eqA_compat with x0; trivial. elim (Hsub x x_in_us); intros H3 H4; unfold transp in H4; simpl in H4; apply H4; trivial. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)