proposition: Lemma mem_table_finals: forall i, StateSet.mem i (table_finals table) = StateSet.exists_ (fun x => StateSet.mem x finaux) (theta i).
proof: Proof. intros i. rewrite bool_prop_iff. rewrite <- StateSetProps.exists_iff by trivial. StateSetProps.mem_prop. split; intro H. apply table_finals_correct in H as [u Hu Hu']. exists u. split; auto. StateSetProps.mem_prop. trivial. destruct H as [u [H H']]. StateSetProps.mem_prop. eapply table_finals_complete. eassumption. apply rho_theta; trivial. eapply theta_below, H. assumption. 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)