proposition: Lemma epsilonbrel_add_one: forall i j A s t, epsilonbrel (add_one i j A) s t = epsilonbrel A s t || eq_state_bool i s && eq_state_bool j t.
proof: Proof. intros. destruct A. unfold epsilonbrel, epsilonfun, add_one, augment, statemap_set_to_fun. simpl. repeat StateMapProps.find_analyse; simpl; StateMapProps.find_tac; bool_simpl; simpl; trivial. rewrite eqb_eq_nat_bool. apply orb_comm. num_analyse; bool_simpl; trivial; subst; auto. num_analyse; bool_simpl; trivial; subst; auto. rewrite eqb_eq_nat_bool. trivial. apply <- bool_prop_iff; bool_connectors; intuition. num_prop. subst. auto. apply <- bool_prop_iff; bool_connectors; intuition. num_prop. subst. auto. 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(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)