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 ../../lib/list.bend as LL 8 import ./state.bend as ST 9 import ./tree.bend as TR 10 import ./path.bend as P 11 import ./agree.bend as AG 12 import ./rotm.bend as RM 13 import ./rotn.bend as RN 14 import ./dj.bend as DJ 15 import ./spath.bend as SP 16 import ../../lib/nat_list.bend as NL 17 18 # Rotations along a path: rotating the subtree the path leads to (a node x 19 # with a child y) gives the rotated subtree, linked as the ghost says below 20 # the path's parent, and the path still leads to it (now rooted at y). 21 # (source: tools/generators/tm_hand/rot.src) 22 23 24 # ---- ids are positive ---- 25 26 def ne0(+x: Nat, +h: {Nat.is_lt(0n, x) == True{} : Bool}) -> {Nat.is_eq(0n, x) == False{} : Bool}: 27 match x: 28 case 0n: 29 Empty.absurd({Nat.is_eq(0n, 0n) == False{} : Bool}, L.false_true(h)) 30 case 1n+j: 31 {==} 32 33 def zero_ids(~K: Data, +nl: List<&2, M.Node>, +t: ST.Tr, +p: Nat, +hr: {ST.rep(~K, t, p, nl) == True{} : Bool}) -> {NL.memn(0n, ST.ids(t)) == False{} : Bool}: 34 match t: 35 case ST.TE{}: 36 {==} 37 case ST.TN{+i, +l, +r}: 38 DJ.nm_app(0n, ST.ids(l), Con{i, ST.ids(r)}, zero_ids(~K, nl, l, i, TR.rep_l(~K, i, l, r, p, nl, hr)), DJ.nm_cons(0n, i, ST.ids(r), N.is_eq_sym_false(0n, i, ne0(i, L.and_left(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl))), hr))), zero_ids(~K, nl, r, i, TR.rep_r(~K, i, l, r, p, nl, hr)))) 39 40 41 def zero_ctx(~K: Data, +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +x: Nat, +hc: {P.ctxok(~K, c, x, nl) == True{} : Bool}) -> {NL.memn(0n, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}: 42 match c: 43 case Nil{}: 44 {==} 45 case Con{P.FR{+p, True{}, +s}, +u}: 46 +hk = L.and_left(P.cok1(~K, P.FR{p, True{}, s}, x, P.top(u), nl), P.ctxok(~K, u, p, nl), hc) 47 +h0 = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, x, ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), x), P.top(u)), ST.rep(~K, s, p, nl)), hk) 48 +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, True{}, x, ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), x), P.top(u)), 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{}, x, ST.rid(s)), ST.pk(Nat, True{}, ST.rid(s), x), P.top(u)), ST.rep(~K, s, p, nl)), hk)) 49 +hu = zero_ctx(~K, nl, u, p, L.and_right(P.cok1(~K, P.FR{p, True{}, s}, x, P.top(u), nl), P.ctxok(~K, u, p, nl), hc)) 50 +zs = zero_ids(~K, nl, s, p, hs) 51 +zp = N.is_eq_sym_false(0n, p, ne0(p, h0)) 52 DJ.nm_app(0n, P.before(u), Con{p, SC.append(Nat, ST.ids(s), P.after(u))}, DJ.nm_l(0n, P.before(u), P.after(u), hu), DJ.nm_cons(0n, p, SC.append(Nat, ST.ids(s), P.after(u)), zp, DJ.nm_app(0n, ST.ids(s), P.after(u), zs, DJ.nm_r(0n, P.before(u), P.after(u), hu)))) 53 case Con{P.FR{+p, False{}, +s}, +u}: 54 +hk = L.and_left(P.cok1(~K, P.FR{p, False{}, s}, x, P.top(u), nl), P.ctxok(~K, u, p, nl), hc) 55 +h0 = L.and_left(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, x, ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), x), P.top(u)), ST.rep(~K, s, p, nl)), hk) 56 +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, False{}, x, ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), x), P.top(u)), 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{}, x, ST.rid(s)), ST.pk(Nat, False{}, ST.rid(s), x), P.top(u)), ST.rep(~K, s, p, nl)), hk)) 57 +hu = zero_ctx(~K, nl, u, p, L.and_right(P.cok1(~K, P.FR{p, False{}, s}, x, P.top(u), nl), P.ctxok(~K, u, p, nl), hc)) 58 +zs = zero_ids(~K, nl, s, p, hs) 59 +zp = N.is_eq_sym_false(0n, p, ne0(p, h0)) 60 DJ.nm_app(0n, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{p, Nil{}})), P.after(u), DJ.nm_app(0n, P.before(u), SC.append(Nat, ST.ids(s), Con{p, Nil{}}), DJ.nm_l(0n, P.before(u), P.after(u), hu), DJ.nm_app(0n, ST.ids(s), Con{p, Nil{}}, zs, DJ.nm_cons(0n, p, Nil{}, zp, {==}))), DJ.nm_r(0n, P.before(u), P.after(u), hu)) 61 62 # ---- lists around a frame ---- 63 64 65 def nd_drop(+b: List<&2, Nat>, +s: List<&2, Nat>, +a: List<&2, Nat>, +h: {NL.nodupn(SC.append(Nat, b, SC.append(Nat, s, a))) == True{} : Bool}) -> {NL.nodupn(SC.append(Nat, b, a)) == True{} : Bool}: 66 match s: 67 case Nil{}: 68 h 69 case Con{+z, +t}: 70 +e = NL.nd_mid(b, z, SC.append(Nat, t, a)) 71 nd_drop(b, t, a, L.and_left(NL.nodupn(SC.append(Nat, b, SC.append(Nat, t, a))), Bool.not(NL.memn(z, SC.append(Nat, b, SC.append(Nat, t, a)))), L.subst(Bool, w => {w == True{} : Bool}, NL.nodupn(SC.append(Nat, b, Con{z, SC.append(Nat, t, a)})), Bool.and(NL.nodupn(SC.append(Nat, b, SC.append(Nat, t, a))), Bool.not(NL.memn(z, SC.append(Nat, b, SC.append(Nat, t, a))))), e, h))) 72 73 def nd_mid_nm(+b: List<&2, Nat>, +z: Nat, +a: List<&2, Nat>, +h: {NL.nodupn(SC.append(Nat, b, Con{z, a})) == True{} : Bool}) -> {NL.memn(z, SC.append(Nat, b, a)) == False{} : Bool}: 74 NL.not_t_f(NL.memn(z, SC.append(Nat, b, a)), L.and_right(NL.nodupn(SC.append(Nat, b, a)), Bool.not(NL.memn(z, SC.append(Nat, b, a))), L.subst(Bool, w => {w == True{} : Bool}, NL.nodupn(SC.append(Nat, b, Con{z, a})), Bool.and(NL.nodupn(SC.append(Nat, b, a)), Bool.not(NL.memn(z, SC.append(Nat, b, a)))), NL.nd_mid(b, z, a), h))) 75 76 77 78 # the parent of a frame is neither in the sibling nor in the frames above 79 def fq_s(+q: Nat, +lft: Bool, +s: ST.Tr, +u: List<&2, P.Fr>, +h: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{q, lft, s}, u}), P.after(Con{P.FR{q, lft, s}, u}))) == True{} : Bool}) -> {NL.memn(q, ST.ids(s)) == False{} : Bool} & {NL.memn(q, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}: 80 match lft: 81 case True{}: 82 +hm = nd_mid_nm(P.before(u), q, SC.append(Nat, ST.ids(s), P.after(u)), h) 83 +hr = DJ.nm_r(q, P.before(u), SC.append(Nat, ST.ids(s), P.after(u)), hm) 84 (DJ.nm_l(q, ST.ids(s), P.after(u), hr), DJ.nm_app(q, P.before(u), P.after(u), DJ.nm_l(q, P.before(u), SC.append(Nat, ST.ids(s), P.after(u)), hm), DJ.nm_r(q, ST.ids(s), P.after(u), hr))) 85 case False{}: 86 +e1 = LL.append_assoc(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{q, Nil{}}), P.after(u)) 87 +e2 = LL.append_assoc(Nat, ST.ids(s), Con{q, Nil{}}, P.after(u)) 88 +e3 = LL.append_assoc(Nat, P.before(u), ST.ids(s), Con{q, P.after(u)}) 89 +h1 = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{q, Nil{}})), P.after(u)), SC.append(Nat, P.before(u), SC.append(Nat, SC.append(Nat, ST.ids(s), Con{q, Nil{}}), P.after(u))), e1, h) 90 +h2 = L.subst(List<&2, Nat>, z => {NL.nodupn(SC.append(Nat, P.before(u), z)) == True{} : Bool}, SC.append(Nat, SC.append(Nat, ST.ids(s), Con{q, Nil{}}), P.after(u)), SC.append(Nat, ST.ids(s), Con{q, P.after(u)}), e2, h1) 91 +h3 = L.subst(List<&2, Nat>, z => {NL.nodupn(z) == True{} : Bool}, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{q, P.after(u)})), SC.append(Nat, SC.append(Nat, P.before(u), ST.ids(s)), Con{q, P.after(u)}), Equal.sym(List<&2, Nat>, SC.append(Nat, SC.append(Nat, P.before(u), ST.ids(s)), Con{q, P.after(u)}), SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{q, P.after(u)})), e3), h2) 92 +hm = nd_mid_nm(SC.append(Nat, P.before(u), ST.ids(s)), q, P.after(u), h3) 93 +hl = DJ.nm_l(q, SC.append(Nat, P.before(u), ST.ids(s)), P.after(u), hm) 94 (DJ.nm_r(q, P.before(u), ST.ids(s), hl), DJ.nm_app(q, P.before(u), P.after(u), DJ.nm_l(q, P.before(u), ST.ids(s), hl), DJ.nm_r(q, SC.append(Nat, P.before(u), ST.ids(s)), P.after(u), hm))) 95 96 # an id absent from a frame's lists is absent from its sibling and above 97 def fw_s(+w: Nat, +q: Nat, +lft: Bool, +s: ST.Tr, +u: List<&2, P.Fr>, +h: {NL.memn(w, SC.append(Nat, P.before(Con{P.FR{q, lft, s}, u}), P.after(Con{P.FR{q, lft, s}, u}))) == False{} : Bool}) -> {NL.memn(w, ST.ids(s)) == False{} : Bool} & {NL.memn(w, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}: 98 match lft: 99 case True{}: 100 +h2 = DJ.nm_ct(w, q, SC.append(Nat, ST.ids(s), P.after(u)), DJ.nm_r(w, P.before(u), Con{q, SC.append(Nat, ST.ids(s), P.after(u))}, h)) 101 (DJ.nm_l(w, ST.ids(s), P.after(u), h2), DJ.nm_app(w, P.before(u), P.after(u), DJ.nm_l(w, P.before(u), Con{q, SC.append(Nat, ST.ids(s), P.after(u))}, h), DJ.nm_r(w, ST.ids(s), P.after(u), h2))) 102 case False{}: 103 +h1 = DJ.nm_l(w, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{q, Nil{}})), P.after(u), h) 104 (DJ.nm_l(w, ST.ids(s), Con{q, Nil{}}, DJ.nm_r(w, P.before(u), SC.append(Nat, ST.ids(s), Con{q, Nil{}}), h1)), DJ.nm_app(w, P.before(u), P.after(u), DJ.nm_l(w, P.before(u), SC.append(Nat, ST.ids(s), Con{q, Nil{}}), h1), DJ.nm_r(w, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{q, Nil{}})), P.after(u), h))) 105 106 # ---- the left rotation: the rotated subtree ---- 107 108 def rep_intro(~K: Data, +nl: List<&2, M.Node>, +i: Nat, +l: ST.Tr, +r: ST.Tr, +p: Nat, +h0: {Nat.is_lt(0n, i) == True{} : Bool}, +hn: {ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p) == True{} : Bool}, +hl: {ST.rep(~K, l, i, nl) == True{} : Bool}, +hr: {ST.rep(~K, r, i, nl) == True{} : Bool}) -> {ST.rep(~K, ST.TN{i, l, r}, p, nl) == True{} : Bool}: 109 L.and_intro(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl))), h0, L.and_intro(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), Bool.and(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl)), hn, L.and_intro(ST.rep(~K, l, i, nl), ST.rep(~K, r, i, nl), hl, hr))) 110 111 def rep_moved(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +t: ST.Tr, +p: Nat, +nl: List<&2, M.Node>, +nl2: List<&2, M.Node>, +ha: {AG.agr(~K, ~cmp, ST.ids(t), nl, nl2) == True{} : Bool}, +h: {ST.rep(~K, t, p, nl) == True{} : Bool}) -> {ST.rep(~K, t, p, nl2) == True{} : Bool}: 112 Equal.trans(Bool, ST.rep(~K, t, p, nl2), ST.rep(~K, t, p, nl), True{}, AG.rep_agr(~K, ~cmp, ~o, t, p, nl, nl2, ha), h) 113 114 115 def rotl_rep(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +x: Nat, +ta: ST.Tr, +y: Nat, +tb: ST.Tr, +tc: ST.Tr, +q: Nat, +dir: Bool, +h0x: {Nat.is_lt(0n, x) == True{} : Bool}, +h0y: {Nat.is_lt(0n, y) == True{} : Bool}, +hxn: {ST.is_node(K, ST.nd(K, nl, x), ST.rid(ta), y, q) == True{} : Bool}, +hyn: {ST.is_node(K, ST.nd(K, nl, y), ST.rid(tb), ST.rid(tc), x) == True{} : Bool}, +hA: {ST.rep(~K, ta, x, nl) == True{} : Bool}, +hB: {ST.rep(~K, tb, y, nl) == True{} : Bool}, +hC: {ST.rep(~K, tc, y, nl) == True{} : Bool}, +hS: {NL.nodupn(SC.append(Nat, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})})) == True{} : Bool}, +hqS: {NL.memn(q, SC.append(Nat, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})})) == False{} : Bool}) -> {ST.rep(~K, ST.TN{y, ST.TN{x, ta, tb}, tc}, q, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir)) == True{} : Bool}: 116 match tb: 117 case ST.TE{}: 118 +hR = DJ.ndr(ST.ids(ta), Con{x, SC.append(Nat, Nil{}, Con{y, ST.ids(tc)})}, hS) 119 +xR1 = DJ.nd_head(x, Con{y, ST.ids(tc)}, hR) 120 +nyx = DJ.nm_ch(x, y, ST.ids(tc), xR1) 121 +xIA = DJ.dj_l(ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}, hS, x, DJ.mem_hd(x, Con{y, ST.ids(tc)})) 122 +yIA = DJ.dj_l(ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}, hS, y, DJ.mem_tl(y, x, Con{y, ST.ids(tc)}, DJ.mem_hd(y, ST.ids(tc)))) 123 +xIC = DJ.nm_ct(x, y, ST.ids(tc), xR1) 124 +yIC = DJ.nd_head(y, ST.ids(tc), DJ.nd_tail(x, Con{y, ST.ids(tc)}, hR)) 125 +mx = DJ.mem_r(x, ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}, DJ.mem_hd(x, Con{y, ST.ids(tc)})) 126 +my = DJ.mem_r(y, ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}, DJ.mem_tl(y, x, Con{y, ST.ids(tc)}, DJ.mem_hd(y, ST.ids(tc)))) 127 +nqx = DJ.ne_nm(q, x, SC.append(Nat, ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}), hqS, mx) 128 +nqy = DJ.ne_nm(q, y, SC.append(Nat, ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}), hqS, my) 129 +qIA = DJ.nm_l(q, ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}, hqS) 130 +qIC = DJ.nm_ct(q, y, ST.ids(tc), DJ.nm_ct(q, x, Con{y, ST.ids(tc)}, DJ.nm_r(q, ST.ids(ta), Con{x, Con{y, ST.ids(tc)}}, hqS))) 131 +agA = RN.rotl_agr(~K, ~cmp, ~o, ST.ids(ta), nl, x, y, 0n, q, dir, xIA, yIA, zero_ids(~K, nl, ta, x, hA), qIA) 132 +agC = RN.rotl_agr(~K, ~cmp, ~o, ST.ids(tc), nl, x, y, 0n, q, dir, xIC, yIC, zero_ids(~K, nl, tc, y, hC), qIC) 133 +rx = RN.rotl_x(K, nl, x, y, 0n, q, dir, ST.rid(ta), hxn, nyx, nqx, ne0(x, h0x)) 134 +ry = RN.rotl_y(K, nl, x, y, 0n, q, dir, ST.rid(tc), hyn, N.is_eq_sym_false(y, x, nyx), nqy, ne0(y, h0y)) 135 rep_intro(~K, RM.rotl_nl(K, nl, x, y, 0n, q, dir), y, ST.TN{x, ta, ST.TE{}}, tc, q, h0y, ry, rep_intro(~K, RM.rotl_nl(K, nl, x, y, 0n, q, dir), x, ta, ST.TE{}, y, h0x, rx, rep_moved(~K, ~cmp, ~o, ta, x, nl, RM.rotl_nl(K, nl, x, y, 0n, q, dir), agA, hA), {==}), rep_moved(~K, ~cmp, ~o, tc, y, nl, RM.rotl_nl(K, nl, x, y, 0n, q, dir), agC, hC)) 136 case ST.TN{+b, +b1, +b2}: 137 +hR = DJ.ndr(ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, hS) 138 +hR1 = DJ.nd_tail(x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), hR) 139 +xR1 = DJ.nd_head(x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), hR) 140 +myR1 = DJ.mem_r(y, ST.ids(tb), Con{y, ST.ids(tc)}, DJ.mem_hd(y, ST.ids(tc))) 141 +mbIB = DJ.mem_r(b, ST.ids(b1), Con{b, ST.ids(b2)}, DJ.mem_hd(b, ST.ids(b2))) 142 +mbR1 = DJ.mem_l(b, ST.ids(tb), Con{y, ST.ids(tc)}, mbIB) 143 +mx = DJ.mem_r(x, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, DJ.mem_hd(x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}))) 144 +my = DJ.mem_r(y, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, DJ.mem_tl(y, x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), myR1)) 145 +mb = DJ.mem_r(b, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, DJ.mem_tl(b, x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), mbR1)) 146 +xIA = DJ.dj_l(ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, hS, x, DJ.mem_hd(x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}))) 147 +yIA = DJ.dj_l(ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, hS, y, DJ.mem_tl(y, x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), myR1)) 148 +bIA = DJ.dj_l(ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, hS, b, DJ.mem_tl(b, x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), mbR1)) 149 +xIB = DJ.nm_l(x, ST.ids(tb), Con{y, ST.ids(tc)}, xR1) 150 +xyc = DJ.nm_r(x, ST.ids(tb), Con{y, ST.ids(tc)}, xR1) 151 +nyx = DJ.nm_ch(x, y, ST.ids(tc), xyc) 152 +xIC = DJ.nm_ct(x, y, ST.ids(tc), xyc) 153 +yIB = DJ.dj_l(ST.ids(tb), Con{y, ST.ids(tc)}, hR1, y, DJ.mem_hd(y, ST.ids(tc))) 154 +yIC = DJ.nd_head(y, ST.ids(tc), DJ.ndr(ST.ids(tb), Con{y, ST.ids(tc)}, hR1)) 155 +nxb = DJ.ne_nm(x, b, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), xR1, mbR1) 156 +byc = DJ.dj_r(ST.ids(tb), Con{y, ST.ids(tc)}, hR1, b, mbIB) 157 +nyb = DJ.nm_ch(b, y, ST.ids(tc), byc) 158 +bIC = DJ.nm_ct(b, y, ST.ids(tc), byc) 159 +nqx = DJ.ne_nm(q, x, SC.append(Nat, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}), hqS, mx) 160 +nqy = DJ.ne_nm(q, y, SC.append(Nat, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}), hqS, my) 161 +nqb = DJ.ne_nm(q, b, SC.append(Nat, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}), hqS, mb) 162 +qIA = DJ.nm_l(q, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, hqS) 163 +qR1 = DJ.nm_ct(q, x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)}), DJ.nm_r(q, ST.ids(ta), Con{x, SC.append(Nat, ST.ids(tb), Con{y, ST.ids(tc)})}, hqS)) 164 +qIB = DJ.nm_l(q, ST.ids(tb), Con{y, ST.ids(tc)}, qR1) 165 +qIC = DJ.nm_ct(q, y, ST.ids(tc), DJ.nm_r(q, ST.ids(tb), Con{y, ST.ids(tc)}, qR1)) 166 +hIB = DJ.ndl(ST.ids(tb), Con{y, ST.ids(tc)}, hR1) 167 +bB1 = DJ.dj_l(ST.ids(b1), Con{b, ST.ids(b2)}, hIB, b, DJ.mem_hd(b, ST.ids(b2))) 168 +bB2 = DJ.nd_head(b, ST.ids(b2), DJ.ndr(ST.ids(b1), Con{b, ST.ids(b2)}, hIB)) 169 +xB1 = DJ.nm_l(x, ST.ids(b1), Con{b, ST.ids(b2)}, xIB) 170 +xB2 = DJ.nm_ct(x, b, ST.ids(b2), DJ.nm_r(x, ST.ids(b1), Con{b, ST.ids(b2)}, xIB)) 171 +yB1 = DJ.nm_l(y, ST.ids(b1), Con{b, ST.ids(b2)}, yIB) 172 +yB2 = DJ.nm_ct(y, b, ST.ids(b2), DJ.nm_r(y, ST.ids(b1), Con{b, ST.ids(b2)}, yIB)) 173 +qB1 = DJ.nm_l(q, ST.ids(b1), Con{b, ST.ids(b2)}, qIB) 174 +qB2 = DJ.nm_ct(q, b, ST.ids(b2), DJ.nm_r(q, ST.ids(b1), Con{b, ST.ids(b2)}, qIB)) 175 +agA = RN.rotl_agr(~K, ~cmp, ~o, ST.ids(ta), nl, x, y, b, q, dir, xIA, yIA, bIA, qIA) 176 +agC = RN.rotl_agr(~K, ~cmp, ~o, ST.ids(tc), nl, x, y, b, q, dir, xIC, yIC, bIC, qIC) 177 +agB1 = RN.rotl_agr(~K, ~cmp, ~o, ST.ids(b1), nl, x, y, b, q, dir, xB1, yB1, bB1, qB1) 178 +agB2 = RN.rotl_agr(~K, ~cmp, ~o, ST.ids(b2), nl, x, y, b, q, dir, xB2, yB2, bB2, qB2) 179 +h0b = L.and_left(Nat.is_lt(0n, b), Bool.and(ST.is_node(K, ST.nd(K, nl, b), ST.rid(b1), ST.rid(b2), y), Bool.and(ST.rep(~K, b1, b, nl), ST.rep(~K, b2, b, nl))), hB) 180 +rx = RN.rotl_x(K, nl, x, y, b, q, dir, ST.rid(ta), hxn, nyx, nqx, N.is_eq_sym_false(x, b, nxb)) 181 +ry = RN.rotl_y(K, nl, x, y, b, q, dir, ST.rid(tc), hyn, N.is_eq_sym_false(y, x, nyx), nqy, N.is_eq_sym_false(y, b, nyb)) 182 +rb = RN.rotl_b(K, nl, x, y, b, q, dir, ST.rid(b1), ST.rid(b2), TR.rep_node(~K, b, b1, b2, y, nl, hB), nxb, nyb, nqb) 183 +repB = rep_intro(~K, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir), b, b1, b2, x, h0b, rb, rep_moved(~K, ~cmp, ~o, b1, b, nl, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir), agB1, TR.rep_l(~K, b, b1, b2, y, nl, hB)), rep_moved(~K, ~cmp, ~o, b2, b, nl, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir), agB2, TR.rep_r(~K, b, b1, b2, y, nl, hB))) 184 rep_intro(~K, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir), y, ST.TN{x, ta, ST.TN{b, b1, b2}}, tc, q, h0y, ry, rep_intro(~K, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir), x, ta, ST.TN{b, b1, b2}, y, h0x, rx, rep_moved(~K, ~cmp, ~o, ta, x, nl, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir), agA, hA), repB), rep_moved(~K, ~cmp, ~o, tc, y, nl, RM.rotl_nl(K, nl, x, y, ST.rid(tb), q, dir), agC, hC)) 185 186 # ---- the left rotation: the path ---- 187 188 189 def ctx_frame(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +i: Nat, +lft: Bool, +s: ST.Tr, +u: List<&2, P.Fr>, +hok: {P.ctxok(~K, Con{P.FR{1n+i, lft, s}, u}, x, nl) == True{} : Bool}, +hx: {NL.memn(x, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == False{} : Bool}, +hy: {NL.memn(y, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == False{} : Bool}, +hb: {NL.memn(b, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == False{} : Bool}, +hBA: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == True{} : Bool}, +mq: {NL.memn(1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == True{} : Bool}) -> {P.ctxok(~K, Con{P.FR{1n+i, lft, s}, u}, y, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft)) == True{} : Bool}: 190 +hk = L.and_left(P.cok1(~K, P.FR{1n+i, lft, s}, x, P.top(u), nl), P.ctxok(~K, u, 1n+i, nl), hok) 191 +hu = L.and_right(P.cok1(~K, P.FR{1n+i, lft, s}, x, P.top(u), nl), P.ctxok(~K, u, 1n+i, nl), hok) 192 +h0 = L.and_left(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk) 193 +hqn = L.and_left(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl), L.and_right(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk)) 194 +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl), L.and_right(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk)) 195 +nxq = DJ.ne_nm(x, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u})), hx, mq) 196 +nyq = DJ.ne_nm(y, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u})), hy, mq) 197 +nbq = DJ.ne_nm(b, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u})), hb, mq) 198 +rq = RN.rotl_q(K, nl, x, y, b, i, lft, ST.rid(s), P.top(u), hqn, nxq, nyq, nbq) 199 +agS = RN.rotl_agr(~K, ~cmp, ~o, ST.ids(s), nl, x, y, b, 1n+i, lft, Pair.fst({NL.memn(x, ST.ids(s)) == False{} : Bool}, {NL.memn(x, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(x, 1n+i, lft, s, u, hx)), Pair.fst({NL.memn(y, ST.ids(s)) == False{} : Bool}, {NL.memn(y, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(y, 1n+i, lft, s, u, hy)), Pair.fst({NL.memn(b, ST.ids(s)) == False{} : Bool}, {NL.memn(b, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(b, 1n+i, lft, s, u, hb)), Pair.fst({NL.memn(1n+i, ST.ids(s)) == False{} : Bool}, {NL.memn(1n+i, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fq_s(1n+i, lft, s, u, hBA))) 200 +agU = RN.rotl_agr(~K, ~cmp, ~o, SC.append(Nat, P.before(u), P.after(u)), nl, x, y, b, 1n+i, lft, Pair.snd({NL.memn(x, ST.ids(s)) == False{} : Bool}, {NL.memn(x, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(x, 1n+i, lft, s, u, hx)), Pair.snd({NL.memn(y, ST.ids(s)) == False{} : Bool}, {NL.memn(y, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(y, 1n+i, lft, s, u, hy)), Pair.snd({NL.memn(b, ST.ids(s)) == False{} : Bool}, {NL.memn(b, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(b, 1n+i, lft, s, u, hb)), Pair.snd({NL.memn(1n+i, ST.ids(s)) == False{} : Bool}, {NL.memn(1n+i, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fq_s(1n+i, lft, s, u, hBA))) 201 +hu2 = Equal.trans(Bool, P.ctxok(~K, u, 1n+i, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft)), P.ctxok(~K, u, 1n+i, nl), True{}, AG.ctx_agr(~K, ~cmp, ~o, u, 1n+i, nl, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft), agU), hu) 202 +hs2 = rep_moved(~K, ~cmp, ~o, s, 1n+i, nl, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft), agS, hs) 203 L.and_intro(P.cok1(~K, P.FR{1n+i, lft, s}, y, P.top(u), RM.rotl_nl(K, nl, x, y, b, 1n+i, lft)), P.ctxok(~K, u, 1n+i, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft)), L.and_intro(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), ST.pk(Nat, lft, y, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), y), P.top(u)), ST.rep(~K, s, 1n+i, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft))), h0, L.and_intro(ST.is_node(K, ST.nd(K, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), ST.pk(Nat, lft, y, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), y), P.top(u)), ST.rep(~K, s, 1n+i, RM.rotl_nl(K, nl, x, y, b, 1n+i, lft)), rq, hs2)), hu2) 204 205 def rotl_ctx(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +x: Nat, +y: Nat, +b: Nat, +hok: {P.ctxok(~K, c, x, nl) == True{} : Bool}, +hx: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hy: {NL.memn(y, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hb: {NL.memn(b, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hBA: {NL.nodupn(SC.append(Nat, P.before(c), P.after(c))) == True{} : Bool}) -> {P.ctxok(~K, c, y, RM.rotl_nl(K, nl, x, y, b, P.top(c), SP.dir(c))) == True{} : Bool}: 206 match c: 207 case Nil{}: 208 {==} 209 case Con{P.FR{0n, +lft, +s}, +u}: 210 Empty.absurd({P.ctxok(~K, Con{P.FR{0n, lft, s}, u}, y, RM.rotl_nl(K, nl, x, y, b, 0n, lft)) == True{} : Bool}, L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 0n, nl)), L.and_left(P.cok1(~K, P.FR{0n, lft, s}, x, P.top(u), nl), P.ctxok(~K, u, 0n, nl), hok)))) 211 case Con{P.FR{1n+i, True{}, +s}, +u}: 212 ctx_frame(~K, ~cmp, ~o, nl, x, y, b, i, True{}, s, u, hok, hx, hy, hb, hBA, DJ.mem_r(1n+i, P.before(u), Con{1n+i, SC.append(Nat, ST.ids(s), P.after(u))}, DJ.mem_hd(1n+i, SC.append(Nat, ST.ids(s), P.after(u))))) 213 case Con{P.FR{1n+i, False{}, +s}, +u}: 214 ctx_frame(~K, ~cmp, ~o, nl, x, y, b, i, False{}, s, u, hok, hx, hy, hb, hBA, DJ.mem_l(1n+i, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}})), P.after(u), DJ.mem_r(1n+i, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}}), DJ.mem_r(1n+i, ST.ids(s), Con{1n+i, Nil{}}, DJ.mem_hd(1n+i, Nil{}))))) 215 216 # ---- the right rotation: the rotated subtree ---- 217 218 219 def rotr_rep(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +ta: ST.Tr, +tb: ST.Tr, +tc: ST.Tr, +q: Nat, +dir: Bool, +h0x: {Nat.is_lt(0n, x) == True{} : Bool}, +h0y: {Nat.is_lt(0n, y) == True{} : Bool}, +hxn: {ST.is_node(K, ST.nd(K, nl, x), y, ST.rid(tc), q) == True{} : Bool}, +hyn: {ST.is_node(K, ST.nd(K, nl, y), ST.rid(ta), ST.rid(tb), x) == True{} : Bool}, +hA: {ST.rep(~K, ta, y, nl) == True{} : Bool}, +hB: {ST.rep(~K, tb, y, nl) == True{} : Bool}, +hC: {ST.rep(~K, tc, x, nl) == True{} : Bool}, +hS: {NL.nodupn(SC.append(Nat, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)})) == True{} : Bool}, +hqS: {NL.memn(q, SC.append(Nat, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)})) == False{} : Bool}) -> {ST.rep(~K, ST.TN{y, ta, ST.TN{x, tb, tc}}, q, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir)) == True{} : Bool}: 220 match tb: 221 case ST.TE{}: 222 +hP1 = DJ.ndl(SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, hS) 223 +xIC = DJ.nd_head(x, ST.ids(tc), DJ.ndr(SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, hS)) 224 +xP1 = DJ.dj_l(SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, hS, x, DJ.mem_hd(x, ST.ids(tc))) 225 +xIA = DJ.nm_l(x, ST.ids(ta), Con{y, Nil{}}, xP1) 226 +nyx = DJ.nm_ch(x, y, Nil{}, DJ.nm_r(x, ST.ids(ta), Con{y, Nil{}}, xP1)) 227 +myP1 = DJ.mem_r(y, ST.ids(ta), Con{y, Nil{}}, DJ.mem_hd(y, Nil{})) 228 +yxc = DJ.dj_r(SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, hS, y, myP1) 229 +nxy = DJ.nm_ch(y, x, ST.ids(tc), yxc) 230 +yIC = DJ.nm_ct(y, x, ST.ids(tc), yxc) 231 +yIA = DJ.dj_l(ST.ids(ta), Con{y, Nil{}}, hP1, y, DJ.mem_hd(y, Nil{})) 232 +mx = DJ.mem_r(x, SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, DJ.mem_hd(x, ST.ids(tc))) 233 +my = DJ.mem_l(y, SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, myP1) 234 +nqx = DJ.ne_nm(q, x, SC.append(Nat, SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}), hqS, mx) 235 +nqy = DJ.ne_nm(q, y, SC.append(Nat, SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}), hqS, my) 236 +qP1 = DJ.nm_l(q, SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, hqS) 237 +qIA = DJ.nm_l(q, ST.ids(ta), Con{y, Nil{}}, qP1) 238 +qIC = DJ.nm_ct(q, x, ST.ids(tc), DJ.nm_r(q, SC.append(Nat, ST.ids(ta), Con{y, Nil{}}), Con{x, ST.ids(tc)}, hqS)) 239 +agA = RN.rotr_agr(~K, ~cmp, ~o, ST.ids(ta), nl, x, y, 0n, q, dir, xIA, yIA, zero_ids(~K, nl, ta, y, hA), qIA) 240 +agC = RN.rotr_agr(~K, ~cmp, ~o, ST.ids(tc), nl, x, y, 0n, q, dir, xIC, yIC, zero_ids(~K, nl, tc, x, hC), qIC) 241 +rx = RN.rotr_x(K, nl, x, y, 0n, q, dir, ST.rid(tc), hxn, nyx, nqx, ne0(x, h0x)) 242 +ry = RN.rotr_y(K, nl, x, y, 0n, q, dir, ST.rid(ta), hyn, nxy, nqy, ne0(y, h0y)) 243 rep_intro(~K, RM.rotr_nl(K, nl, x, y, 0n, q, dir), y, ta, ST.TN{x, ST.TE{}, tc}, q, h0y, ry, rep_moved(~K, ~cmp, ~o, ta, y, nl, RM.rotr_nl(K, nl, x, y, 0n, q, dir), agA, hA), rep_intro(~K, RM.rotr_nl(K, nl, x, y, 0n, q, dir), x, ST.TE{}, tc, y, h0x, rx, {==}, rep_moved(~K, ~cmp, ~o, tc, x, nl, RM.rotr_nl(K, nl, x, y, 0n, q, dir), agC, hC))) 244 case ST.TN{+b, +b1, +b2}: 245 +hP1 = DJ.ndl(SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, hS) 246 +xIC = DJ.nd_head(x, ST.ids(tc), DJ.ndr(SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, hS)) 247 +xP1 = DJ.dj_l(SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, hS, x, DJ.mem_hd(x, ST.ids(tc))) 248 +xIA = DJ.nm_l(x, ST.ids(ta), Con{y, ST.ids(tb)}, xP1) 249 +xyb = DJ.nm_r(x, ST.ids(ta), Con{y, ST.ids(tb)}, xP1) 250 +nyx = DJ.nm_ch(x, y, ST.ids(tb), xyb) 251 +xIB = DJ.nm_ct(x, y, ST.ids(tb), xyb) 252 +myP1 = DJ.mem_r(y, ST.ids(ta), Con{y, ST.ids(tb)}, DJ.mem_hd(y, ST.ids(tb))) 253 +yxc = DJ.dj_r(SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, hS, y, myP1) 254 +nxy = DJ.nm_ch(y, x, ST.ids(tc), yxc) 255 +yIC = DJ.nm_ct(y, x, ST.ids(tc), yxc) 256 +yIA = DJ.dj_l(ST.ids(ta), Con{y, ST.ids(tb)}, hP1, y, DJ.mem_hd(y, ST.ids(tb))) 257 +hYB = DJ.ndr(ST.ids(ta), Con{y, ST.ids(tb)}, hP1) 258 +yIB = DJ.nd_head(y, ST.ids(tb), hYB) 259 +mbIB = DJ.mem_r(b, ST.ids(b1), Con{b, ST.ids(b2)}, DJ.mem_hd(b, ST.ids(b2))) 260 +mbP1 = DJ.mem_r(b, ST.ids(ta), Con{y, ST.ids(tb)}, DJ.mem_tl(b, y, ST.ids(tb), mbIB)) 261 +mx = DJ.mem_r(x, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, DJ.mem_hd(x, ST.ids(tc))) 262 +my = DJ.mem_l(y, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, myP1) 263 +mb = DJ.mem_l(b, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, mbP1) 264 +nyb = DJ.ne_nm(y, b, ST.ids(tb), yIB, mbIB) 265 +bIA = DJ.dj_l(ST.ids(ta), Con{y, ST.ids(tb)}, hP1, b, DJ.mem_tl(b, y, ST.ids(tb), mbIB)) 266 +bxc = DJ.dj_r(SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, hS, b, mbP1) 267 +nxb = DJ.nm_ch(b, x, ST.ids(tc), bxc) 268 +bIC = DJ.nm_ct(b, x, ST.ids(tc), bxc) 269 +nqx = DJ.ne_nm(q, x, SC.append(Nat, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}), hqS, mx) 270 +nqy = DJ.ne_nm(q, y, SC.append(Nat, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}), hqS, my) 271 +nqb = DJ.ne_nm(q, b, SC.append(Nat, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}), hqS, mb) 272 +qP1 = DJ.nm_l(q, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, hqS) 273 +qIA = DJ.nm_l(q, ST.ids(ta), Con{y, ST.ids(tb)}, qP1) 274 +qIB = DJ.nm_ct(q, y, ST.ids(tb), DJ.nm_r(q, ST.ids(ta), Con{y, ST.ids(tb)}, qP1)) 275 +qIC = DJ.nm_ct(q, x, ST.ids(tc), DJ.nm_r(q, SC.append(Nat, ST.ids(ta), Con{y, ST.ids(tb)}), Con{x, ST.ids(tc)}, hqS)) 276 +hIB = DJ.nd_tail(y, ST.ids(tb), hYB) 277 +bB1 = DJ.dj_l(ST.ids(b1), Con{b, ST.ids(b2)}, hIB, b, DJ.mem_hd(b, ST.ids(b2))) 278 +bB2 = DJ.nd_head(b, ST.ids(b2), DJ.ndr(ST.ids(b1), Con{b, ST.ids(b2)}, hIB)) 279 +xB1 = DJ.nm_l(x, ST.ids(b1), Con{b, ST.ids(b2)}, xIB) 280 +xB2 = DJ.nm_ct(x, b, ST.ids(b2), DJ.nm_r(x, ST.ids(b1), Con{b, ST.ids(b2)}, xIB)) 281 +yB1 = DJ.nm_l(y, ST.ids(b1), Con{b, ST.ids(b2)}, yIB) 282 +yB2 = DJ.nm_ct(y, b, ST.ids(b2), DJ.nm_r(y, ST.ids(b1), Con{b, ST.ids(b2)}, yIB)) 283 +qB1 = DJ.nm_l(q, ST.ids(b1), Con{b, ST.ids(b2)}, qIB) 284 +qB2 = DJ.nm_ct(q, b, ST.ids(b2), DJ.nm_r(q, ST.ids(b1), Con{b, ST.ids(b2)}, qIB)) 285 +agA = RN.rotr_agr(~K, ~cmp, ~o, ST.ids(ta), nl, x, y, b, q, dir, xIA, yIA, bIA, qIA) 286 +agC = RN.rotr_agr(~K, ~cmp, ~o, ST.ids(tc), nl, x, y, b, q, dir, xIC, yIC, bIC, qIC) 287 +agB1 = RN.rotr_agr(~K, ~cmp, ~o, ST.ids(b1), nl, x, y, b, q, dir, xB1, yB1, bB1, qB1) 288 +agB2 = RN.rotr_agr(~K, ~cmp, ~o, ST.ids(b2), nl, x, y, b, q, dir, xB2, yB2, bB2, qB2) 289 +h0b = L.and_left(Nat.is_lt(0n, b), Bool.and(ST.is_node(K, ST.nd(K, nl, b), ST.rid(b1), ST.rid(b2), y), Bool.and(ST.rep(~K, b1, b, nl), ST.rep(~K, b2, b, nl))), hB) 290 +rx = RN.rotr_x(K, nl, x, y, b, q, dir, ST.rid(tc), hxn, nyx, nqx, N.is_eq_sym_false(x, b, nxb)) 291 +ry = RN.rotr_y(K, nl, x, y, b, q, dir, ST.rid(ta), hyn, nxy, nqy, N.is_eq_sym_false(y, b, nyb)) 292 +rb = RN.rotr_b(K, nl, x, y, b, q, dir, ST.rid(b1), ST.rid(b2), TR.rep_node(~K, b, b1, b2, y, nl, hB), nxb, nyb, nqb) 293 +repB = rep_intro(~K, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir), b, b1, b2, x, h0b, rb, rep_moved(~K, ~cmp, ~o, b1, b, nl, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir), agB1, TR.rep_l(~K, b, b1, b2, y, nl, hB)), rep_moved(~K, ~cmp, ~o, b2, b, nl, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir), agB2, TR.rep_r(~K, b, b1, b2, y, nl, hB))) 294 rep_intro(~K, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir), y, ta, ST.TN{x, ST.TN{b, b1, b2}, tc}, q, h0y, ry, rep_moved(~K, ~cmp, ~o, ta, y, nl, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir), agA, hA), rep_intro(~K, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir), x, ST.TN{b, b1, b2}, tc, y, h0x, rx, repB, rep_moved(~K, ~cmp, ~o, tc, x, nl, RM.rotr_nl(K, nl, x, y, ST.rid(tb), q, dir), agC, hC))) 295 296 # ---- the right rotation: the path ---- 297 298 299 def ctx_frame_r(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +x: Nat, +y: Nat, +b: Nat, +i: Nat, +lft: Bool, +s: ST.Tr, +u: List<&2, P.Fr>, +hok: {P.ctxok(~K, Con{P.FR{1n+i, lft, s}, u}, x, nl) == True{} : Bool}, +hx: {NL.memn(x, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == False{} : Bool}, +hy: {NL.memn(y, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == False{} : Bool}, +hb: {NL.memn(b, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == False{} : Bool}, +hBA: {NL.nodupn(SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == True{} : Bool}, +mq: {NL.memn(1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u}))) == True{} : Bool}) -> {P.ctxok(~K, Con{P.FR{1n+i, lft, s}, u}, y, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft)) == True{} : Bool}: 300 +hk = L.and_left(P.cok1(~K, P.FR{1n+i, lft, s}, x, P.top(u), nl), P.ctxok(~K, u, 1n+i, nl), hok) 301 +hu = L.and_right(P.cok1(~K, P.FR{1n+i, lft, s}, x, P.top(u), nl), P.ctxok(~K, u, 1n+i, nl), hok) 302 +h0 = L.and_left(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk) 303 +hqn = L.and_left(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl), L.and_right(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk)) 304 +hs = L.and_right(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl), L.and_right(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, nl, 1n+i), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 1n+i, nl)), hk)) 305 +nxq = DJ.ne_nm(x, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u})), hx, mq) 306 +nyq = DJ.ne_nm(y, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u})), hy, mq) 307 +nbq = DJ.ne_nm(b, 1n+i, SC.append(Nat, P.before(Con{P.FR{1n+i, lft, s}, u}), P.after(Con{P.FR{1n+i, lft, s}, u})), hb, mq) 308 +rq = RN.rotr_q(K, nl, x, y, b, i, lft, ST.rid(s), P.top(u), hqn, nxq, nyq, nbq) 309 +agS = RN.rotr_agr(~K, ~cmp, ~o, ST.ids(s), nl, x, y, b, 1n+i, lft, Pair.fst({NL.memn(x, ST.ids(s)) == False{} : Bool}, {NL.memn(x, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(x, 1n+i, lft, s, u, hx)), Pair.fst({NL.memn(y, ST.ids(s)) == False{} : Bool}, {NL.memn(y, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(y, 1n+i, lft, s, u, hy)), Pair.fst({NL.memn(b, ST.ids(s)) == False{} : Bool}, {NL.memn(b, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(b, 1n+i, lft, s, u, hb)), Pair.fst({NL.memn(1n+i, ST.ids(s)) == False{} : Bool}, {NL.memn(1n+i, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fq_s(1n+i, lft, s, u, hBA))) 310 +agU = RN.rotr_agr(~K, ~cmp, ~o, SC.append(Nat, P.before(u), P.after(u)), nl, x, y, b, 1n+i, lft, Pair.snd({NL.memn(x, ST.ids(s)) == False{} : Bool}, {NL.memn(x, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(x, 1n+i, lft, s, u, hx)), Pair.snd({NL.memn(y, ST.ids(s)) == False{} : Bool}, {NL.memn(y, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(y, 1n+i, lft, s, u, hy)), Pair.snd({NL.memn(b, ST.ids(s)) == False{} : Bool}, {NL.memn(b, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fw_s(b, 1n+i, lft, s, u, hb)), Pair.snd({NL.memn(1n+i, ST.ids(s)) == False{} : Bool}, {NL.memn(1n+i, SC.append(Nat, P.before(u), P.after(u))) == False{} : Bool}, fq_s(1n+i, lft, s, u, hBA))) 311 +hu2 = Equal.trans(Bool, P.ctxok(~K, u, 1n+i, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft)), P.ctxok(~K, u, 1n+i, nl), True{}, AG.ctx_agr(~K, ~cmp, ~o, u, 1n+i, nl, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft), agU), hu) 312 +hs2 = rep_moved(~K, ~cmp, ~o, s, 1n+i, nl, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft), agS, hs) 313 L.and_intro(P.cok1(~K, P.FR{1n+i, lft, s}, y, P.top(u), RM.rotr_nl(K, nl, x, y, b, 1n+i, lft)), P.ctxok(~K, u, 1n+i, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft)), L.and_intro(Nat.is_lt(0n, 1n+i), Bool.and(ST.is_node(K, ST.nd(K, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), ST.pk(Nat, lft, y, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), y), P.top(u)), ST.rep(~K, s, 1n+i, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft))), h0, L.and_intro(ST.is_node(K, ST.nd(K, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft), 1n+i), ST.pk(Nat, lft, y, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), y), P.top(u)), ST.rep(~K, s, 1n+i, RM.rotr_nl(K, nl, x, y, b, 1n+i, lft)), rq, hs2)), hu2) 314 315 def rotr_ctx(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node>, +c: List<&2, P.Fr>, +x: Nat, +y: Nat, +b: Nat, +hok: {P.ctxok(~K, c, x, nl) == True{} : Bool}, +hx: {NL.memn(x, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hy: {NL.memn(y, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hb: {NL.memn(b, SC.append(Nat, P.before(c), P.after(c))) == False{} : Bool}, +hBA: {NL.nodupn(SC.append(Nat, P.before(c), P.after(c))) == True{} : Bool}) -> {P.ctxok(~K, c, y, RM.rotr_nl(K, nl, x, y, b, P.top(c), SP.dir(c))) == True{} : Bool}: 316 match c: 317 case Nil{}: 318 {==} 319 case Con{P.FR{0n, +lft, +s}, +u}: 320 Empty.absurd({P.ctxok(~K, Con{P.FR{0n, lft, s}, u}, y, RM.rotr_nl(K, nl, x, y, b, 0n, lft)) == True{} : Bool}, L.false_true(L.and_left(Nat.is_lt(0n, 0n), Bool.and(ST.is_node(K, ST.nd(K, nl, 0n), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, 0n, nl)), L.and_left(P.cok1(~K, P.FR{0n, lft, s}, x, P.top(u), nl), P.ctxok(~K, u, 0n, nl), hok)))) 321 case Con{P.FR{1n+i, True{}, +s}, +u}: 322 ctx_frame_r(~K, ~cmp, ~o, nl, x, y, b, i, True{}, s, u, hok, hx, hy, hb, hBA, DJ.mem_r(1n+i, P.before(u), Con{1n+i, SC.append(Nat, ST.ids(s), P.after(u))}, DJ.mem_hd(1n+i, SC.append(Nat, ST.ids(s), P.after(u))))) 323 case Con{P.FR{1n+i, False{}, +s}, +u}: 324 ctx_frame_r(~K, ~cmp, ~o, nl, x, y, b, i, False{}, s, u, hok, hx, hy, hb, hBA, DJ.mem_l(1n+i, SC.append(Nat, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}})), P.after(u), DJ.mem_r(1n+i, P.before(u), SC.append(Nat, ST.ids(s), Con{1n+i, Nil{}}), DJ.mem_r(1n+i, ST.ids(s), Con{1n+i, Nil{}}, DJ.mem_hd(1n+i, Nil{})))))