proofs/containers/balanced_search_tree/ends.bend
bend-collections-laws-containers@1.0.0.0 · 168 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/spec/lib/common.bend as SC
5import bend-collections-laws-containers@1.0.0.0/spec/containers/balanced_search_tree/main.bend as S
6import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/tree.bend as TR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/find.bend as FI
11
12# The first and last entries: the header's first and last ids are the ends
13# of the ghost order, and every id of the tree has an entry, so the entry
14# (or key) at them is the head (or last) of the specification's entries.
15# (source: tools/generators/tm_hand/ends.src)
16
17
18# every id has an entry
19def oks(~K: Data, ~V: Data, xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>) -> Bool:
20 match xs:
21 case Nil{}:
22 True{}
23 case Con{+x, t}:
24 Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl))
25
26
27def oks_app(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {oks(~K, ~V, xs, nl, pl) == True{} : Bool}, +hy: {oks(~K, ~V, ys, nl, pl) == True{} : Bool}) -> {oks(~K, ~V, SC.append(Nat, xs, ys), nl, pl) == True{} : Bool}:
28 match xs:
29 case Nil{}:
30 hy
31 case Con{+x, +t}:
32 L.and_intro(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, SC.append(Nat, t, ys), nl, pl), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl), hx), oks_app(~K, ~V, nl, pl, t, ys, L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl), hx), hy))
33
34def ent_some(-K: Data, -V: Data, +x: M.Node<K>, +m: Maybe<&2, V>, +a: Nat, +b: Nat, +q: Nat, +hx: {ST.is_node(K, x, a, b, q) == True{} : Bool}, +hm: {ST.some2(V, m) == True{} : Bool}) -> {S.is_some(M.Entry<K, V>, ST.ent(K, V, x, m)) == True{} : Bool}:
35 match x m:
36 case M.Free{f} _:
37 Empty.absurd({S.is_some(M.Entry<K, V>, ST.ent(K, V, M.Free{f}, m)) == True{} : Bool}, L.false_true(hx))
38 case M.N{c, x1, x2, x3, key} None{}:
39 Empty.absurd({S.is_some(M.Entry<K, V>, ST.ent(K, V, M.N{c, x1, x2, x3, key}, None{})) == True{} : Bool}, L.false_true(hm))
40 case M.N{c, x1, x2, x3, key} Some{v}:
41 {==}
42
43def oks_tree(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: ST.Tr, +p: Nat, +hr: {ST.rep(~K, t, p, nl) == True{} : Bool}, +hp: {ST.pay(~V, t, pl) == True{} : Bool}) -> {oks(~K, ~V, ST.ids(t), nl, pl) == True{} : Bool}:
44 match t:
45 case ST.TE{}:
46 {==}
47 case ST.TN{+i, +tl, +tr}:
48 oks_app(~K, ~V, nl, pl, ST.ids(tl), Con{i, ST.ids(tr)}, oks_tree(~K, ~V, nl, pl, tl, i, TR.rep_l(~K, i, tl, tr, p, nl, hr), FI.pay_l(~V, i, tl, tr, pl, hp)), L.and_intro(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i))), oks(~K, ~V, ST.ids(tr), nl, pl), ent_some(K, V, ST.nd(K, nl, i), ST.pv(V, pl, i), ST.rid(tl), ST.rid(tr), p, TR.rep_node(~K, i, tl, tr, p, nl, hr), FI.pay_node(~V, i, tl, tr, pl, hp)), oks_tree(~K, ~V, nl, pl, tr, i, TR.rep_r(~K, i, tl, tr, p, nl, hr), FI.pay_r(~V, i, tl, tr, pl, hp))))
49
50# ---- ends of the entries ----
51
52def hd_cm(-K: Data, -V: Data, +m: Maybe<&2, M.Entry<K, V>>, +r: List<&2, M.Entry<K, V>>, +hm: {S.is_some(M.Entry<K, V>, m) == True{} : Bool}) -> {S.head(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, m, r)) == m : Maybe<&2, M.Entry<K, V>>}:
53 match m:
54 case None{}:
55 Empty.absurd({S.head(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, None{}, r)) == None{} : Maybe<&2, M.Entry<K, V>>}, L.false_true(hm))
56 case Some{e}:
57 {==}
58
59def head_ents(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +h: {oks(~K, ~V, xs, nl, pl) == True{} : Bool}) -> {S.head(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl)) == ST.ent(K, V, ST.nd(K, nl, ST.fst0(xs)), ST.pv(V, pl, ST.fst0(xs))) : Maybe<&2, M.Entry<K, V>>}:
60 match xs:
61 case Nil{}:
62 {==}
63 case Con{+x, +t}:
64 hd_cm(K, V, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x)), ST.ents(~K, ~V, t, nl, pl), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl), h))
65
66def last_cm1(-K: Data, -V: Data, +m: Maybe<&2, M.Entry<K, V>>, +hm: {S.is_some(M.Entry<K, V>, m) == True{} : Bool}) -> {S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, m, Nil{})) == m : Maybe<&2, M.Entry<K, V>>}:
67 match m:
68 case None{}:
69 Empty.absurd({S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, None{}, Nil{})) == None{} : Maybe<&2, M.Entry<K, V>>}, L.false_true(hm))
70 case Some{e}:
71 {==}
72
73def last_cm2(-K: Data, -V: Data, +m1: Maybe<&2, M.Entry<K, V>>, +m2: Maybe<&2, M.Entry<K, V>>, +r: List<&2, M.Entry<K, V>>, +h1: {S.is_some(M.Entry<K, V>, m1) == True{} : Bool}, +h2: {S.is_some(M.Entry<K, V>, m2) == True{} : Bool}) -> {S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, m1, ST.cons_m(M.Entry<K, V>, m2, r))) == S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, m2, r)) : Maybe<&2, M.Entry<K, V>>}:
74 match m1 m2:
75 case None{} _:
76 Empty.absurd({S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, None{}, ST.cons_m(M.Entry<K, V>, m2, r))) == S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, m2, r)) : Maybe<&2, M.Entry<K, V>>}, L.false_true(h1))
77 case Some{e} None{}:
78 Empty.absurd({S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, Some{e}, ST.cons_m(M.Entry<K, V>, None{}, r))) == S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, None{}, r)) : Maybe<&2, M.Entry<K, V>>}, L.false_true(h2))
79 case Some{e} Some{e2}:
80 {==}
81
82def last_ents(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: List<&2, Nat>, +x: Nat, +h: {oks(~K, ~V, Con{x, t}, nl, pl) == True{} : Bool}) -> {S.last(M.Entry<K, V>, ST.ents(~K, ~V, Con{x, t}, nl, pl)) == ST.ent(K, V, ST.nd(K, nl, ST.last0(Con{x, t})), ST.pv(V, pl, ST.last0(Con{x, t}))) : Maybe<&2, M.Entry<K, V>>}:
83 match t:
84 case Nil{}:
85 last_cm1(K, V, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x)), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), True{}, h))
86 case Con{+y, +u}:
87 +h2 = L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, Con{y, u}, nl, pl), h)
88 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x)), ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, y), ST.pv(V, pl, y)), ST.ents(~K, ~V, u, nl, pl)))), S.last(M.Entry<K, V>, ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, y), ST.pv(V, pl, y)), ST.ents(~K, ~V, u, nl, pl))), last_cm2(K, V, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x)), ST.ent(K, V, ST.nd(K, nl, y), ST.pv(V, pl, y)), ST.ents(~K, ~V, u, nl, pl), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, Con{y, u}, nl, pl), h), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, y), ST.pv(V, pl, y))), oks(~K, ~V, u, nl, pl), h2))) : {_ == ST.ent(K, V, ST.nd(K, nl, ST.last0(Con{y, u})), ST.pv(V, pl, ST.last0(Con{y, u}))) : Maybe<&2, M.Entry<K, V>>}
89 last_ents(~K, ~V, nl, pl, u, y, h2)
90
91def last0_some(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +t: List<&2, Nat>, +x: Nat, +h: {oks(~K, ~V, Con{x, t}, nl, pl) == True{} : Bool}) -> {S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, ST.last0(Con{x, t})), ST.pv(V, pl, ST.last0(Con{x, t})))) == True{} : Bool}:
92 match t:
93 case Nil{}:
94 L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), True{}, h)
95 case Con{+y, +u}:
96 last0_some(~K, ~V, nl, pl, u, y, L.and_right(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, Con{y, u}, nl, pl), h))
97
98def km_some(-K: Data, -V: Data, +x: M.Node<K>, +m: Maybe<&2, V>, +h: {S.is_some(M.Entry<K, V>, ST.ent(K, V, x, m)) == True{} : Bool}) -> {S.key_m(K, V, ST.ent(K, V, x, m)) == M.node_key(~K, x) : Maybe<&2, K>}:
99 match x m:
100 case M.Free{f} _:
101 Empty.absurd({S.key_m(K, V, ST.ent(K, V, M.Free{f}, m)) == M.node_key(~K, M.Free{f}) : Maybe<&2, K>}, L.false_true(h))
102 case M.N{c, x1, x2, x3, key} None{}:
103 Empty.absurd({S.key_m(K, V, ST.ent(K, V, M.N{c, x1, x2, x3, key}, None{})) == M.node_key(~K, M.N{c, x1, x2, x3, key}) : Maybe<&2, K>}, L.false_true(h))
104 case M.N{c, x1, x2, x3, key} Some{v}:
105 {==}
106
107def first_key_eq(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +h: {oks(~K, ~V, xs, nl, pl) == True{} : Bool}) -> {S.key_m(K, V, S.head(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl))) == M.node_key(~K, ST.nd(K, nl, ST.fst0(xs))) : Maybe<&2, K>}:
108 match xs:
109 case Nil{}:
110 {==}
111 case Con{+x, +t}:
112 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, ST.ents(~K, ~V, Con{x, t}, nl, pl)), ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x)), head_ents(~K, ~V, nl, pl, Con{x, t}, h)) : {S.key_m(K, V, _) == M.node_key(~K, ST.nd(K, nl, x)) : Maybe<&2, K>}
113 km_some(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x), L.and_left(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl), h))
114
115def last_key_eq(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +h: {oks(~K, ~V, xs, nl, pl) == True{} : Bool}) -> {S.key_m(K, V, S.last(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl))) == M.node_key(~K, ST.nd(K, nl, ST.last0(xs))) : Maybe<&2, K>}:
116 match xs:
117 case Nil{}:
118 {==}
119 case Con{+x, +t}:
120 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, Con{x, t}, nl, pl)), ST.ent(K, V, ST.nd(K, nl, ST.last0(Con{x, t})), ST.pv(V, pl, ST.last0(Con{x, t}))), last_ents(~K, ~V, nl, pl, t, x, h)) : {S.key_m(K, V, _) == M.node_key(~K, ST.nd(K, nl, ST.last0(Con{x, t}))) : Maybe<&2, K>}
121 km_some(K, V, ST.nd(K, nl, ST.last0(Con{x, t})), ST.pv(V, pl, ST.last0(Con{x, t})), last0_some(~K, ~V, nl, pl, t, x, h))
122
123def last_ents_all(~K: Data, ~V: Data, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +h: {oks(~K, ~V, xs, nl, pl) == True{} : Bool}) -> {S.last(M.Entry<K, V>, ST.ents(~K, ~V, xs, nl, pl)) == ST.ent(K, V, ST.nd(K, nl, ST.last0(xs)), ST.pv(V, pl, ST.last0(xs))) : Maybe<&2, M.Entry<K, V>>}:
124 match xs:
125 case Nil{}:
126 {==}
127 case Con{+x, +t}:
128 last_ents(~K, ~V, nl, pl, t, x, h)
129
130# ---- the mirror's reads at an id ----
131
132def ev_m(~K: Data, ~V: Data, ~cmp: K -> 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>, +x: M.Node<K>, +m: Maybe<&2, V>) -> {MI.entry_value(~K, ~V, ~cmp, M.node_key(~K, x), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, m)) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.ent(K, V, x, m)) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}:
133 match x m:
134 case M.Free{f} None{}:
135 {==}
136 case M.Free{f} Some{v}:
137 {==}
138 case M.N{c, x1, x2, x3, key} None{}:
139 {==}
140 case M.N{c, x1, x2, x3, key} Some{v}:
141 {==}
142
143
144def first_entry_m(~K: Data, ~V: Data, ~cmp: K -> 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}) -> {MI.first_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}:
145 +e = N.eq_from_is_eq(lo, ST.fst0(ST.ids(tg)), ST.g_clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
146 %Equal.sym(ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>, MI.entry_snapshot(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo)), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.ent(K, V, ST.nd(K, nl, lo), ST.pv(V, pl, lo))), ev_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, ST.nd(K, nl, lo), ST.pv(V, pl, lo))) : {_ == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}
147 %Equal.sym(Nat, lo, ST.fst0(ST.ids(tg)), e) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.ent(K, V, ST.nd(K, nl, _), ST.pv(V, pl, _))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}
148 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ent(K, V, ST.nd(K, nl, ST.fst0(ST.ids(tg))), ST.pv(V, pl, ST.fst0(ST.ids(tg)))), head_ents(~K, ~V, nl, pl, ST.ids(tg), 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)))) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.ent(K, V, ST.nd(K, nl, ST.fst0(ST.ids(tg))), ST.pv(V, pl, ST.fst0(ST.ids(tg))))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}
149 {==}
150
151def last_entry_m(~K: Data, ~V: Data, ~cmp: K -> 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}) -> {MI.last_entry(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}:
152 +e = N.eq_from_is_eq(hi, ST.last0(ST.ids(tg)), ST.g_chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
153 %Equal.sym(ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>, MI.entry_snapshot(~K, ~V, ~cmp, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi)), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.ent(K, V, ST.nd(K, nl, hi), ST.pv(V, pl, hi))), ev_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, ST.nd(K, nl, hi), ST.pv(V, pl, hi))) : {_ == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}
154 %Equal.sym(Nat, hi, ST.last0(ST.ids(tg)), e) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.ent(K, V, ST.nd(K, nl, _), ST.pv(V, pl, _))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}
155 %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), ST.ent(K, V, ST.nd(K, nl, ST.last0(ST.ids(tg))), ST.pv(V, pl, ST.last0(ST.ids(tg)))), last_ents_all(~K, ~V, nl, pl, ST.ids(tg), 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)))) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.ent(K, V, ST.nd(K, nl, ST.last0(ST.ids(tg))), ST.pv(V, pl, ST.last0(ST.ids(tg))))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh<K, V> & Maybe<&2, M.Entry<K, V>>}
156 {==}
157
158def first_key_m(~K: Data, ~V: Data, ~cmp: K -> 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}) -> {MI.first_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh<K, V> & Maybe<&2, K>}:
159 +e = N.eq_from_is_eq(lo, ST.fst0(ST.ids(tg)), ST.g_clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
160 %Equal.sym(Nat, lo, ST.fst0(ST.ids(tg)), e) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.node_key(~K, ST.nd(K, nl, _))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh<K, V> & Maybe<&2, K>}
161 %Equal.sym(Maybe<&2, K>, S.key_m(K, V, S.head(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), M.node_key(~K, ST.nd(K, nl, ST.fst0(ST.ids(tg)))), first_key_eq(~K, ~V, nl, pl, ST.ids(tg), 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)))) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.node_key(~K, ST.nd(K, nl, ST.fst0(ST.ids(tg))))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh<K, V> & Maybe<&2, K>}
162 {==}
163
164def last_key_m(~K: Data, ~V: Data, ~cmp: K -> 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}) -> {MI.last_key(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh<K, V> & Maybe<&2, K>}:
165 +e = N.eq_from_is_eq(hi, ST.last0(ST.ids(tg)), ST.g_chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
166 %Equal.sym(Nat, hi, ST.last0(ST.ids(tg)), e) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.node_key(~K, ST.nd(K, nl, _))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, S.key_m(K, V, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh<K, V> & Maybe<&2, K>}
167 %Equal.sym(Maybe<&2, K>, S.key_m(K, V, S.last(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), M.node_key(~K, ST.nd(K, nl, ST.last0(ST.ids(tg)))), last_key_eq(~K, ~V, nl, pl, ST.ids(tg), 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)))) : {(ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.node_key(~K, ST.nd(K, nl, ST.last0(ST.ids(tg))))) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _) : ST.Sh<K, V> & Maybe<&2, K>}
168 {==}