1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/order.bend as O 5 import ../../../spec/lib/common.bend as SC 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 ./ends.bend as EN 11 import ./path.bend as P 12 import ./plug.bend as PG 13 import ./setters.bend as SE 14 import ./rotm.bend as RM 15 import ./rotp.bend as RP 16 import ./nbr.bend as NB 17 import ./dj.bend as DJ 18 import ./spath.bend as SP 19 import ./fix.bend as FX 20 import ../../lib/nat_list.bend as NL 21 22 23 # The deletion fix-up: from the position x the unlinked node's child took 24 # (its subtree possibly empty) under its parent, the loop recolours and 25 # rotates on either side; whatever it does and however far its fuel goes, it 26 # ends with a black root over a linked tree of the same ids, entries and free 27 # chain. (source: tools/generators/tm_hand/dfix.src) 28 29 30 # recolouring keeps the links, the entries, the free chain and the length 31 32 # so do rotations 33 34 # a frame's facts: its parent's check, the frames above, the parent's node 35 # and the sibling's links 36 37 # ---- the end ---- 38 39 # a linked tree of the ids and a step that stopped: the loop blackens the root 40 def dstop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +t: ST.Tr, +h1: {ST.rep(~K, t, 0n, nl) == True{} : Bool}, +h2: {root == ST.rid(t) : Nat}, +h3: {ST.ids(t) == i0 : List<&2, Nat>}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 41 match gf: 42 case 0n: 43 FX.fin(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, root, nl, t, h1, h2, h3, h4, h5, h6, h7) 44 case 1n+g: 45 FX.fin(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, root, nl, t, h1, h2, h3, h4, h5, h6, h7) 46 47 # the path invariant gives the whole tree 48 def dfin(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +root: Nat, +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +i2: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(c, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.black_root(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 49 FX.fin(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, root, nl, PG.plug(c, t), PG.rep_plug(~K, nl, c, t, i1, i2), i5, Equal.trans(List<&2, Nat>, ST.ids(PG.plug(c, t)), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))), i0, PG.ids_plug(c, t), i4), h4, h5, h6, h7) 50 51 # ---- the left side: x under p on the left, its sibling s on the right ---- 52 53 54 # both nephews black: the sibling red, then on from the parent 55 def dup_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, True{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, True{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, True{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l, 56 +hk = L.and_left(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2) 57 %Equal.sym(Nat, M.node_parent(~K, ST.nd(K, nl, p)), P.top(c1), NB.parent_eq(~K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(c1), L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl)), hk)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(s), True{}), M.DF{p, _, True{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 58 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(s), True{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, ST.rid(s), True{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, ST.rid(s), True{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (_, M.DF{p, P.top(c1), True{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 59 kont(root, SE.setc(K, nl, ST.rid(s), True{}), c1, ST.TN{p, t, s}, Equal.trans(Bool, ST.rep(~K, ST.TN{p, t, s}, P.top(c1), SE.setc(K, nl, ST.rid(s), True{})), ST.rep(~K, ST.TN{p, t, s}, P.top(c1), nl), True{}, SE.rep_setc(~K, ST.TN{p, t, s}, P.top(c1), nl, ST.rid(s), True{}), FX.up_t(~K, nl, p, s, t, P.top(c1), i1, hk)), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, nl, ST.rid(s), True{})), P.ctxok(~K, c1, p, nl), True{}, SE.ctx_setc(~K, c1, p, nl, ST.rid(s), True{}), L.and_right(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, s}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, s}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))), P.ids_l(c1, p, t, s)), i3), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, s}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))), i0, P.ids_l(c1, p, t, s), i4), i5, Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, nl, ST.rid(s), True{}), pl), ST.ents(~K, ~V, i0, nl, pl), e0, SE.ents_setc(~K, ~V, i0, nl, pl, ST.rid(s), True{}), h4), Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, nl, ST.rid(s), True{}), pl), EN.oks(~K, ~V, i0, nl, pl), True{}, SE.oks_setc(~K, ~V, i0, nl, pl, ST.rid(s), True{}), h5), Equal.trans(Bool, ST.fll(~K, SE.setc(K, nl, ST.rid(s), True{}), fx), ST.fll(~K, nl, fx), True{}, SE.fll_setc(~K, fx, nl, ST.rid(s), True{}), h6), Equal.trans(Nat, SC.length(M.Node, SE.setc(K, nl, ST.rid(s), True{})), SC.length(M.Node, nl), l0, SE.setc_len(K, nl, ST.rid(s), T 60 61 # the far nephew red: three recolourings and a rotation at the parent end it 62 63 def dborrow_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +t: ST.Tr, +w: Nat, +sa: ST.Tr, +sb: ST.Tr, +hr: {ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c1, p, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1)))) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c1, ST.TN{p, t, ST.TN{w, sa, sb}})) : Nat}, +hids: {SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))) == i0 : List<&2, Nat>}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 64 +hw = TR.rep_node(~K, w, sa, sb, p, nl, TR.rep_r(~K, p, t, ST.TN{w, sa, sb}, P.top(c1), nl, hr)) 65 %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, w)), ST.rid(sb), NB.child_eq(~K, ST.nd(K, nl, w), ST.rid(sa), ST.rid(sb), p, True{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_left(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), _, False{}), p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 66 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, M.node_red(~K, ST.nd(K, nl, p))), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, M.node_red(~K, ST.nd(K, nl, p)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_left(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, p, False{}), ST.rid(sb), False{}), p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 67 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, tg, fl}, p, False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, tg, fl, p, False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_left(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, ST.rid(sb), False{}), p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 68 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, tg, fl}, ST.rid(sb), False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, tg, fl, ST.rid(sb), False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_left(~K, ~V, ~cmp, _, p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 69 +hr3 = Equal.trans(Bool, ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{})), ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), True{}, SE.rep_setc(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), Equal.trans(Bool, ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), True{}, SE.rep_setc(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Bool, ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), nl), True{}, SE.rep_setc(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), nl, w, M.node_red(~K, ST.nd(K, nl, p))), hr))) 70 +hok3 = Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{})), P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), True{}, SE.ctx_setc(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), P.ctxok(~K, c1, p, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), True{}, SE.ctx_setc(~K, c1, p, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), P.ctxok(~K, c1, p, nl), True{}, SE.ctx_setc(~K, c1, p, nl, w, M.node_red(~K, ST.nd(K, nl, p))), hok))) 71 %Equal.sym(ST.Sh, MI.rotate_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), pl, tg, fl}, p), ST.SH{n, RM.rootq(P.top(c1), root, w), lo, hi, free, l, d, RM.rotl_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), pl, tg, fl}, RP.rotl_path_eq(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), pl, tg, fl, c1, p, t, w, sa, sb, hr3, hok3, hnd)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (_, M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 72 +hrr = PG.rep_plug(~K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), c1, ST.TN{w, ST.TN{p, t, sa}, sb}, RP.rotl_path_rep(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), c1, p, t, w, sa, sb, hr3, hok3, hnd), RP.rotl_path_ctx(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), c1, p, t, w, sa, sb, hr3, hok3, hnd)) 73 +hq = RP.root_rot(~K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), c1, p, w, ST.TN{p, t, ST.TN{w, sa, sb}}, ST.TN{w, ST.TN{p, t, sa}, sb}, root, {==}, {==}, hok3, hroot) 74 +ho = Equal.trans(List<&2, Nat>, ST.ids(PG.plug(c1, ST.TN{w, ST.TN{p, t, sa}, sb})), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{p, t, sa}, sb}), P.after(c1))), i0, PG.ids_plug(c1, ST.TN{w, ST.TN{p, t, sa}, sb}), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{p, t, sa}, sb}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), i0, RP.wh_eq(c1, ST.TN{w, ST.TN{p, t, sa}, sb}, ST.TN{p, t, ST.TN{w, sa, sb}}, RP.ids_rl(p, t, w, sa, sb)), hids)) 75 +g4 = Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), pl), ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), e0, SE.ents_setc(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, ST.rid(sb), False{}), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), ST.ents(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), e0, SE.ents_setc(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, p, False{}), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), ST.ents(~K, ~V, i0, nl, pl), e0, SE.ents_setc(~K, ~V, i0, nl, pl, w, M.node_red(~K, ST.nd(K, nl, p))), h4))) 76 +g5 = Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), pl), EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), True{}, SE.oks_setc(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, ST.rid(sb), False{}), Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), EN.oks(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), True{}, SE.oks_setc(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, p, False{}), Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), EN.oks(~K, ~V, i0, nl, pl), True{}, SE.oks_setc(~K, ~V, i0, nl, pl, w, M.node_red(~K, ST.nd(K, nl, p))), h5))) 77 +g6 = Equal.trans(Bool, ST.fll(~K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), fx), ST.fll(~K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), fx), True{}, SE.fll_setc(~K, fx, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), Equal.trans(Bool, ST.fll(~K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), fx), ST.fll(~K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), fx), True{}, SE.fll_setc(~K, fx, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Bool, ST.fll(~K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), fx), ST.fll(~K, nl, fx), True{}, SE.fll_setc(~K, fx, nl, w, M.node_red(~K, ST.nd(K, nl, p))), h6))) 78 +g7 = Equal.trans(Nat, SC.length(M.Node, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{})), SC.length(M.Node, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), l0, SE.setc_len(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), Equal.trans(Nat, SC.length(M.Node, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), SC.length(M.Node, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), l0, SE.setc_len(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Nat, SC.length(M.Node, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), SC.length(M.Node, nl), l0, SE.setc_len(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), h7))) 79 dstop(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, RM.rootq(P.top(c1), root, w), RM.rotl_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), PG.plug(c1, ST.TN{w, ST.TN{p, t, sa}, sb}), hrr, hq, ho, Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, RM.rotl_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), pl), ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), pl), e0, RP.rotl_ents(~K, ~V, i0, pl, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), g4), Equal.trans(Bool, EN.oks(~K, ~V, i0, RM.rotl_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), pl), EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), pl), True{}, RP.rotl_oks(~K, ~V, i0, pl, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), g5), Equal.trans(Bool, ST.fll(~K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), fx), ST.fll(~K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), fx), True{}, RP.rotl_fll(~K, fx, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sb), False{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), g6), Equal.trans(Nat, SC.length(M.Node, RM.rotl_nl(K, SE.setc(K, SE.setc(K, SE. 80 81 # only the near nephew red: it goes black, the sibling red, a rotation at 82 # the sibling makes the nephew the sibling, whose far child is now red 83 84 def dfar_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +t: ST.Tr, +w: Nat, +y: Nat, +ya: ST.Tr, +yb: ST.Tr, +sb: ST.Tr, +hr: {ST.rep(~K, ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}, P.top(c1), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c1, p, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1)))) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c1, ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}})) : Nat}, +hids: {SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))) == i0 : List<&2, Nat>}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_far_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), False{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 85 +hsw = TR.rep_r(~K, p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}, P.top(c1), nl, hr) 86 +hw = TR.rep_node(~K, w, ST.TN{y, ya, yb}, sb, p, nl, hsw) 87 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, w)), y, NB.child_eq(~K, ST.nd(K, nl, w), y, ST.rid(sb), p, False{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_left(~K, ~V, ~cmp, MI.rotate_right(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _, False{}), w, True{}), w), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 88 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y, False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, y, False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, y, False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_left(~K, ~V, ~cmp, MI.rotate_right(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, w, True{}), w), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 89 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, y, False{}), pl, tg, fl}, w, True{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, nl, y, False{}), pl, tg, fl, w, True{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_left(~K, ~V, ~cmp, MI.rotate_right(~K, ~V, ~cmp, _, w), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 90 okr = P.ok_r(~K, nl, c1, p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}, hr, hok) 91 +hrw = Equal.trans(Bool, ST.rep(~K, ST.TN{w, ST.TN{y, ya, yb}, sb}, p, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{})), ST.rep(~K, ST.TN{w, ST.TN{y, ya, yb}, sb}, p, SE.setc(K, nl, y, False{})), True{}, SE.rep_setc(~K, ST.TN{w, ST.TN{y, ya, yb}, sb}, p, SE.setc(K, nl, y, False{}), w, True{}), Equal.trans(Bool, ST.rep(~K, ST.TN{w, ST.TN{y, ya, yb}, sb}, p, SE.setc(K, nl, y, False{})), ST.rep(~K, ST.TN{w, ST.TN{y, ya, yb}, sb}, p, nl), True{}, SE.rep_setc(~K, ST.TN{w, ST.TN{y, ya, yb}, sb}, p, nl, y, False{}), hsw)) 92 +hcw = Equal.trans(Bool, P.ctxok(~K, Con{P.FR{p, False{}, t}, c1}, w, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{})), P.ctxok(~K, Con{P.FR{p, False{}, t}, c1}, w, SE.setc(K, nl, y, False{})), True{}, SE.ctx_setc(~K, Con{P.FR{p, False{}, t}, c1}, w, SE.setc(K, nl, y, False{}), w, True{}), Equal.trans(Bool, P.ctxok(~K, Con{P.FR{p, False{}, t}, c1}, w, SE.setc(K, nl, y, False{})), P.ctxok(~K, Con{P.FR{p, False{}, t}, c1}, w, nl), True{}, SE.ctx_setc(~K, Con{P.FR{p, False{}, t}, c1}, w, nl, y, False{}), Pair.fst({P.ctxok(~K, Con{P.FR{p, False{}, t}, c1}, w, nl) == True{} : Bool}, {ST.rep(~K, ST.TN{w, ST.TN{y, ya, yb}, sb}, p, nl) == True{} : Bool}, okr))) 93 +ew = P.ids_r(c1, p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}) 94 +hndw = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{y, ya, yb}, sb}), P.after(Con{P.FR{p, False{}, t}, c1}))), ew, hnd) 95 %Equal.sym(ST.Sh, MI.rotate_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl, tg, fl}, w), ST.SH{n, RM.rootq(p, root, y), lo, hi, free, l, d, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), pl, tg, fl}, RP.rotr_path_eq(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl, tg, fl, Con{P.FR{p, False{}, t}, c1}, w, ya, y, yb, sb, hrw, hcw, hndw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_left(~K, ~V, ~cmp, _, p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 96 +hr2 = RP.rotr_path_rep(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), Con{P.FR{p, False{}, t}, c1}, w, ya, y, yb, sb, hrw, hcw, hndw) 97 +hc2 = RP.rotr_path_ctx(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), Con{P.FR{p, False{}, t}, c1}, w, ya, y, yb, sb, hrw, hcw, hndw) 98 +hk2 = L.and_left(P.cok1(~K, P.FR{p, False{}, t}, y, P.top(c1), RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1}))), P.ctxok(~K, c1, p, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1}))), hc2) 99 %Equal.sym(Nat, M.node_right(~K, ST.nd(K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), p)), y, NB.child_eq(~K, ST.nd(K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), p), ST.rid(t), y, P.top(c1), True{}, L.and_left(ST.is_node(K, ST.nd(K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), p), ST.pk(Nat, False{}, y, ST.rid(t)), ST.pk(Nat, False{}, ST.rid(t), y), P.top(c1)), ST.rep(~K, t, p, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1}))), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), p), ST.pk(Nat, False{}, y, ST.rid(t)), ST.pk(Nat, False{}, ST.rid(t), y), P.top(c1)), ST.rep(~K, t, p, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})))), hk2)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_left(~K, ~V, ~cmp, ST.SH{n, RM.rootq(p, root, y), lo, hi, free, l, d, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), pl, tg, fl}, p, _, ST.nd(K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), p), ST.nd(K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), _))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, N 100 +eW = Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{y, ya, ST.TN{w, yb, sb}}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{y, ya, ST.TN{w, yb, sb}}), P.after(Con{P.FR{p, False{}, t}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))), P.ids_r(c1, p, t, ST.TN{y, ya, ST.TN{w, yb, sb}}), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{p, False{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{y, ya, ST.TN{w, yb, sb}}), P.after(Con{P.FR{p, False{}, t}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, False{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{y, ya, yb}, sb}), P.after(Con{P.FR{p, False{}, t}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))), RP.wh_eq(Con{P.FR{p, False{}, t}, c1}, ST.TN{y, ya, ST.TN{w, yb, sb}}, ST.TN{w, ST.TN{y, ya, yb}, sb}, RP.ids_rr(w, y, ya, yb, sb)), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{y, ya, yb}, sb}), P.after(Con{P.FR{p, False{}, t}, c1}))), ew))) 101 +hq = RP.root_rot(~K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), Con{P.FR{p, False{}, t}, c1}, w, y, ST.TN{w, ST.TN{y, ya, yb}, sb}, ST.TN{y, ya, ST.TN{w, yb, sb}}, root, {==}, {==}, hcw, hroot) 102 dborrow_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, RM.rootq(p, root, y), RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), c1, p, t, y, ya, ST.TN{w, yb, sb}, FX.up_f(~K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), p, t, ST.TN{y, ya, ST.TN{w, yb, sb}}, P.top(c1), hr2, hk2), L.and_right(P.cok1(~K, P.FR{p, False{}, t}, y, P.top(c1), RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1}))), P.ctxok(~K, c1, p, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1}))), hc2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{y, ya, ST.TN{w, yb, sb}}}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{y, ya, ST.TN{w, yb, sb}}}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))), eW), hnd), hq, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{y, ya, ST.TN{w, yb, sb}}}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, ST.TN{y, ya, yb}, sb}}), P.after(c1))), i0, eW, hids), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, False{}, t}, c1})), pl), ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl), e0, RP.rotr_ents(~K, ~V, i0, pl, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(yb), p, SP.dir(Con{P.FR{p, 103 104 # a red near nephew is a node 105 def dfar0_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +t: ST.Tr, +w: Nat, +sa: ST.Tr, +sb: ST.Tr, +hnr: {M.node_red(~K, ST.nd(K, nl, ST.rid(sa))) == True{} : Bool}, +hr: {ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c1, p, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1)))) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c1, ST.TN{p, t, ST.TN{w, sa, sb}})) : Nat}, +hids: {SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))) == i0 : List<&2, Nat>}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_far_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), False{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 106 match sa: 107 case ST.TE{}: 108 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_far_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), False{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(hnr)) 109 case ST.TN{+y, +ya, +yb}: 110 dfar_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, y, ya, yb, sb, hr, hok, hnd, hroot, hids, h4, h5, h6, h7) 111 112 113 # the nephews' colours 114 def dkids_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +w: Nat, +sa: ST.Tr, +sb: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, & 115 match nr fr: 116 case False{} False{}: 117 dup_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TN{w, sa, sb}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 118 case True{} True{}: 119 dborrow_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, sa, sb, FX.up_t(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.and_right(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), P.ids_l(c1, p, t, ST.TN{w, sa, sb})), i3), i5, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), i0, P.ids_l(c1, p, t, ST.TN{w, sa, sb}), i4), h4, h5, h6, h7) 120 case False{} True{}: 121 dborrow_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, sa, sb, FX.up_t(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.and_right(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), P.ids_l(c1, p, t, ST.TN{w, sa, sb})), i3), i5, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), i0, P.ids_l(c1, p, t, ST.TN{w, sa, sb}), i4), h4, h5, h6, h7) 122 case True{} False{}: 123 dfar0_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, sa, sb, hnr, FX.up_t(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.and_right(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), P.ids_l(c1, p, t, ST.TN{w, sa, sb})), i3), i5, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), i0, P.ids_l(c1, p, t, ST.TN{w, sa, sb}), i4), h4, h5, h6, h7) 124 125 126 # the sibling's children 127 def dsib2_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, True{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, True{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, True{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l 128 match s: 129 case ST.TE{}: 130 dup_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TE{}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 131 case ST.TN{+w, +sa, +sb}: 132 +hw = TR.rep_node(~K, w, sa, sb, p, nl, L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(ST.TN{w, sa, sb})), ST.pk(Nat, True{}, ST.rid(ST.TN{w, sa, sb}), ST.rid(t)), P.top(c1)), ST.rep(~K, ST.TN{w, sa, sb}, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(ST.TN{w, sa, sb})), ST.pk(Nat, True{}, ST.rid(ST.TN{w, sa, sb}), ST.rid(t)), P.top(c1)), ST.rep(~K, ST.TN{w, sa, sb}, p, nl)), L.and_left(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)))) 133 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, w)), ST.rid(sa), NB.child_eq(~K, ST.nd(K, nl, w), ST.rid(sa), ST.rid(sb), p, False{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_children_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), M.node_red(~K, ST.nd(K, nl, _)), M.node_red(~K, ST.nd(K, nl, M.node_right(~K, ST.nd(K, nl, w)))))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 134 %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, w)), ST.rid(sb), NB.child_eq(~K, ST.nd(K, nl, w), ST.rid(sa), ST.rid(sb), p, True{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_children_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), M.node_red(~K, ST.nd(K, nl, ST.rid(sa))), M.node_red(~K, ST.nd(K, nl, _)))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 135 dkids_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, w, sa, sb, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, M.node_red(~K, ST.nd(K, nl, ST.rid(sa))), {==}, M.node_red(~K, ST.nd(K, nl, ST.rid(sb))), {==}) 136 137 # reading the parent and the sibling 138 def dsib_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, True{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, True{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, True{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l, 139 +hk = L.and_left(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2) 140 %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, p)), ST.rid(s), NB.child_eq(~K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(c1), True{}, L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl)), hk)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_children_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, _, ST.nd(K, nl, p), ST.nd(K, nl, _), M.node_red(~K, ST.nd(K, nl, M.node_left(~K, ST.nd(K, nl, _)))), M.node_red(~K, ST.nd(K, nl, M.node_right(~K, ST.nd(K, nl, _)))))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 141 dsib2_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 142 143 # a red sibling: it goes black, the parent red, a rotation at the parent 144 # gives x the sibling's near child as its new sibling 145 146 def dred_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, True{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, True{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, True{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l, 147 match s b: 148 case ST.TE{} False{}: 149 dsib_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TE{}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 150 case ST.TE{} True{}: 151 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_red_sibling_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, 0n, True{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(hb)) 152 case ST.TN{+w, +sa, +sb} False{}: 153 dsib_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TN{w, sa, sb}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 154 case ST.TN{+w, +sa, +sb} True{}: 155 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_sibling_left(~K, ~V, ~cmp, MI.rotate_left(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, p, True{}), p), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 156 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, False{}), pl, tg, fl}, p, True{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, nl, w, False{}), pl, tg, fl, p, True{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_sibling_left(~K, ~V, ~cmp, MI.rotate_left(~K, ~V, ~cmp, _, p), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 157 +hr2 = Equal.trans(Bool, ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, False{}), p, True{})), ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, nl, w, False{})), True{}, SE.rep_setc(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, nl, w, False{}), p, True{}), Equal.trans(Bool, ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), SE.setc(K, nl, w, False{})), ST.rep(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), nl), True{}, SE.rep_setc(~K, ST.TN{p, t, ST.TN{w, sa, sb}}, P.top(c1), nl, w, False{}), FX.up_t(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)))) 158 +hok2 = Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{})), P.ctxok(~K, c1, p, SE.setc(K, nl, w, False{})), True{}, SE.ctx_setc(~K, c1, p, SE.setc(K, nl, w, False{}), p, True{}), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, nl, w, False{})), P.ctxok(~K, c1, p, nl), True{}, SE.ctx_setc(~K, c1, p, nl, w, False{}), L.and_right(P.cok1(~K, P.FR{p, True{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2))) 159 +hnd = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), P.ids_l(c1, p, t, ST.TN{w, sa, sb})), i3) 160 %Equal.sym(ST.Sh, MI.rotate_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), pl, tg, fl}, p), ST.SH{n, RM.rootq(P.top(c1), root, w), lo, hi, free, l, d, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), pl, tg, fl}, RP.rotl_path_eq(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), pl, tg, fl, c1, p, t, w, sa, sb, hr2, hok2, hnd)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_sibling_left(~K, ~V, ~cmp, _, p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 161 +eW = Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{p, True{}, sa}, Con{P.FR{w, True{}, sb}, c1}}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, sa}, Con{P.FR{w, True{}, sb}, c1}}))), SC.append(Nat, P.before(Con{P.FR{w, True{}, sb}, c1}), SC.append(Nat, ST.ids(ST.TN{p, t, sa}), P.after(Con{P.FR{w, True{}, sb}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{w, True{}, sb}, c1}), SC.append(Nat, ST.ids(ST.TN{p, t, sa}), P.after(Con{P.FR{w, True{}, sb}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, True{}, sa}, Con{P.FR{w, True{}, sb}, c1}}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, sa}, Con{P.FR{w, True{}, sb}, c1}}))), P.ids_l(Con{P.FR{w, True{}, sb}, c1}, p, t, sa)), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{w, True{}, sb}, c1}), SC.append(Nat, ST.ids(ST.TN{p, t, sa}), P.after(Con{P.FR{w, True{}, sb}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{p, t, sa}, sb}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{p, t, sa}, sb}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{w, True{}, sb}, c1}), SC.append(Nat, ST.ids(ST.TN{p, t, sa}), P.after(Con{P.FR{w, True{}, sb}, c1}))), P.ids_l(c1, w, ST.TN{p, t, sa}, sb)), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, ST.TN{p, t, sa}, sb}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, t, ST.TN{w, sa, sb}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, ST.TN{w, sa, sb}}, c1}))), RP.wh_eq(c1, ST.TN{w, ST.TN{p, t, s 162 dsib_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, RM.rootq(P.top(c1), root, w), RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), Con{P.FR{w, True{}, sb}, c1}, p, sa, t, Pair.snd({P.ctxok(~K, Con{P.FR{p, True{}, sa}, Con{P.FR{w, True{}, sb}, c1}}, ST.rid(t), RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1))) == True{} : Bool}, {ST.rep(~K, t, p, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1))) == True{} : Bool}, P.ok_l(~K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), Con{P.FR{w, True{}, sb}, c1}, p, t, sa, Pair.snd({P.ctxok(~K, Con{P.FR{w, True{}, sb}, c1}, p, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1))) == True{} : Bool}, {ST.rep(~K, ST.TN{p, t, sa}, w, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1))) == True{} : Bool}, P.ok_l(~K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), c1, w, ST.TN{p, t, sa}, sb, RP.rotl_path_rep(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), c1, p, t, w, sa, sb, hr2, hok2, hnd), RP.rotl_path_ctx(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), c1, p, t, w, sa, sb, hr2, hok2, hnd))), Pair.fst({P.ctxok(~K, Con{P.FR{w, True{}, sb}, c1}, p, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1))) == True{} : Bool}, {ST.rep(~K, ST.TN{p, t, sa}, w, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1))) == True{} : Bool}, P.ok_l(~K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sa), P.top(c1), SP.dir(c1)), c1, w, ST.TN{p, t, sa}, sb, RP.rotl_ 163 164 # x on the left: read the sibling 165 def dside_l(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, True{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, True{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, True{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, True{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, True{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l 166 +hk = L.and_left(P.cok1(~K, P.FR{p, True{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2) 167 %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, p)), ST.rid(s), NB.child_eq(~K, ST.nd(K, nl, p), ST.rid(t), ST.rid(s), P.top(c1), True{}, L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl)), hk)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_red_sibling_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, _, M.node_red(~K, ST.nd(K, nl, _)))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 168 dred_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, M.node_red(~K, ST.nd(K, nl, ST.rid(s))), {==}) 169 170 # ---- the right side: x under p on the right, its sibling s on the left ---- 171 172 def dup_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, fr 173 +hk = L.and_left(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2) 174 %Equal.sym(Nat, M.node_parent(~K, ST.nd(K, nl, p)), P.top(c1), NB.parent_eq(~K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(c1), L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl)), hk)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(s), True{}), M.DF{p, _, True{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 175 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(s), True{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, ST.rid(s), True{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, ST.rid(s), True{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (_, M.DF{p, P.top(c1), True{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 176 kont(root, SE.setc(K, nl, ST.rid(s), True{}), c1, ST.TN{p, s, t}, Equal.trans(Bool, ST.rep(~K, ST.TN{p, s, t}, P.top(c1), SE.setc(K, nl, ST.rid(s), True{})), ST.rep(~K, ST.TN{p, s, t}, P.top(c1), nl), True{}, SE.rep_setc(~K, ST.TN{p, s, t}, P.top(c1), nl, ST.rid(s), True{}), FX.up_f(~K, nl, p, s, t, P.top(c1), i1, hk)), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, nl, ST.rid(s), True{})), P.ctxok(~K, c1, p, nl), True{}, SE.ctx_setc(~K, c1, p, nl, ST.rid(s), True{}), L.and_right(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, s, t}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, s, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))), P.ids_r(c1, p, s, t)), i3), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, s, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))), i0, P.ids_r(c1, p, s, t), i4), i5, Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, nl, ST.rid(s), True{}), pl), ST.ents(~K, ~V, i0, nl, pl), e0, SE.ents_setc(~K, ~V, i0, nl, pl, ST.rid(s), True{}), h4), Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, nl, ST.rid(s), True{}), pl), EN.oks(~K, ~V, i0, nl, pl), True{}, SE.oks_setc(~K, ~V, i0, nl, pl, ST.rid(s), True{}), h5), Equal.trans(Bool, ST.fll(~K, SE.setc(K, nl, ST.rid(s), True{}), fx), ST.fll(~K, nl, fx), True{}, SE.fll_setc(~K, fx, nl, ST.rid(s), True{}), h6), Equal.trans(Nat, SC.length(M.Node, SE.setc(K, nl, ST.rid(s), True{})), SC.length(M.Node, nl), l0, SE.setc_len(K, nl, ST.ri 177 178 179 def dborrow_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +t: ST.Tr, +w: Nat, +sa: ST.Tr, +sb: ST.Tr, +hr: {ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c1, p, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1)))) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c1, ST.TN{p, ST.TN{w, sa, sb}, t})) : Nat}, +hids: {SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))) == i0 : List<&2, Nat>}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 180 +hw = TR.rep_node(~K, w, sa, sb, p, nl, TR.rep_l(~K, p, ST.TN{w, sa, sb}, t, P.top(c1), nl, hr)) 181 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, w)), ST.rid(sa), NB.child_eq(~K, ST.nd(K, nl, w), ST.rid(sa), ST.rid(sb), p, False{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_right(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), _, False{}), p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 182 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, M.node_red(~K, ST.nd(K, nl, p))), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, M.node_red(~K, ST.nd(K, nl, p)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_right(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, p, False{}), ST.rid(sa), False{}), p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 183 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, tg, fl}, p, False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, tg, fl, p, False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_right(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, ST.rid(sa), False{}), p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 184 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, tg, fl}, ST.rid(sa), False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, tg, fl, ST.rid(sa), False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (MI.rotate_right(~K, ~V, ~cmp, _, p), M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 185 +hr3 = Equal.trans(Bool, ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{})), ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), True{}, SE.rep_setc(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), Equal.trans(Bool, ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), True{}, SE.rep_setc(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Bool, ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), nl), True{}, SE.rep_setc(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), nl, w, M.node_red(~K, ST.nd(K, nl, p))), hr))) 186 +hok3 = Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{})), P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), True{}, SE.ctx_setc(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), P.ctxok(~K, c1, p, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), True{}, SE.ctx_setc(~K, c1, p, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), P.ctxok(~K, c1, p, nl), True{}, SE.ctx_setc(~K, c1, p, nl, w, M.node_red(~K, ST.nd(K, nl, p))), hok))) 187 %Equal.sym(ST.Sh, MI.rotate_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), pl, tg, fl}, p), ST.SH{n, RM.rootq(P.top(c1), root, w), lo, hi, free, l, d, RM.rotr_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), pl, tg, fl}, RP.rotr_path_eq(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), pl, tg, fl, c1, p, sa, w, sb, t, hr3, hok3, hnd)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (_, M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 188 +hrr = PG.rep_plug(~K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), c1, ST.TN{w, sa, ST.TN{p, sb, t}}, RP.rotr_path_rep(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), c1, p, sa, w, sb, t, hr3, hok3, hnd), RP.rotr_path_ctx(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), c1, p, sa, w, sb, t, hr3, hok3, hnd)) 189 +hq = RP.root_rot(~K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), c1, p, w, ST.TN{p, ST.TN{w, sa, sb}, t}, ST.TN{w, sa, ST.TN{p, sb, t}}, root, {==}, {==}, hok3, hroot) 190 +ho = Equal.trans(List<&2, Nat>, ST.ids(PG.plug(c1, ST.TN{w, sa, ST.TN{p, sb, t}})), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{p, sb, t}}), P.after(c1))), i0, PG.ids_plug(c1, ST.TN{w, sa, ST.TN{p, sb, t}}), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{p, sb, t}}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), i0, RP.wh_eq(c1, ST.TN{w, sa, ST.TN{p, sb, t}}, ST.TN{p, ST.TN{w, sa, sb}, t}, RP.ids_rr(p, w, sa, sb, t)), hids)) 191 +g4 = Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), pl), ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), e0, SE.ents_setc(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, ST.rid(sa), False{}), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), ST.ents(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), e0, SE.ents_setc(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, p, False{}), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), ST.ents(~K, ~V, i0, nl, pl), e0, SE.ents_setc(~K, ~V, i0, nl, pl, w, M.node_red(~K, ST.nd(K, nl, p))), h4))) 192 +g5 = Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), pl), EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), True{}, SE.oks_setc(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl, ST.rid(sa), False{}), Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), pl), EN.oks(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), True{}, SE.oks_setc(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl, p, False{}), Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), pl), EN.oks(~K, ~V, i0, nl, pl), True{}, SE.oks_setc(~K, ~V, i0, nl, pl, w, M.node_red(~K, ST.nd(K, nl, p))), h5))) 193 +g6 = Equal.trans(Bool, ST.fll(~K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), fx), ST.fll(~K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), fx), True{}, SE.fll_setc(~K, fx, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), Equal.trans(Bool, ST.fll(~K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), fx), ST.fll(~K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), fx), True{}, SE.fll_setc(~K, fx, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Bool, ST.fll(~K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), fx), ST.fll(~K, nl, fx), True{}, SE.fll_setc(~K, fx, nl, w, M.node_red(~K, ST.nd(K, nl, p))), h6))) 194 +g7 = Equal.trans(Nat, SC.length(M.Node, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{})), SC.length(M.Node, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), l0, SE.setc_len(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), Equal.trans(Nat, SC.length(M.Node, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{})), SC.length(M.Node, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), l0, SE.setc_len(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), Equal.trans(Nat, SC.length(M.Node, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p)))), SC.length(M.Node, nl), l0, SE.setc_len(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), h7))) 195 dstop(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, RM.rootq(P.top(c1), root, w), RM.rotr_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), PG.plug(c1, ST.TN{w, sa, ST.TN{p, sb, t}}), hrr, hq, ho, Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, RM.rotr_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), pl), ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), pl), e0, RP.rotr_ents(~K, ~V, i0, pl, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), g4), Equal.trans(Bool, EN.oks(~K, ~V, i0, RM.rotr_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), pl), EN.oks(~K, ~V, i0, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), pl), True{}, RP.rotr_oks(~K, ~V, i0, pl, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), g5), Equal.trans(Bool, ST.fll(~K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), fx), ST.fll(~K, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), fx), True{}, RP.rotr_fll(~K, fx, SE.setc(K, SE.setc(K, SE.setc(K, nl, w, M.node_red(~K, ST.nd(K, nl, p))), p, False{}), ST.rid(sa), False{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), g6), Equal.trans(Nat, SC.length(M.Node, RM.rotr_nl(K, SE.setc(K, SE.setc(K, SE. 196 197 198 def dfar_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +t: ST.Tr, +w: Nat, +sa: ST.Tr, +y: Nat, +ya: ST.Tr, +yb: ST.Tr, +hr: {ST.rep(~K, ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}, P.top(c1), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c1, p, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1)))) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c1, ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t})) : Nat}, +hids: {SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))) == i0 : List<&2, Nat>}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_far_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), False{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 199 +hsw = TR.rep_l(~K, p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t, P.top(c1), nl, hr) 200 +hw = TR.rep_node(~K, w, sa, ST.TN{y, ya, yb}, p, nl, hsw) 201 %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, w)), y, NB.child_eq(~K, ST.nd(K, nl, w), ST.rid(sa), y, p, True{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_right(~K, ~V, ~cmp, MI.rotate_left(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, _, False{}), w, True{}), w), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 202 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y, False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, y, False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, y, False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_right(~K, ~V, ~cmp, MI.rotate_left(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, w, True{}), w), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 203 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, y, False{}), pl, tg, fl}, w, True{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, nl, y, False{}), pl, tg, fl, w, True{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_right(~K, ~V, ~cmp, MI.rotate_left(~K, ~V, ~cmp, _, w), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 204 okl = P.ok_l(~K, nl, c1, p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t, hr, hok) 205 +hrw = Equal.trans(Bool, ST.rep(~K, ST.TN{w, sa, ST.TN{y, ya, yb}}, p, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{})), ST.rep(~K, ST.TN{w, sa, ST.TN{y, ya, yb}}, p, SE.setc(K, nl, y, False{})), True{}, SE.rep_setc(~K, ST.TN{w, sa, ST.TN{y, ya, yb}}, p, SE.setc(K, nl, y, False{}), w, True{}), Equal.trans(Bool, ST.rep(~K, ST.TN{w, sa, ST.TN{y, ya, yb}}, p, SE.setc(K, nl, y, False{})), ST.rep(~K, ST.TN{w, sa, ST.TN{y, ya, yb}}, p, nl), True{}, SE.rep_setc(~K, ST.TN{w, sa, ST.TN{y, ya, yb}}, p, nl, y, False{}), hsw)) 206 +hcw = Equal.trans(Bool, P.ctxok(~K, Con{P.FR{p, True{}, t}, c1}, w, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{})), P.ctxok(~K, Con{P.FR{p, True{}, t}, c1}, w, SE.setc(K, nl, y, False{})), True{}, SE.ctx_setc(~K, Con{P.FR{p, True{}, t}, c1}, w, SE.setc(K, nl, y, False{}), w, True{}), Equal.trans(Bool, P.ctxok(~K, Con{P.FR{p, True{}, t}, c1}, w, SE.setc(K, nl, y, False{})), P.ctxok(~K, Con{P.FR{p, True{}, t}, c1}, w, nl), True{}, SE.ctx_setc(~K, Con{P.FR{p, True{}, t}, c1}, w, nl, y, False{}), Pair.fst({P.ctxok(~K, Con{P.FR{p, True{}, t}, c1}, w, nl) == True{} : Bool}, {ST.rep(~K, ST.TN{w, sa, ST.TN{y, ya, yb}}, p, nl) == True{} : Bool}, okl))) 207 +ew = P.ids_l(c1, p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t) 208 +hndw = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{y, ya, yb}}), P.after(Con{P.FR{p, True{}, t}, c1}))), ew, hnd) 209 %Equal.sym(ST.Sh, MI.rotate_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl, tg, fl}, w), ST.SH{n, RM.rootq(p, root, y), lo, hi, free, l, d, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), pl, tg, fl}, RP.rotl_path_eq(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl, tg, fl, Con{P.FR{p, True{}, t}, c1}, w, sa, y, ya, yb, hrw, hcw, hndw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_read_right(~K, ~V, ~cmp, _, p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 210 +hr2 = RP.rotl_path_rep(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), Con{P.FR{p, True{}, t}, c1}, w, sa, y, ya, yb, hrw, hcw, hndw) 211 +hc2 = RP.rotl_path_ctx(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), Con{P.FR{p, True{}, t}, c1}, w, sa, y, ya, yb, hrw, hcw, hndw) 212 +hk2 = L.and_left(P.cok1(~K, P.FR{p, True{}, t}, y, P.top(c1), RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1}))), P.ctxok(~K, c1, p, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1}))), hc2) 213 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), p)), y, NB.child_eq(~K, ST.nd(K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), p), y, ST.rid(t), P.top(c1), False{}, L.and_left(ST.is_node(K, ST.nd(K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), p), ST.pk(Nat, True{}, y, ST.rid(t)), ST.pk(Nat, True{}, ST.rid(t), y), P.top(c1)), ST.rep(~K, t, p, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1}))), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), p), ST.pk(Nat, True{}, y, ST.rid(t)), ST.pk(Nat, True{}, ST.rid(t), y), P.top(c1)), ST.rep(~K, t, p, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})))), hk2)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_borrow_right(~K, ~V, ~cmp, ST.SH{n, RM.rootq(p, root, y), lo, hi, free, l, d, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), pl, tg, fl}, p, _, ST.nd(K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), p), ST.nd(K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), _))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST. 214 +eW = Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{y, ST.TN{w, sa, ya}, yb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{y, ST.TN{w, sa, ya}, yb}), P.after(Con{P.FR{p, True{}, t}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))), P.ids_l(c1, p, ST.TN{y, ST.TN{w, sa, ya}, yb}, t), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{p, True{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{y, ST.TN{w, sa, ya}, yb}), P.after(Con{P.FR{p, True{}, t}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, True{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{y, ya, yb}}), P.after(Con{P.FR{p, True{}, t}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))), RP.wh_eq(Con{P.FR{p, True{}, t}, c1}, ST.TN{y, ST.TN{w, sa, ya}, yb}, ST.TN{w, sa, ST.TN{y, ya, yb}}, RP.ids_rl(w, sa, y, ya, yb)), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, t}, c1}), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{y, ya, yb}}), P.after(Con{P.FR{p, True{}, t}, c1}))), ew))) 215 +hq = RP.root_rot(~K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), Con{P.FR{p, True{}, t}, c1}, w, y, ST.TN{w, sa, ST.TN{y, ya, yb}}, ST.TN{y, ST.TN{w, sa, ya}, yb}, root, {==}, {==}, hcw, hroot) 216 dborrow_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, RM.rootq(p, root, y), RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), c1, p, t, y, ST.TN{w, sa, ya}, yb, FX.up_t(~K, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), p, t, ST.TN{y, ST.TN{w, sa, ya}, yb}, P.top(c1), hr2, hk2), L.and_right(P.cok1(~K, P.FR{p, True{}, t}, y, P.top(c1), RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1}))), P.ctxok(~K, c1, p, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1}))), hc2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{y, ST.TN{w, sa, ya}, yb}, t}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{y, ST.TN{w, sa, ya}, yb}, t}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))), eW), hnd), hq, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{y, ST.TN{w, sa, ya}, yb}, t}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, ST.TN{y, ya, yb}}, t}), P.after(c1))), i0, eW, hids), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, RM.rotl_nl(K, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{}, t}, c1})), pl), ST.ents(~K, ~V, i0, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), pl), e0, RP.rotl_ents(~K, ~V, i0, pl, SE.setc(K, SE.setc(K, nl, y, False{}), w, True{}), w, y, ST.rid(ya), p, SP.dir(Con{P.FR{p, True{ 217 218 def dfar0_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +t: ST.Tr, +w: Nat, +sa: ST.Tr, +sb: ST.Tr, +hnr: {M.node_red(~K, ST.nd(K, nl, ST.rid(sb))) == True{} : Bool}, +hr: {ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), nl) == True{} : Bool}, +hok: {P.ctxok(~K, c1, p, nl) == True{} : Bool}, +hnd: {NL.nodupn(SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1)))) == True{} : Bool}, +hroot: {root == ST.rid(PG.plug(c1, ST.TN{p, ST.TN{w, sa, sb}, t})) : Nat}, +hids: {SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))) == i0 : List<&2, Nat>}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_far_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), False{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 219 match sb: 220 case ST.TE{}: 221 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_far_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), False{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(hnr)) 222 case ST.TN{+y, +ya, +yb}: 223 dfar_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, sa, y, ya, yb, hr, hok, hnd, hroot, hids, h4, h5, h6, h7) 224 225 226 def dkids_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +w: Nat, +sa: ST.Tr, +sb: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigm 227 match nr fr: 228 case False{} False{}: 229 dup_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TN{w, sa, sb}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 230 case True{} True{}: 231 dborrow_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, sa, sb, FX.up_f(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.and_right(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), P.ids_r(c1, p, ST.TN{w, sa, sb}, t)), i3), i5, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), i0, P.ids_r(c1, p, ST.TN{w, sa, sb}, t), i4), h4, h5, h6, h7) 232 case False{} True{}: 233 dborrow_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, sa, sb, FX.up_f(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.and_right(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), P.ids_r(c1, p, ST.TN{w, sa, sb}, t)), i3), i5, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), i0, P.ids_r(c1, p, ST.TN{w, sa, sb}, t), i4), h4, h5, h6, h7) 234 case True{} False{}: 235 dfar0_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, t, w, sa, sb, hnr, FX.up_f(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)), L.and_right(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2), L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), P.ids_r(c1, p, ST.TN{w, sa, sb}, t)), i3), i5, Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), i0, P.ids_r(c1, p, ST.TN{w, sa, sb}, t), i4), h4, h5, h6, h7) 236 237 238 def dsib2_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, 239 match s: 240 case ST.TE{}: 241 dup_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TE{}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 242 case ST.TN{+w, +sa, +sb}: 243 +hw = TR.rep_node(~K, w, sa, sb, p, nl, L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(ST.TN{w, sa, sb})), ST.pk(Nat, False{}, ST.rid(ST.TN{w, sa, sb}), ST.rid(t)), P.top(c1)), ST.rep(~K, ST.TN{w, sa, sb}, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(ST.TN{w, sa, sb})), ST.pk(Nat, False{}, ST.rid(ST.TN{w, sa, sb}), ST.rid(t)), P.top(c1)), ST.rep(~K, ST.TN{w, sa, sb}, p, nl)), L.and_left(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)))) 244 %Equal.sym(Nat, M.node_right(~K, ST.nd(K, nl, w)), ST.rid(sb), NB.child_eq(~K, ST.nd(K, nl, w), ST.rid(sa), ST.rid(sb), p, True{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_children_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), M.node_red(~K, ST.nd(K, nl, _)), M.node_red(~K, ST.nd(K, nl, M.node_left(~K, ST.nd(K, nl, w)))))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 245 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, w)), ST.rid(sa), NB.child_eq(~K, ST.nd(K, nl, w), ST.rid(sa), ST.rid(sb), p, False{}, hw)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_children_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, w, ST.nd(K, nl, p), ST.nd(K, nl, w), M.node_red(~K, ST.nd(K, nl, ST.rid(sb))), M.node_red(~K, ST.nd(K, nl, _)))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 246 dkids_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, w, sa, sb, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, M.node_red(~K, ST.nd(K, nl, ST.rid(sb))), {==}, M.node_red(~K, ST.nd(K, nl, ST.rid(sa))), {==}) 247 248 def dsib_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, f 249 +hk = L.and_left(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2) 250 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, p)), ST.rid(s), NB.child_eq(~K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(c1), False{}, L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl)), hk)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_children_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, _, ST.nd(K, nl, p), ST.nd(K, nl, _), M.node_red(~K, ST.nd(K, nl, M.node_right(~K, ST.nd(K, nl, _)))), M.node_red(~K, ST.nd(K, nl, M.node_left(~K, ST.nd(K, nl, _)))))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 251 dsib2_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 252 253 254 def dred_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, f 255 match s b: 256 case ST.TE{} False{}: 257 dsib_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TE{}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 258 case ST.TE{} True{}: 259 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_red_sibling_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, 0n, True{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(hb)) 260 case ST.TN{+w, +sa, +sb} False{}: 261 dsib_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TN{w, sa, sb}, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 262 case ST.TN{+w, +sa, +sb} True{}: 263 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, w, False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, w, False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_sibling_right(~K, ~V, ~cmp, MI.rotate_right(~K, ~V, ~cmp, MI.set_red(~K, ~V, ~cmp, _, p, True{}), p), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 264 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, w, False{}), pl, tg, fl}, p, True{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, SE.setc(K, nl, w, False{}), pl, tg, fl, p, True{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_sibling_right(~K, ~V, ~cmp, MI.rotate_right(~K, ~V, ~cmp, _, p), p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 265 +hr2 = Equal.trans(Bool, ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, SE.setc(K, nl, w, False{}), p, True{})), ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, nl, w, False{})), True{}, SE.rep_setc(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, nl, w, False{}), p, True{}), Equal.trans(Bool, ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), SE.setc(K, nl, w, False{})), ST.rep(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), nl), True{}, SE.rep_setc(~K, ST.TN{p, ST.TN{w, sa, sb}, t}, P.top(c1), nl, w, False{}), FX.up_f(~K, nl, p, ST.TN{w, sa, sb}, t, P.top(c1), i1, L.and_left(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2)))) 266 +hok2 = Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{})), P.ctxok(~K, c1, p, SE.setc(K, nl, w, False{})), True{}, SE.ctx_setc(~K, c1, p, SE.setc(K, nl, w, False{}), p, True{}), Equal.trans(Bool, P.ctxok(~K, c1, p, SE.setc(K, nl, w, False{})), P.ctxok(~K, c1, p, nl), True{}, SE.ctx_setc(~K, c1, p, nl, w, False{}), L.and_right(P.cok1(~K, P.FR{p, False{}, ST.TN{w, sa, sb}}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2))) 267 +hnd = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), P.ids_r(c1, p, ST.TN{w, sa, sb}, t)), i3) 268 %Equal.sym(ST.Sh, MI.rotate_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), pl, tg, fl}, p), ST.SH{n, RM.rootq(P.top(c1), root, w), lo, hi, free, l, d, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), pl, tg, fl}, RP.rotr_path_eq(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), pl, tg, fl, c1, p, sa, w, sb, t, hr2, hok2, hnd)) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_sibling_right(~K, ~V, ~cmp, _, p)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 269 +eW = Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{p, False{}, sb}, Con{P.FR{w, False{}, sa}, c1}}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, sb}, Con{P.FR{w, False{}, sa}, c1}}))), SC.append(Nat, P.before(Con{P.FR{w, False{}, sa}, c1}), SC.append(Nat, ST.ids(ST.TN{p, sb, t}), P.after(Con{P.FR{w, False{}, sa}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{w, False{}, sa}, c1}), SC.append(Nat, ST.ids(ST.TN{p, sb, t}), P.after(Con{P.FR{w, False{}, sa}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, False{}, sb}, Con{P.FR{w, False{}, sa}, c1}}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, sb}, Con{P.FR{w, False{}, sa}, c1}}))), P.ids_r(Con{P.FR{w, False{}, sa}, c1}, p, sb, t)), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{w, False{}, sa}, c1}), SC.append(Nat, ST.ids(ST.TN{p, sb, t}), P.after(Con{P.FR{w, False{}, sa}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{p, sb, t}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{p, sb, t}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{w, False{}, sa}, c1}), SC.append(Nat, ST.ids(ST.TN{p, sb, t}), P.after(Con{P.FR{w, False{}, sa}, c1}))), P.ids_r(c1, w, sa, ST.TN{p, sb, t})), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{w, sa, ST.TN{p, sb, t}}), P.after(c1))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TN{w, sa, sb}, t}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, ST.TN{w, sa, sb}}, c1}))), RP.wh_eq(c1, 270 dsib_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, RM.rootq(P.top(c1), root, w), RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), Con{P.FR{w, False{}, sa}, c1}, p, sb, t, Pair.snd({P.ctxok(~K, Con{P.FR{p, False{}, sb}, Con{P.FR{w, False{}, sa}, c1}}, ST.rid(t), RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1))) == True{} : Bool}, {ST.rep(~K, t, p, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1))) == True{} : Bool}, P.ok_r(~K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), Con{P.FR{w, False{}, sa}, c1}, p, sb, t, Pair.snd({P.ctxok(~K, Con{P.FR{w, False{}, sa}, c1}, p, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1))) == True{} : Bool}, {ST.rep(~K, ST.TN{p, sb, t}, w, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1))) == True{} : Bool}, P.ok_r(~K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), c1, w, sa, ST.TN{p, sb, t}, RP.rotr_path_rep(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), c1, p, sa, w, sb, t, hr2, hok2, hnd), RP.rotr_path_ctx(~K, ~cmp, ~o, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), c1, p, sa, w, sb, t, hr2, hok2, hnd))), Pair.fst({P.ctxok(~K, Con{P.FR{w, False{}, sa}, c1}, p, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1))) == True{} : Bool}, {ST.rep(~K, ST.TN{p, sb, t}, w, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1))) == True{} : Bool}, P.ok_r(~K, RM.rotr_nl(K, SE.setc(K, SE.setc(K, nl, w, False{}), p, True{}), p, w, ST.rid(sb), P.top(c1), SP.dir(c1)), c1, w, sa, ST.TN{p, sb, t}, RP 271 272 def dside_r(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, 273 +hk = L.and_left(P.cok1(~K, P.FR{p, False{}, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2) 274 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, p)), ST.rid(s), NB.child_eq(~K, ST.nd(K, nl, p), ST.rid(s), ST.rid(t), P.top(c1), False{}, L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, ST.rid(t), ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl)), hk)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_red_sibling_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, p, _, M.node_red(~K, ST.nd(K, nl, _)))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 275 dred_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, M.node_red(~K, ST.nd(K, nl, ST.rid(s))), {==}) 276 277 # ---- a step, and the loop ---- 278 279 280 # x and its sibling with the same id: both empty, so x may as well be on the left 281 def dsame(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, fr 282 match s t: 283 case ST.TE{} ST.TE{}: 284 +ew0 = Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, False{}, ST.TE{}}, c1}))), SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TE{}, ST.TE{}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, True{}, ST.TE{}}, c1}))), Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(c1), SC.append(Nat, ST.ids(ST.TN{p, ST.TE{}, ST.TE{}}), P.after(c1))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, False{}, ST.TE{}}, c1}))), P.ids_r(c1, p, ST.TE{}, ST.TE{})), P.ids_l(c1, p, ST.TE{}, ST.TE{})) 285 dside_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, ST.TE{}, ST.TE{}, i1, i2, L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, False{}, ST.TE{}}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, True{}, ST.TE{}}, c1}))), ew0, i3), Equal.trans(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, True{}, ST.TE{}}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, False{}, ST.TE{}}, c1}))), i0, Equal.sym(List<&2, Nat>, SC.append(Nat, P.before(Con{P.FR{p, False{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, False{}, ST.TE{}}, c1}))), SC.append(Nat, P.before(Con{P.FR{p, True{}, ST.TE{}}, c1}), SC.append(Nat, ST.ids(ST.TE{}), P.after(Con{P.FR{p, True{}, ST.TE{}}, c1}))), ew0), i4), i5, h4, h5, h6, h7, kont) 286 case ST.TN{+j, +sa, +sb} ST.TE{}: 287 +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, 0n, ST.rid(ST.TN{j, sa, sb})), ST.pk(Nat, False{}, ST.rid(ST.TN{j, sa, sb}), 0n), P.top(c1)), ST.rep(~K, ST.TN{j, sa, sb}, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, 0n, ST.rid(ST.TN{j, sa, sb})), ST.pk(Nat, False{}, ST.rid(ST.TN{j, sa, sb}), 0n), P.top(c1)), ST.rep(~K, ST.TN{j, sa, sb}, p, nl)), L.and_left(P.cok1(~K, P.FR{p, False{}, ST.TN{j, sa, sb}}, 0n, P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2))) 288 +hj = L.and_left(Nat.is_lt(0n, j), Bool.and(ST.is_node(K, ST.nd(K, nl, j), ST.rid(sa), ST.rid(sb), p), Bool.and(ST.rep(~K, sa, j, nl), ST.rep(~K, sb, j, nl))), hs) 289 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_side(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, 0n, p, ST.nd(K, nl, p), True{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(L.subst(Nat, z => {Nat.is_lt(0n, z) == True{} : Bool}, j, 0n, Equal.sym(Nat, 0n, j, N.eq_from_is_eq(0n, j, he)), hj))) 290 case ST.TE{} ST.TN{+i, +ta, +tb}: 291 +hpi = L.and_left(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(ta), ST.rid(tb), p), Bool.and(ST.rep(~K, ta, i, nl), ST.rep(~K, tb, i, nl))), i1) 292 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_side(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, i, p, ST.nd(K, nl, p), True{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(L.subst(Nat, z => {Nat.is_lt(0n, z) == True{} : Bool}, i, 0n, N.eq_from_is_eq(i, 0n, he), hpi))) 293 case ST.TN{+j, +sa, +sb} ST.TN{+i, +ta, +tb}: 294 +mb = DJ.mem_r(j, P.before(c1), SC.append(Nat, ST.ids(ST.TN{j, sa, sb}), Con{p, Nil{}}), DJ.mem_l(j, ST.ids(ST.TN{j, sa, sb}), Con{p, Nil{}}, P.mem_root(j, sa, sb))) 295 +dj = DJ.dj_r(P.before(Con{P.FR{p, False{}, ST.TN{j, sa, sb}}, c1}), SC.append(Nat, ST.ids(ST.TN{i, ta, tb}), P.after(c1)), i3, j, mb) 296 +mt = L.subst(Nat, z => {NL.memn(z, SC.append(Nat, ST.ids(ST.TN{i, ta, tb}), P.after(c1))) == True{} : Bool}, i, j, N.eq_from_is_eq(i, j, he), DJ.mem_l(i, ST.ids(ST.TN{i, ta, tb}), P.after(c1), P.mem_root(i, ta, tb))) 297 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_side(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, i, p, ST.nd(K, nl, p), True{})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(Equal.trans(Bool, False{}, NL.memn(j, SC.append(Nat, ST.ids(ST.TN{i, ta, tb}), P.after(c1))), True{}, Equal.sym(Bool, NL.memn(j, SC.append(Nat, ST.ids(ST.TN{i, ta, tb}), P.after(c1))), False{}, dj), mt))) 298 299 # x on the right: its id against the sibling's 300 def dsd(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, False{}, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, False{}, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, False{}, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, False{}, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, False{}, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free 301 match e: 302 case False{}: 303 dside_r(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 304 case True{}: 305 dsame(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, he) 306 307 # the side x hangs on 308 def dlft(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c1: List<&2, P.Fr>, +p: Nat, +lft: Bool, +s: ST.Tr, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(Con{P.FR{p, lft, s}, c1}), nl) == True{} : Bool}, +i2: {P.ctxok(~K, Con{P.FR{p, lft, s}, c1}, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{p, lft, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, lft, s}, c1})))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(Con{P.FR{p, lft, s}, c1}), SC.append(Nat, ST.ids(t), P.after(Con{P.FR{p, lft, s}, c1}))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(Con{P.FR{p, lft, s}, c1}, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l, d, kn_, pl 309 match lft: 310 case True{}: 311 %Equal.sym(Bool, Nat.is_eq(ST.rid(t), ST.rid(t)), True{}, N.is_eq_refl(ST.rid(t))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_side(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), p, ST.nd(K, nl, p), _)) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 312 dside_l(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 313 case False{}: 314 dsd(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, Nat.is_eq(ST.rid(t), ST.rid(s)), {==}) 315 316 317 # not stopping: x is not the root, so it has a parent 318 def dside(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +i2: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(c, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l, d, kn_, pl, tg, fl}, M.DF{ST.rid(kt_), P.top(kc_), True{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Na 319 match c: 320 case Nil{}: 321 +e1 = L.subst(Nat, z => {Nat.is_eq(ST.rid(t), z) == True{} : Bool}, ST.rid(t), root, Equal.sym(Nat, root, ST.rid(t), i5), N.is_eq_refl(ST.rid(t))) 322 Empty.absurd(Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_side(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), 0n, ST.nd(K, nl, 0n), Nat.is_eq(ST.rid(t), M.node_left(~K, ST.nd(K, nl, 0n))))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>, L.false_true(Equal.trans(Bool, False{}, Bool.or(Nat.is_eq(ST.rid(t), root), M.node_red(~K, ST.nd(K, nl, ST.rid(t)))), True{}, Equal.sym(Bool, Bool.or(Nat.is_eq(ST.rid(t), root), M.node_red(~K, ST.nd(K, nl, ST.rid(t)))), False{}, hb), FX.or_lt(Nat.is_eq(ST.rid(t), root), M.node_red(~K, ST.nd(K, nl, ST.rid(t))), e1)))) 323 case Con{P.FR{+p, +lft, +s}, +c1}: 324 +hk = L.and_left(P.cok1(~K, P.FR{p, lft, s}, ST.rid(t), P.top(c1), nl), P.ctxok(~K, c1, p, nl), i2) 325 %Equal.sym(Nat, M.node_left(~K, ST.nd(K, nl, p)), ST.pk(Nat, lft, ST.rid(t), ST.rid(s)), NB.child_eq(~K, ST.nd(K, nl, p), ST.pk(Nat, lft, ST.rid(t), ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), ST.rid(t)), P.top(c1), False{}, L.and_left(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, ST.rid(t), ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl), L.and_right(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, ST.rid(t), ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), ST.rid(t)), P.top(c1)), ST.rep(~K, s, p, nl)), hk)))) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, MI.delete_side(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), p, ST.nd(K, nl, p), Nat.is_eq(ST.rid(t), _))) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 326 dlft(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c1, p, lft, s, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont) 327 328 # stopping: x goes black, and the loop blackens the root 329 def dstop2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +i2: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(c, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l, d, kn_, pl, tg, fl}, M.DF{ST.rid(kt_), P.top(kc_), True{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : N 330 match b: 331 case True{}: 332 %Equal.sym(ST.Sh, MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ST.rid(t), False{}), ST.SH{n, root, lo, hi, free, l, d, SE.setc(K, nl, ST.rid(t), False{}), pl, tg, fl}, SE.set_red_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, ST.rid(t), False{})) : Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (_, M.DF{0n, 0n, False{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>> 333 dstop(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, SE.setc(K, nl, ST.rid(t), False{}), PG.plug(c, t), PG.rep_plug(~K, SE.setc(K, nl, ST.rid(t), False{}), c, t, Equal.trans(Bool, ST.rep(~K, t, P.top(c), SE.setc(K, nl, ST.rid(t), False{})), ST.rep(~K, t, P.top(c), nl), True{}, SE.rep_setc(~K, t, P.top(c), nl, ST.rid(t), False{}), i1), Equal.trans(Bool, P.ctxok(~K, c, ST.rid(t), SE.setc(K, nl, ST.rid(t), False{})), P.ctxok(~K, c, ST.rid(t), nl), True{}, SE.ctx_setc(~K, c, ST.rid(t), nl, ST.rid(t), False{}), i2)), i5, Equal.trans(List<&2, Nat>, ST.ids(PG.plug(c, t)), SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))), i0, PG.ids_plug(c, t), i4), Equal.trans(List<&2, M.Entry>, ST.ents(~K, ~V, i0, SE.setc(K, nl, ST.rid(t), False{}), pl), ST.ents(~K, ~V, i0, nl, pl), e0, SE.ents_setc(~K, ~V, i0, nl, pl, ST.rid(t), False{}), h4), Equal.trans(Bool, EN.oks(~K, ~V, i0, SE.setc(K, nl, ST.rid(t), False{}), pl), EN.oks(~K, ~V, i0, nl, pl), True{}, SE.oks_setc(~K, ~V, i0, nl, pl, ST.rid(t), False{}), h5), Equal.trans(Bool, ST.fll(~K, SE.setc(K, nl, ST.rid(t), False{}), fx), ST.fll(~K, nl, fx), True{}, SE.fll_setc(~K, fx, nl, ST.rid(t), False{}), h6), Equal.trans(Nat, SC.length(M.Node, SE.setc(K, nl, ST.rid(t), False{})), SC.length(M.Node, nl), l0, SE.setc_len(K, nl, ST.rid(t), False{}), h7)) 334 case False{}: 335 dside(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, hb) 336 337 def dstep(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +i2: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(c, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, kont: @+kr_: Nat -> @+kn_: List<&2, M.Node> -> @+kc_: List<&2, P.Fr> -> @+kt_: ST.Tr -> @+ki1: {ST.rep(~K, kt_, P.top(kc_), kn_) == True{} : Bool} -> @+ki2: {P.ctxok(~K, kc_, ST.rid(kt_), kn_) == True{} : Bool} -> @+ki3: {NL.nodupn(SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_)))) == True{} : Bool} -> @+ki4: {SC.append(Nat, P.before(kc_), SC.append(Nat, ST.ids(kt_), P.after(kc_))) == i0 : List<&2, Nat>} -> @+ki5: {kr_ == ST.rid(PG.plug(kc_, kt_)) : Nat} -> @+kh4: {ST.ents(~K, ~V, i0, kn_, pl) == e0 : List<&2, M.Entry>} -> @+kh5: {EN.oks(~K, ~V, i0, kn_, pl) == True{} : Bool} -> @+kh6: {ST.fll(~K, kn_, fx) == True{} : Bool} -> @+kh7: {SC.length(M.Node, kn_) == l0 : Nat} -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, kr_, lo, hi, free, l, d, kn_, pl, tg, fl}, M.DF{ST.rid(kt_), P.top(kc_), True{}})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Na 338 dstop2(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, gf, root, nl, c, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kont, Bool.or(Nat.is_eq(ST.rid(t), root), M.node_red(~K, ST.nd(K, nl, ST.rid(t)))), {==}) 339 340 # from the position x under its parent, the loop ends with the ghost tree's 341 # properties, whatever its fuel and flag 342 def dloop(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +n: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +fx: List<&2, Nat>, +i0: List<&2, Nat>, +e0: List<&2, M.Entry>, +l0: Nat, +gf: Nat, +root: Nat, +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +t: ST.Tr, +i1: {ST.rep(~K, t, P.top(c), nl) == True{} : Bool}, +i2: {P.ctxok(~K, c, ST.rid(t), nl) == True{} : Bool}, +i3: {NL.nodupn(SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c)))) == True{} : Bool}, +i4: {SC.append(Nat, P.before(c), SC.append(Nat, ST.ids(t), P.after(c))) == i0 : List<&2, Nat>}, +i5: {root == ST.rid(PG.plug(c, t)) : Nat}, +h4: {ST.ents(~K, ~V, i0, nl, pl) == e0 : List<&2, M.Entry>}, +h5: {EN.oks(~K, ~V, i0, nl, pl) == True{} : Bool}, +h6: {ST.fll(~K, nl, fx) == True{} : Bool}, +h7: {SC.length(M.Node, nl) == l0 : Nat}, +b: Bool) -> Sigma<&1, &1, Nat, fr_ => Sigma<&1, &1, List<&2, M.Node>, fn_ => Sigma<&1, &1, ST.Tr, ft_ => {MI.delete_fix_loop(~K, ~V, ~cmp, gf, (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, M.DF{ST.rid(t), P.top(c), b})) == ST.SH{n, fr_, lo, hi, free, l, d, fn_, pl, tg, fl} : ST.Sh} & {ST.rep(~K, ft_, 0n, fn_) == True{} : Bool} & ({fr_ == ST.rid(ft_) : Nat} & ({ST.ids(ft_) == i0 : List<&2, Nat>} & ({ST.root_black(~K, ft_, fn_) == True{} : Bool} & {ST.ents(~K, ~V, i0, fn_, pl) == e0 : List<&2, M.Entry>} & ({EN.oks(~K, ~V, i0, fn_, pl) == True{} : Bool} & ({ST.fll(~K, fn_, fx) == True{} : Bool} & {SC.length(M.Node, fn_) == l0 : Nat})))))>>>: 343 match gf b: 344 case 0n +b: 345 dfin(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, root, nl, c, t, i1, i2, i3, i4, i5, h4, h5, h6, h7) 346 case 1n+g False{}: 347 dfin(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, root, nl, c, t, i1, i2, i3, i4, i5, h4, h5, h6, h7) 348 case 1n+g True{}: 349 dstep(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, g, root, nl, c, t, i1, i2, i3, i4, i5, h4, h5, h6, h7, kr_ => kn_ => kc_ => kt_ => ki1 => ki2 => ki3 => ki4 => ki5 => kh4 => kh5 => kh6 => kh7 => dloop(~K, ~V, ~cmp, ~o, n, lo, hi, free, l, d, pl, tg, fl, fx, i0, e0, l0, g, kr_, kn_, kc_, kt_, ki1, ki2, ki3, ki4, ki5, kh4, kh5, kh6, kh7, True{}))