proofs/containers/balanced_search_tree/crk.bend
bend-collections-laws-containers@1.0.0.0 · 105 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/tree.bend as TR
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as EN
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as P
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/plug.bend as PG
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dj.bend as DJ
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ord.bend as OR
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/cur.bend as CU
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/spath.bend as SP
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/agree.bend as AG
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/lib/nat_list.bend as NL
21
22# Keys present are found: a list split at a member, the entry of a member
23# found by its key in sorted entries, and the search for a present key ending
24# at a node holding it. (source: tools/generators/tm_hand/crk.src)
25
26
27def sp_up(+x: Nat, +t: List<&2, Nat>, +j: Nat, r: Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {t == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>) -> Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {Con{x, t} == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>:
28 match r:
29 case Tuple{+sa, Tuple{+sb, h}}:
30 (Con{x, sa}, (sb, L.subst(List<&2, Nat>, z => {Con{x, t} == Con{x, z} : List<&2, Nat>}, t, SC.append(Nat, sa, Con{j, sb}), h, {==})))
31
32# a list at a member
33def split_c(+x: Nat, +t: List<&2, Nat>, +j: Nat, +e: Bool, +he: {Nat.is_eq(x, j) == e : Bool}, +hm: {Bool.or(e, NL.memn(j, t)) == True{} : Bool}, ih: @+hmt: {NL.memn(j, t) == True{} : Bool} -> Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {t == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>) -> Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {Con{x, t} == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>:
34 match e:
35 case True{}:
36 L.subst(Nat, z => Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {Con{z, t} == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>, j, x, Equal.sym(Nat, x, j, N.eq_from_is_eq(x, j, he)), (Nil{}, (t, {==})))
37 case False{}:
38 sp_up(x, t, j, ih(hm))
39
40def split_mem(+xs: List<&2, Nat>, +j: Nat, +hm: {NL.memn(j, xs) == True{} : Bool}) -> 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>}>>:
41 match xs:
42 case Nil{}:
43 Empty.absurd(Sigma<&1, &1, List<&2, Nat>, sa_ => Sigma<&1, &1, List<&2, Nat>, sb_ => {Nil{} == SC.append(Nat, sa_, Con{j, sb_}) : List<&2, Nat>}>>, L.false_true(hm))
44 case Con{+x, +t}:
45 split_c(x, t, j, Nat.is_eq(x, j), {==}, hm, hmt => split_mem(t, j, hmt))
46
47
48def fi_s(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +j: Nat, +hord: {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, xs, nl, pl)) == True{} : Bool}, +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>}, +v: V, +hv: {ST.pv(V, pl, j) == Some{v} : Maybe<&2, V>}, 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.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, xs, nl, pl)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
49 match r:
50 case Tuple{+sa, Tuple{+sb, h}}:
51 +eent = L.subst(Maybe<&2, V>, z => {ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)) == ST.ent(K, V, M.N{c0, x1, x2, x3, k}, z) : Maybe<&2, M.Entry<K, V>>}, ST.pv(V, pl, j), Some{v}, hv, L.subst(M.Node<K>, z => {ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)) == ST.ent(K, V, z, ST.pv(V, pl, j)) : Maybe<&2, M.Entry<K, V>>}, ST.nd(K, nl, j), M.N{c0, x1, x2, x3, k}, hx, {==}))
52 +hE = Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, xs, nl, pl), ST.ents(~K, ~V, SC.append(Nat, sa, Con{j, sb}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, sb, nl, pl)}), L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, xs, nl, pl) == ST.ents(~K, ~V, z, nl, pl) : List<&2, M.Entry<K, V>>}, xs, SC.append(Nat, sa, Con{j, sb}), h, {==}), Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, SC.append(Nat, sa, Con{j, sb}), nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ST.ents(~K, ~V, sb, nl, pl))), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, sb, nl, pl)}), FI.ents_app(~K, ~V, sa, Con{j, sb}, nl, pl), L.subst(Maybe<&2, M.Entry<K, V>>, z => {SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ST.ents(~K, ~V, sb, nl, pl))) == SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), ST.cons_m(M.Entry<K, V>, z, ST.ents(~K, ~V, sb, nl, pl))) : List<&2, M.Entry<K, V>>}, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), Some{M.Entry{k, v}}, eent, {==})))
53 Equal.trans(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, xs, nl, pl)), S.find_e(~K, ~V, ~cmp, k, SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, sb, nl, pl)})), Some{M.Entry{k, v}}, L.subst(List<&2, M.Entry<K, V>>, z => {S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, xs, nl, pl)) == S.find_e(~K, ~V, ~cmp, k, z) : Maybe<&2, M.Entry<K, V>>}, ST.ents(~K, ~V, xs, nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, sb, nl, pl)}), hE, {==}), OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, ST.ents(~K, ~V, sa, nl, pl), M.Entry{k, v}, ST.ents(~K, ~V, sb, nl, pl), L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, xs, nl, pl), SC.append(M.Entry<K, V>, ST.ents(~K, ~V, sa, nl, pl), Con{M.Entry{k, v}, ST.ents(~K, ~V, sb, nl, pl)}), hE, hord), O.refl(~K, ~cmp, ~o, k)))
54
55# the entry of a member, found by its key
56def find_in(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +j: Nat, +hm: {NL.memn(j, xs) == True{} : Bool}, +hord: {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, xs, nl, pl)) == True{} : Bool}, +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>}, +v: V, +hv: {ST.pv(V, pl, j) == Some{v} : Maybe<&2, V>}) -> {S.find_e(~K, ~V, ~cmp, k, ST.ents(~K, ~V, xs, nl, pl)) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
57 fi_s(~K, ~V, ~cmp, ~o, nl, pl, xs, j, hord, c0, x1, x2, x3, k, hx, v, hv, split_mem(xs, j, hm))
58
59# ---- a present key: the search ends at a node holding it ----
60
61
62def fk_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>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +k: K, +c: List<&2, P.Fr>, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))) : List<&2, Nat>}, +hr: {ST.rep(~K, ST.TN{i, a, b}, P.top(c), nl) == True{} : Bool}, +x: M.Node<K>, +hx: {ST.nd(K, nl, i) == x : M.Node<K>}, +hq: {S.is_eq(TR.kc(~K, ~cmp, k, x)) == True{} : Bool}) -> {CU.ck(~K, nl, ST.rid(ST.TN{i, a, b})) == Some{k} : Maybe<&2, K>} & {CU.idok(ST.ids(tg), ST.rid(ST.TN{i, a, b})) == True{} : Bool}:
63 match x:
64 case M.Free{f}:
65 Empty.absurd({CU.ck(~K, nl, ST.rid(ST.TN{i, a, b})) == Some{k} : Maybe<&2, K>} & {CU.idok(ST.ids(tg), ST.rid(ST.TN{i, a, b})) == True{} : Bool}, L.false_true(L.subst(M.Node<K>, z => {ST.is_node(K, z, ST.rid(a), ST.rid(b), P.top(c)) == True{} : Bool}, ST.nd(K, nl, i), M.Free{f}, hx, TR.rep_node(~K, i, a, b, P.top(c), nl, hr))))
66 case M.N{+c0, +x1, +x2, +x3, +key}:
67 +ek = O.antisym(~K, ~cmp, o, k, key, AG.iseq_eq(cmp(k, key), hq))
68 +eck = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, i), Some{key}, Some{k}, L.subst(M.Node<K>, z => {CU.ck(~K, nl, i) == M.node_key(~K, z) : Maybe<&2, K>}, ST.nd(K, nl, i), M.N{c0, x1, x2, x3, key}, hx, {==}), L.subst(K, z => {Some{key} == Some{z} : Maybe<&2, K>}, key, k, Equal.sym(K, k, key, ek), {==}))
69 +hm0 = DJ.mem_r(i, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c)), DJ.mem_l(i, ST.ids(ST.TN{i, a, b}), P.after(c), P.mem_root(i, a, b)))
70 +hm = L.subst(List<&2, Nat>, z => {NL.memn(i, z) == True{} : Bool}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), ST.ids(tg), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), hwh), LL.append_nil(Nat, ST.ids(tg))), hm0)
71 (eck, CU.or_r(Nat.is_eq(i, 0n), NL.memn(i, ST.ids(tg)), hm))
72
73def fk_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>, +t: ST.Tr, +k: K, +w: V, +hpv: {ST.pv(V, pl, ST.rid(t)) == Some{w} : Maybe<&2, V>}, +c: List<&2, P.Fr>, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +hfin: {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> {CU.ck(~K, nl, ST.rid(t)) == Some{k} : Maybe<&2, K>} & {CU.idok(ST.ids(tg), ST.rid(t)) == True{} : Bool}:
74 match t:
75 case ST.TE{}:
76 Empty.absurd({CU.ck(~K, nl, ST.rid(ST.TE{})) == Some{k} : Maybe<&2, K>} & {CU.idok(ST.ids(tg), ST.rid(ST.TE{})) == True{} : Bool}, L.none_some(V, w, hpv))
77 case ST.TN{+i, +a, +b}:
78 fk_x(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, i, a, b, k, c, hwh, hr, ST.nd(K, nl, i), {==}, hfin)
79
80
81def fk_c2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +w: V, +c: List<&2, P.Fr>, +t: ST.Tr, +hts: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search}, +hpv0: {ST.pv(V, pl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == Some{w} : Maybe<&2, V>}, +hwh: {SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>}, +hr: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, r2: {OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}) -> {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}:
82 match r2:
83 case Tuple{ha, hfin}:
84 %Equal.sym(M.Search, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts) : {CU.ck(~K, nl, FI.sfound(_)) == Some{k} : Maybe<&2, K>} & {CU.idok(ST.ids(tg), FI.sfound(_)) == True{} : Bool}
85 fk_t(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, t, k, w, L.subst(M.Search, z => {ST.pv(V, pl, FI.sfound(z)) == Some{w} : Maybe<&2, V>}, TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}), M.Search{ST.rid(t), P.top(c), SP.dir(c)}, hts, hpv0), c, hwh, hr, hfin)
86
87def fk_c(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +w: V, +hpv0: {ST.pv(V, pl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == Some{w} : Maybe<&2, V>}, +c: List<&2, P.Fr>, +t: ST.Tr, r: {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))) -> {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}:
88 match r:
89 case Tuple{hts, Tuple{hwh, Tuple{hplug, Tuple{hr, Tuple{hokc, Tuple{hb, r2}}}}}}:
90 fk_c2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, w, c, t, hts, hpv0, hwh, hr, r2)
91
92def fk_sp(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +k: K, +w: V, +hpv0: {ST.pv(V, pl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))) == Some{w} : Maybe<&2, V>}, sp: Sigma<&1, &1, List<&2, P.Fr>, c => Sigma<&1, &1, ST.Tr, t => {TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}) == M.Search{ST.rid(t), P.top(c), SP.dir(c)} : M.Search} & ({SC.append(Nat, ST.ids(tg), Nil{}) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) : List<&2, Nat>} & ({tg == PG.plug(c, t) : ST.Tr} & ({ST.rep(~K, t, P.top(c), nl) == True{} : Bool} & ({P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool} & ({OR.ltall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.before(c), nl, pl)) == True{} : Bool} & ({OR.gtall(~K, ~V, ~cmp, k, ST.ents(~K, ~V, P.after(c), nl, pl)) == True{} : Bool} & {SP.fin(~K, ~cmp, k, t, nl) == True{} : Bool}))))))>>) -> {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}:
93 match sp:
94 case Tuple{+c, Tuple{+t, r}}:
95 fk_c(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, w, hpv0, c, t, r)
96
97
98# a present key: the search's id holds it and is in the tree
99def fkey(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +k: K, +w: V, +hf: {S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == Some{w} : Maybe<&2, V>}) -> {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}:
100 +ean = LL.append_nil(Nat, ST.ids(tg))
101 +hk1 = EN.oks_tree(~K, ~V, nl, pl, tg, 0n, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
102 +hk0 = L.subst(List<&2, Nat>, z => {EN.oks(~K, ~V, z, nl, pl) == True{} : Bool}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), ean), hk1)
103 +ho0 = L.subst(List<&2, Nat>, z => {ST.ordered(~K, ~V, ~cmp, ST.ents(~K, ~V, z, nl, pl)) == True{} : Bool}, ST.ids(tg), SC.append(Nat, ST.ids(tg), Nil{}), Equal.sym(List<&2, Nat>, SC.append(Nat, ST.ids(tg), Nil{}), ST.ids(tg), ean), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
104 +hpv0 = Equal.trans(Maybe<&2, V>, ST.pv(V, pl, FI.sfound(TR.tsearch(~K, ~V, ~cmp, tg, nl, k, 0n, False{}))), S.find(~K, ~V, ~cmp, k, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Some{w}, FI.tfind(~K, ~V, ~cmp, ~o, nl, pl, tg, 0n, False{}, k, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), hf)
105 fk_sp(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, k, w, hpv0, SP.spath(~K, ~V, ~cmp, ~o, nl, pl, tg, Nil{}, k, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), {==}, ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ho0, hk0, {==}, {==}))