proposition: Lemma merge_bounded: forall A B, bounded A -> bounded B -> bounded (merge_DFAs A B).
proof: Proof. intros A B HA HB. constructor. intros a i. simpl. case_eq (pimatch i); intros p Hp. apply below_max_pi0. apply (bounded_delta HA). apply below_max_pi1. apply (bounded_delta HB). rewrite lt_nat_spec. apply Nat.le_lt_trans with (nat_of_state (pi0 (delta A 0 0))). apply Nat.le_0_l. rewrite <- lt_nat_spec. rapply below_max_pi0. apply (bounded_delta HA). unfold finaux, merge_DFAs. apply NumSetProps.Props.fold_rec_nodep. apply NumSetProps.Props.fold_rec_nodep. intro i. NumSetProps.setdec. intros p a Hp IH x. NumSetProps.set_iff. intuition. subst. apply below_max_pi1. apply HB, Hp. intros p a Hp IH x. NumSetProps.set_iff. intuition. subst. apply below_max_pi0. apply HA, Hp. 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)