proposition: Lemma correct_ind_idem : forall x y tarjan, {{tarjan}} x y -> invariant tarjan -> correct_ind tarjan ( DS.union tarjan x y ) x y.
proof: Proof. intros x y tarjan Hxy Hstat. constructor. assert (heq : tarjan [=T=] DS.union tarjan x y). apply DSUtils.eq_union, Hxy. unfold prog. intros. exact (diag_compat_left heq H). apply DSUtils.le_union. rewrite measure_union_idem; trivial. rewrite DS.sameclass_union. 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)