1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../lib/order.bend as O 6 import ../../../spec/lib/common.bend as SC 7 import ../../../spec/containers/balanced_search_tree/main.bend as S 8 import ../../../src/containers/balanced_search_tree.bend as M 9 import ./state.bend as ST 10 import ./tree.bend as TR 11 import ./find.bend as FI 12 import ./path.bend as P 13 import ./prim.bend as PR 14 import ./ord.bend as OR 15 import ./slot.bend as SL 16 import ./alls.bend as AL 17 import ./dj.bend as DJ 18 import ./agree.bend as AG 19 import ./navs.bend as NS 20 import ./spath.bend as SP 21 import ../../lib/nat_list.bend as NL 22 23 # A key found: the payload at its node is the specification's lookup, and 24 # exchanging it is the specification's set_val; the invariant holds with the 25 # new payload list. (source: tools/generators/tm_hand/putf.src) 26 27 28 # setting the value of the entry equal to k 29 def set_val_mid(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +k: K, +v: V, +xs: List<&2, M.Entry>, +e: M.Entry, +ys: List<&2, M.Entry>, +hl: {OR.ltall(~K, ~V, ~cmp, k, xs) == True{} : Bool}, +hc: {cmp(k, S.key(K, V, e)) == EQ{} : Cmp}) -> {S.set_val(~K, ~V, ~cmp, k, v, SC.append(M.Entry, xs, Con{e, ys})) == SC.append(M.Entry, xs, Con{M.Entry{S.key(K, V, e), v}, ys}) : List<&2, M.Entry>}: 30 match xs: 31 case Nil{}: 32 %Equal.sym(Cmp, cmp(k, S.key(K, V, e)), EQ{}, hc) : {S.pick(List<&2, M.Entry>, S.is_eq(_), Con{M.Entry{S.key(K, V, e), v}, ys}, Con{e, S.set_val(~K, ~V, ~cmp, k, v, ys)}) == Con{M.Entry{S.key(K, V, e), v}, ys} : List<&2, M.Entry>} 33 {==} 34 case Con{+a, +t}: 35 %Equal.sym(Cmp, cmp(k, S.key(K, V, a)), GT{}, OR.lt_gt(~K, ~cmp, ~o, S.key(K, V, a), k, L.and_left(Cmp.is_lt(cmp(S.key(K, V, a), k)), OR.ltall(~K, ~V, ~cmp, k, t), hl))) : {S.pick(List<&2, M.Entry>, S.is_eq(_), Con{M.Entry{S.key(K, V, a), v}, SC.append(M.Entry, t, Con{e, ys})}, Con{a, S.set_val(~K, ~V, ~cmp, k, v, SC.append(M.Entry, t, Con{e, ys}))}) == Con{a, SC.append(M.Entry, t, Con{M.Entry{S.key(K, V, e), v}, ys})} : List<&2, M.Entry>} 36 %Equal.sym(List<&2, M.Entry>, S.set_val(~K, ~V, ~cmp, k, v, SC.append(M.Entry, t, Con{e, ys})), SC.append(M.Entry, t, Con{M.Entry{S.key(K, V, e), v}, ys}), set_val_mid(~K, ~V, ~cmp, ~o, k, v, t, e, ys, L.and_right(Cmp.is_lt(cmp(S.key(K, V, a), k)), OR.ltall(~K, ~V, ~cmp, k, t), hl), hc)) : {Con{a, _} == Con{a, SC.append(M.Entry, t, Con{M.Entry{S.key(K, V, e), v}, ys})} : List<&2, M.Entry>} 37 {==} 38 39 # order reads only keys 40 def ord_key(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +xs: List<&2, M.Entry>, +e: M.Entry, +e2: M.Entry, +ys: List<&2, M.Entry>, +hk: {S.key(K, V, e) == S.key(K, V, e2) : K}, +h: {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry, xs, Con{e, ys})) == True{} : Bool}) -> {ST.ordered(~K, ~V, ~cmp, SC.append(M.Entry, xs, Con{e2, ys})) == True{} : Bool}: 41 match xs: 42 case Nil{}: 43 match ys: 44 case Nil{}: 45 {==} 46 case Con{+b, +u}: 47 L.subst(K, z => {Bool.and(Cmp.is_lt(cmp(z, S.key(K, V, b))), ST.ordered(~K, ~V, ~cmp, Con{b, u})) == True{} : Bool}, S.key(K, V, e), S.key(K, V, e2), hk, h) 48 case Con{+a, +t}: 49 match t: 50 case Nil{}: 51 +h1 = L.and_left(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))), ST.ordered(~K, ~V, ~cmp, Con{e, ys}), h) 52 +h2 = L.and_right(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e))), ST.ordered(~K, ~V, ~cmp, Con{e, ys}), h) 53 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, e2))), ST.ordered(~K, ~V, ~cmp, Con{e2, ys}), L.subst(K, z => {Cmp.is_lt(cmp(S.key(K, V, a), z)) == True{} : Bool}, S.key(K, V, e), S.key(K, V, e2), hk, h1), ord_key(~K, ~V, ~cmp, Nil{}, e, e2, ys, hk, h2)) 54 case Con{+a2, +u}: 55 +h1 = L.and_left(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, a2))), ST.ordered(~K, ~V, ~cmp, Con{a2, SC.append(M.Entry, u, Con{e, ys})}), h) 56 +h2 = L.and_right(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, a2))), ST.ordered(~K, ~V, ~cmp, Con{a2, SC.append(M.Entry, u, Con{e, ys})}), h) 57 L.and_intro(Cmp.is_lt(cmp(S.key(K, V, a), S.key(K, V, a2))), ST.ordered(~K, ~V, ~cmp, Con{a2, SC.append(M.Entry, u, Con{e2, ys})}), h1, ord_key(~K, ~V, ~cmp, Con{a2, u}, e, e2, ys, hk, h2)) 58 59 # ---- a payload exchanged ---- 60 61 def some_ex_c(-V: Data, +pl: List<&2, Maybe<&2, V>>, +i: Nat, +w: Maybe<&2, V>, +jj: Nat, +hj: {ST.some2(V, ST.pv(V, pl, 1n+jj)) == True{} : Bool}, +hw: {ST.some2(V, w) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)) == b : Bool}, +e: Bool, +he: {Nat.is_eq(i, jj) == e : Bool}) -> {ST.some2(V, ST.nth_or(Maybe<&2, V>, ST.pk(List<&2, Maybe<&2, V>>, b, SC.update(Maybe<&2, V>, pl, i, w), pl), jj, None{})) == True{} : Bool}: 62 match b e: 63 case True{} True{}: 64 +ei = N.eq_from_is_eq(i, jj, he) 65 +hin = L.subst(Nat, z => {Nat.is_lt(z, SC.length(Maybe<&2, V>, pl)) == True{} : Bool}, i, jj, ei, hb) 66 %Equal.sym(Nat, i, jj, ei) : {ST.some2(V, ST.nth_or(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, _, w), jj, None{})) == True{} : Bool} 67 %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, jj, w), jj, None{}), w, Equal.trans(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, jj, w), jj, None{}), PR.or_else(Maybe<&2, V>, SC.nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, jj, w), jj), None{}), w, PR.nth_or_nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, jj, w), jj, None{}), L.subst(Maybe<&2, Maybe<&2, V>>, z => {PR.or_else(Maybe<&2, V>, z, None{}) == w : Maybe<&2, V>}, Some{w}, SC.nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, jj, w), jj), Equal.sym(Maybe<&2, Maybe<&2, V>>, SC.nth(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, jj, w), jj), Some{w}, LL.nth_update_same(Maybe<&2, V>, pl, jj, w, hin)), {==}))) : {ST.some2(V, _) == True{} : Bool} 68 hw 69 case True{} False{}: 70 %Equal.sym(Maybe<&2, V>, ST.nth_or(Maybe<&2, V>, SC.update(Maybe<&2, V>, pl, i, w), jj, None{}), ST.nth_or(Maybe<&2, V>, pl, jj, None{}), SL.nth_upd_c(Maybe<&2, V>, pl, i, w, jj, None{}, he, True{})) : {ST.some2(V, _) == True{} : Bool} 71 hj 72 case False{} +e: 73 hj 74 75 def some_ex(-V: Data, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +j: Nat, +hj: {ST.some2(V, ST.pv(V, pl, j)) == True{} : Bool}, +hw: {ST.some2(V, w) == True{} : Bool}) -> {ST.some2(V, ST.pv(V, PR.ex_pl(V, pl, id, w), j)) == True{} : Bool}: 76 match id j: 77 case 0n +j: 78 hj 79 case 1n+i 0n: 80 Empty.absurd({ST.some2(V, None{}) == True{} : Bool}, L.false_true(hj)) 81 case 1n+i 1n+jj: 82 some_ex_c(V, pl, i, w, jj, hj, hw, Nat.is_lt(i, SC.length(Maybe<&2, V>, pl)), {==}, Nat.is_eq(i, jj), {==}) 83 84 def pay_ex(~V: Data, +t: ST.Tr, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +w: Maybe<&2, V>, +hp: {ST.pay(~V, t, pl) == True{} : Bool}, +hw: {ST.some2(V, w) == True{} : Bool}) -> {ST.pay(~V, t, PR.ex_pl(V, pl, id, w)) == True{} : Bool}: 85 match t: 86 case ST.TE{}: 87 {==} 88 case ST.TN{+i, +a, +b}: 89 L.and_intro(ST.some2(V, ST.pv(V, PR.ex_pl(V, pl, id, w), i)), Bool.and(ST.pay(~V, a, PR.ex_pl(V, pl, id, w)), ST.pay(~V, b, PR.ex_pl(V, pl, id, w))), some_ex(V, pl, id, w, i, FI.pay_node(~V, i, a, b, pl, hp), hw), L.and_intro(ST.pay(~V, a, PR.ex_pl(V, pl, id, w)), ST.pay(~V, b, PR.ex_pl(V, pl, id, w)), pay_ex(~V, a, pl, id, w, FI.pay_l(~V, i, a, b, pl, hp), hw), pay_ex(~V, b, pl, id, w, FI.pay_r(~V, i, a, b, pl, hp), hw))) 90 91 # ---- the key found: put replaces the value ---- 92 93 94 # the entries around a node the path leads to, for a payload list 95 def ents_at(~K: Data, ~V: Data, +nl: List<&2, M.Node>, +q: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +c: List<&2, P.Fr>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +hbc: {ST.ids(tg) == SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))) : List<&2, Nat>}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, q) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, q), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, q, i)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, q))) : List<&2, M.Entry>}: 96 +e1 = L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, ST.ids(tg), nl, q) == ST.ents(~K, ~V, z, nl, q) : List<&2, M.Entry>}, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), hbc, {==}) 97 +e2 = L.subst(List<&2, Nat>, z => {ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), nl, q) == ST.ents(~K, ~V, z, nl, q) : List<&2, M.Entry>}, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(a)), Con{i, SC.append(Nat, ST.ids(b), P.after(c))}), NS.wh_node(c, i, a, b), {==}) 98 Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, q), ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), nl, q), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, q), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, q, i)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, q))), e1, Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{i, a, b}), P.after(c))), nl, q), ST.ents(~K, ~V, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(a)), Con{i, SC.append(Nat, ST.ids(b), P.after(c))}), nl, q), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, q), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, i), ST.pv(V, q, i)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, q))), e2, FI.ents_app(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), Con{i, SC.append(Nat, ST.ids(b), P.after(c))}, nl, q))) 99 100 101 # the node of k found: exchanging its payload for v gives the entries 102 # set_val(k, v) and keeps the invariant 103 def hit_core(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +hg: {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl) == True{} : Bool}, +c: List<&2, P.Fr>, +i: Nat, +a: ST.Tr, +b: ST.Tr, +k: K, +v: V, +hbc: {ST.ids(tg) == 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}, +hfin: {SP.fin(~K, ~cmp, k, ST.TN{i, a, b}, nl) == True{} : Bool}, +x: M.Node, +m: Maybe<&2, V>, +hxi: {ST.nd(K, nl, i) == x : M.Node}, +hmi: {ST.pv(V, pl, i) == m : Maybe<&2, V>}, +hx: {ST.is_node(K, x, ST.rid(a), ST.rid(b), P.top(c)) == True{} : Bool}, +hm: {ST.some2(V, m) == True{} : Bool}) -> {ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, i, Some{v})) == S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>} & {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, i, Some{v}), tg, fl) == True{} : Bool}: 104 match i x m: 105 case 0n +x +m: 106 Empty.absurd({ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 0n, Some{v})) == S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>} & {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 0n, Some{v}), tg, fl) == True{} : Bool}, L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.rid(a), ST.rid(b), P.top(c)), Bool.and(ST.rep(~K, a, 0n, nl), ST.rep(~K, b, 0n, nl))), hr))) 107 case 1n+j M.Free{f} +m: 108 Empty.absurd({ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})) == S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>} & {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl) == True{} : Bool}, L.false_true(hx)) 109 case 1n+j M.N{c0, x1, x2, x3, key} None{}: 110 Empty.absurd({ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})) == S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : List<&2, M.Entry>} & {ST.goodF(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl) == True{} : Bool}, L.false_true(hm)) 111 case 1n+j M.N{+c0, +x1, +x2, +x3, +key} Some{+vi}: 112 +hW0 = ents_at(~K, ~V, nl, pl, tg, c, 1n+j, a, b, hbc) 113 +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, key}, z) : Maybe<&2, M.Entry>}, ST.pv(V, pl, 1n+j), Some{vi}, hmi, L.subst(M.Node, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)) == ST.ent(K, V, z, ST.pv(V, pl, 1n+j)) : Maybe<&2, M.Entry>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, key}, hxi, {==})) 114 +hW = Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl))), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), hW0, L.subst(Maybe<&2, M.Entry>, z => {SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl))) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), ST.cons_m(M.Entry, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl))) : List<&2, M.Entry>}, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, pl, 1n+j)), Some{M.Entry{key, vi}}, eent, {==})) 115 +hord = L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), hW, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 116 +hc = AG.iseq_eq(cmp(k, key), L.subst(M.Node, z => {S.is_eq(TR.kc(~K, ~cmp, k, z)) == True{} : Bool}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, key}, hxi, hfin)) 117 +ek = O.antisym(~K, ~cmp, o, k, key, hc) 118 +hlx = L.subst(K, z => {OR.ltall(~K, ~V, ~cmp, z, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl)) == True{} : Bool}, key, k, Equal.sym(K, k, key, ek), OR.ord_mid_l(~K, ~V, ~cmp, ~o, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), M.Entry{key, vi}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl), hord)) 119 +hnd0 = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}), Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+j, a, b}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}), hbc, NS.wh_node(c, 1n+j, a, b)), DJ.ndl(ST.ids(tg), fl, ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))) 120 +nX = DJ.dj_l(SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}, hnd0, 1n+j, DJ.mem_hd(1n+j, SC.append(Nat, ST.ids(b), P.after(c)))) 121 +nY = DJ.nd_head(1n+j, SC.append(Nat, ST.ids(b), P.after(c)), DJ.ndr(SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}, hnd0)) 122 +mi = L.subst(List<&2, Nat>, z => {NL.memn(1n+j, z) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}), ST.ids(tg), Equal.sym(List<&2, Nat>, ST.ids(tg), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}), Equal.trans(List<&2, Nat>, ST.ids(tg), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(ST.TN{1n+j, a, b}), P.after(c))), SC.append(Nat, SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}), hbc, NS.wh_node(c, 1n+j, a, b))), DJ.mem_r(1n+j, SC.append(Nat, P.before(c), ST.ids(a)), Con{1n+j, SC.append(Nat, ST.ids(b), P.after(c))}, DJ.mem_hd(1n+j, SC.append(Nat, ST.ids(b), P.after(c))))) 123 +hib = AL.allin_mem(ST.ids(tg), SC.length(M.Node, nl), 1n+j, AL.allin_l(ST.ids(tg), fl, SC.length(M.Node, nl), ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)), mi) 124 +hjl = L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, SC.length(M.Node, nl), SC.length(Maybe<&2, V>, pl), Equal.sym(Nat, SC.length(Maybe<&2, V>, pl), SC.length(M.Node, nl), N.eq_from_is_eq(SC.length(Maybe<&2, V>, pl), SC.length(M.Node, nl), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))), N.succ_le_lt(j, SC.length(M.Node, nl), L.and_right(Nat.is_lt(0n, 1n+j), Nat.is_le(1n+j, SC.length(M.Node, nl)), hib))) 125 +hW2a = ents_at(~K, ~V, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, c, 1n+j, a, b, hbc) 126 +eX2 = SL.ents_pex(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl, 1n+j, Some{v}, nX) 127 +eY2 = SL.ents_pex(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl, 1n+j, Some{v}, nY) 128 +epv = SL.pv_ex_same(V, pl, j, Some{v}, hjl) 129 +eent2 = L.subst(Maybe<&2, V>, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j)) == ST.ent(K, V, M.N{c0, x1, x2, x3, key}, z) : Maybe<&2, M.Entry>}, ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j), Some{v}, epv, L.subst(M.Node, z => {ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j)) == ST.ent(K, V, z, ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j)) : Maybe<&2, M.Entry>}, ST.nd(K, nl, 1n+j), M.N{c0, x1, x2, x3, key}, hxi, {==})) 130 +hW2b = L.subst(Maybe<&2, M.Entry>, z => {SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})))) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), ST.cons_m(M.Entry, z, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})))) : List<&2, M.Entry>}, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j)), Some{M.Entry{key, v}}, eent2, {==}) 131 +hW2c = L.subst(List<&2, M.Entry>, z => {SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}) == SC.append(M.Entry, z, Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}) : List<&2, M.Entry>}, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), eX2, {==}) 132 +hW2d = L.subst(List<&2, M.Entry>, z => {SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}) == SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, z}) : List<&2, M.Entry>}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl), eY2, {==}) 133 +hW2 = Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})))), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), hW2a, Equal.trans(List<&2, M.Entry>, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), ST.cons_m(M.Entry, ST.ent(K, V, ST.nd(K, nl, 1n+j), ST.pv(V, PR.ex_pl(V, pl, 1n+j, Some{v}), 1n+j)), ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})))), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), hW2b, Equal.trans(List<&2, M.Entry>, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, PR.ex_pl(V, pl, 1n+j, Some{v}))}), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append 134 +hsv = Equal.trans(List<&2, M.Entry>, S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.set_val(~K, ~V, ~cmp, k, v, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)})), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), L.subst(List<&2, M.Entry>, z => {S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.set_val(~K, ~V, ~cmp, k, v, z) : List<&2, M.Entry>}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, vi}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), hW, {==}), set_val_mid(~K, ~V, ~cmp, ~o, k, v, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), M.Entry{key, vi}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl), hlx, hc)) 135 +gcpl = L.subst(Nat, z => {Nat.is_eq(z, SC.length(M.Node, nl)) == True{} : Bool}, SC.length(Maybe<&2, V>, pl), SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+j, Some{v})), Equal.sym(Nat, SC.length(Maybe<&2, V>, PR.ex_pl(V, pl, 1n+j, Some{v})), SC.length(Maybe<&2, V>, pl), SL.len_ex(V, pl, 1n+j, Some{v})), ST.g_cpl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 136 +gcord = L.subst(List<&2, M.Entry>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), Equal.sym(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), hW2), ord_key(~K, ~V, ~cmp, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), M.Entry{key, vi}, M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl), {==}, hord)) 137 +good = ST.good_intro(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, PR.ex_pl(V, pl, 1n+j, Some{v}), tg, fl, ST.g_cl(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_ccap(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), gcpl, ST.g_crep(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), pay_ex(~V, tg, pl, 1n+j, Some{v}, ST.g_cpay(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), {==}), ST.g_cfll(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cnd(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cin(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_clen(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), gcord, ST.g_cblk(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_csz(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_croot(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_clo(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_chi(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), ST.g_cfree(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)) 138 (Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, ST.ids(tg), nl, PR.ex_pl(V, pl, 1n+j, Some{v})), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), hW2, Equal.sym(List<&2, M.Entry>, S.set_val(~K, ~V, ~cmp, k, v, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.append(M.Entry, ST.ents(~K, ~V, SC.append(Nat, P.before(c), ST.ids(a)), nl, pl), Con{M.Entry{key, v}, ST.ents(~K, ~V, SC.append(Nat, ST.ids(b), P.after(c)), nl, pl)}), hsv)), good)