proposition: Theorem rt_closure_spec: forall f Hwf size i, below i size -> forall j, steps f i j <-> StateSet.In j (@rt_closure f Hwf size i).
proof: Proof. intros f Hwf size i Hi j. pose proof (rt_closure_prespec Hwf size (acc:=StateMap.empty _)) as H. apply apply in H. destruct H as [Happrox Hin]. eapply apply in Hin; eauto. destruct Hin as [p Hip]. specialize (Happrox _ _ Hip). unfold valid in Happrox. rewrite <- Happrox. apply -> StateMapProps.find_mapsto_iff in Hip. unfold rt_closure, statemap_set_to_fun. rewrite Hip. reflexivity. clear. intros j acc. StateMapProps.map_iff. tauto. 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)