proposition: Remark measure_map_remove: forall m x, measure_map m = (V.measure (get x (Top_except m)) + measure_map (IdentMap.remove x m))%nat.
proof: Proof. intros. unfold get. destruct (IdentMap.find x m) as [v|] eqn:F. - apply measure_map_add with x. apply IMFact.not_find_in_iff. rewrite IMFact.remove_eq_o; auto. red; intros. rewrite IMFact.add_o, IMFact.remove_o. destruct (AbstrInterp.IdentMap.E.eq_dec x y); congruence. - rewrite V.measure_top. unfold measure_map. eapply IMProp.fold_Equal. auto. repeat (hnf; intros). congruence. hnf; intros; lia. red; intros. rewrite IMFact.remove_o. destruct (AbstrInterp.IdentMap.E.eq_dec x y); congruence. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)