1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/list.bend as LL 4 import ../../lib/order.bend as O 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/balanced_search_tree/main.bend as S 7 import ../../../src/containers/balanced_search_tree.bend as M 8 import ./state.bend as ST 9 import ./mirror.bend as MI 10 import ./ok.bend as OK 11 import ./reads.bend as RD 12 import ./find.bend as FI 13 import ./ends.bend as EN 14 import ./path.bend as P 15 import ./plug.bend as PG 16 import ./ord.bend as OR 17 import ./slot.bend as SL 18 import ./prim.bend as PR 19 import ./tree.bend as TR 20 import ./spath.bend as SP 21 import ./alloc.bend as AC 22 import ./putf.bend as PF 23 24 # put, put_if_absent, replace and replace_if_equal over a good shadow: the 25 # search from the root ends at a path and a subtree (WRAP below, shared by 26 # every operation); an empty subtree means the key is absent (put allocates, 27 # appending or reusing a freed slot, and inserts), a node holds it (its 28 # payload is the lookup, exchanging it is set_val). Each mirror operation 29 # refines the specification's. (source: tools/generators/tm_hand/putm.src) 30 31 32 33 # ---- the node found by the search ---- 34 35 def tn_zero(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +c: List<&2, P.Fr>, +a: ST.Tr, +b: ST.Tr, +hr: {ST.rep(~K, ST.TN{0n, a, b}, P.top(c), nl) == True{} : Bool}) -> Empty: 36 L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.rid(a), ST.rid(b), P.top(c)), Bool.and(ST.rep(~K, a, 0n, nl), ST.rep(~K, b, 0n, nl))), hr)) 37 38 def tn_hx(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +c: List<&2, P.Fr>, +j: Nat, +a: ST.Tr, +b: ST.Tr, +hr: {ST.rep(~K, ST.TN{1n+j, a, b}, P.top(c), nl) == True{} : Bool}) -> {ST.is_node(K, ST.nd(K, nl, 1n+j), ST.rid(a), ST.rid(b), P.top(c)) == True{} : Bool}: 39 L.and_left(ST.is_node(K, ST.nd(K, nl, 1n+j), ST.rid(a), ST.rid(b), P.top(c)), Bool.and(ST.rep(~K, a, 1n+j, nl), ST.rep(~K, b, 1n+j, nl)), L.and_right(Nat.is_lt(0n, 1n+j), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+j), ST.rid(a), ST.rid(b), P.top(c)), Bool.and(ST.rep(~K, a, 1n+j, nl), ST.rep(~K, b, 1n+j, nl))), hr)) 40 41 def tn_hm(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +c: List<&2, P.Fr>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), nl, pl) == True{} : Bool}) -> {ST.some2(V, ST.pv(V, pl, i)) == True{} : Bool}: 42 FI.pay_node(~V, i, a, b, pl, SL.pay_oks(~K, ~V, ST.TN{i, a, b}, nl, pl, SL.oks_split_l(~K, ~V, ST.ids(ST.TN{i, a, b}), P.after(c), nl, pl, SL.oks_split_r(~K, ~V, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c)), nl, pl, hk)))) 43 44 def tn_hbc(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +c: List<&2, P.Fr>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))) : List<&2, Nat>}) -> {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))) : List<&2, Nat>}: 45 Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), hwh) 46 47 # exchanging the found payload for w: the entries set_val(k, w), still good 48 def tn_core(~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>, +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}, +k: K, +w: V, +c: List<&2, P.Fr>, +j: Nat, +a: ST.Tr, +b: ST.Tr, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+j, a, b}), P.after(c))), nl, pl) == True{} : Bool}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+j, a, b}), P.after(c))) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{1n+j, a, b}, P.top(c), nl) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, ST.TN{1n+j, a, b}, nl) == True{} : Bool}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{w})) == S.set_val(~K, ~V, ~cmp, k, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>} & {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{w}), tg, fl) == True{} : Bool}: 49 PF.hit_core(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, c, 1n+j, a, b, k, w, tn_hbc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+j, a, b, hwh), hr, hfin, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j), {==}, {==}, tn_hx(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, j, a, b, hr), tn_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+j, a, b, hk)) 50 51 # ---- put ---- 52 53 54 # an empty subtree: allocate by the free chain, then insert 55 def put_te(~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>, +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}, +k: K, +v: V, +c: List<&2, P.Fr>, +t: ST.Tr, +ht: {t == ST.TE{} : ST.Tr}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), 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}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))): 56 match free: 57 case 0n: 58 +hwh2 = L.subst(ST.Tr, z => {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(z), P.after(c))) : List<&2, Nat>}, t, ST.TE{}, ht, hwh) 59 +hbc = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), P.after(c)), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), hwh2) 60 +hpl = L.subst(ST.Tr, z => {tg == PG.plug(c, z) : ST.Tr}, t, ST.TE{}, ht, hplug) 61 +hok = L.subst(ST.Tr, z => {P.ctxok(~K, c, ST.rid(z), nl) == True{} : Bool}, t, ST.TE{}, ht, hokc) 62 AC.app_case(~K, ~V, ~cmp, ~o, n, root, lo, hi, l, d, nl, pl, tg, fl, hg, c, k, v, hbc, hpl, hok, hb, ha, Nat.is_lt(SC.length(M.Node, nl), SC.pow2(d)), {==}, Nat.is_lt(d, l), {==}) 63 case 1n+f: 64 +hwh2 = L.subst(ST.Tr, z => {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(z), P.after(c))) : List<&2, Nat>}, t, ST.TE{}, ht, hwh) 65 +hbc = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), P.after(c)), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), hwh2) 66 +hpl = L.subst(ST.Tr, z => {tg == PG.plug(c, z) : ST.Tr}, t, ST.TE{}, ht, hplug) 67 +hok = L.subst(ST.Tr, z => {P.ctxok(~K, c, ST.rid(z), nl) == True{} : Bool}, t, ST.TE{}, ht, hokc) 68 AC.reuse_case(~K, ~V, ~cmp, ~o, n, root, lo, hi, f, l, d, nl, pl, tg, fl, hg, c, k, v, hbc, hpl, hok, hb, ha, ST.nd(K, nl, 1n+f), {==}) 69 70 def put_h(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +v: V, +c: List<&2, P.Fr>, +j: Nat, +hfd: {ST.pv(V, pl, 1n+j) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}, +hm: {ST.some2(V, m) == True{} : Bool}, +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>}, +hgd: {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}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))): 71 match m: 72 case None{}: 73 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))), L.false_true(hm)) 74 case Some{+vi}: 75 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vi}, Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), Some{vi}, Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd), hmi)) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, v, _), MI.put_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))) 76 %Equal.sym(List<&2, M.Entry>, S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), Equal.sym(List<&2, M.Entry>, 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)) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, (S.TM{l, _}, Done{Some{vi}}), MI.put_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))) 77 (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, (Done{Some{vi}}, (L.subst(Maybe<&2, V>, z => {MI.rp(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, Done{z})) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}), Done{Some{vi}}) : M.TreeMap & Result<&2, &2, M.Rejected, Maybe<&2, V>>}, Some{vi}, ST.pv(V, pl, 1n+j), Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), Some{vi}, hmi), {==}), ({==}, hgd)))) 78 79 def put_hc(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +v: V, +c: List<&2, P.Fr>, +j: Nat, +hfd: {ST.pv(V, pl, 1n+j) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hm: {ST.some2(V, ST.pv(V, pl, 1n+j)) == True{} : Bool}, hc: {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>} & {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}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))): 80 match hc: 81 case Tuple{he, hgd}: 82 put_h(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, v, c, j, hfd, ST.pv(V, pl, 1n+j), {==}, hm, he, hgd) 83 84 def put_tn(~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>, +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}, +k: K, +v: V, +c: List<&2, P.Fr>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +hfd: {ST.pv(V, pl, i) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hk: {EN.oks(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), nl, pl) == True{} : Bool}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{i, a, b}, P.top(c), nl) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, ST.TN{i, a, b}, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{i, P.top(c), SP.dir(c)}))): 85 match i: 86 case 0n: 87 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))), tn_zero(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, a, b, hr)) 88 case 1n+j: 89 put_hc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, v, c, j, hfd, tn_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+j, a, b, hk), tn_core(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, c, j, a, b, hk, hwh, hr, hfin)) 90 91 def put_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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), 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}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 92 match t: 93 case ST.TE{}: 94 put_te(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, c, ST.TE{}, {==}, hwh, hplug, hr, hokc, hb, ha, hfin) 95 case ST.TN{+i, +a, +b}: 96 put_tn(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, c, i, a, b, hfd, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), hwh, hk0), hwh, hr, hfin) 97 98 def put_c2(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, r2: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 99 match r2: 100 case Tuple{ha, hfin}: 101 put_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, hfd, hwh, hplug, hr, hokc, hb, ha, hfin) 102 103 def put_c(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, r: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 104 match r: 105 case Tuple{hts, Tuple{hwh, Tuple{hplug, Tuple{hr, Tuple{hokc, Tuple{hb, r2}}}}}}: 106 +hts2 = hts 107 %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))) 108 put_c2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, L.subst(M.Search, z => {ST.pv(V, pl, FI.sfound(z)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2, FI.tfind(~K, ~V, ~cmp, ~o, nl, pl, tg, 0n, False{}, k, 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), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), hwh, hplug, hr, hokc, hb, r2) 109 110 def put_sp(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, P.Fr>, c => Sigma<&1, &1, ST.Tr, t => {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))>>) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 111 match sp: 112 case Tuple{+c, Tuple{+t, r}}: 113 put_c(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, r) 114 115 def put_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>, +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}, +k: K, +v: V) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v)): 116 +ean = LL.append_nil(Nat, ST.ids(tg)) 117 +hk1 = 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)) 118 +hk0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, 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), ean), hk1) 119 +ho0 = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, 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), ean), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 120 %Equal.sym(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), RD.search_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, 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_found(~K, ~V, ~cmp, k, v, _)) 121 put_sp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, SP.spath(~K, ~V, ~cmp, ~o, nl, pl, tg, Nil{}, k, 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), ho0, hk0, {==}, {==})) 122 123 # ---- put_if_absent: a found key is left, an absent one put ---- 124 125 126 def absent_h(~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>, +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}, +k: K, +v: V, +c: List<&2, P.Fr>, +j: Nat, +hfd: {ST.pv(V, pl, 1n+j) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}, +hm: {ST.some2(V, m) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))): 127 match m: 128 case None{}: 129 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))), L.false_true(hm)) 130 case Some{+vi}: 131 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vi}, Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), Some{vi}, Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd), hmi)) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.absent_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, v, _), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))) 132 (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (Done{Some{vi}}, (L.subst(Maybe<&2, V>, z => {MI.rp(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, Done{z})) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), Done{Some{vi}}) : M.TreeMap & Result<&2, &2, M.Rejected, Maybe<&2, V>>}, Some{vi}, ST.pv(V, pl, 1n+j), Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), Some{vi}, hmi), {==}), ({==}, hg)))) 133 134 def absent_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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), 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}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 135 match t: 136 case ST.TE{}: 137 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}, Equal.sym(Maybe<&2, V>, None{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd)) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.absent_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, v, _), MI.put_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), MI.allocate(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, P.top(c), k, v))) 138 L.subst(Maybe<&2, V>, z => OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, v, z), MI.put_allocated(~K, ~V, ~cmp, P.top(c), SP.dir(c), MI.allocate(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, P.top(c), k, v))), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}, Equal.sym(Maybe<&2, V>, None{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd), put_te(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, c, ST.TE{}, {==}, hwh, hplug, hr, hokc, hb, ha, hfin)) 139 case ST.TN{+i, +a, +b}: 140 match i: 141 case 0n: 142 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))), tn_zero(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, a, b, hr)) 143 case 1n+j: 144 absent_h(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, c, j, hfd, ST.pv(V, pl, 1n+j), {==}, tn_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+j, a, b, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+j, a, b}), P.after(c))), hwh, hk0))) 145 146 def absent_c2(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, r2: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 147 match r2: 148 case Tuple{ha, hfin}: 149 absent_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, hfd, hwh, hplug, hr, hokc, hb, ha, hfin) 150 151 def absent_c(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, r: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 152 match r: 153 case Tuple{hts, Tuple{hwh, Tuple{hplug, Tuple{hr, Tuple{hokc, Tuple{hb, r2}}}}}}: 154 +hts2 = hts 155 %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))) 156 absent_c2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, L.subst(M.Search, z => {ST.pv(V, pl, FI.sfound(z)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2, FI.tfind(~K, ~V, ~cmp, ~o, nl, pl, tg, 0n, False{}, k, 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), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), hwh, hplug, hr, hokc, hb, r2) 157 158 def absent_sp(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, P.Fr>, c => Sigma<&1, &1, ST.Tr, t => {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))>>) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 159 match sp: 160 case Tuple{+c, Tuple{+t, r}}: 161 absent_c(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, r) 162 163 def absent_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>, +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}, +k: K, +v: V) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_if_absent(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v)): 164 +ean = LL.append_nil(Nat, ST.ids(tg)) 165 +hk1 = 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)) 166 +hk0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, 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), ean), hk1) 167 +ho0 = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, 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), ean), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 168 %Equal.sym(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), RD.search_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_absent_found(~K, ~V, ~cmp, k, v, _)) 169 absent_sp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, SP.spath(~K, ~V, ~cmp, ~o, nl, pl, tg, Nil{}, k, 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), ho0, hk0, {==}, {==})) 170 171 # ---- replace: a found key's value exchanged, an absent key left ---- 172 173 174 def replace_h(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +v: V, +c: List<&2, P.Fr>, +j: Nat, +hfd: {ST.pv(V, pl, 1n+j) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}, +hm: {ST.some2(V, m) == True{} : Bool}, +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>}, +hgd: {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}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))): 175 match m: 176 case None{}: 177 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))), L.false_true(hm)) 178 case Some{+vi}: 179 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vi}, Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), Some{vi}, Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd), hmi)) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, v, _), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))) 180 %Equal.sym(List<&2, M.Entry>, S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), Equal.sym(List<&2, M.Entry>, 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)) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, _}, Some{vi}), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))) 181 (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, (Some{vi}, (L.subst(Maybe<&2, V>, z => {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}, z)) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl}), Some{vi}) : M.TreeMap & Maybe<&2, V>}, Some{vi}, ST.pv(V, pl, 1n+j), Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), Some{vi}, hmi), {==}), ({==}, hgd)))) 182 183 def replace_hc(~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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +v: V, +c: List<&2, P.Fr>, +j: Nat, +hfd: {ST.pv(V, pl, 1n+j) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hm: {ST.some2(V, ST.pv(V, pl, 1n+j)) == True{} : Bool}, hc: {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>} & {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}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))): 184 match hc: 185 case Tuple{he, hgd}: 186 replace_h(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, v, c, j, hfd, ST.pv(V, pl, 1n+j), {==}, hm, he, hgd) 187 188 def replace_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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), 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}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 189 match t: 190 case ST.TE{}: 191 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}, Equal.sym(Maybe<&2, V>, None{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd)) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace_at(~K, ~V, ~cmp, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, v, _), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, None{})) 192 (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (None{}, ({==}, ({==}, hg)))) 193 case ST.TN{+i, +a, +b}: 194 match i: 195 case 0n: 196 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))), tn_zero(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, a, b, hr)) 197 case 1n+j: 198 +hk = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+j, a, b}), P.after(c))), hwh, hk0) 199 replace_hc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, v, c, j, hfd, tn_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+j, a, b, hk), tn_core(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, c, j, a, b, hk, hwh, hr, hfin)) 200 201 def replace_c2(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, r2: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 202 match r2: 203 case Tuple{ha, hfin}: 204 replace_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, hfd, hwh, hplug, hr, hokc, hb, ha, hfin) 205 206 def replace_c(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, r: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 207 match r: 208 case Tuple{hts, Tuple{hwh, Tuple{hplug, Tuple{hr, Tuple{hokc, Tuple{hb, r2}}}}}}: 209 +hts2 = hts 210 %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))) 211 replace_c2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, L.subst(M.Search, z => {ST.pv(V, pl, FI.sfound(z)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2, FI.tfind(~K, ~V, ~cmp, ~o, nl, pl, tg, 0n, False{}, k, 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), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), hwh, hplug, hr, hokc, hb, r2) 212 213 def replace_sp(~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>, +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}, +k: K, +v: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, P.Fr>, c => Sigma<&1, &1, ST.Tr, t => {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))>>) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 214 match sp: 215 case Tuple{+c, Tuple{+t, r}}: 216 replace_c(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, c, t, r) 217 218 def replace_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>, +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}, +k: K, +v: V) -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v)): 219 +ean = LL.append_nil(Nat, ST.ids(tg)) 220 +hk1 = 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)) 221 +hk0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, 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), ean), hk1) 222 +ho0 = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, 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), ean), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 223 %Equal.sym(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), RD.search_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)) : OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, S.replace(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.replace_found(~K, ~V, ~cmp, v, _)) 224 replace_sp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hk0, SP.spath(~K, ~V, ~cmp, ~o, nl, pl, tg, Nil{}, k, 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), ho0, hk0, {==}, {==})) 225 226 # ---- replace_if_equal: exchanged when the found value equals expected ---- 227 228 229 def rie_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V, +c: List<&2, P.Fr>, +j: Nat, +vi: V, +hmi: {ST.pv(V, pl, 1n+j) == Some{vi} : Maybe<&2, V>}, +he: {ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{w})) == S.set_val(~K, ~V, ~cmp, k, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>}, +hgd: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{w}), tg, fl) == True{} : Bool}, +bq: Bool) -> OK.MOK(~K, ~V, ~cmp, Bool, S.pick(S.Model & Bool, bq, (S.TM{l, S.set_val(~K, ~V, ~cmp, k, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, True{}), (S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, False{})), MI.replace_if_apply(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, w, bq)): 230 match bq: 231 case True{}: 232 %Equal.sym(List<&2, M.Entry>, S.set_val(~K, ~V, ~cmp, k, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{w})), Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{w})), S.set_val(~K, ~V, ~cmp, k, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), he)) : OK.MOK(~K, ~V, ~cmp, Bool, (S.TM{l, _}, True{}), MI.replace_if_apply(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 1n+j, w, True{})) 233 (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{w}), tg, fl}, (True{}, (L.subst(Maybe<&2, V>, z => {MI.rp(~K, ~V, ~cmp, Bool, MI.changed_value(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{w}), tg, fl}, z))) == (ST.real(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{w}), tg, fl}), True{}) : M.TreeMap & Bool}, Some{vi}, ST.pv(V, pl, 1n+j), Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), Some{vi}, hmi), {==}), ({==}, hgd)))) 234 case False{}: 235 (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (False{}, ({==}, ({==}, hg)))) 236 237 def rie_h(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V, +c: List<&2, P.Fr>, +j: Nat, +hfd: {ST.pv(V, pl, 1n+j) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +m: Maybe<&2, V>, +hmi: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}, +hm: {ST.some2(V, m) == True{} : Bool}, +he: {ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{w})) == S.set_val(~K, ~V, ~cmp, k, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>}, +hgd: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{w}), tg, fl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))): 238 match m: 239 case None{}: 240 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))), L.false_true(hm)) 241 case Some{+vi}: 242 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vi}, Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), Some{vi}, Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd), hmi)) : OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, w, _), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))) 243 %Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), Some{vi}, hmi) : OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, w, Some{vi}), MI.replace_if_value(~K, ~V, ~cmp, ~eq, 1n+j, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))) 244 rie_b(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w, c, j, vi, hmi, he, hgd, eq(vi, e)) 245 246 def rie_hc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V, +c: List<&2, P.Fr>, +j: Nat, +hfd: {ST.pv(V, pl, 1n+j) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hm: {ST.some2(V, ST.pv(V, pl, 1n+j)) == True{} : Bool}, hc: {ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{w})) == S.set_val(~K, ~V, ~cmp, k, w, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>} & {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{w}), tg, fl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{1n+j, P.top(c), SP.dir(c)}))): 247 match hc: 248 case Tuple{he, hgd}: 249 rie_h(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w, c, j, hfd, ST.pv(V, pl, 1n+j), {==}, hm, he, hgd) 250 251 def rie_t(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), 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}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 252 match t: 253 case ST.TE{}: 254 %Equal.sym(Maybe<&2, V>, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), None{}, Equal.sym(Maybe<&2, V>, None{}, S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hfd)) : OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_at(~K, ~V, ~cmp, ~eq, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), k, e, w, _), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, False{})) 255 (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, (False{}, ({==}, ({==}, hg)))) 256 case ST.TN{+i, +a, +b}: 257 match i: 258 case 0n: 259 Empty.absurd(OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{0n, P.top(c), SP.dir(c)}))), tn_zero(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, c, a, b, hr)) 260 case 1n+j: 261 +hk = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+j, a, b}), P.after(c))), hwh, hk0) 262 rie_hc(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w, c, j, hfd, tn_hm(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, c, 1n+j, a, b, hk), tn_core(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, w, c, j, a, b, hk, hwh, hr, hfin)) 263 264 def rie_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, +hfd: {ST.pv(V, pl, ST.rid(t)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hplug: {tg == PG.plug(c, t) : ST.Tr}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hokc: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +hb: {OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool}, r2: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{ST.rid(t), P.top(c), SP.dir(c)}))): 265 match r2: 266 case Tuple{ha, hfin}: 267 rie_t(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w, hk0, c, t, hfd, hwh, hplug, hr, hokc, hb, ha, hfin) 268 269 def rie_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, +c: List<&2, P.Fr>, +t: ST.Tr, r: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))) -> OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 270 match r: 271 case Tuple{hts, Tuple{hwh, Tuple{hplug, Tuple{hr, Tuple{hokc, Tuple{hb, r2}}}}}}: 272 +hts2 = hts 273 %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2) : OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))) 274 rie_c2(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w, hk0, c, t, L.subst(M.Search, z => {ST.pv(V, pl, FI.sfound(z)) == S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, V>}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts2, FI.tfind(~K, ~V, ~cmp, ~o, nl, pl, tg, 0n, False{}, k, 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), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), hwh, hplug, hr, hokc, hb, r2) 275 276 def rie_sp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V, +hk0: {EN.oks(~K, ~V, SC.append(Nat, ST.ids(tg), Nil{}), nl, pl) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, P.Fr>, c => Sigma<&1, &1, ST.Tr, t => {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))>>) -> OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})))): 277 match sp: 278 case Tuple{+c, Tuple{+t, r}}: 279 rie_c(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w, hk0, c, t, r) 280 281 def rie_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), ~eq: V -> V -> Bool, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +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}, +k: K, +e: V, +w: V) -> OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, e, w)): 282 +ean = LL.append_nil(Nat, ST.ids(tg)) 283 +hk1 = 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)) 284 +hk0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, 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), ean), hk1) 285 +ho0 = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, 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), ean), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 286 %Equal.sym(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), RD.search_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, hg)) : OK.MOK(~K, ~V, ~cmp, Bool, S.replace_if_equal(~K, ~V, ~cmp, ~eq, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, e, w), MI.replace_if_found(~K, ~V, ~cmp, ~eq, e, w, _)) 287 rie_sp(~K, ~V, ~cmp, ~o, ~eq, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, e, w, hk0, SP.spath(~K, ~V, ~cmp, ~o, nl, pl, tg, Nil{}, k, 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), ho0, hk0, {==}, {==}))