proofs/containers/balanced_search_tree/api.bend source

proofs/containers/balanced_search_tree/api.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/order.bend as Oimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/balanced_search_tree/main.bend as Simport ../../../src/containers/balanced_search_tree.bend as Mimport ./state.bend as STimport ./mirror.bend as MIimport ./sim.bend as SMimport ./ok.bend as OKimport ./reads.bend as RDimport ./ends.bend as ENimport ./navm.bend as NMimport ./putm.bend as PMimport ./rmv.bend as RVimport ./rmi.bend as RIimport ./rmp.bend as RPimport ./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 answerdef 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))))