proposition: Lemma bounded: forall A HA, eNFA.bounded A -> NFA.bounded (eNFA_to_NFA A HA).
proof: Proof. intros [size eps delta initial final max_label] Hwf Hb. unfold eNFA_to_NFA. constructor; simpl. intros a i j Hj. unfold statelabelmap_set_to_fun in Hj. rewrite StateLabelMapProps.map_o in Hj. StateLabelMapProps.find_analyse; simpl in Hj. 2: StateSetProps.setdec. apply StateSet.mem_1 in Hj. rewrite mem_set_closure in Hj. rewrite <- StateSetProps.exists_iff in Hj by (repeat intro; psubst; reflexivity). destruct Hj as [n [Hnx Hjn]]. eapply rt_closure_bounded. 3: apply StateSet.mem_2, Hjn. intros. apply Hb. apply (delta_bounded Hb H Hnx). intros i Hi. eapply rt_closure_bounded. 3: apply Hi. 2: apply Hb. clear i Hi. intros i Hi. apply Hb. intros i. StateSetProps.set_iff. intro Hi. psubst. apply Hb. 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)