import Base
import ../../lib/logic.bend as L
import ../../lib/order.bend as O
import ../../../spec/lib/common.bend as SC
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 ./reads.bend as RD
import ./ends.bend as EN
import ./navm.bend as NM
import ./putm.bend as PM
import ./rmv.bend as RV
import ./rmi.bend as RI
import ./rmp.bend as RP
import ./life.bend as LF

# The implementation's operations refine the specification's, for every
# good shadow and a lawful comparator. (source: tools/generators/tm_hand/api.src)


# an implementation read through the simulation, given the mirror's answer
def via(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, -X: Data, -impl: M.TreeMap<K, V, cmp> & X, -mir: ST.Sh<K, V> & X, +s: ST.Sh<K, V>, +o: X, +hs: {impl == MI.rp(~K, ~V, ~cmp, X, mir) : M.TreeMap<K, V, cmp> & X}, +hm: {mir == (s, o) : ST.Sh<K, V> & X}) -> {impl == (ST.real(~K, ~V, ~cmp, s), o) : M.TreeMap<K, V, cmp> & X}:
  L.subst(ST.Sh<K, V> & X, z => {impl == MI.rp(~K, ~V, ~cmp, X, z) : M.TreeMap<K, V, cmp> & X}, mir, (s, o), hm, hs)

def get_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.get(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.get(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, V>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.get(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), M.get(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, V>, M.get(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.get(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.get_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), RD.get_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)))

def contains_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Bool, S.contains_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.contains_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  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.is_some(V, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.contains_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), M.contains_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Bool, M.contains_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.contains_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.is_some(V, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SM.contains_key_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), RD.contains_key_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)))

def get_or_default_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +fb: V) -> OK.POK(~K, ~V, ~cmp, V, S.get_or_default(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, fb), M.get_or_default(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, fb)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, V, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.or_default(V, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), fb), S.get_or_default(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, fb), M.get_or_default(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, fb), {==}, via(~K, ~V, ~cmp, V, M.get_or_default(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, fb), MI.get_or_default(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, fb), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.or_default(V, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), fb), SM.get_or_default_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, fb, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), RD.get_or_default_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, fb, hg)))

def size_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Nat, S.size(K, V, ST.model(~K, ~V, ~cmp, sh)), M.size(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      +es = L.subst(Nat, z => {S.size(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == (ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), z) : S.Model<K, V> & Nat}, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), n, Equal.sym(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), {==})
      OK.pok_read(~K, ~V, ~cmp, Nat, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, n, S.size(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), M.size(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), es, via(~K, ~V, ~cmp, Nat, M.size(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.size(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, n, SM.size_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)), {==}))

def is_empty_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Bool, S.is_empty(K, V, ST.model(~K, ~V, ~cmp, sh)), M.is_empty(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      +es = L.subst(Nat, z => {S.is_empty(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == (ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), Nat.is_eq(z, 0n)) : S.Model<K, V> & Bool}, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), n, Equal.sym(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), {==})
      OK.pok_read(~K, ~V, ~cmp, Bool, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, Nat.is_eq(n, 0n), S.is_empty(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), M.is_empty(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), es, via(~K, ~V, ~cmp, Bool, M.is_empty(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.is_empty(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Nat.is_eq(n, 0n), SM.is_empty_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)), {==}))

def first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.first_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), M.first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), {==}, via(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, M.first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.first_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.first_entry_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)), EN.first_entry_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))

def last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.last_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), M.last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), {==}, via(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, M.last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.last_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.last_entry_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)), EN.last_entry_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))

def first_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.first_key(K, V, ST.model(~K, ~V, ~cmp, sh)), M.first_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, K>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.key_m(K, V, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.first_key(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), M.first_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), {==}, via(~K, ~V, ~cmp, Maybe<&2, K>, M.first_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.first_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SM.first_key_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)), EN.first_key_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))

def last_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.last_key(K, V, ST.model(~K, ~V, ~cmp, sh)), M.last_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, K>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.key_m(K, V, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.last_key(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), M.last_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), {==}, via(~K, ~V, ~cmp, Maybe<&2, K>, M.last_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.last_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SM.last_key_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)), EN.last_key_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))

def lower_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, False{}), M.lower_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.nav(~K, ~V, ~cmp, k, False{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, False{}, False{}), M.lower_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, M.lower_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.lower_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.nav(~K, ~V, ~cmp, k, False{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.lower_entry_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, False{}, False{}, hg)))

def lower_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, False{}), M.lower_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, K>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, False{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, False{}, False{}), M.lower_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, K>, M.lower_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.lower_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, False{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SM.lower_key_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_key_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, False{}, False{}, hg)))

def floor_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, True{}), M.floor_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.nav(~K, ~V, ~cmp, k, False{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, False{}, True{}), M.floor_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, M.floor_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.floor_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.nav(~K, ~V, ~cmp, k, False{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.floor_entry_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, False{}, True{}, hg)))

def floor_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, False{}, True{}), M.floor_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, K>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, False{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, False{}, True{}), M.floor_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, K>, M.floor_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.floor_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, False{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SM.floor_key_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_key_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, False{}, True{}, hg)))

def ceiling_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, True{}), M.ceiling_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.nav(~K, ~V, ~cmp, k, True{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, True{}, True{}), M.ceiling_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, M.ceiling_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.ceiling_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.nav(~K, ~V, ~cmp, k, True{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.ceiling_entry_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, True{}, True{}, hg)))

def ceiling_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, True{}), M.ceiling_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, K>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, True{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, True{}, True{}), M.ceiling_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, K>, M.ceiling_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.ceiling_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, True{}, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SM.ceiling_key_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_key_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, True{}, True{}, hg)))

def higher_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, False{}), M.higher_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.nav(~K, ~V, ~cmp, k, True{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.nav_entry(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, True{}, False{}), M.higher_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, M.higher_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.higher_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.nav(~K, ~V, ~cmp, k, True{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SM.higher_entry_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_entry_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, True{}, False{}, hg)))

def higher_key_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, K>, S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, True{}, False{}), M.higher_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.pok_read(~K, ~V, ~cmp, Maybe<&2, K>, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, True{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.nav_key(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, True{}, False{}), M.higher_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), {==}, via(~K, ~V, ~cmp, Maybe<&2, K>, M.higher_key(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.higher_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.nav(~K, ~V, ~cmp, k, True{}, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SM.higher_key_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), NM.nav_key_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, True{}, False{}, hg)))

# ---- put ----


def put_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.put(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v), M.put(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), SM.put_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), PM.put_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v))

def put_if_absent_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.put_if_absent(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_if_absent(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v), M.put_if_absent(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), SM.put_if_absent_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), PM.absent_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v))

def replace_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K, +v: V) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k, v), M.replace(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k, v)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v), M.replace(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), SM.replace_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), PM.replace_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v))

def replace_if_equal_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}, +k: K, +e: V, +w: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, sh), k, e, w), M.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), k, e, w)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, e, w), M.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), SM.replace_if_equal_s(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, e, w, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), PM.rie_m(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w))

# ---- remove ----

def remove_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}, +k: K) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, sh), k), M.remove(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh), k)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Maybe<&2, V>, S.remove(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), MI.remove(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), M.remove(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k), SM.remove_s(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), RV.rm_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k))

def remove_if_equal_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}, +k: K, +e: V) -> OK.POK(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, sh), k, e), M.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, sh), k, e)):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Bool, S.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), MI.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, e), M.remove_if_equal(~K, ~V, ~cmp, ~eq, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e), SM.remove_if_equal_s(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, e, OK.dg_good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hg)), RI.rmi_m(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e))

# ---- the polls ----


def poll_first_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.poll_first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_first_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.poll_first_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), M.poll_first_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), SM.poll_first_entry_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)), RP.pf_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))

def poll_last_entry_ok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +sh: ST.Sh<K, V>, +hg: {ST.good(~K, ~V, ~cmp, sh) == True{} : Bool}) -> OK.POK(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, sh)), M.poll_last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh))):
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      OK.mok_pok(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.poll_last_entry(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), MI.poll_last_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), M.poll_last_entry(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), SM.poll_last_entry_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)), RP.pl_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))

# ---- clear ----


def clear_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, ST.Sh<K, V>, s2_ => {M.clear(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, sh)) == ST.real(~K, ~V, ~cmp, s2_) : M.TreeMap<K, V, cmp>} & ({S.clear(K, V, ST.model(~K, ~V, ~cmp, sh)) == ST.model(~K, ~V, ~cmp, s2_) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, s2_) == True{} : Bool})>:
  match sh:
    case ST.SH{+n, +root, +lo, +hi, +free, +l, +d, +nl, +pl, +tg, +fl}:
      (ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}, (Equal.trans(M.TreeMap<K, V, cmp>, M.clear(~K, ~V, ~cmp, ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), ST.real(~K, ~V, ~cmp, MI.clear(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})), ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}), SM.clear_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)), Pair.fst({ST.real(~K, ~V, ~cmp, MI.clear(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) : M.TreeMap<K, V, cmp>}, {S.clear(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}, LF.clear_ok(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), Pair.snd({ST.real(~K, ~V, ~cmp, MI.clear(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == ST.real(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) : M.TreeMap<K, V, cmp>}, {S.clear(K, V, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl})) == ST.model(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) : S.Model<K, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{0n, 0n, 0n, 0n, 0n, l, d, Nil{}, Nil{}, ST.TE{}, Nil{}}) == True{} : Bool}, LF.clear_ok(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))))