proposition: Lemma invariant_prog : forall tarjan x y, invariant tarjan -> final x = final y -> invariant (DS.union tarjan x y).
proof: Proof. intros tarjan x y H Hxy. constructor. ti_auto. intros np nq H'. rewrite DS.sameclass_union in H'. assert (wlog : forall P Q : relation state, (forall x y, Q x y <-> Q y x) -> (forall x y, P x y -> Q x y) -> forall u v, (P u v \/ P v u) -> Q u v). clear. intros. destruct H1. apply H0. auto. rewrite H. apply H0. auto. destruct H' as [H' | H']. apply H. auto. revert H'. generalize np nq. clear np nq. apply wlog. intros. intuition. intros. destruct H0. apply H in H0. apply H in H1. eauto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_StateSetSets) ATBR(Utils_WF) Coq(Relations) Coq(List)