proofs/containers/balanced_search_tree/putm.bend
bend-collections-laws-containers@1.0.0.0 · 287 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
7import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as OK
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/reads.bend as RD
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/find.bend as FI
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as EN
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as P
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/plug.bend as PG
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as OR
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/slot.bend as SL
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/tree.bend as TR
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/spath.bend as SP
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/alloc.bend as AC
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/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
35def 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<K>>, +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
38def 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<K>>, +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
41def 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<K>>, +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
44def 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<K>>, +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
48def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>>} & {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
55def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K>, 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
70def 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<K>>, +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<K, V>>}, +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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, 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<K, V>>, 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<K, 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)) : OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, 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<K, V>, 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<K, V, cmp> & Result<&2, &2, M.Rejected<K, V>, 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
79def 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<K>>, +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<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}) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
84def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
91def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
98def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
103def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
110def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
115def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +v: V) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put(~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<K, V> & 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<K, V>, Maybe<&2, V>>, S.put(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
126def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, 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<K, V>, 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<K, V, cmp> & Result<&2, &2, M.Rejected<K, V>, 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
134def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, 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<K, V>, 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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
146def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
151def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
158def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
163def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +v: V) -> OK.MOK(~K, ~V, ~cmp, Result<&2, &2, M.Rejected<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_if_absent(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, k, v)):
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<K, V> & 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<K, V>, Maybe<&2, V>>, S.put_if_absent(~K, ~V, ~cmp, ST.model(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}), k, v), MI.put_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
174def 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<K>>, +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<K, V>>}, +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<K, V>>, 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<K, 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)) : 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<K, V, cmp> & 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
183def 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<K>>, +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<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}) -> 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
188def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
201def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
206def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
213def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
218def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V> & 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
229def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>>}, +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<K, V> & 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<K, V>>, 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<K, V>>, 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<K, V, cmp> & 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
237def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>>}, +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
246def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V>>} & {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
251def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
264def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
269def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
276def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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
281def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +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<K, V> & 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, {==}, {==}))