1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../../spec/lib/common.bend as SC 5 import ../../../spec/containers/balanced_search_tree/main.bend as S 6 import ../../../src/containers/balanced_search_tree.bend as M 7 import ./state.bend as ST 8 import ./mirror.bend as MI 9 import ./tree.bend as TR 10 import ./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 19 def oks(~K: Data, ~V: Data, xs: List<&2, Nat>, +nl: List<&2, M.Node>, +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, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl)) 25 26 27 def oks_app(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +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, 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, 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, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl), hx), hy)) 33 34 def ent_some(-K: Data, -V: Data, +x: M.Node, +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, 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, 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, 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 43 def oks_tree(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +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, 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 52 def hd_cm(-K: Data, -V: Data, +m: Maybe<&2, M.Entry>, +r: List<&2, M.Entry>, +hm: {S.is_some(M.Entry, m) == True{} : Bool}) -> {S.head(M.Entry, ST.cons_m(M.Entry, m, r)) == m : Maybe<&2, M.Entry>}: 53 match m: 54 case None{}: 55 Empty.absurd({S.head(M.Entry, ST.cons_m(M.Entry, None{}, r)) == None{} : Maybe<&2, M.Entry>}, L.false_true(hm)) 56 case Some{e}: 57 {==} 58 59 def head_ents(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +h: {oks(~K, ~V, xs, nl, pl) == True{} : Bool}) -> {S.head(M.Entry, 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>}: 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, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl), h)) 65 66 def last_cm1(-K: Data, -V: Data, +m: Maybe<&2, M.Entry>, +hm: {S.is_some(M.Entry, m) == True{} : Bool}) -> {S.last(M.Entry, ST.cons_m(M.Entry, m, Nil{})) == m : Maybe<&2, M.Entry>}: 67 match m: 68 case None{}: 69 Empty.absurd({S.last(M.Entry, ST.cons_m(M.Entry, None{}, Nil{})) == None{} : Maybe<&2, M.Entry>}, L.false_true(hm)) 70 case Some{e}: 71 {==} 72 73 def last_cm2(-K: Data, -V: Data, +m1: Maybe<&2, M.Entry>, +m2: Maybe<&2, M.Entry>, +r: List<&2, M.Entry>, +h1: {S.is_some(M.Entry, m1) == True{} : Bool}, +h2: {S.is_some(M.Entry, m2) == True{} : Bool}) -> {S.last(M.Entry, ST.cons_m(M.Entry, m1, ST.cons_m(M.Entry, m2, r))) == S.last(M.Entry, ST.cons_m(M.Entry, m2, r)) : Maybe<&2, M.Entry>}: 74 match m1 m2: 75 case None{} _: 76 Empty.absurd({S.last(M.Entry, ST.cons_m(M.Entry, None{}, ST.cons_m(M.Entry, m2, r))) == S.last(M.Entry, ST.cons_m(M.Entry, m2, r)) : Maybe<&2, M.Entry>}, L.false_true(h1)) 77 case Some{e} None{}: 78 Empty.absurd({S.last(M.Entry, ST.cons_m(M.Entry, Some{e}, ST.cons_m(M.Entry, None{}, r))) == S.last(M.Entry, ST.cons_m(M.Entry, None{}, r)) : Maybe<&2, M.Entry>}, L.false_true(h2)) 79 case Some{e} Some{e2}: 80 {==} 81 82 def last_ents(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +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, 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>}: 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, 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, 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>, S.last(M.Entry, ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x)), ST.cons_m(M.Entry, 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, ST.cons_m(M.Entry, 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, 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, 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>} 89 last_ents(~K, ~V, nl, pl, u, y, h2) 90 91 def last0_some(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +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, 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, 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, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, Con{y, u}, nl, pl), h)) 97 98 def km_some(-K: Data, -V: Data, +x: M.Node, +m: Maybe<&2, V>, +h: {S.is_some(M.Entry, 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 107 def first_key_eq(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +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, 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>, S.head(M.Entry, 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, ST.ent(K, V, ST.nd(K, nl, x), ST.pv(V, pl, x))), oks(~K, ~V, t, nl, pl), h)) 114 115 def last_key_eq(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +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, 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>, S.last(M.Entry, 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 123 def last_ents_all(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +xs: List<&2, Nat>, +h: {oks(~K, ~V, xs, nl, pl) == True{} : Bool}) -> {S.last(M.Entry, 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>}: 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 132 def 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>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +x: M.Node, +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 & Maybe<&2, M.Entry>}: 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 144 def 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>, +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, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh & Maybe<&2, M.Entry>}: 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 & Maybe<&2, M.Entry>, 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh & Maybe<&2, M.Entry>} 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh & Maybe<&2, M.Entry>} 148 %Equal.sym(Maybe<&2, M.Entry>, S.head(M.Entry, 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 & Maybe<&2, M.Entry>} 149 {==} 150 151 def 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>, +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, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh & Maybe<&2, M.Entry>}: 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 & Maybe<&2, M.Entry>, 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh & Maybe<&2, M.Entry>} 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl))) : ST.Sh & Maybe<&2, M.Entry>} 155 %Equal.sym(Maybe<&2, M.Entry>, S.last(M.Entry, 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 & Maybe<&2, M.Entry>} 156 {==} 157 158 def 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>, +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, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh & 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh & Maybe<&2, K>} 161 %Equal.sym(Maybe<&2, K>, S.key_m(K, V, S.head(M.Entry, 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 & Maybe<&2, K>} 162 {==} 163 164 def 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>, +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, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh & 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, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : ST.Sh & Maybe<&2, K>} 167 %Equal.sym(Maybe<&2, K>, S.key_m(K, V, S.last(M.Entry, 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 & Maybe<&2, K>} 168 {==}