import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
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 ./reads.bend as RD
import ./path.bend as P
import ./plug.bend as PG
import ./agree.bend as AG
import ./prim.bend as PR
import ./frame.bend as FR
import ./ord.bend as OR
import ./ins.bend as INS
import ./slot.bend as SL
import ./alls.bend as AL
import ./dj.bend as DJ
import ./spath.bend as SP
import ./insf.bend as IF
import ../../lib/nat_list.bend as NL

# Allocating the new slot where the search stopped: appending (room in the
# block, or growing it, or failing at the capacity) or reusing the free
# list's head; each gives the insertion's facts or the specification's
# rejection. (source: tools/generators/tm_hand/alloc.src)


def fl_nil(+fl: List<&2, Nat>, +n: Nat, +h0: {0n == ST.fst0(fl) : Nat}, +ha: {ST.allin(fl, n) == True{} : Bool}) -> {fl == Nil{} : List<&2, Nat>}:
  match fl:
    case Nil{}:
      {==}
    case Con{+y, +t}:
      +hy = L.and_left(Nat.is_lt(0n, y), Nat.is_le(y, n), L.and_left(Bool.and(Nat.is_lt(0n, y), Nat.is_le(y, n)), ST.allin(t, n), ha))
      Empty.absurd({Con{y, t} == Nil{} : List<&2, Nat>}, L.false_true(L.subst(Nat, z => {Nat.is_lt(0n, z) == True{} : Bool}, y, 0n, Equal.sym(Nat, 0n, y, h0), hy)))

# the specification rejects at the capacity
def spec_rej(~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}, +hfull: {Nat.is_lt(n, SC.pow2(l)) == False{} : Bool}) -> {S.put(~K, ~V, ~cmp, S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, k, v) == (S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}:
  +es = IF.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)) == False{} : Bool}, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hsz, hfull)
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}, L.subst(List<&2, M.Entry<K, V>>, z => {S.find_e(~K, ~V, ~cmp, k, z) == None{} : Maybe<&2, 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)), ST.ents(~K, ~V, ST.ids(tg), nl, pl), 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), hf)) : {S.put_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, v, S.val_m(K, V, _)) == (S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : 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>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.pow2(l)), False{}, hl) : {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, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Done{None{}}), (S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}})) == (S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Fail{M.Rejected{M.CapacityExceeded{}, k, v}}) : S.Model<K, V> & Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>}
  {==}


# appending: into room, growing the block, or rejected at the capacity
def app_case(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: 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, 0n, l, d, nl, pl, tg, fl) == True{} : Bool}, +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>}, +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}, +room: Bool, +hr: {Nat.is_lt(SC.length(M.Node<K>, nl), SC.pow2(d)) == room : Bool}, +grow: Bool, +hgw: {Nat.is_lt(d, l) == grow : 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, 0n, l, d, nl, pl, tg, fl}), k, v), MI.put_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), MI.app_room(~K, ~V, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, k, v, P.top(c), room, grow))):
  match room grow:
    case True{} +grow:

      +hin0 = ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)
      +hflnil = fl_nil(fl, SC.length(M.Node<K>, nl), N.eq_from_is_eq(0n, ST.fst0(fl), ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)), AL.allin_r(ST.ids(tg), fl, SC.length(M.Node<K>, nl), hin0))
      +hinB = L.subst(List<&2, Nat>, z => {ST.allin(z, SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, AL.allin_l(ST.ids(tg), fl, SC.length(M.Node<K>, nl), hin0))
      +hxf = AL.allin_out(SC.append(Nat, P.before(c), P.after(c)), SC.length(M.Node<K>, nl), hinB)
      +hcpl0 = N.eq_from_is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg))
      +hxfp = L.subst(Nat, z => {NL.memn(1n+z, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, pl), Equal.sym(Nat, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hcpl0), hxf)
      +hpx = L.subst(Nat, z => {ST.pv(V, SC.snoc(Maybe<&2, V>, pl, Some{v}), 1n+z) == Some{v} : Maybe<&2, V>}, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hcpl0, SL.pv_snoc_same(V, pl, Some{v}))
      +hpb = SL.ents_psnoc(~K, ~V, P.before(c), nl, pl, Some{v}, DJ.nm_l(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +hpa = SL.ents_psnoc(~K, ~V, P.after(c), nl, pl, Some{v}, DJ.nm_r(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +hob = SL.oks_psnoc(~K, ~V, P.before(c), nl, pl, Some{v}, DJ.nm_l(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +hoa = SL.oks_psnoc(~K, ~V, P.after(c), nl, pl, Some{v}, DJ.nm_r(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +ls = LL.length_snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})
      +hcap = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls), N.lt_succ_le_succ(SC.length(M.Node<K>, nl), SC.pow2(d), hr))
      +hcpl = Equal.trans(Nat, SC.length(Maybe<&2, V>, SC.snoc(Maybe<&2, V>, pl, Some{v})), 1n+SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), LL.length_snoc(Maybe<&2, V>, pl, Some{v}), Equal.trans(Nat, 1n+SC.length(Maybe<&2, V>, pl), 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), L.subst(Nat, z => {1n+SC.length(Maybe<&2, V>, pl) == 1n+z : Nat}, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hcpl0, {==}), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls)))
      +hndB = 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, 0n, l, d, nl, pl, tg, fl, hg)))
      +hnd = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), LL.append_nil(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}))), AL.nd_put(P.before(c), 1n+SC.length(M.Node<K>, nl), P.after(c), hndB, hxf))
      +inbx = L.and_intro(Nat.is_lt(0n, 1n+SC.length(M.Node<K>, nl)), Nat.is_le(1n+SC.length(M.Node<K>, nl), 1n+SC.length(M.Node<K>, nl)), {==}, N.le_refl(1n+SC.length(M.Node<K>, nl)))
      +hin1 = AL.allin_app(P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}, 1n+SC.length(M.Node<K>, nl), AL.allin_up(P.before(c), SC.length(M.Node<K>, nl), AL.allin_l(P.before(c), P.after(c), SC.length(M.Node<K>, nl), hinB)), L.and_intro(Bool.and(Nat.is_lt(0n, 1n+SC.length(M.Node<K>, nl)), Nat.is_le(1n+SC.length(M.Node<K>, nl), 1n+SC.length(M.Node<K>, nl))), ST.allin(P.after(c), 1n+SC.length(M.Node<K>, nl)), inbx, AL.allin_up(P.after(c), SC.length(M.Node<K>, nl), AL.allin_r(P.before(c), P.after(c), SC.length(M.Node<K>, nl), hinB))))
      +hin = L.subst(Nat, z => {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), z) == True{} : Bool}, 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls), L.subst(List<&2, Nat>, z => {ST.allin(z, 1n+SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), LL.append_nil(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}))), hin1))
      +hlt = L.subst(List<&2, Nat>, z => {SC.length(Nat, SC.append(Nat, ST.ids(tg), z)) == SC.length(M.Node<K>, nl) : Nat}, fl, Nil{}, hflnil, N.eq_from_is_eq(SC.length(Nat, SC.append(Nat, ST.ids(tg), fl)), SC.length(M.Node<K>, nl), ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)))
      +hlt2 = Equal.trans(Nat, SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, ST.ids(tg), Nil{})), SC.length(M.Node<K>, nl), L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(tg)) == SC.length(Nat, z) : Nat}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), {==}), hlt)
      +hlb = Equal.trans(Nat, SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), SC.length(Nat, ST.ids(tg)), SC.length(M.Node<K>, nl), L.subst(List<&2, Nat>, z => {SC.length(Nat, z) == SC.length(Nat, ST.ids(tg)) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, {==}), hlt2)
      +hlen = Equal.trans(Nat, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{})), SC.length(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)})), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), L.subst(List<&2, Nat>, z => {SC.length(Nat, z) == SC.length(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)})) : Nat}, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), LL.append_nil(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}))), {==}), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)})), 1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), AL.len_put(P.before(c), 1n+SC.length(M.Node<K>, nl), P.after(c)), Equal.trans(Nat, 1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), L.subst(Nat, z => {1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))) == 1n+z : Nat}, SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), SC.length(M.Node<K>, nl), hlb, {==}), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls))))
      +hn = Equal.trans(Nat, n, SC.length(Nat, ST.ids(tg)), SC.length(M.Node<K>, nl), N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)), hlt2)
      +hroom = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(l)) == True{} : Bool}, SC.length(M.Node<K>, nl), n, Equal.sym(Nat, n, SC.length(M.Node<K>, nl), hn), N.lt_le_trans(SC.length(M.Node<K>, nl), SC.pow2(d), SC.pow2(l), hr, N.pow2_mono(d, l, ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg))))
      IF.ins_fin(~K, ~V, ~cmp, ~o, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg, c, 1n+SC.length(M.Node<K>, nl), k, v, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k}), SC.snoc(Maybe<&2, V>, pl, Some{v}), Nil{}, SL.agr_snoc(~K, ~cmp, ~o, SC.append(Nat, P.before(c), P.after(c)), nl, M.N{True{}, 0n, 0n, P.top(c), k}, hxf), SL.nd_snoc_same(K, nl, M.N{True{}, 0n, 0n, P.top(c), k}), {==}, hxf, hpx, hpb, hpa, hob, hoa, hbc, hplug, hok, hb, ha, 0n, d, {==}, {==}, ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg), hcap, hcpl, hnd, hin, hlen, hroom)
    case False{} True{}:

      +hin0 = ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)
      +hflnil = fl_nil(fl, SC.length(M.Node<K>, nl), N.eq_from_is_eq(0n, ST.fst0(fl), ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)), AL.allin_r(ST.ids(tg), fl, SC.length(M.Node<K>, nl), hin0))
      +hinB = L.subst(List<&2, Nat>, z => {ST.allin(z, SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, AL.allin_l(ST.ids(tg), fl, SC.length(M.Node<K>, nl), hin0))
      +hxf = AL.allin_out(SC.append(Nat, P.before(c), P.after(c)), SC.length(M.Node<K>, nl), hinB)
      +hcpl0 = N.eq_from_is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg))
      +hxfp = L.subst(Nat, z => {NL.memn(1n+z, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, pl), Equal.sym(Nat, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hcpl0), hxf)
      +hpx = L.subst(Nat, z => {ST.pv(V, SC.snoc(Maybe<&2, V>, pl, Some{v}), 1n+z) == Some{v} : Maybe<&2, V>}, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hcpl0, SL.pv_snoc_same(V, pl, Some{v}))
      +hpb = SL.ents_psnoc(~K, ~V, P.before(c), nl, pl, Some{v}, DJ.nm_l(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +hpa = SL.ents_psnoc(~K, ~V, P.after(c), nl, pl, Some{v}, DJ.nm_r(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +hob = SL.oks_psnoc(~K, ~V, P.before(c), nl, pl, Some{v}, DJ.nm_l(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +hoa = SL.oks_psnoc(~K, ~V, P.after(c), nl, pl, Some{v}, DJ.nm_r(1n+SC.length(Maybe<&2, V>, pl), P.before(c), P.after(c), hxfp))
      +ls = LL.length_snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})
      +hcap = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(1n+d)) == True{} : Bool}, 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls), N.lt_succ_le_succ(SC.length(M.Node<K>, nl), SC.pow2(1n+d), N.le_lt_trans(SC.length(M.Node<K>, nl), SC.pow2(d), SC.pow2(1n+d), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg), N.pow2_lt_succ(d))))
      +hcpl = Equal.trans(Nat, SC.length(Maybe<&2, V>, SC.snoc(Maybe<&2, V>, pl, Some{v})), 1n+SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), LL.length_snoc(Maybe<&2, V>, pl, Some{v}), Equal.trans(Nat, 1n+SC.length(Maybe<&2, V>, pl), 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), L.subst(Nat, z => {1n+SC.length(Maybe<&2, V>, pl) == 1n+z : Nat}, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hcpl0, {==}), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls)))
      +hndB = 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, 0n, l, d, nl, pl, tg, fl, hg)))
      +hnd = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), LL.append_nil(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}))), AL.nd_put(P.before(c), 1n+SC.length(M.Node<K>, nl), P.after(c), hndB, hxf))
      +inbx = L.and_intro(Nat.is_lt(0n, 1n+SC.length(M.Node<K>, nl)), Nat.is_le(1n+SC.length(M.Node<K>, nl), 1n+SC.length(M.Node<K>, nl)), {==}, N.le_refl(1n+SC.length(M.Node<K>, nl)))
      +hin1 = AL.allin_app(P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}, 1n+SC.length(M.Node<K>, nl), AL.allin_up(P.before(c), SC.length(M.Node<K>, nl), AL.allin_l(P.before(c), P.after(c), SC.length(M.Node<K>, nl), hinB)), L.and_intro(Bool.and(Nat.is_lt(0n, 1n+SC.length(M.Node<K>, nl)), Nat.is_le(1n+SC.length(M.Node<K>, nl), 1n+SC.length(M.Node<K>, nl))), ST.allin(P.after(c), 1n+SC.length(M.Node<K>, nl)), inbx, AL.allin_up(P.after(c), SC.length(M.Node<K>, nl), AL.allin_r(P.before(c), P.after(c), SC.length(M.Node<K>, nl), hinB))))
      +hin = L.subst(Nat, z => {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), z) == True{} : Bool}, 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls), L.subst(List<&2, Nat>, z => {ST.allin(z, 1n+SC.length(M.Node<K>, nl)) == True{} : Bool}, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), LL.append_nil(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}))), hin1))
      +hlt = L.subst(List<&2, Nat>, z => {SC.length(Nat, SC.append(Nat, ST.ids(tg), z)) == SC.length(M.Node<K>, nl) : Nat}, fl, Nil{}, hflnil, N.eq_from_is_eq(SC.length(Nat, SC.append(Nat, ST.ids(tg), fl)), SC.length(M.Node<K>, nl), ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)))
      +hlt2 = Equal.trans(Nat, SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, ST.ids(tg), Nil{})), SC.length(M.Node<K>, nl), L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(tg)) == SC.length(Nat, z) : Nat}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), {==}), hlt)
      +hlb = Equal.trans(Nat, SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), SC.length(Nat, ST.ids(tg)), SC.length(M.Node<K>, nl), L.subst(List<&2, Nat>, z => {SC.length(Nat, z) == SC.length(Nat, ST.ids(tg)) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, {==}), hlt2)
      +hlen = Equal.trans(Nat, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{})), SC.length(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)})), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), L.subst(List<&2, Nat>, z => {SC.length(Nat, z) == SC.length(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)})) : Nat}, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), Nil{}), SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}), LL.append_nil(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)}))), {==}), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, P.before(c), Con{1n+SC.length(M.Node<K>, nl), P.after(c)})), 1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), AL.len_put(P.before(c), 1n+SC.length(M.Node<K>, nl), P.after(c)), Equal.trans(Nat, 1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), 1n+SC.length(M.Node<K>, nl), SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), L.subst(Nat, z => {1n+SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))) == 1n+z : Nat}, SC.length(Nat, SC.append(Nat, P.before(c), P.after(c))), SC.length(M.Node<K>, nl), hlb, {==}), Equal.sym(Nat, SC.length(M.Node<K>, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k})), 1n+SC.length(M.Node<K>, nl), ls))))
      +hn = Equal.trans(Nat, n, SC.length(Nat, ST.ids(tg)), SC.length(M.Node<K>, nl), N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)), hlt2)
      +hroom = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(l)) == True{} : Bool}, SC.length(M.Node<K>, nl), n, Equal.sym(Nat, n, SC.length(M.Node<K>, nl), hn), N.lt_le_trans(SC.length(M.Node<K>, nl), SC.pow2(1n+d), SC.pow2(l), N.le_lt_trans(SC.length(M.Node<K>, nl), SC.pow2(d), SC.pow2(1n+d), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg), N.pow2_lt_succ(d)), N.pow2_mono(1n+d, l, N.lt_succ_le_succ(d, l, hgw))))
      IF.ins_fin(~K, ~V, ~cmp, ~o, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg, c, 1n+SC.length(M.Node<K>, nl), k, v, SC.snoc(M.Node<K>, nl, M.N{True{}, 0n, 0n, P.top(c), k}), SC.snoc(Maybe<&2, V>, pl, Some{v}), Nil{}, SL.agr_snoc(~K, ~cmp, ~o, SC.append(Nat, P.before(c), P.after(c)), nl, M.N{True{}, 0n, 0n, P.top(c), k}, hxf), SL.nd_snoc_same(K, nl, M.N{True{}, 0n, 0n, P.top(c), k}), {==}, hxf, hpx, hpb, hpa, hob, hoa, hbc, hplug, hok, hb, ha, 0n, 1n+d, {==}, {==}, N.lt_succ_le_succ(d, l, hgw), hcap, hcpl, hnd, hin, hlen, hroom)
    case False{} False{}:
      +hin0 = ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)
      +hflnil = fl_nil(fl, SC.length(M.Node<K>, nl), N.eq_from_is_eq(0n, ST.fst0(fl), ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)), AL.allin_r(ST.ids(tg), fl, SC.length(M.Node<K>, nl), hin0))
      +hlt = L.subst(List<&2, Nat>, z => {SC.length(Nat, SC.append(Nat, ST.ids(tg), z)) == SC.length(M.Node<K>, nl) : Nat}, fl, Nil{}, hflnil, N.eq_from_is_eq(SC.length(Nat, SC.append(Nat, ST.ids(tg), fl)), SC.length(M.Node<K>, nl), ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)))
      +hlt2 = Equal.trans(Nat, SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, ST.ids(tg), Nil{})), SC.length(M.Node<K>, nl), L.subst(List<&2, Nat>, z => {SC.length(Nat, ST.ids(tg)) == SC.length(Nat, z) : Nat}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), {==}), hlt)
      +hn = Equal.trans(Nat, n, SC.length(Nat, ST.ids(tg)), SC.length(M.Node<K>, nl), N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg)), hlt2)
      +edl = N.le_antisym(d, l, ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, 0n, l, d, nl, pl, tg, fl, hg), N.not_lt_le(d, l, hgw))
      +hful0 = L.subst(Nat, z => {Nat.is_lt(SC.length(M.Node<K>, nl), SC.pow2(z)) == False{} : Bool}, d, l, edl, hr)
      +hful = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(l)) == False{} : Bool}, SC.length(M.Node<K>, nl), n, Equal.sym(Nat, n, SC.length(M.Node<K>, nl), hn), hful0)
      +es = spec_rej(~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, 0n, l, d, nl, pl, tg, fl, hg), hful)
      (ST.SH{n, root, lo, hi, 0n, l, d, nl, pl, tg, fl}, (Fail{M.Rejected{M.CapacityExceeded{}, k, v}}, ({==}, (es, hg))))

# ---- reusing the free list's head ----


def reuse_case(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +f: 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, 1n+f, l, d, nl, pl, tg, fl) == True{} : Bool}, +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>}, +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}, +y: M.Node<K>, +hy: {ST.nd(K, nl, 1n+f) == y : M.Node<K>}) -> 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, 1n+f, l, d, nl, pl, tg, fl}), k, v), MI.put_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), MI.alloc_read(~K, ~V, ~cmp, 1n+f, P.top(c), k, v, (ST.SH{n, root, lo, hi, 1n+f, l, d, nl, pl, tg, fl}, y)))):
  match fl y:
    case Nil{} +y:
      Empty.absurd(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, 1n+f, l, d, nl, pl, tg, Nil{}}), k, v), MI.put_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), MI.alloc_read(~K, ~V, ~cmp, 1n+f, P.top(c), k, v, (ST.SH{n, root, lo, hi, 1n+f, l, d, nl, pl, tg, fl}, y)))), L.false_true(ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Nil{}, hg)))
    case Con{+h, +t} M.N{+c0, +a, +b, +q, +kk}:
      +eh = N.eq_from_is_eq(1n+f, h, ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hf0 = L.and_left(ST.is_free(K, ST.nd(K, nl, h), ST.fst0(t)), ST.fll(~K, nl, t), ST.g_cfll(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hf1 = L.subst(Nat, z => {ST.is_free(K, ST.nd(K, nl, z), ST.fst0(t)) == True{} : Bool}, h, 1n+f, Equal.sym(Nat, 1n+f, h, eh), hf0)
      Empty.absurd(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, 1n+f, l, d, nl, pl, tg, Con{h, t}}), k, v), MI.put_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), MI.alloc_read(~K, ~V, ~cmp, 1n+f, P.top(c), k, v, (ST.SH{n, root, lo, hi, 1n+f, l, d, nl, pl, tg, fl}, M.N{c0, a, b, q, kk})))), L.false_true(L.subst(M.Node<K>, z => {ST.is_free(K, z, ST.fst0(t)) == True{} : Bool}, ST.nd(K, nl, 1n+f), M.N{c0, a, b, q, kk}, hy, hf1)))
    case Con{+h, +t} M.Free{+nx}:
      +eh = N.eq_from_is_eq(1n+f, h, ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hnd0 = L.subst(Nat, z => {NL.nodupn(SC.append(Nat, ST.ids(tg), Con{z, t})) == True{} : Bool}, h, 1n+f, Equal.sym(Nat, 1n+f, h, eh), ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hnd1 = L.subst(List<&2, Nat>, z => {NL.nodupn(SC.append(Nat, z, Con{1n+f, t})) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, hnd0)
      +hxf = DJ.dj_l(SC.append(Nat, P.before(c), P.after(c)), Con{1n+f, t}, hnd1, 1n+f, DJ.mem_hd(1n+f, t))
      +hxt = DJ.nd_head(1n+f, t, DJ.ndr(SC.append(Nat, P.before(c), P.after(c)), Con{1n+f, t}, hnd1))
      +hin0 = L.subst(Nat, z => {ST.allin(SC.append(Nat, ST.ids(tg), Con{z, t}), SC.length(M.Node<K>, nl)) == True{} : Bool}, h, 1n+f, Equal.sym(Nat, 1n+f, h, eh), ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hin1 = L.subst(List<&2, Nat>, z => {ST.allin(SC.append(Nat, z, Con{1n+f, t}), SC.length(M.Node<K>, nl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, hin0)
      +hxin = L.and_left(Bool.and(Nat.is_lt(0n, 1n+f), Nat.is_le(1n+f, SC.length(M.Node<K>, nl))), ST.allin(t, SC.length(M.Node<K>, nl)), AL.allin_r(SC.append(Nat, P.before(c), P.after(c)), Con{1n+f, t}, SC.length(M.Node<K>, nl), hin1))
      +hflt = N.succ_le_lt(f, SC.length(M.Node<K>, nl), L.and_right(Nat.is_lt(0n, 1n+f), Nat.is_le(1n+f, SC.length(M.Node<K>, nl)), hxin))
      +hcpl0 = N.eq_from_is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hfltp = L.subst(Nat, z => {Nat.is_lt(f, z) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(Maybe<&2, V>, pl), Equal.sym(Nat, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), hcpl0), hflt)
      +hfl0 = L.and_right(ST.is_free(K, ST.nd(K, nl, h), ST.fst0(t)), ST.fll(~K, nl, t), ST.g_cfll(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hfll = Equal.trans(Bool, ST.fll(~K, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k}), t), ST.fll(~K, nl, t), True{}, FR.fll_frame(~K, t, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k}, hxt), hfl0)
      +hf0 = L.and_left(ST.is_free(K, ST.nd(K, nl, h), ST.fst0(t)), ST.fll(~K, nl, t), ST.g_cfll(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hf1 = L.subst(Nat, z => {ST.is_free(K, ST.nd(K, nl, z), ST.fst0(t)) == True{} : Bool}, h, 1n+f, Equal.sym(Nat, 1n+f, h, eh), hf0)
      +hfree = N.eq_from_is_eq(nx, ST.fst0(t), L.subst(M.Node<K>, z => {ST.is_free(K, z, ST.fst0(t)) == True{} : Bool}, ST.nd(K, nl, 1n+f), M.Free{nx}, hy, hf1))
      +lw = FR.len_wr(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})
      +hcap = L.subst(Nat, z => {Nat.is_le(z, SC.pow2(d)) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), SC.length(M.Node<K>, nl), lw), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hcpl = Equal.trans(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+f, Some{v})), SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), SL.len_ex(V, pl, 1n+f, Some{v}), Equal.trans(Nat, SC.length(Maybe<&2, V>, pl), SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), hcpl0, Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), SC.length(M.Node<K>, nl), lw)))
      +hnd = AL.nd_move(P.before(c), P.after(c), 1n+f, t, hnd1)
      +hin = L.subst(Nat, z => {ST.allin(SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+f, P.after(c)}), t), z) == True{} : Bool}, SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), SC.length(M.Node<K>, nl), lw), AL.allin_move(P.before(c), P.after(c), 1n+f, t, SC.length(M.Node<K>, nl), hin1))
      +hl0 = L.subst(Nat, z => {SC.length(Nat, SC.append(Nat, ST.ids(tg), Con{z, t})) == SC.length(M.Node<K>, nl) : Nat}, h, 1n+f, Equal.sym(Nat, 1n+f, h, eh), N.eq_from_is_eq(SC.length(Nat, SC.append(Nat, ST.ids(tg), Con{h, t})), SC.length(M.Node<K>, nl), ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg)))
      +hl1 = L.subst(List<&2, Nat>, z => {SC.length(Nat, SC.append(Nat, z, Con{1n+f, t})) == SC.length(M.Node<K>, nl) : Nat}, ST.ids(tg), SC.append(Nat, P.before(c), P.after(c)), hbc, hl0)
      +hlen = Equal.trans(Nat, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), Con{1n+f, P.after(c)}), t)), SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), P.after(c)), Con{1n+f, t})), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), AL.len_move(P.before(c), P.after(c), 1n+f, t), Equal.trans(Nat, SC.length(Nat, SC.append(Nat, SC.append(Nat, P.before(c), P.after(c)), Con{1n+f, t})), SC.length(M.Node<K>, nl), SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), hl1, Equal.sym(Nat, SC.length(M.Node<K>, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k})), SC.length(M.Node<K>, nl), lw)))
      +hn = N.eq_from_is_eq(n, SC.length(Nat, ST.ids(tg)), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))
      +hlt0 = Equal.trans(Nat, 1n+SC.length(Nat, SC.append(Nat, ST.ids(tg), t)), SC.length(Nat, SC.append(Nat, ST.ids(tg), Con{1n+f, t})), SC.length(M.Node<K>, nl), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, ST.ids(tg), Con{1n+f, t})), 1n+SC.length(Nat, SC.append(Nat, ST.ids(tg), t)), P.cons_len(ST.ids(tg), 1n+f, t)), hl0)
      +hle = L.subst(Nat, z => {Nat.is_le(SC.length(Nat, ST.ids(tg)), z) == True{} : Bool}, Nat.add(SC.length(Nat, ST.ids(tg)), SC.length(Nat, t)), SC.length(Nat, SC.append(Nat, ST.ids(tg), t)), Equal.sym(Nat, SC.length(Nat, SC.append(Nat, ST.ids(tg), t)), Nat.add(SC.length(Nat, ST.ids(tg)), SC.length(Nat, t)), LL.length_append(Nat, ST.ids(tg), t)), N.le_add_right(SC.length(Nat, ST.ids(tg)), SC.length(Nat, t)))
      +hltL = L.subst(Nat, z => {Nat.is_lt(SC.length(Nat, ST.ids(tg)), z) == True{} : Bool}, 1n+SC.length(Nat, SC.append(Nat, ST.ids(tg), t)), SC.length(M.Node<K>, nl), hlt0, N.le_lt_succ(SC.length(Nat, ST.ids(tg)), SC.length(Nat, SC.append(Nat, ST.ids(tg), t)), hle))
      +hroom0 = N.lt_le_trans(SC.length(Nat, ST.ids(tg)), SC.length(M.Node<K>, nl), SC.pow2(l), hltL, N.le_trans(SC.length(M.Node<K>, nl), SC.pow2(d), SC.pow2(l), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg), N.pow2_mono(d, l, ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg))))
      +hroom = L.subst(Nat, z => {Nat.is_lt(z, SC.pow2(l)) == True{} : Bool}, SC.length(Nat, ST.ids(tg)), n, Equal.sym(Nat, n, SC.length(Nat, ST.ids(tg)), hn), hroom0)
      IF.ins_fin(~K, ~V, ~cmp, ~o, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg, c, 1n+f, k, v, PR.wr_nl(K, nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k}), PR.ex_pl(V, pl, 1n+f, Some{v}), t, AG.agr_wr(~K, ~cmp, ~o, SC.append(Nat, P.before(c), P.after(c)), nl, 1n+f, M.N{True{}, 0n, 0n, P.top(c), k}, hxf), FR.nd_wr_same(K, nl, f, M.N{True{}, 0n, 0n, P.top(c), k}, hflt), {==}, hxf, SL.pv_ex_same(V, pl, f, Some{v}, hfltp), SL.ents_pex(~K, ~V, P.before(c), nl, pl, 1n+f, Some{v}, DJ.nm_l(1n+f, P.before(c), P.after(c), hxf)), SL.ents_pex(~K, ~V, P.after(c), nl, pl, 1n+f, Some{v}, DJ.nm_r(1n+f, P.before(c), P.after(c), hxf)), SL.oks_pex(~K, ~V, P.before(c), nl, pl, 1n+f, Some{v}, DJ.nm_l(1n+f, P.before(c), P.after(c), hxf)), SL.oks_pex(~K, ~V, P.after(c), nl, pl, 1n+f, Some{v}, DJ.nm_r(1n+f, P.before(c), P.after(c), hxf)), hbc, hplug, hok, hb, ha, nx, d, hfll, hfree, ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, 1n+f, l, d, nl, pl, tg, Con{h, t}, hg), hcap, hcpl, hnd, hin, hlen, hroom)