proposition: Lemma rho_theta i: i<size' -> rho (theta i) i.
proof: Proof. intro Hi. unfold theta. generalize (i_table_surj invariant_build_store Hi). clear. generalize table. intro t. refine (StateSetMapProps.fold_rec_bis (P := fun t acc => (exists p : StateSetMap.key, StateSetMap.MapsTo p i t) -> StateSetMap.MapsTo acc i t) _ _ _). intros ? ? ? H. setoid_rewrite H. tauto. intros [? ?]. apply StateSetMap.empty_1 in H. elim H. intros p j q t' Hp Hp' IH [r Hr]. num_analyse. subst. auto with map. StateSetMapProps.find_tac. right. apply apply in IH. split; auto. intro F. elim Hp'. rewrite F. eauto with map. eauto. 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)