proposition: Lemma table_finals_complete: forall u p i, StateSet.In u finaux -> rho p i -> StateSet.In u p -> StateSet.In i (table_finals table).
proof: Proof. intros u p i Hu Hpi Hi. revert Hpi. refine (StateSetMapProps.fold_rec_bis (P:=fun t acc => StateSetMap.MapsTo p i t -> StateSet.In i acc) _ _ _). intros ? ? ? H. setoid_rewrite H. tauto. StateSetMapProps.map_iff. tauto. intros q j q' t Hqj Hq IH. StateSetMapProps.map_iff. intros [[Hqp ->]|[Hqp Hpi]]. replace (StateSet.exists_ (fun s : StateSet.elt => StateSet.mem s finaux) q) with true. auto with set. symmetry. rewrite <- StateSetProps.exists_iff by trivial. exists u. rewrite Hqp. StateSetProps.mem_prop. auto. apply IH in Hpi. clear IH. case StateSet.exists_; auto with set. 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)