proofs/containers/balanced_search_tree/rot.bend
bend-collections-laws-containers@1.0.0.0 · 324 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/src/containers/balanced_search_tree.bend as M
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/tree.bend as TR
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as P
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/agree.bend as AG
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rotm.bend as RM
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/rotn.bend as RN
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/dj.bend as DJ
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/spath.bend as SP
16import bend-collections-laws-containers@1.0.0.0/proofs/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
26def 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
33def zero_ids(~K: Data, +nl: List<&2, M.Node<K>>, +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
41def zero_ctx(~K: Data, +nl: List<&2, M.Node<K>>, +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
65def 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
73def 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
79def 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
97def 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
108def rep_intro(~K: Data, +nl: List<&2, M.Node<K>>, +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
111def rep_moved(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +t: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +nl2: List<&2, M.Node<K>>, +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
115def rotl_rep(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +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
189def ctx_frame(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +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
205def rotl_ctx(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +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
219def rotr_rep(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +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
299def ctx_frame_r(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +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
315def rotr_ctx(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +nl: List<&2, M.Node<K>>, +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{})))))