proposition: Lemma rt_closure_aux'_spec: forall f Hwf n acc, approx f acc -> approx f (@rt_closure_aux' f Hwf n acc) /\ forall i, StateMap.In i acc \/ i=n -> StateMap.In i (@rt_closure_aux' f Hwf n acc).
proof: Proof. intros. unfold rt_closure_aux'. case_eq (rt_closure_aux Hwf n acc); intros acc' p H'. apply rt_closure_aux_spec in H'; auto. split. apply H'. intros i [Hi| ->]; simpl. apply H', Hi. exists p. apply H'. 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(Utils_WF) Coq(Relations) Coq(Eqdep_dec)