proposition: Lemma mem_set_closure: forall f i p, StateSet.mem i (set_closure f p) = StateSet.exists_ (fun j => StateSet.mem i (f j)) p.
proof: Proof. intros f i p. unfold set_closure. rewrite StateSetProps.exists_fold by (repeat intro; psubst; reflexivity). assert (StateSet.mem i StateSet.empty = false) by auto with set. revert H; generalize StateSet.empty; generalize false. change stateset with NumSet.t in *. induction p using StateSetProps.set_induction_below; intros b acc Hbacc. rewrite 2 StateSetProps.fold_empty; (repeat intro; num_prop; psubst; try reflexivity || ti_auto). rewrite H1; reflexivity. assert (SetoidList.compat_op eq StateSet.Equal (fun i => StateSet.union (f i))). repeat intro. rewrite H3. psubst. reflexivity. assert (SetoidList.compat_op eq (@eq bool) (fun x acc => StateSet.mem i (f x) || acc)). repeat intro. psubst. reflexivity. rewrite (StateSetProps.fold_equal _ H2 _ H1). rewrite (StateSetProps.fold_equal _ H3 _ H1). setoid_rewrite StateSetProps.fold_add_below; try solve [(repeat intro; num_prop; subst; try reflexivity || ti_auto)]. rewrite (IHp1 (StateSet.mem i (f x) || b)); [reflexivity|]. rewrite <- Hbacc. rewrite bool_prop_iff. bool_connectors. rewrite <- 3NumSetProps.mem_iff. StateSetProps.setdec. repeat intro; num_prop; psubst; rewrite H5; reflexivity. 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)