proposition: Lemma rt_closure_bounded: forall f Hwf size, (forall i, below i size -> setbelow (f i) size) -> forall i, below i size -> setbelow (@rt_closure f Hwf size i) size.
proof: Proof. intros f Hwf size H i Hi j Hj. rewrite <- rt_closure_spec in Hj by trivial. revert Hi. induction Hj; intro Hi; trivial. apply IHHj. apply (H x Hi). apply StateSet.mem_2, H0. 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)