import Base
import ../../lib/logic.bend as L
import ../../lib/order.bend as O
import ../../../spec/containers/balanced_search_tree/main.bend as S
import ../../../src/containers/balanced_search_tree.bend as M
import ./state.bend as ST
import ./mirror.bend as MI
import ./sim.bend as SM
import ./ok.bend as OK
import ./prim.bend as PR
import ./cur.bend as CU
import ./cnx.bend as CX
import ./csv.bend as CS
import ./crm.bend as CR
import ./rmv.bend as RV
import ./ccv.bend as CV

# The implementation's cursors refine the specification's: from a good
# cursor (a good shadow, its ids 0 or in the tree), each operation gives the
# real cursor of a good cursor whose model is the specification's result.
# (source: tools/generators/tm_hand/capi.src)


# ---- starting ----


def cst_up(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -sp: S.Cursor<K, V>, -mc: MI.MCursor<K, V>, -r: M.Cursor<K, V, cmp>, +hs: {r == MI.rc(~K, ~V, ~cmp, mc) : M.Cursor<K, V, cmp>}, p: Sigma<&1, &1, MI.MCursor<K, V>, c2 => {MI.rc(~K, ~V, ~cmp, mc) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {r == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({sp == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
  match p:
    case Tuple{+c2, Tuple{+h1, rest}}:
      (c2, (Equal.trans(M.Cursor<K, V, cmp>, r, MI.rc(~K, ~V, ~cmp, mc), MI.rc(~K, ~V, ~cmp, c2), hs, h1), rest))

def iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      cst_up(~K, ~V, ~cmp, S.iterator(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.iterator(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), M.iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), SM.iterator_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), CU.iterator_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))

def descending_iterator_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> Sigma<&1, &1, MI.MCursor<K, V>, c2 => {M.descending_iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == MI.rc(~K, ~V, ~cmp, c2) : M.Cursor<K, V, cmp>} & ({S.descending_iterator(K, V, ST.model(~K, ~V, ~cmp, sh)) == CU.cmod(~K, ~V, ~cmp, c2) : S.Cursor<K, V>} & {CU.cgood(~K, ~V, ~cmp, c2) == True{} : Bool})>:
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      cst_up(~K, ~V, ~cmp, S.descending_iterator(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.descending_iterator(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), M.descending_iterator(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), SM.descending_iterator_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), CU.descending_iterator_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))

# ---- stepping ----

def iterator_has_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Bool, S.iterator_has_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_has_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
  match c:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
      CU.cok_cpok(~K, ~V, ~cmp, Bool, S.iterator_has_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_has_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_has_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_has_next_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CU.has_next_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc))

def iterator_next_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
  match c:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
      CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_next(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_next_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CU.cstep_cok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw, CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc)))

def iterator_next_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, K>, S.iterator_next_key(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_key(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
  match c:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
      CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, K>, S.iterator_next_key(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next_key(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_next_key(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_next_key_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CX.next_key_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc))

def iterator_next_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_next_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_next_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
  match c:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
      CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_next_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), M.iterator_next_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), SM.iterator_next_value_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CX.next_value_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, fw, hc))

# ---- changing the map through the cursor ----


def iterator_set_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}, +v: V) -> CU.CPOK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c), v), M.iterator_set_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c), v)):
  match c:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
      CU.cok_cpok(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), v), MI.iterator_set_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, v), M.iterator_set_value(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), v), SM.iterator_set_value_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, v, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), CS.set_value_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, cu, nx, lo2, hi2, fw, v, hc))


def iterator_remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> CU.CPOK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, c)), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c))):
  match c:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, 0n, +lo2, +hi2, +fw}:
      CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})), SM.iterator_remove_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n))))), hc))), CR.rmz(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, hc))
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, 1n+ +j, +lo2, +hi2, +fw}:
      CU.cok_cpok(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), M.iterator_remove(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), SM.iterator_remove_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))), CR.rmu(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, kk => pc => pa => pb => hbc => hplug => hr => hok => hfin => RV.rm_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc), kk, pc, j, pa, pb, hbc, hplug, hr, hok, hfin, ST.nd(K, nl, 1n+j), {==}), kk => s2 => e => hd => Equal.trans(M.TreeMap<K, V, cmp> & M.Search, MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)), M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)), Equal.sym(M.TreeMap<K, V, cmp> & M.Search, M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)), SM.search_s(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk, SM.remove_id_g(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))))), Equal.trans(M.TreeMap<K, V, cmp> & M.Search, M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk), M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, s2), kk), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)), L.subst(M.TreeMap<K, V, cmp>, z => {M.search(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), kk) == M.search(~K, ~V, ~cmp, z, kk) : M.TreeMap<K, V, cmp> & M.Search}, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.real(~K, ~V, ~cmp, s2), e, {==}), SM.search_s(~K, ~V, ~cmp, s2, kk, hd)))))

# ---- finishing ----

def iterator_finish_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +c: MI.MCursor<K, V>, +hc: {CU.cgood(~K, ~V, ~cmp, c) == True{} : Bool}) -> Sigma<&1, &1, ST.Sh<K, V>, s2 => {M.iterator_finish(~K, ~V, ~cmp, MI.rc(~K, ~V, ~cmp, c)) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap<K, V, cmp>} & ({S.iterator_finish(K, V, CU.cmod(~K, ~V, ~cmp, c)) == ST.model(~K, ~V, ~cmp, s2) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, s2) == True{} : Bool})>:
  match c:
    case MI.MC{ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}, +nx, +cu, +lo2, +hi2, +fw}:
      (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (SM.iterator_finish_s(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))), ({==}, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), cu), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, cu))))), hc))))

# ---- contains_value: the walk over the entries ----


def via_cv(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -impl: M.TreeMap<K, V, cmp> & Bool, -mir: ST.Sh<K, V> & Bool, +s: ST.Sh<K, V>, +o: Bool, +hs: {impl == MI.rp(~K, ~V, ~cmp, Bool, mir) : M.TreeMap<K, V, cmp> & Bool}, +hm: {mir == (s, o) : ST.Sh<K, V> & Bool}) -> {impl == (ST.real(~K, ~V, ~cmp, s), o) : M.TreeMap<K, V, cmp> & Bool}:
  L.subst(ST.Sh<K, V> & Bool, z => {impl == MI.rp(~K, ~V, ~cmp, Bool, z) : M.TreeMap<K, V, cmp> & Bool}, mir, (s, o), hm, hs)

def contains_value_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +w: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.contains_value(~K, ~V, ~eq, ST.model(~K, ~V, ~cmp, sh), w), M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), w)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Bool, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.any_value(~K, ~V, ~eq, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.contains_value(~K, ~V, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), w), M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), w), {==}, via_cv(~K, ~V, ~cmp, M.contains_value(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), w), MI.contains_value(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.any_value(~K, ~V, ~eq, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.contains_value_s(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), CV.contains_value_m(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, w)))