proofs/containers/balanced_search_tree/crm.bend

bend-collections-laws-containers@1.0.0.0 · 250 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/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
8import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ok.bend as OK
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/tree.bend as TR
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/cur.bend as CU
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/reads.bend as RD
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/find.bend as FI
20import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/slot.bend as SL
21import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cnx.bend as CX
22import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/crk.bend as CK
23import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dord.bend as DO
24import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
25import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/fix.bend as FX
26import bend-collections-laws-containers@1.0.0.0/proofs/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
36def sr_p(s: M.Search) -> Nat:
37  match s:
38    case M.Search{i, p, lft}:
39      p
40
41def sr_l(s: M.Search) -> Bool:
42  match s:
43    case M.Search{i, p, lft}:
44      lft
45
46def 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
52def mem_c(-K: Data, +nl: List<&2, M.Node<K>>, +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<K>}, +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<K>, 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<K>, 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
60def some_at_s(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +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<K, V>, 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<K, V>, 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
68def 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<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}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>}, +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<K, V>, 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<K, V>>, 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<K, V> & 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
79def 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<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}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, nx) == x : M.Node<K>}, +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<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)) : 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<K>, z => {S.is_some(M.Entry<K, V>, 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
90def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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
97def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>>, +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<K, V, cmp> & 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<K, V> & 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>}, 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
103def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>>, +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<K, V, cmp> & 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<K, V> & 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<K, V, cmp>, 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<K, V, cmp>, 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<K, V, cmp>, 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<K, V, cmp>, 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<K, V, cmp>}, 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
110def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V>, +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<K, V, cmp> & 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<K, V> & 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
115def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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
123def tm_es(-K: Data, -V: Data, m: S.Model<K, V>) -> List<&2, M.Entry<K, V>>:
124  match m:
125    case S.TM{+l, +es}:
126      es
127
128def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>>, +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<K, V, cmp>}, +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<K, V> & 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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & M.Search}) -> 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(K, nl, 1n+j)))), k2))):
129  +eps = Equal.trans(ST.Sh<K, V> & 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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)), z) : ST.Sh<K, V> & M.Search}, Pair.snd(ST.Sh<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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_eta(Pair.snd(ST.Sh<K, V>, 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))), {==}))
130  +hrp0 = Equal.trans(M.TreeMap<K, V, cmp> & 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<K, V> & 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<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.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<K, V> & 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<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), (Pair.fst(ST.Sh<K, V>, 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<K, V>, 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<K, V>, 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<K, V, cmp>, M.Search, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V, cmp>, M.Search, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh<K, V>, 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<K, V>, 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<K, V> & 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>, 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<K, V>>}, 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<K, V>>, 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<K, V>, 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<K, V>, 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<K, V, cmp>}, FI.sfound(Pair.snd(ST.Sh<K, V>, 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<K, V, cmp>, z => {M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh<K, V>, 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<K, V>, 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<K, V>, 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<K, V, cmp>}, ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh<K, V>, 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}), e1, {==}))
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<K, V>}, 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<K, V>, 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<K, V>}, 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<K, V, cmp>, Maybe<&2, V>, M.Cursor{ST.real(~K, ~V, ~cmp, Pair.fst(ST.Sh<K, V>, 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<K, V>, 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<K, V>, 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
144def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>>, +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<K, V, cmp> & 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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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<K, V> & 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))}, 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(K, nl, 1n+j)))), k2))):
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<K, V, cmp>, 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<K, V, cmp>, 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
149def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V>, +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<K, V, cmp> & 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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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<K, V> & 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_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(K, nl, 1n+j)))), k2))):
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
154def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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(K, nl, 1n+j)))), k2))):
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
163def 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<K>>, +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<K>}, +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<K, V>, 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<K, V>>}:
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<K, V>>}, ST.pv(V, pl, 1n+j), Some{vU}, hmu, L.subst(M.Node<K>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, z, ST.pv(V, pl, 1n+j)) : Maybe<&2, M.Entry<K, V>>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, kU}, hxu, {==}))
165  Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{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<K, V>>}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), hw, {==}), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(pc), ST.ids(pa)), Con{1n+j, SC.append(Nat, ST.ids(pb), P.after(pc))}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{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<K, V>>, z => {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), ST.cons_m(M.Entry<K, V>, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(pb), P.after(pc)), nl, pl))) : List<&2, M.Entry<K, V>>}, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), Some{M.Entry{kU, vU}}, eent, {==})))
166
167
168# after the removal, the entries before and after: the next key found there
169def 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<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}, +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<K>}, +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<K>}, +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<K, V>>, 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<K, V>, 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<K, V>>, 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<K, V>>}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{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<K, V>>, S.del(~K, ~V, ~cmp, kU, SC.append(M.Entry<K, V>, 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<K, V>, 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<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{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))), O.refl(~K, ~cmp, ~o, kU)), Equal.sym(List<&2, M.Entry<K, 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), SC.append(M.Entry<K, V>, 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))))
171  +hordxy = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry<K, V>, 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<K, 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), SC.append(M.Entry<K, V>, 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<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, SC.append(Nat, P.before(pc), ST.ids(pa)), nl, pl), Con{M.Entry{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<K, V>>, 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<K, V>>, 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<K, V>>, 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<K, V>>, 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
176def ne0y(-K: Data, +nl: List<&2, M.Node<K>>, +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<K>}) -> {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<K>, 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<K>, ST.nd(K, nl, 0n), M.N{d0, y1, y2, y3, k2}, hy), {==})))
180    case 1n+i:
181      {==}
182
183def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>}, +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<K>}, +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<K, V>, ST.ent(K, V, M.N{d0, y1, y2, y3, k2}, m2)) == True{} : Bool}, hst: @+kk: K -> @+s2: ST.Sh<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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))}, 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)))):
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
190def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>}, +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<K>, +hy: {ST.nd(K, nl, nx) == y : M.Node<K>}, hst: @+kk: K -> @+s2: ST.Sh<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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))}, M.node_key(~K, y), 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, y), 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)))):
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<K>, z => {S.is_some(M.Entry<K, V>, 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
207def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K>}, +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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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, 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})):
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<K, V>>, 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<K>, 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<K>, 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<K>, 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
215def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & M.Search}, +x: M.Node<K>, +hx: {ST.nd(K, nl, 1n+j) == x : M.Node<K>}, +m: Maybe<&2, V>, +hm: {ST.pv(V, pl, 1n+j) == m : Maybe<&2, V>}) -> CU.COK(~K, ~V, ~cmp, 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})):
216  match x m:
217    case M.Free{f} +m:
218      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(M.Node<K>, z => {ST.is_node(K, z, ST.rid(pa), ST.rid(pb), P.top(pc)) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.Free{f}, hx, TR.rep_node(~K, 1n+j, pa, pb, P.top(pc), nl, h3))))
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<K, V>, 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<K>, z => {S.is_some(M.Entry<K, V>, 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<K, V>, 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
225def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, +h2: {PG.plug(pc, ST.TN{1n+j, pa, pb}) == PG.plug(Nil{}, tg) : ST.Tr}, r3: {ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool}) -> CU.COK(~K, ~V, ~cmp, 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})):
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
234def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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, pa, pb}), P.after(pc))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>}, rest: {PG.plug(pc, ST.TN{1n+j, pa, pb}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa, pb}, P.top(pc), nl) == True{} : Bool} & {P.ctxok(~K, pc, 1n+j, nl) == True{} : Bool})) -> CU.COK(~K, ~V, ~cmp, 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})):
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
240def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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, P.before(pc_), SC.append(Nat, ST.ids(ST.TN{1n+j, pa_, pb_}), P.after(pc_))) == SC.append(Nat, P.before(Nil{}), SC.append(Nat, ST.ids(tg), P.after(Nil{}))) : List<&2, Nat>} & ({PG.plug(pc_, ST.TN{1n+j, pa_, pb_}) == PG.plug(Nil{}, tg) : ST.Tr} & ({ST.rep(~K, ST.TN{1n+j, pa_, pb_}, P.top(pc_), nl) == True{} : Bool} & {P.ctxok(~K, pc_, 1n+j, nl) == True{} : Bool}))>>>) -> CU.COK(~K, ~V, ~cmp, 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})):
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)
248def 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<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +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<K, V> -> @+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<K, V, cmp>} -> @+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<K, V, cmp> & 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, 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})):
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)))))