proposition: Lemma rt_closure_prespec: forall f Hwf size acc, approx f acc -> approx f (fold_states (@rt_closure_aux' f Hwf) size acc) /\ forall i, below i size \/ StateMap.In i acc -> StateMap.In i (fold_states (rt_closure_aux' Hwf) size acc).
proof: Proof. induction size using Pind; intros acc H. split. apply H. intros i [Hi|H']. destruct i; discriminate Hi. apply H'. specialize (IHsize (rt_closure_aux' Hwf size acc)). pose proof (rt_closure_aux'_spec Hwf size H) as [Happrox Hin]. apply apply in IHsize as [IHapprox IHin]; auto. unfold fold_states. rewrite Prect_succ. split; trivial. intros i Hi. destruct (eq_num_dec i size). subst. auto. apply IHin. destruct Hi as [Hi|Hi]; auto. left. clear -Hi n. num_lia. 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)