import Base
import ../../lib/logic.bend as L
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 ./tree.bend as TR
import ./ends.bend as EN
import ./path.bend as P
import ./plug.bend as PG
import ./ord.bend as OR
import ./cur.bend as CU
import ./cnx.bend as CX
import ./prim.bend as PR
import ./putf.bend as PF
import ./find.bend as FI
import ./slot.bend as SL

# iterator_set_value: the current id, when a node, gets the value: the
# specification's set_val of the current key, the old value the answer.
# (source: tools/generators/tm_hand/csv.src)


def sv_w(~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>, +j: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +ov: V, +hx: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, k} : M.Node<K>}, +hm: {ST.pv(V, pl, 1n+j) == Some{ov} : Maybe<&2, V>}, +he: {ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})) == S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry<K, V>>}, +hg2: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_done(~K, ~V, ~cmp, nx, 1n+j, lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, Some{ov}))):
  +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)
  +eent = L.subst(Maybe<&2, V>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, M.N{c0, x1, x2, x3, k}, z) : Maybe<&2, M.Entry<K, V>>}, ST.pv(V, pl, 1n+j), Some{ov}, hm, L.subst(M.Node<K>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, z, ST.pv(V, pl, 1n+j)) : Maybe<&2, M.Entry<K, V>>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx, {==}))
  +hE = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, ov}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), 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, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, {==}), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, ov}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), FI.ents_app(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl), L.subst(Maybe<&2, M.Entry<K, V>>, z => {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) : List<&2, M.Entry<K, V>>}, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), Some{M.Entry{k, ov}}, eent, {==})))
  +hord = 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, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, ov}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), hE, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
  +efe = Equal.trans(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, ov}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})), Some{M.Entry{k, ov}}, L.subst(List<&2, M.Entry<K, V>>, z => {S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.find_e(~K, ~V, ~cmp, k, z) : Maybe<&2, M.Entry<K, V>>}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{k, ov}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), hE, {==}), OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{k, ov}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), hord, O.refl(~K, ~cmp, ~o, k)))
  %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx) : CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), M.node_key(~K, _), lo2, hi2, fw}, v), MI.iterator_set_done(~K, ~V, ~cmp, nx, 1n+j, lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, Some{ov})))
  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{M.Entry{k, ov}}, efe) : CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.set_value_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), CU.ck(~K, nl, nx), k, lo2, hi2, fw, v, S.val_m(K, V, _)), MI.iterator_set_done(~K, ~V, ~cmp, nx, 1n+j, lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, Some{ov})))
  +ek = Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, 1n+j), Some{k}, L.subst(M.Node<K>, z => {CU.ck(~K, nl, 1n+j) == M.node_key(~K, z) : Maybe<&2, K>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx, {==}))
  +esp = L.subst(Maybe<&2, K>, z => {(S.CR{S.TM{l, S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, CU.ck(~K, nl, nx), z, lo2, hi2, fw}, Done{ov}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}, CU.ck(~K, nl, nx), CU.ck(~K, nl, 1n+j), lo2, hi2, fw}, Done{ov}) : S.Cursor<K, V> & Result<&2, &2, M.Error, V>}, CU.ck(~K, nl, 1n+j), Some{k}, Equal.sym(Maybe<&2, K>, Some{k}, CU.ck(~K, nl, 1n+j), ek), L.subst(List<&2, M.Entry<K, V>>, z => {(S.CR{S.TM{l, z}, CU.ck(~K, nl, nx), CU.ck(~K, nl, 1n+j), lo2, hi2, fw}, Done{ov}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}, CU.ck(~K, nl, nx), CU.ck(~K, nl, 1n+j), lo2, hi2, fw}, Done{ov}) : S.Cursor<K, V> & Result<&2, &2, M.Error, V>}, ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), he, {==}))
  (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, nx, 1n+j, lo2, hi2, fw}, (Done{ov}, ({==}, (esp, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hg2, L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))))))

def sv_u(~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>, +j: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +ov: V, +hx: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, k} : M.Node<K>}, +hm: {ST.pv(V, pl, 1n+j) == Some{ov} : Maybe<&2, V>}, hc2: {ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})) == S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry<K, V>>} & {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_done(~K, ~V, ~cmp, nx, 1n+j, lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, Some{ov}))):
  match hc2:
    case Tuple{he, hg2}:
      sv_w(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, nx, lo2, hi2, fw, v, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, ov, hx, hm, he, hg2)


def sv_t(~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>, +j: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, +x: M.Node<K>, +hx: {ST.nd(K, nl, 1n+j) == x : M.Node<K>}, +m: Maybe<&2, V>, +hm: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_done(~K, ~V, ~cmp, nx, 1n+j, lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, m))):
  match x m:
    case M.Free{f} +m:
      Empty.absurd(CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_done(~K, ~V, ~cmp, nx, 1n+j, lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, m))), L.false_true(L.subst(M.Node<K>, z => {ST.is_node(K, z, ST.rid(pa), ST.rid(pb), P.top(pc)) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.Free{f}, hx, TR.rep_node(~K, 1n+j, pa, pb, P.top(pc), nl, h3))))
    case M.N{c0, x1, x2, x3, k} None{}:
      Empty.absurd(CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_done(~K, ~V, ~cmp, nx, 1n+j, lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, None{}))), L.false_true(L.subst(Maybe<&2, V>, z => {ST.some2(V, z) == True{} : Bool}, ST.pv(V, pl, 1n+j), None{}, hm, FI.pay_node(~V, 1n+j, pa, pb, pl, SL.pay_oks(~K, ~V, ST.TN{1n+j, pa, pb}, nl, pl, SL.oks_split_l(~K, ~V, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc), nl, pl, SL.oks_split_r(~K, ~V, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc)), nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), hid, 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, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)))))))))))
    case M.N{+c0, +x1, +x2, +x3, +k} Some{+ov}:
      +hfin = L.subst(M.Node<K>, z => {S.is_eq(TR.kc(~K, ~cmp, k, z)) == True{} : Bool}, M.N{c0, x1, x2, x3, k}, ST.nd(K, nl, 1n+j), Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, k}, hx), L.subst(Cmp, w => {S.is_eq(w) == True{} : Bool}, EQ{}, cmp(k, k), Equal.sym(Cmp, cmp(k, k), EQ{}, O.refl(~K, ~cmp, ~o, k)), {==}))
      sv_u(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, nx, lo2, hi2, fw, v, hc, pc, pa, pb, hid, hw, h3, h4, c0, x1, x2, x3, k, ov, hx, hm, PF.hit_core(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc), pc, 1n+j, pa, pb, k, v, hid, h3, hfin, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j), {==}, {==}, TR.rep_node(~K, 1n+j, pa, pb, P.top(pc), nl, h3), FI.pay_node(~V, 1n+j, pa, pb, pl, SL.pay_oks(~K, ~V, ST.TN{1n+j, pa, pb}, nl, pl, SL.oks_split_l(~K, ~V, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc), nl, pl, SL.oks_split_r(~K, ~V, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc)), nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), hid, 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, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))))))))))


def sv_s(~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>, +j: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}, v)):
  sv_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, nx, lo2, hi2, fw, v, hc, pc, pa, pb, hid, hw, h3, h4, ST.nd(K, nl, 1n+j), {==}, ST.pv(V, pl, 1n+j), {==})

def sv_r(~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>, +j: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, r3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}, v)):
  match r3:
    case Tuple{h3, h4}:
      +hid = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), h1))
      +e1 = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(pc), z) : List<&2, Nat>}, SC.append(Nat, SC.append(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}), P.after(pc)), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), LL.append_assoc(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}, P.after(pc)), {==})
      +e2 = Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), LL.append_assoc(Nat, P.before(pc), ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}))
      sv_s(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, nx, lo2, hi2, fw, v, hc, pc, pa, pb, hid, Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hid, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), e1, e2)), h3, h4)

def sv_q(~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>, +j: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, rest: {PG.plug(pc, ST.TN{1n+j, pa, pb}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool})) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}, v)):
  match rest:
    case Tuple{h2, r3}:
      sv_r(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, nx, lo2, hi2, fw, v, hc, pc, pa, pb, h1, r3)


def sv_p(~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>, +j: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, pt: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{1n+j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{1n+j, pa_, pb_}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, 1n+j, nl) == True{} : Bool}))>>>) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}), v), MI.iterator_set_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}, v)):
  match pt:
    case Tuple{+pc, Tuple{+pa, Tuple{+pb, Tuple{h1, rest}}}}:
      sv_q(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, nx, lo2, hi2, fw, v, hc, pc, pa, pb, h1, rest)


def set_value_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>, +cu: Nat, +nx: Nat, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +v: V, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Result<&2, &2, M.Error, V>, S.iterator_set_value(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), v), MI.iterator_set_value(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, v)):
  match cu:
    case 0n:
      (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}, (Fail{M.NoCurrent{}}, ({==}, ({==}, hc))))
    case 1n+j:
      sv_p(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, nx, lo2, hi2, fw, v, hc, CX.path_to(~K, ~cmp, ~o, tg, nl, Nil{}, 1n+j, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)), {==}, L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))), L.and_right(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)))))