1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/order.bend as O 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/balanced_search_tree/main.bend as S 8 import ../../../src/containers/balanced_search_tree.bend as M 9 import ./state.bend as ST 10 import ./mirror.bend as MI 11 import ./ok.bend as OK 12 import ./tree.bend as TR 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 ./cur.bend as CU 18 import ./reads.bend as RD 19 import ./find.bend as FI 20 import ./slot.bend as SL 21 import ./cnx.bend as CX 22 import ./crk.bend as CK 23 import ./dord.bend as DO 24 import ./prim.bend as PR 25 import ./fix.bend as FX 26 import ../../lib/nat_list.bend as NL 27 28 # iterator_remove: the current id's node removed (as remove removes it) and 29 # the cursor re-seeking its next key, which stays present; the mirror's 30 # search after the removal answers as the good shadow's (given as a fact about 31 # searches: they read only the real map). (source: tools/generators/tm_hand/crm.src) 32 33 34 # ---- facts at a member ---- 35 36 def sr_p(s: M.Search) -> Nat: 37 match s: 38 case M.Search{i, p, lft}: 39 p 40 41 def sr_l(s: M.Search) -> Bool: 42 match s: 43 case M.Search{i, p, lft}: 44 lft 45 46 def sr_eta(+s: M.Search) -> {s == M.Search{FI.sfound(s), sr_p(s), sr_l(s)} : M.Search}: 47 match s: 48 case M.Search{+i, +p, +lft}: 49 {==} 50 51 # a node's id among ok ids is one of them 52 def mem_c(-K: Data, +nl: List<&2, M.Node>, +xs: List<&2, Nat>, +j: Nat, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +hx: {ST.nd(K, nl, j) == M.N{c0, x1, x2, x3, k} : M.Node}, +h: {CU.idok(xs, j) == True{} : Bool}) -> {NL.memn(j, xs) == True{} : Bool}: 53 match j: 54 case 0n: 55 Empty.absurd({NL.memn(0n, xs) == True{} : Bool}, L.none_some(K, k, L.subst(M.Node, z => {M.node_key(~K, z) == Some{k} : Maybe<&2, K>}, M.N{c0, x1, x2, x3, k}, ST.nd(K, nl, 0n), Equal.sym(M.Node, ST.nd(K, nl, 0n), M.N{c0, x1, x2, x3, k}, hx), {==}))) 56 case 1n+i: 57 h 58 59 # a member's entry is some 60 def some_at_s(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +j: Nat, +hk: {EN.oks(~K, ~V, xs, nl, pl) == True{} : Bool}, r: Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {xs == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>) -> {S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))) == True{} : Bool}: 61 match r: 62 case Tuple{+sa, Tuple{+sb, h}}: 63 L.and_left(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), EN.oks(~K, ~V, sb, nl, pl), SL.oks_split_r(~K, ~V, sa, Con{j, sb}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, xs, SC.append(Nat, sa, Con{j, sb}), h, hk))) 64 65 # ---- no current id: nothing removed, the cursor re-seeks its next key ---- 66 67 68 def rmz_n(~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}, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +k: K, +hx: {ST.nd(K, nl, nx) == M.N{c0, x1, x2, x3, k} : M.Node}, +hmem: {NL.memn(nx, ST.ids(tg)) == True{} : Bool}, +m: Maybe<&2, V>, +hm: {ST.pv(V, pl, nx) == m : Maybe<&2, V>}, +hs: {S.is_some(M.Entry, ST.ent(K, V, M.N{c0, x1, x2, x3, k}, m)) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_p(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_l(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))}))): 69 match m: 70 case None{}: 71 Empty.absurd(CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.Search{FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_p(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_l(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))}))), L.false_true(hs)) 72 case Some{+v}: 73 +hfe = CK.find_in(~K, ~V, ~cmp, ~o, nl, pl, ST.ids(tg), nx, hmem, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), c0, x1, x2, x3, k, hx, v, hm) 74 +hfind = L.subst(Maybe<&2, M.Entry>, z => {S.val_m(K, V, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == S.val_m(K, V, z) : Maybe<&2, V>}, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{M.Entry{k, v}}, hfe, {==}) 75 +esp = L.subst(Maybe<&2, K>, z => {(S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}, None{}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, z, None{}, lo2, hi2, fw}, None{}) : S.Cursor & Maybe<&2, V>}, Some{k}, CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Some{k}, Pair.fst({CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == Some{k} : Maybe<&2, K>}, {CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hfind))), {==}) 76 (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n, lo2, hi2, fw}, (None{}, ({==}, (esp, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n))))), hg, L.and_intro(CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), Bool.and(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n)))), Pair.snd({CU.ck(~K, nl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == Some{k} : Maybe<&2, K>}, {CU.idok(ST.ids(tg), FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, k, v, hfind)), L.and_intro(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n))), {==}, CU.or_not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), 0n))))))))) 77 78 79 def rmz_x(~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}, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +x: M.Node, +hx: {ST.nd(K, nl, nx) == x : M.Node}, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, M.node_key(~K, x), None{}, lo2, hi2, fw}), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, x), lo2, hi2, fw, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, None{}))): 80 match x: 81 case M.Free{f}: 82 (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 0n, 0n, lo2, hi2, fw}, (None{}, ({==}, ({==}, L.and_intro(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(0n, 0n), Bool.not(Nat.is_eq(0n, 0n))))), hg, {==}))))) 83 case M.N{+c0, +x1, +x2, +x3, +k}: 84 %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)) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, _)) 85 %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_p(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{})), sr_l(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))}, sr_eta(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, None{}, lo2, hi2, fw}), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, None{}, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _))) 86 +hmem = mem_c(K, nl, ST.ids(tg), nx, c0, x1, x2, x3, k, hx, L.and_left(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n))))), hc))) 87 +hs0 = some_at_s(~K, ~V, nl, pl, ST.ids(tg), nx, 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)), CK.split_mem(ST.ids(tg), nx, hmem)) 88 rmz_n(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, fw, nx, c0, x1, x2, x3, k, hx, hmem, ST.pv(V, pl, nx), {==}, L.subst(M.Node, z => {S.is_some(M.Entry, ST.ent(K, V, z, ST.pv(V, pl, nx))) == True{} : Bool}, ST.nd(K, nl, nx), M.N{c0, x1, x2, x3, k}, hx, hs0)) 89 90 def rmz(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 0n, lo2, hi2, fw})): 91 rmz_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 0n), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 0n))))), hc), lo2, hi2, fw, nx, ST.nd(K, nl, nx), {==}, hc) 92 93 # ---- a current node: removed, then the next key re-sought ---- 94 95 96 # no next node: the cursor at nothing, over the shadow after the removal 97 def rmn3(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +erp: {(M.Cursor{ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j)) == (M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), 0n, 0n, lo2, hi2, fw}, oa) : M.Cursor & Maybe<&2, V>}, +esp: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>}, +hg2: {ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): 98 +em = L.pair_fst(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp) 99 +eo = Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), oa, hfu, L.pair_snd(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp)) 100 (MI.MC{ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, 0n, 0n, lo2, hi2, fw}, (oa, (erp, (L.pair_eq(S.Cursor, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.CR{ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), None{}, None{}, lo2, hi2, fw}, oa, L.subst(S.Model, z => {S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw} == S.CR{z, None{}, None{}, lo2, hi2, fw} : S.Cursor}, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), em, {==}), eo), L.and_intro(ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2), Bool.and(True{}, Bool.and(True{}, True{})), hg2, {==}))))) 101 102 103 def rmn_m3(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : M.TreeMap & Maybe<&2, V>}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): 104 match r: 105 case Tuple{esp, hg2}: 106 +ea = L.pair_fst(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0) 107 +eb = L.pair_snd(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0) 108 rmn3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, L.pair_eq(M.Cursor, Maybe<&2, V>, M.Cursor{ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j), M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), 0n, 0n, lo2, hi2, fw}, oa, L.subst(M.TreeMap, z => {M.Cursor{ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), 0n, 0n, lo2, hi2, fw} == M.Cursor{z, 0n, 0n, lo2, hi2, fw} : M.Cursor}, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), ea, {==}), eb), esp, hg2) 109 110 def rmn_m2(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +sh2: ST.Sh, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, sh2), oa) : M.TreeMap & Maybe<&2, V>}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, sh2), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): 111 match sh2: 112 case ST.SH{+n2, +r2, +lo3, +hi3, +fr2, +l2, +d2, +nl2, +pl2, +t2, +fl2}: 113 rmn_m3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, erp0, r) 114 115 def rmn_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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, rmr: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, None{}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), (MI.MC{MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), 0n, 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j))): 116 match rmr: 117 case Tuple{+sh2, Tuple{+oa, Tuple{+erp0, r}}}: 118 rmn_m2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, sh2, oa, erp0, r) 119 120 # ---- a next key: re-sought after the removal ---- 121 122 123 def tm_es(-K: Data, -V: Data, m: S.Model) -> List<&2, M.Entry>: 124 match m: 125 case S.TM{+l, +es}: 126 es 127 128 def rmk3(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +ea: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}) : M.TreeMap}, +eb: {ST.pv(V, pl, 1n+j) == oa : Maybe<&2, V>}, +esp: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>}, +hg2: {ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2) == True{} : Bool}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, M 129 +eps = Equal.trans(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), M.Search{FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_p(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_l(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)))}), L.pair_eta(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), L.subst(M.Search, z => {(Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.u 130 +hrp0 = Equal.trans(M.TreeMap & M.Search, MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, k2)), (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), hst(k2, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, ea, OK.dg_good(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, hg2)), L.subst(ST.Sh & M.Search, z => {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, k2)) == MI.rp(~K, ~V, ~cmp, M.Search, z) : M.TreeMap & M.Search}, MI.search(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, k2), (ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), RD.search_m(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, k2, hg2), {==})) 131 +hrp = L.subst(ST.Sh & M.Search, z => {MI.rp(~K, ~V, ~cmp, M.Search, z) == (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})) : M.TreeMap & M.Search}, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), L.pair_eta(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), hrp0) 132 +e1 = L.pair_fst(M.TreeMap, M.Search, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}), hrp) 133 +e3 = L.subst(M.Search, z => {FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))) == FI.sfound(z) : Nat}, Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}), L.pair_snd(M.TreeMap, M.Search, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}), hrp), {==}) 134 %Equal.sym(ST.Sh & M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2), (Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)), M.Search{FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_p(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), sr_l(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2)))}), eps) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, ST.pv(V, pl, 1n+j), _)) 135 +em = L.pair_fst(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp) 136 +eo = Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.pv(V, pl, 1n+j), oa, hfu, L.pair_snd(S.Model, Maybe<&2, V>, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j), ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, esp)) 137 +ees = L.subst(S.Model, z => {S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == tm_es(K, V, z) : List<&2, M.Entry>}, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), em, {==}) 138 +hfk = L.subst(List<&2, M.Entry>, z => {S.find(~K, ~V, ~cmp, k2, z) == Some{w2} : Maybe<&2, V>}, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, ST.ids(t2), nl2, pl2), ees, hfd2) 139 +ecur = L.subst(Nat, z => {M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw} == M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), z, 0n, lo2, hi2, fw} : M.Cursor}, FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), e3, L.subst(M.TreeMap, z => {M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw} == M.Cursor{z, FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw} : M.Cursor}, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V 140 +esc = L.subst(Maybe<&2, K>, z => {S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw} == S.CR{ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), z, None{}, lo2, hi2, fw} : S.Cursor}, Some{k2}, CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Some{k2}, Pair.fst({CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == Some{k2} : Maybe<&2, K>}, {CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, hg2, k2, w2, hfk))), L.subst(S.Model, z => {S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw} == S.CR{z, Some{k2}, None{}, lo2, hi2, fw} : S.Cursor}, S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), em, {==})) 141 +cg = L.and_intro(ST.goodF(~K, ~V, ~cmp, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2), Bool.and(CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Bool.and(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n))))), hg2, L.and_intro(CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), Bool.and(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n)))), Pair.snd({CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == Some{k2} : Maybe<&2, K>}, {CU.idok(ST.ids(t2), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))) == True{} : Bool}, CK.fkey(~K, ~V, ~cmp, ~o, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, hg2, k2, w2, hfk)), L.and_intro(True{}, Bool.or(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n), Bool.not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n))), {==}, CU.or_not(Nat.is_eq(FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n))))) 142 (MI.MC{ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n, lo2, hi2, fw}, (oa, (L.pair_eq(M.Cursor, Maybe<&2, V>, M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), FI.sfound(Pair.snd(ST.Sh, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), k2))), 0n, lo2, hi2, fw}, ST.pv(V, pl, 1n+j), M.Cursor{ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{})), 0n, lo2, hi2, fw}, oa, ecur, eb), (L.pair_eq(S.Cursor, Maybe<&2, V>, S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.CR{ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), CU.ck(~K, nl2, FI.sfound(TR.tsearch(~K, ~V, ~cmp, t2, nl2, k2, 0n, False{}))), None{}, lo2, hi2, fw}, oa, esc, eo), cg)))) 143 144 def rmk_m3(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +n2: Nat, +r2: Nat, +lo3: Nat, +hi3: Nat, +fr2: Nat, +l2: Nat, +d2: Nat, +nl2: List<&2, M.Node>, +pl2: List<&2, Maybe<&2, V>>, +t2: ST.Tr, +fl2: List<&2, Nat>, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : M.TreeMap & Maybe<&2, V>}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, 145 match r: 146 case Tuple{esp, hg2}: 147 rmk3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, L.pair_fst(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0), L.pair_snd(M.TreeMap, Maybe<&2, V>, ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))), ST.pv(V, pl, 1n+j), ST.real(~K, ~V, ~cmp, ST.SH{n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2}), oa, erp0), esp, hg2, k2, w2, hfd2, hst) 148 149 def rmk_m2(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +sh2: ST.Sh, +oa: Maybe<&2, V>, +erp0: {MI.rp(~K, ~V, ~cmp, Maybe<&2, V>, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))) == (ST.real(~K, ~V, ~cmp, sh2), oa) : M.TreeMap & Maybe<&2, V>}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, r: {(S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)) == (ST.model(~K, ~V, ~cmp, sh2), oa) : S.Model & Maybe<&2, V>} & {ST.good(~K, ~V, ~cmp, sh2) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator 150 match sh2: 151 case ST.SH{+n2, +r2, +lo3, +hi3, +fr2, +l2, +d2, +nl2, +pl2, +t2, +fl2}: 152 rmk_m3(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, n2, r2, lo3, hi3, fr2, l2, d2, nl2, pl2, t2, fl2, oa, erp0, k2, w2, hfd2, hst, r) 153 154 def rmk_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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +j: Nat, +kU: K, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +k2: K, +w2: V, +hfd2: {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, rmr: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, Some{k2}, None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_relocated(~K, ~V, ~cmp, lo2, hi2, fw, ST.pv(V, pl, 1n+j), MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd( 155 match rmr: 156 case Tuple{+sh2, Tuple{+oa, Tuple{+erp0, r}}}: 157 rmk_m2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, sh2, oa, erp0, k2, w2, hfd2, hst, r) 158 159 # ---- the current node's facts, and the next node's ---- 160 161 162 # the entries: those before and after the current node, with its own between 163 def ru_est(~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>, +j: Nat, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}) : List<&2, M.Entry>}: 164 +eent = L.subst(Maybe<&2, V>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, z) : Maybe<&2, M.Entry>}, ST.pv(V, pl, 1n+j), Some{vU}, hmu, L.subst(M.Node, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, z, ST.pv(V, pl, 1n+j)) : Maybe<&2, M.Entry>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hxu, {==})) 165 Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry>}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, {==}), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), FI.ents_app(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl), L.subst(Maybe<&2, M.Entry>, z => {SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) : List<&2, M.Entry>}, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), Some{M.Entry{kU, vU}}, eent, {==}))) 166 167 168 # after the removal, the entries before and after: the next key found there 169 def ru_fd(~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}, +j: Nat, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +nx: Nat, +hmxy: {NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))) == True{} : Bool}, +d0: Bool, +y1: Nat, +y2: Nat, +y3: Nat, +k2: K, +hy: {ST.nd(K, nl, nx) == M.N{d0, y1, y2, y3, k2} : M.Node}, +w2: V, +hm2: {ST.pv(V, pl, nx) == Some{w2} : Maybe<&2, V>}) -> {S.find(~K, ~V, ~cmp, k2, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == Some{w2} : Maybe<&2, V>}: 170 +edel = Equal.trans(List<&2, M.Entry>, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.del(~K, ~V, ~cmp, kU, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), L.subst(List<&2, M.Entry>, z => {S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.del(~K, ~V, ~cmp, kU, z) : List<&2, M.Entry>}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), ru_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu), {==}), Equal.trans(List<&2, M.Entry>, S.del(~K, ~V, ~cmp, kU, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)})), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), DO.del_mid(~K, ~V, ~cmp, ~o, kU, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), OR.ord_mid_l(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, 171 +hordxy = L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), FI.ents_app(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)), DO.ord_drop(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{kU, vU}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl)}), ru_est(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, j, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))) 172 +hfe = CK.find_in(~K, ~V, ~cmp, ~o, nl, pl, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nx, hmxy, hordxy, d0, y1, y2, y3, k2, hy, w2, hm2) 173 L.subst(List<&2, M.Entry>, z => {S.val_m(K, V, S.find_e(~K, ~V, ~cmp, k2, z)) == Some{w2} : Maybe<&2, V>}, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Equal.sym(List<&2, M.Entry>, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl), edel), L.subst(Maybe<&2, M.Entry>, z => {S.val_m(K, V, z) == Some{w2} : Maybe<&2, V>}, Some{M.Entry{k2, w2}}, S.find_e(~K, ~V, ~cmp, k2, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl)), Equal.sym(Maybe<&2, M.Entry>, S.find_e(~K, ~V, ~cmp, k2, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc))), nl, pl)), Some{M.Entry{k2, w2}}, hfe), {==})) 174 175 176 def ne0y(-K: Data, +nl: List<&2, M.Node>, +nx: Nat, +d0: Bool, +y1: Nat, +y2: Nat, +y3: Nat, +k2: K, +hy: {ST.nd(K, nl, nx) == M.N{d0, y1, y2, y3, k2} : M.Node}) -> {Nat.is_eq(nx, 0n) == False{} : Bool}: 177 match nx: 178 case 0n: 179 Empty.absurd({True{} == False{} : Bool}, L.none_some(K, k2, L.subst(M.Node, z => {M.node_key(~K, z) == Some{k2} : Maybe<&2, K>}, M.N{d0, y1, y2, y3, k2}, ST.nd(K, nl, 0n), Equal.sym(M.Node, ST.nd(K, nl, 0n), M.N{d0, y1, y2, y3, k2}, hy), {==}))) 180 case 1n+i: 181 {==} 182 183 def ru_w(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +d0: Bool, +y1: Nat, +y2: Nat, +y3: Nat, +k2: K, +hy: {ST.nd(K, nl, nx) == M.N{d0, y1, y2, y3, k2} : M.Node}, +hmxy: {NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))) == True{} : Bool}, +m2: Maybe<&2, V>, +hm2: {ST.pv(V, pl, nx) == m2 : Maybe<&2, V>}, +hs: {S.is_some(M.Entry, ST.ent(K, V, M.N{d0, y1, y2, y3, k2}, m2)) == True{} : Bool}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, rmr: OK.MOK(~K 184 match m2: 185 case None{}: 186 Empty.absurd(CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S.CR{S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, M.node_key(~K, M.N{d0, y1, y2, y3, k2}), None{}, lo2, hi2, fw}, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, M.N{d0, y1, y2, y3, k2}), lo2, hi2, fw, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))), L.false_true(hs)) 187 case Some{+w2}: 188 rmk_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, k2, w2, ru_fd(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc), j, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu, nx, hmxy, d0, y1, y2, y3, k2, hy, w2, hm2), hst, rmr) 189 190 def ru_y(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +hfu: {S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == ST.pv(V, pl, 1n+j) : Maybe<&2, V>}, +y: M.Node, +hy: {ST.nd(K, nl, nx) == y : M.Node}, hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, rmr: OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, (S 191 match y: 192 case M.Free{f}: 193 rmn_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, j, kU, hfu, rmr) 194 case M.N{+d0, +y1, +y2, +y3, +k2}: 195 +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) 196 +hmx = mem_c(K, nl, ST.ids(tg), nx, d0, y1, y2, y3, k2, hy, L.and_left(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))) 197 +h0 = ne0y(K, nl, nx, d0, y1, y2, y3, k2, hy) 198 +hnu = L.not_true(Nat.is_eq(nx, 1n+j), L.subst(Bool, z => {Bool.or(z, Bool.not(Nat.is_eq(nx, 1n+j))) == True{} : Bool}, Nat.is_eq(nx, 0n), False{}, h0, L.and_right(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))), L.and_right(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))))) 199 +hm1 = L.subst(List<&2, Nat>, z => {NL.memn(nx, z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, hmx) 200 +hor = Equal.trans(Bool, Bool.or(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), Nat.is_eq(1n+j, nx)), NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), True{}, Equal.sym(Bool, NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), Bool.or(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), Nat.is_eq(1n+j, nx)), NL.memn_mid(nx, SC.append(Nat, P.before(pc), ST.ids(pa)), 1n+j, SC.append(Nat, ST.ids(pb), P.after(pc)))), hm1) 201 +hmxy = FX.or_f(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), L.subst(Bool, z => {Bool.or(NL.memn(nx, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), SC.append(Nat, ST.ids(pb), P.after(pc)))), z) == True{} : Bool}, Nat.is_eq(1n+j, nx), False{}, N.is_eq_sym_false(nx, 1n+j, hnu), hor)) 202 +hs0 = some_at_s(~K, ~V, nl, pl, ST.ids(tg), nx, 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)), CK.split_mem(ST.ids(tg), nx, hmx)) 203 ru_w(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu, hfu, d0, y1, y2, y3, k2, hy, hmxy, ST.pv(V, pl, nx), {==}, L.subst(M.Node, z => {S.is_some(M.Entry, ST.ent(K, V, z, ST.pv(V, pl, nx))) == True{} : Bool}, ST.nd(K, nl, nx), M.N{d0, y1, y2, y3, k2}, hy, hs0), hst, rmr) 204 205 206 # the current node: its key's removal, then the next node 207 def ru_u(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +c0: Bool, +x1: Nat, +x2: Nat, +x3: Nat, +kU: K, +vU: V, +hxu: {ST.nd(K, nl, 1n+j) == M.N{c0, x1, x2, x3, kU} : M.Node}, +hmu: {ST.pv(V, pl, 1n+j) == Some{vU} : Maybe<&2, V>}, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.dele 208 +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) 209 +hfe = CK.find_in(~K, ~V, ~cmp, ~o, nl, pl, ST.ids(tg), 1n+j, L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))), L.and_right(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc))), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), c0, x1, x2, x3, kU, hxu, vU, hmu) 210 +hfu = Equal.trans(Maybe<&2, V>, S.find(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{vU}, ST.pv(V, pl, 1n+j), L.subst(Maybe<&2, M.Entry>, z => {S.val_m(K, V, S.find_e(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) == S.val_m(K, V, z) : Maybe<&2, V>}, S.find_e(~K, ~V, ~cmp, kU, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{M.Entry{kU, vU}}, hfe, {==}), Equal.sym(Maybe<&2, V>, ST.pv(V, pl, 1n+j), Some{vU}, hmu)) 211 %Equal.sym(M.Node, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hxu) : CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), M.node_key(~K, _), lo2, hi2, fw}), MI.iterator_reseek(~K, ~V, ~cmp, M.node_key(~K, ST.nd(K, nl, nx)), lo2, hi2, fw, (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j)))) 212 ru_y(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hxu, hmu, hfu, ST.nd(K, nl, nx), {==}, hst, frm(kU, pc, pa, pb, hid, hplug, h3, h4, L.subst(M.Node, z => {S.is_eq(TR.kc(~K, ~cmp, kU, z)) == True{} : Bool}, M.N{c0, x1, x2, x3, kU}, ST.nd(K, nl, 1n+j), Equal.sym(M.Node, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hxu), L.subst(Cmp, w => {S.is_eq(w) == True{} : Bool}, EQ{}, cmp(kU, kU), Equal.sym(Cmp, cmp(kU, kU), EQ{}, O.refl(~K, ~cmp, ~o, kU)), {==})))) 213 214 215 def ru_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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +hw: {ST.ids(tg) == SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}) : List<&2, Nat>}, +hid: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>}, +hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr}, +h3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool}, +h4: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), L.false_true(L.subst(M.Node, z => {ST.is_node(K, z, ST.rid(pa), ST.rid(pb), P.top(pc)) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.Free{f}, hx, TR.rep_node(~K, 1n+j, pa, pb, P.top(pc), nl, h3)))) 219 case M.N{c0, x1, x2, x3, kU} None{}: 220 +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) 221 Empty.absurd(CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), MI.iterator_remove(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw})), L.false_true(L.subst(Maybe<&2, V>, z => {S.is_some(M.Entry, ST.ent(K, V, M.N{c0, x1, x2, x3, kU}, z)) == True{} : Bool}, ST.pv(V, pl, 1n+j), None{}, hm, L.subst(M.Node, z => {S.is_some(M.Entry, ST.ent(K, V, z, ST.pv(V, pl, 1n+j))) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hx, L.and_left(S.is_some(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j))), EN.oks(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl), SL.oks_split_r(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}, nl, pl, L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, 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))))))))) 222 case M.N{+c0, +x1, +x2, +x3, +kU} Some{+vU}: 223 ru_u(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, c0, x1, x2, x3, kU, vU, hx, hm, hid, hplug, h3, h4, frm, hst) 224 225 def ru_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j 226 match r3: 227 case Tuple{h3, h4}: 228 +hid = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), LL.append_nil(Nat, ST.ids(tg))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))), h1)) 229 +e1 = L.subst(List<&2, Nat>, z => {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(pc), z) : List<&2, Nat>}, SC.append(Nat, SC.append(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}), P.after(pc)), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), LL.append_assoc(Nat, ST.ids(pa), Con{1n+j, ST.ids(pb)}, P.after(pc)), {==}) 230 +e2 = Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), LL.append_assoc(Nat, P.before(pc), ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})) 231 +hw = Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hid, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))), SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(pa), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))})), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), e1, e2)) 232 ru_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, pc, pa, pb, hw, hid, Equal.sym(ST.Tr, PG.plug(pc, ST.TN{1n+j, pa, pb}), tg, h2), h3, h4, frm, hst, ST.nd(K, nl, 1n+j), {==}, ST.pv(V, pl, 1n+j), {==}) 233 234 def ru_q(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, +pc: List<&2, P.Fr>, +pa: ST.Tr, +pb: ST.Tr, +h1: {SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j 235 match rest: 236 case Tuple{h2, r3}: 237 ru_r(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, frm, hst, pc, pa, pb, h1, h2, r3) 238 239 240 def ru_p(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}, pt: Sigma<&1, &1, List<&2, P.Fr>, pc_ => Sigma<&1, &1, ST.Tr, pa_ => Sigma<&1, &1, ST.Tr, pb_ => {SC.append(Nat, 241 match pt: 242 case Tuple{+pc, Tuple{+pa, Tuple{+pb, Tuple{h1, rest}}}}: 243 ru_q(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, frm, hst, pc, pa, pb, h1, rest) 244 245 # a current node: removed as remove removes it, the next key re-sought; 246 # frm is the removal's refinement (RV.rm_x at the node's path), hst the 247 # searches' agreement over the real map (the simulation's search) 248 def rmu(~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>, +lo2: M.Bound, +hi2: M.Bound, +fw: Bool, +nx: Nat, +j: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, 1n+j, lo2, hi2, fw}) == True{} : Bool}, frm: @+kk: K -> @+pc: List<&2, P.Fr> -> @+pa: ST.Tr -> @+pb: ST.Tr -> @+hbc: {ST.ids(tg) == SC.append(Nat, P.before(pc), SC.append(Nat, ST.ids(ST.TN{1n+j, pa, pb}), P.after(pc))) : List<&2, Nat>} -> @+hplug: {tg == PG.plug(pc, ST.TN{1n+j, pa, pb}) : ST.Tr} -> @+hr: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} -> @+hok: {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool} -> @+hfin: {S.is_eq(TR.kc(~K, ~cmp, kk, ST.nd(K, nl, 1n+j))) == True{} : Bool} -> OK.MOK(~K, ~V, ~cmp, Maybe<&2, V>, (S.TM{l, S.del(~K, ~V, ~cmp, kk, ST.ents(~K, ~V, ST.ids(tg), nl, pl))}, ST.pv(V, pl, 1n+j)), (MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), ST.pv(V, pl, 1n+j))), hst: @+kk: K -> @+s2: ST.Sh -> @+e: {ST.real(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j))))) == ST.real(~K, ~V, ~cmp, s2) : M.TreeMap} -> @+hd: {MI.dg(K, V, s2) == True{} : Bool} -> {MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, MI.unlink_target(~K, ~V, ~cmp, MI.delete_target(~K, ~V, ~cmp, 1n+j, (ST.SH{n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, None{}), tg, fl}, ST.nd(K, nl, 1n+j)))), kk)) == MI.rp(~K, ~V, ~cmp, M.Search, MI.search(~K, ~V, ~cmp, s2, kk)) : M.TreeMap & M.Search}) -> CU.COK(~K, ~V, ~cmp, Maybe<&2, V>, S.iterator_remove(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, 249 +hg = L.and_left(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc) 250 ru_p(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, j, hc, frm, hst, CX.path_to(~K, ~cmp, ~o, tg, nl, Nil{}, 1n+j, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), {==}, L.and_left(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))), L.and_right(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j)))), L.and_right(ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl), Bool.and(CU.idok(ST.ids(tg), nx), Bool.and(CU.idok(ST.ids(tg), 1n+j), Bool.or(Nat.is_eq(nx, 0n), Bool.not(Nat.is_eq(nx, 1n+j))))), hc)))))