import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
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 ./ok.bend as OK
import ./find.bend as FI
import ./reads.bend as RD
import ./ends.bend as EN
import ./path.bend as P
import ./plug.bend as PG
import ./agree.bend as AG
import ./setters.bend as SE
import ./rotm.bend as RM
import ./rotp.bend as RP
import ./fix.bend as FX
import ./attach.bend as AT
import ./hdr.bend as HD
import ./ins.bend as INS
import ./ord.bend as OR
import ./slot.bend as SL
import ./alls.bend as AL
import ./dj.bend as DJ
import ./spath.bend as SP
import ../../lib/nat_list.bend as NL

# The insertion after the new slot is allocated: attach, header, fix-up;
# the result is the real map of a good shadow whose model is the
# specification's insertion. (source: tools/generators/tm_hand/insf.src)


# the old entries split around the gap
def es_split(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +c: List<&2, P.Fr>, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), P.after(c)) : List<&2, Nat>}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)) : List<&2, M.Entry<K, V>>}:
  Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, P.before(c), P.after(c)), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry<K, V>>}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, {==}), FI.ents_app(~K, ~V, P.before(c), P.after(c), nl, pl))

# the specification inserts
def spec_ins(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +l: Nat, +n: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +c: List<&2, P.Fr>, +k: K, +v: V, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), P.after(c)) : List<&2, Nat>}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, +ha: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool}, +hsz: {n == SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Nat}, +hroom: {Nat.is_lt(n, SC.pow2(l)) == True{} : Bool}) -> {S.put(~K, ~V, ~cmp, S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, k, v) == (S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}:
  +es = es_split(~K, ~V, nl, pl, tg, c, hbc)
  +hf = INS.find_gap(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl), hb, ha)
  +hl = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(l)) == True{} : Bool}, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hsz, hroom)
  +hl2 = L.subst(List<&2, M.Entry<K, V>>, z => {Nat.is_lt(SC.length(M.Entry<K, V>, z), SC.pow2(l)) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), es, hl)
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), es) : {S.put_at(~K, ~V, ~cmp, l, _, k, v, S.val_m(K, V, S.find_e(~K, ~V, ~cmp, k, _))) == (S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl))), None{}, hf) : {S.put_at(~K, ~V, ~cmp, l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), k, v, S.val_m(K, V, _)) == (S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
  %Equal.sym(Bool, Nat.is_lt(SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl))), SC.pow2(l)), True{}, hl2) : {S.pick(S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, _, (S.TM{l, S.ins(~K, ~V, ~cmp, k, v, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)))}, Done{None{}}), (S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl))}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
  %Equal.sym(List<&2, M.Entry<K, V>>, S.ins(~K, ~V, ~cmp, k, v, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}), INS.ins_gap(~K, ~V, ~cmp, ~o, k, v, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl), hb, ha)) : {(S.TM{l, _}, Done{None{}}) == (S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
  {==}

# ---- after allocating: attach, header, fix-up ----


def ent_new(-K: Data, -V: Data, +nla: List<&2, M.Node<K>>, +pla: List<&2, Maybe<&2, V>>, +x: Nat, +q: Nat, +k: K, +v: V, +hxn: {ST.nd(K, nla, x) == M.N{True{}, 0n, 0n, q, k} : M.Node<K>}, +hpx: {ST.pv(V, pla, x) == Some{v} : Maybe<&2, V>}) -> {ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
  %Equal.sym(M.Node<K>, ST.nd(K, nla, x), M.N{True{}, 0n, 0n, q, k}, hxn) : {ST.ent(K, V, _, ST.pv(V, pla, x)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}
  %Equal.sym(Maybe<&2, V>, ST.pv(V, pla, x), Some{v}, hpx) : {ST.ent(K, V, M.N{True{}, 0n, 0n, q, k}, _) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}
  {==}

# the entries after attaching: the new one in the gap
def pre_ents(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +c: List<&2, P.Fr>, +x: Nat, +k: K, +v: V, +nla: List<&2, M.Node<K>>, +pla: List<&2, Maybe<&2, V>>, +fla: List<&2, Nat>, +hag: {AG.agr(~K, ~cmp, SC.append(Nat, P.before(c), P.after(c)), nl, nla) == True{} : Bool}, +hxn: {ST.nd(K, nla, x) == M.N{True{}, 0n, 0n, P.top(c), k} : M.Node<K>}, +hx0: {Nat.is_lt(0n, x) == True{} : Bool}, +hxf: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hpx: {ST.pv(V, pla, x) == Some{v} : Maybe<&2, V>}, +hpb: {ST.ents(~K, ~V, P.before(c), nl, pla) == ST.ents(~K, ~V, P.before(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hpa: {ST.ents(~K, ~V, P.after(c), nl, pla) == ST.ents(~K, ~V, P.after(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hob: {EN.oks(~K, ~V, P.before(c), nl, pla) == EN.oks(~K, ~V, P.before(c), nl, pl) : Bool}, +hoa: {EN.oks(~K, ~V, P.after(c), nl, pla) == EN.oks(~K, ~V, P.after(c), nl, pl) : Bool}) -> {ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}) : List<&2, M.Entry<K, V>>}:
  +e1 = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla), ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), RM.attn(K, nla, P.top(c), x, SP.dir(c)), pla), ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nla, pla), SE.ents_setp(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), RM.attn(K, nla, P.top(c), x, SP.dir(c)), pla, x, P.top(c)), RP.attn_ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), pla, nla, P.top(c), x, SP.dir(c)))
  +e2 = FI.ents_app(~K, ~V, P.before(c), Con{x, P.after(c)}, nla, pla)
  +eb = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, P.before(c), nla, pla), ST.ents(~K, ~V, P.before(c), nl, pla), ST.ents(~K, ~V, P.before(c), nl, pl), AG.ents_agr(~K, ~V, ~cmp, ~o, P.before(c), nl, nla, pla, AG.agr_l(~K, ~cmp, ~o, P.before(c), P.after(c), nl, nla, hag)), hpb)
  +ea = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, P.after(c), nla, pla), ST.ents(~K, ~V, P.after(c), nl, pla), ST.ents(~K, ~V, P.after(c), nl, pl), AG.ents_agr(~K, ~V, ~cmp, ~o, P.after(c), nl, nla, pla, AG.agr_r(~K, ~cmp, ~o, P.before(c), P.after(c), nl, nla, hag)), hpa)
  +ex = ent_new(K, V, nla, pla, x, P.top(c), k, v, hxn, hpx)
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nla, pla), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x)), ST.ents(~K, ~V, P.after(c), nla, pla))), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla), ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nla, pla), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nla, pla), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x)), ST.ents(~K, ~V, P.after(c), nla, pla))), e1, e2)) : {_ == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}) : List<&2, M.Entry<K, V>>}
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, P.before(c), nla, pla), ST.ents(~K, ~V, P.before(c), nl, pl), eb) : {SC.append(M.Entry<K, V>, _, ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x)), ST.ents(~K, ~V, P.after(c), nla, pla))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}) : List<&2, M.Entry<K, V>>}
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x)), Some{M.Entry{k, v}}, ex) : {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, P.after(c), nla, pla))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}) : List<&2, M.Entry<K, V>>}
  %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, P.after(c), nla, pla), ST.ents(~K, ~V, P.after(c), nl, pl), ea) : {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, _}) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}) : List<&2, M.Entry<K, V>>}
  {==}


def pre_oks(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +c: List<&2, P.Fr>, +x: Nat, +k: K, +v: V, +nla: List<&2, M.Node<K>>, +pla: List<&2, Maybe<&2, V>>, +fla: List<&2, Nat>, +hag: {AG.agr(~K, ~cmp, SC.append(Nat, P.before(c), P.after(c)), nl, nla) == True{} : Bool}, +hxn: {ST.nd(K, nla, x) == M.N{True{}, 0n, 0n, P.top(c), k} : M.Node<K>}, +hx0: {Nat.is_lt(0n, x) == True{} : Bool}, +hxf: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hpx: {ST.pv(V, pla, x) == Some{v} : Maybe<&2, V>}, +hpb: {ST.ents(~K, ~V, P.before(c), nl, pla) == ST.ents(~K, ~V, P.before(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hpa: {ST.ents(~K, ~V, P.after(c), nl, pla) == ST.ents(~K, ~V, P.after(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hob: {EN.oks(~K, ~V, P.before(c), nl, pla) == EN.oks(~K, ~V, P.before(c), nl, pl) : Bool}, +hoa: {EN.oks(~K, ~V, P.after(c), nl, pla) == EN.oks(~K, ~V, P.after(c), nl, pl) : Bool}, +hok0: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), P.after(c)), nl, pl) == True{} : Bool}) -> {EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla) == True{} : Bool}:
  +e1 = Equal.trans(Bool, EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla), EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), RM.attn(K, nla, P.top(c), x, SP.dir(c)), pla), EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nla, pla), SE.oks_setp(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), RM.attn(K, nla, P.top(c), x, SP.dir(c)), pla, x, P.top(c)), RP.attn_oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), pla, nla, P.top(c), x, SP.dir(c)))
  +hb = Equal.trans(Bool, EN.oks(~K, ~V, P.before(c), nla, pla), EN.oks(~K, ~V, P.before(c), nl, pla), True{}, AG.oks_agr(~K, ~V, ~cmp, ~o, P.before(c), nl, nla, pla, AG.agr_l(~K, ~cmp, ~o, P.before(c), P.after(c), nl, nla, hag)), Equal.trans(Bool, EN.oks(~K, ~V, P.before(c), nl, pla), EN.oks(~K, ~V, P.before(c), nl, pl), True{}, hob, SL.oks_split_l(~K, ~V, P.before(c), P.after(c), nl, pl, hok0)))
  +ha = Equal.trans(Bool, EN.oks(~K, ~V, P.after(c), nla, pla), EN.oks(~K, ~V, P.after(c), nl, pla), True{}, AG.oks_agr(~K, ~V, ~cmp, ~o, P.after(c), nl, nla, pla, AG.agr_r(~K, ~cmp, ~o, P.before(c), P.after(c), nl, nla, hag)), Equal.trans(Bool, EN.oks(~K, ~V, P.after(c), nl, pla), EN.oks(~K, ~V, P.after(c), nl, pl), True{}, hoa, SL.oks_split_r(~K, ~V, P.before(c), P.after(c), nl, pl, hok0)))
  +hx = L.subst(Maybe<&2, M.Entry<K, V>>, z => {S.is_some(M.Entry<K, V>, z) == True{} : Bool}, Some{M.Entry{k, v}}, ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x)), Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x)), Some{M.Entry{k, v}}, ent_new(K, V, nla, pla, x, P.top(c), k, v, hxn, hpx)), {==})
  Equal.trans(Bool, EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla), EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nla, pla), True{}, e1, EN.oks_app(~K, ~V, nla, pla, P.before(c), Con{x, P.after(c)}, hb, L.and_intro(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nla, x), ST.pv(V, pla, x))), EN.oks(~K, ~V, P.after(c), nla, pla), hx, ha)))

def pre_fll(~K: Data, +c: List<&2, P.Fr>, +x: Nat, +nla: List<&2, M.Node<K>>, +fla: List<&2, Nat>, +hfll: {ST.fll(~K, nla, fla) == True{} : Bool}) -> {ST.fll(~K, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), fla) == True{} : Bool}:
  Equal.trans(Bool, ST.fll(~K, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), fla), ST.fll(~K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), fla), True{}, SE.fll_setp(~K, fla, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), Equal.trans(Bool, ST.fll(~K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), fla), ST.fll(~K, nla, fla), True{}, RP.attn_fll(~K, fla, nla, P.top(c), x, SP.dir(c)), hfll))

def pre_len(~K: Data, +c: List<&2, P.Fr>, +x: Nat, +nla: List<&2, M.Node<K>>) -> {SC.length(M.Node<K>, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c))) == SC.length(M.Node<K>, nla) : Nat}:
  Equal.trans(Nat, SC.length(M.Node<K>, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c))), SC.length(M.Node<K>, RM.attn(K, nla, P.top(c), x, SP.dir(c))), SC.length(M.Node<K>, nla), SE.setp_len(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), RP.attn_len(~K, nla, P.top(c), x, SP.dir(c)))

# ---- the end ----

def ieq(+a: Nat, +b: Nat, +e: {a == b : Nat}) -> {Nat.is_eq(a, b) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_eq(a, z) == True{} : Bool}, a, b, e, N.is_eq_refl(a))


def ins_mok2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +c: List<&2, P.Fr>, +x: Nat, +k: K, +v: V, +nla: List<&2, M.Node<K>>, +pla: List<&2, Maybe<&2, V>>, +fla: List<&2, Nat>, +hag: {AG.agr(~K, ~cmp, SC.append(Nat, P.before(c), P.after(c)), nl, nla) == True{} : Bool}, +hxn: {ST.nd(K, nla, x) == M.N{True{}, 0n, 0n, P.top(c), k} : M.Node<K>}, +hx0: {Nat.is_lt(0n, x) == True{} : Bool}, +hxf: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hpx: {ST.pv(V, pla, x) == Some{v} : Maybe<&2, V>}, +hpb: {ST.ents(~K, ~V, P.before(c), nl, pla) == ST.ents(~K, ~V, P.before(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hpa: {ST.ents(~K, ~V, P.after(c), nl, pla) == ST.ents(~K, ~V, P.after(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hob: {EN.oks(~K, ~V, P.before(c), nl, pla) == EN.oks(~K, ~V, P.before(c), nl, pl) : Bool}, +hoa: {EN.oks(~K, ~V, P.after(c), nl, pla) == EN.oks(~K, ~V, P.after(c), nl, pl) : Bool}, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), P.after(c)) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TE{}) : ST.Tr}, +hok: {P.ctxok(~K, c, 0n, nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, +ha: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool}, +fra: Nat, +dra: Nat, +hfll: {ST.fll(~K, nla, fla) == True{} : Bool}, +hfree: {fra == ST.fst0(fla) : Nat}, +hcd: {Nat.is_le(dra, l) == True{} : Bool}, +hcap: {Nat.is_le(SC.length(M.Node<K>, nla), SC.pow2(dra)) == True{} : Bool}, +hcpl: {SC.length(Maybe<&2, V>, pla) == SC.length(M.Node<K>, nla) : Nat}, +hnd: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla)) == True{} : Bool}, +hin: {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla), SC.length(M.Node<K>, nla)) == True{} : Bool}, +hlen: {SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla)) == SC.length(M.Node<K>, nla) : Nat}, +hroom: {Nat.is_lt(n, SC.pow2(l)) == True{} : Bool}, +r: Nat, +nf: List<&2, M.Node<K>>, +T: ST.Tr, +eqf: {MI.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})) == ST.SH{1n+n, r, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, nf, pla, tg, fl} : ST.Sh<K, V>}, +hrep: {ST.rep(~K, T, 0n, nf) == True{} : Bool}, +hr: {r == ST.rid(T) : Nat}, +hids: {ST.ids(T) == SC.append(Nat, P.before(c), Con{x, P.after(c)}) : List<&2, Nat>}, +hrb: {ST.root_black(~K, T, nf) == True{} : Bool}, +he: {ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nf, pla) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}) : List<&2, M.Entry<K, V>>}, +hoks: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nf, pla) == True{} : Bool}, rest7: {ST.fll(~K, nf, fla) == True{} : Bool} & {SC.length(M.Node<K>, nf) == SC.length(M.Node<K>, nla) : Nat}) -> OK.MOK(~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.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})), Done{None{}})):
  match rest7:
    case Tuple{hfl0, hln0}:
      +hfl = hfl0
      +hln = hln0
      +erp = L.subst(ST.Sh<K, V>, z => {MI.rp(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, (z, Done{None{}})) == (ST.real(~K, ~V, ~cmp, ST.SH{1n+n, r, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, nf, pla, T, fla}), Done{None{}}) : M.TreeMap<K, V, cmp> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}, ST.SH{1n+n, r, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, nf, pla, tg, fl}, MI.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})), Equal.sym(ST.Sh<K, V>, MI.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})), ST.SH{1n+n, r, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, nf, pla, tg, fl}, eqf), {==})
      +es1 = spec_ins(~K, ~V, ~cmp, ~o, l, n, nl, pl, tg, c, k, v, hbc, hb, ha, RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), hroom)
      +em = L.subst(List<&2, Nat>, z => {S.TM{l, ST.ents(~K, ~V, z, nf, pla)} == S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})} : S.Model<K, V>}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), L.subst(List<&2, M.Entry<K, V>>, z => {S.TM{l, z} == S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})} : S.Model<K, V>}, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}), ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nf, pla), Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nf, pla), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}), he), {==}))
      +esp = Equal.trans(S.Model<K, V> & 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), (S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, Done{None{}}), (ST.model(~K, ~V, ~cmp, ST.SH{1n+n, r, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, nf, pla, T, fla}), Done{None{}}), es1, L.subst(S.Model<K, V>, z => {(S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, Done{None{}}) == (z, Done{None{}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}, S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, S.TM{l, ST.ents(~K, ~V, ST.ids(T), nf, pla)}, Equal.sym(S.Model<K, V>, S.TM{l, ST.ents(~K, ~V, ST.ids(T), nf, pla)}, S.TM{l, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)})}, em), {==}))
      +lnf = Equal.trans(Nat, SC.length(M.Node<K>, nf), SC.length(M.Node<K>, nla), SC.length(M.Node<K>, nla), hln, {==})
      +gcap = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(dra)) == True{} : Bool}, SC.length(M.Node<K>, nla), SC.length(M.Node<K>, nf), Equal.sym(Nat, SC.length(M.Node<K>, nf), SC.length(M.Node<K>, nla), hln), hcap)
      +gcpl = ieq(SC.length(Maybe<&2, V>, pla), SC.length(M.Node<K>, nf), Equal.trans(Nat, SC.length(Maybe<&2, V>, pla), SC.length(M.Node<K>, nla), SC.length(M.Node<K>, nf), hcpl, Equal.sym(Nat, SC.length(M.Node<K>, nf), SC.length(M.Node<K>, nla), hln)))
      +gpay = SL.pay_oks(~K, ~V, T, nf, pla, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nf, pla) == True{} : Bool}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), hoks))
      +gnd = L.subst(List<&2, Nat>, z => {NL.nodupn(SC.append(Nat, z, fla)) == True{} : Bool}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), hnd)
      +gin = L.subst(Nat, z => {ST.allin(SC.append(Nat, ST.ids(T), fla), z) == True{} : Bool}, SC.length(M.Node<K>, nla), SC.length(M.Node<K>, nf), Equal.sym(Nat, SC.length(M.Node<K>, nf), SC.length(M.Node<K>, nla), hln), L.subst(List<&2, Nat>, z => {ST.allin(SC.append(Nat, z, fla), SC.length(M.Node<K>, nla)) == True{} : Bool}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), hin))
      +glen = ieq(SC.length(Nat, SC.append(Nat, ST.ids(T), fla)), SC.length(M.Node<K>, nf), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, ST.ids(T), fla)), SC.length(M.Node<K>, nla), SC.length(M.Node<K>, nf), L.subst(List<&2, Nat>, z => {SC.length(Nat, SC.append(Nat, z, fla)) == SC.length(M.Node<K>, nla) : Nat}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), hlen), Equal.sym(Nat, SC.length(M.Node<K>, nf), SC.length(M.Node<K>, nla), hln)))
      +gord0 = INS.ord_ins(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, P.before(c), nl, pl), M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl), L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), ST.ents(~K, ~V, P.after(c), nl, pl)), es_split(~K, ~V, nl, pl, tg, c, hbc), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), hb, ha)
      +gord = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nf, pla)) == True{} : Bool}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}), ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nf, pla), Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), nf, pla), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}), he), gord0))
      +hsz = N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
      +hnb = Equal.trans(Nat, n, SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), hsz, L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(tg)) == SC.length(Nat, z) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, {==}))
      +gsz = ieq(1n+n, SC.length(Nat, ST.ids(T)), Equal.trans(Nat, 1n+n, SC.length(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)})), SC.length(Nat, ST.ids(T)), Equal.trans(Nat, 1n+n, 1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), SC.length(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)})), L.subst(Nat, z => {1n+n == 1n+z : Nat}, n, SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), hnb, {==}), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)})), 1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), AL.len_put(P.before(c), x, P.after(c)))), L.subst(List<&2, Nat>, z => {SC.length(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)})) == SC.length(Nat, z) : Nat}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), {==})))
      +hlo = Equal.trans(Nat, lo, ST.fst0(ST.ids(tg)), ST.fst0(SC.append(Nat, P.before(c), P.after(c))), N.eq_from_is_eq(lo, ST.fst0(ST.ids(tg)), ST.g_clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), L.subst(List<&2, Nat>, z => {ST.fst0(ST.ids(tg)) == ST.fst0(z) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, {==}))
      +hhi = Equal.trans(Nat, hi, ST.last0(ST.ids(tg)), ST.last0(SC.append(Nat, P.before(c), P.after(c))), N.eq_from_is_eq(hi, ST.last0(ST.ids(tg)), ST.g_chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), L.subst(List<&2, Nat>, z => {ST.last0(ST.ids(tg)) == ST.last0(z) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, {==}))
      +hnd0 = DJ.ndl(SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla, hnd)
      +glo = ieq(M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), ST.fst0(ST.ids(T)), Equal.trans(Nat, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), ST.fst0(SC.append(Nat, P.before(c), Con{x, P.after(c)})), ST.fst0(ST.ids(T)), HD.lo_new(c, x, n, lo, hlo, hnb, hnd0), L.subst(List<&2, Nat>, z => {ST.fst0(SC.append(Nat, P.before(c), Con{x, P.after(c)})) == ST.fst0(z) : Nat}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), {==})))
      +ghi = ieq(M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), ST.last0(ST.ids(T)), Equal.trans(Nat, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), ST.last0(SC.append(Nat, P.before(c), Con{x, P.after(c)})), ST.last0(ST.ids(T)), HD.hi_new(c, x, n, hi, hhi, hnb, hnd0), L.subst(List<&2, Nat>, z => {ST.last0(SC.append(Nat, P.before(c), Con{x, P.after(c)})) == ST.last0(z) : Nat}, SC.append(Nat, P.before(c), Con{x, P.after(c)}), ST.ids(T), Equal.sym(List<&2, Nat>, ST.ids(T), SC.append(Nat, P.before(c), Con{x, P.after(c)}), hids), {==})))
      +good = ST.good_intro(~K, ~V, ~cmp, 1n+n, r, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, nf, pla, T, fla, ST.g_cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), hcd, gcap, gcpl, hrep, gpay, hfl, gnd, gin, glen, gord, hrb, gsz, ieq(r, ST.rid(T), hr), glo, ghi, ieq(fra, ST.fst0(fla), hfree))
      (ST.SH{1n+n, r, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, nf, pla, T, fla}, (Done{None{}}, (erp, (esp, good))))

def ins_mok(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +c: List<&2, P.Fr>, +x: Nat, +k: K, +v: V, +nla: List<&2, M.Node<K>>, +pla: List<&2, Maybe<&2, V>>, +fla: List<&2, Nat>, +hag: {AG.agr(~K, ~cmp, SC.append(Nat, P.before(c), P.after(c)), nl, nla) == True{} : Bool}, +hxn: {ST.nd(K, nla, x) == M.N{True{}, 0n, 0n, P.top(c), k} : M.Node<K>}, +hx0: {Nat.is_lt(0n, x) == True{} : Bool}, +hxf: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hpx: {ST.pv(V, pla, x) == Some{v} : Maybe<&2, V>}, +hpb: {ST.ents(~K, ~V, P.before(c), nl, pla) == ST.ents(~K, ~V, P.before(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hpa: {ST.ents(~K, ~V, P.after(c), nl, pla) == ST.ents(~K, ~V, P.after(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hob: {EN.oks(~K, ~V, P.before(c), nl, pla) == EN.oks(~K, ~V, P.before(c), nl, pl) : Bool}, +hoa: {EN.oks(~K, ~V, P.after(c), nl, pla) == EN.oks(~K, ~V, P.after(c), nl, pl) : Bool}, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), P.after(c)) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TE{}) : ST.Tr}, +hok: {P.ctxok(~K, c, 0n, nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, +ha: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool}, +fra: Nat, +dra: Nat, +hfll: {ST.fll(~K, nla, fla) == True{} : Bool}, +hfree: {fra == ST.fst0(fla) : Nat}, +hcd: {Nat.is_le(dra, l) == True{} : Bool}, +hcap: {Nat.is_le(SC.length(M.Node<K>, nla), SC.pow2(dra)) == True{} : Bool}, +hcpl: {SC.length(Maybe<&2, V>, pla) == SC.length(M.Node<K>, nla) : Nat}, +hnd: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla)) == True{} : Bool}, +hin: {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla), SC.length(M.Node<K>, nla)) == True{} : Bool}, +hlen: {SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla)) == SC.length(M.Node<K>, nla) : Nat}, +hroom: {Nat.is_lt(n, SC.pow2(l)) == True{} : Bool}, fp: Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node<K>>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})) == ST.SH{1n+n, fr_, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, fn_, pla, tg, fl} : ST.Sh<K, V>} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == SC.append(Nat, P.before(c), Con{x, P.after(c)}) : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & ({ST.ents(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fn_, pla) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}) : List<&2, M.Entry<K, V>>} & ({EN.oks(~K, ~V, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fn_, pla) == True{} : Bool} & ({ST.fll(~K, fn_, fla) == True{} : Bool} & {SC.length(M.Node<K>, fn_) == SC.length(M.Node<K>, nla) : Nat}))))))>>>) -> OK.MOK(~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.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})), Done{None{}})):
  match fp:
    case Tuple{+r, Tuple{nf, Tuple{T, Tuple{eqf0, Tuple{hrep0, Tuple{hr0, Tuple{hids0, Tuple{hrb0, Tuple{he0, Tuple{hoks0, rest7}}}}}}}}}}:
      ins_mok2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, c, x, k, v, nla, pla, fla, hag, hxn, hx0, hxf, hpx, hpb, hpa, hob, hoa, hbc, hplug, hok, hb, ha, fra, dra, hfll, hfree, hcd, hcap, hcpl, hnd, hin, hlen, hroom, r, nf, T, eqf0, hrep0, hr0, hids0, hrb0, he0, hoks0, rest7)


def put_alloc_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +c: List<&2, P.Fr>, +x: Nat, +nla: List<&2, M.Node<K>>, +pla: List<&2, Maybe<&2, V>>, +fra: Nat, +dra: Nat) -> {MI.put_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), (ST.SH{n, root, lo, hi, fra, l, dra, nla, pla, tg, fl}, Done{x})) == (MI.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})), Done{None{}}) : ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}:
  %Equal.sym(ST.Sh<K, V>, MI.attach(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, fra, l, dra, nla, pla, tg, fl}, P.top(c), x, SP.dir(c)), ST.SH{n, RM.rootq(P.top(c), root, x), lo, hi, fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, RM.attach_m(~K, ~V, ~cmp, n, root, lo, hi, fra, l, dra, nla, pla, tg, fl, P.top(c), x, SP.dir(c))) : {(MI.insert_fixed(~K, ~V, ~cmp, x, MI.size(~K, ~V, ~cmp, MI.insert_header(~K, ~V, ~cmp, _, x, P.top(c), SP.dir(c)))), Done{None{}}) == (MI.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})), Done{None{}}) : ST.Sh<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
  {==}

# the insertion after allocating the slot x
def ins_fin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +c: List<&2, P.Fr>, +x: Nat, +k: K, +v: V, +nla: List<&2, M.Node<K>>, +pla: List<&2, Maybe<&2, V>>, +fla: List<&2, Nat>, +hag: {AG.agr(~K, ~cmp, SC.append(Nat, P.before(c), P.after(c)), nl, nla) == True{} : Bool}, +hxn: {ST.nd(K, nla, x) == M.N{True{}, 0n, 0n, P.top(c), k} : M.Node<K>}, +hx0: {Nat.is_lt(0n, x) == True{} : Bool}, +hxf: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hpx: {ST.pv(V, pla, x) == Some{v} : Maybe<&2, V>}, +hpb: {ST.ents(~K, ~V, P.before(c), nl, pla) == ST.ents(~K, ~V, P.before(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hpa: {ST.ents(~K, ~V, P.after(c), nl, pla) == ST.ents(~K, ~V, P.after(c), nl, pl) : List<&2, M.Entry<K, V>>}, +hob: {EN.oks(~K, ~V, P.before(c), nl, pla) == EN.oks(~K, ~V, P.before(c), nl, pl) : Bool}, +hoa: {EN.oks(~K, ~V, P.after(c), nl, pla) == EN.oks(~K, ~V, P.after(c), nl, pl) : Bool}, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), P.after(c)) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, ST.TE{}) : ST.Tr}, +hok: {P.ctxok(~K, c, 0n, nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, +ha: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool}, +fra: Nat, +dra: Nat, +hfll: {ST.fll(~K, nla, fla) == True{} : Bool}, +hfree: {fra == ST.fst0(fla) : Nat}, +hcd: {Nat.is_le(dra, l) == True{} : Bool}, +hcap: {Nat.is_le(SC.length(M.Node<K>, nla), SC.pow2(dra)) == True{} : Bool}, +hcpl: {SC.length(Maybe<&2, V>, pla) == SC.length(M.Node<K>, nla) : Nat}, +hnd: {NL.nodupn(SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla)) == True{} : Bool}, +hin: {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla), SC.length(M.Node<K>, nla)) == True{} : Bool}, +hlen: {SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla)) == SC.length(M.Node<K>, nla) : Nat}, +hroom: {Nat.is_lt(n, SC.pow2(l)) == True{} : Bool}) -> OK.MOK(~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_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), (ST.SH{n, root, lo, hi, fra, l, dra, nla, pla, tg, fl}, Done{x}))):
  +hnd0 = DJ.ndl(SC.append(Nat, P.before(c), Con{x, P.after(c)}), fla, hnd)
  +hbad = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, DJ.ndl(ST.ids(tg), fl, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
  +hroot = Equal.trans(Nat, root, ST.rid(tg), ST.rid(PG.plug(c, ST.TE{})), N.eq_from_is_eq(root, ST.rid(tg), ST.g_croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), L.subst(ST.Tr, z => {ST.rid(tg) == ST.rid(z) : Nat}, tg, PG.plug(c, ST.TE{}), hplug, {==}))
  +hrb = L.subst(ST.Tr, z => {ST.root_black(~K, z, nl) == True{} : Bool}, tg, PG.plug(c, ST.TE{}), hplug, ST.g_cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +hok0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
  +i1 = AT.att_leaf(~K, ~cmp, ~o, nl, nla, c, x, k, hok, hbad, hag, hxn, hx0, hxf)
  +i2 = AT.att_ctx(~K, ~cmp, ~o, nl, nla, c, x, k, hok, hbad, hag, hxn, hx0, hxf)
  +i5 = RP.root_rot(~K, nl, c, 0n, x, ST.TE{}, ST.TN{x, ST.TE{}, ST.TE{}}, root, {==}, {==}, hok, hroot)
  +i6 = AT.att_rb(~K, ~cmp, ~o, nl, nla, c, x, k, hok, hbad, hag, hxn, hx0, hxf, hrb)
  +h4 = pre_ents(~K, ~V, ~cmp, ~o, nl, pl, c, x, k, v, nla, pla, fla, hag, hxn, hx0, hxf, hpx, hpb, hpa, hob, hoa)
  +h5 = pre_oks(~K, ~V, ~cmp, ~o, nl, pl, c, x, k, v, nla, pla, fla, hag, hxn, hx0, hxf, hpx, hpb, hpa, hob, hoa, hok0)
  +h6 = pre_fll(~K, c, x, nla, fla, hfll)
  +h7 = pre_len(~K, c, x, nla)
  OK.mok_eq(~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_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), (ST.SH{n, root, lo, hi, fra, l, dra, nla, pla, tg, fl}, Done{x})), (MI.insert_fix_loop(~K, ~V, ~cmp, 2n+n, (ST.SH{1n+n, RM.rootq(P.top(c), root, x), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), pla, tg, fl}, M.Fix{x, True{}})), Done{None{}}), put_alloc_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, x, nla, pla, fra, dra), ins_mok(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, c, x, k, v, nla, pla, fla, hag, hxn, hx0, hxf, hpx, hpb, hpa, hob, hoa, hbc, hplug, hok, hb, ha, fra, dra, hfll, hfree, hcd, hcap, hcpl, hnd, hin, hlen, hroom, FX.loop(~K, ~V, ~cmp, ~o, 1n+n, M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(SP.dir(c), Nat.is_eq(P.top(c), lo))), x, lo), M.pick(Nat, Bool.or(Nat.is_eq(n, 0n), Bool.and(Bool.not(SP.dir(c)), Nat.is_eq(P.top(c), hi))), x, hi), fra, l, dra, pla, tg, fl, fla, SC.append(Nat, P.before(c), Con{x, P.after(c)}), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, P.before(c), nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, P.after(c), nl, pl)}), SC.length(M.Node<K>, nla), 2n+n, RM.rootq(P.top(c), root, x), SE.setp(K, RM.attn(K, nla, P.top(c), x, SP.dir(c)), x, P.top(c)), c, x, ST.TE{}, ST.TE{}, i1, i2, hnd0, {==}, i5, i6, h4, h5, h6, h7)))