proposition: Theorem correct: forall A HA, eNFA.bounded A -> NFA.eval (eNFA_to_NFA A HA) == eNFA.eval A.
proof: Proof. intros [size eps delta initial final max_label] Hwf Hb. apply mx_to_scal_compat. simpl. symmetry. apply algebraic_correctness with (mx_bool tt (ns size) (ns size) (fun i j => StateSet.mem (sn j) (rt_closure (guard 100 Hwf) size (sn i)))). symmetry. apply rt_closure_star. intros. apply Hb. #[local] Transparent dot plus zero one equal. mx_intros i j Hi Hj. simpl. unfold labelling. fold_regex. setoid_rewrite sum_distr_left. rewrite sum_inversion. apply sum_compat. intros a Ha. simpl; fold_regex. unfold eNFA.delta, eNFA.deltamap, statelabelmap_set_to_fun. setoid_rewrite dot_xif_zero. setoid_rewrite dot_neutral_right. rewrite StateLabelMapProps.map_o. unfold numota_of_nat. StateLabelMapProps.find_analyse; simpl; fold_regex. rewrite mem_set_closure. match goal with |- context [StateSet.exists_ ?f ?p] => set (e:=StateSet.exists_ f p) end. apply leq_antisym. case_eq e; intros Hj'; trivial with algebra. apply leq_sum. subst e; apply <- StateSetProps.exists_iff in Hj'. destruct Hj' as [n [Hnx Hjn]]. exists (ns n); repeat split; auto with arith. simpl. rewrite <- lt_nat_spec. apply (delta_bounded Hb H Hnx). apply StateSet.mem_1 in Hnx. rewrite 2id_num. rewrite Hnx. unfold statesetelt_of_nat in Hjn. rewrite Hjn. reflexivity. repeat intro. psubst. reflexivity. apply sum_leq. intros n _ Hn. apply xif_bool_incr. bool_connectors. intros [Hnx Hjn]. apply -> StateSetProps.exists_iff. 2: repeat intro; psubst; reflexivity. exists (sn n); split; assumption. symmetry. rapply sum_fun_zero. mx_intros i j Hi Hj. simpl; fold_regex. rewrite (sum_collapse (n:=ns initial)). simpl. bool_simpl. simpl. fold_regex. unfold statesetelt_of_nat. auto with algebra. apply -> lt_nat_spec. apply Hb. simpl. intros k Hk. nat_analyse. simpl. fold_regex. auto with algebra. mx_intros i j Hi Hj. simpl. fold_regex. apply xif_compat; trivial. bool_simpl. rewrite bool_prop_iff. num_prop. nat_prop. num_lia. 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)