proposition: Lemma table_finals_correct: forall i, StateSet.In i (table_finals table) -> exists2 u, StateSet.In u (theta i) & StateSet.In u finaux.
proof: Proof. intros i. unfold table_finals. apply StateSetMapProps.fold_rec_nodep. StateSetProps.setdec. intros p j a Hpj IH H. case_eq (StateSet.exists_ (fun s => StateSet.mem s finaux) p); intro He; rewrite He in H. 2: auto. revert H. StateSetProps.set_iff. intros [H|H]; auto. psubst. clear IH. rewrite <- StateSetProps.exists_iff in He by trivial. destruct He as [k [Hk Hk']]. exists k; auto. rewrite (theta_rho Hpj). trivial. 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)