proposition: Lemma in_delta_set: forall j p b, StateSet.In j (delta_set b p) <-> exists k, StateSet.In k p /\ StateSet.In j (delta b k).
proof: Proof. unfold delta_set; split. apply StateSetProps.Props.fold_rec_nodep. StateSetProps.setdec. intros i a Hip IH. StateSetProps.set_iff. intros [Hi|Hi]; eauto. intros [i [Hip Hj]]. revert Hip. apply (StateSetProps.Props.fold_rec_bis (P:=fun p a => StateSet.In i p -> StateSet.In j a)); StateSetProps.setdec. 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_StateSetSets) ATBR(Numbers) ATBR(Utils_WF)