proposition: Lemma invariant_idem : forall tarjan x y, invariant tarjan -> {{tarjan}} x y -> invariant (DS.union tarjan x y).
proof: Proof. intros tarjan x y H Hxy. assert (Hprog : forall np nq, {{DS.union tarjan x y}} np nq -> {{tarjan}} np nq). intros np nq H'. rewrite DS.sameclass_union in H'. intuition; symmetry. rewrite H0, Hxy. assumption. rewrite H2, <- Hxy. assumption. constructor. ti_auto. intros np nq H'. apply Hprog in H'. apply H; auto. 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)