proofs/containers/balanced_search_tree/setters.bend
bend-collections-laws-containers@1.0.0.0 · 729 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/containers/balanced_search_tree/state.bend as ST
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/prim.bend as PR
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/mirror.bend as MI
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/frame.bend as FR
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/spec/containers/balanced_search_tree/main.bend as S
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/ends.bend as EN
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/balanced_search_tree/path.bend as P
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
16
17# The mirror's node setters as functions of the node list: each rewrites one
18# field of an id's node (nothing for a free or absent node). The written
19# node, the length, and agreement off the id.
20# (source: tools/generators/tm_hand/setters.src)
21
22
23# ---- left ----
24
25def setl_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, x: M.Node<K>) -> List<&2, M.Node<K>>:
26 match x:
27 case M.Free{f}:
28 nl
29 case M.N{+c, +a, +b, +q, +k}:
30 PR.wr_nl(K, nl, id, M.N{c, v, b, q, k})
31
32def setl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> List<&2, M.Node<K>>:
33 setl_n(K, nl, id, v, ST.nd(K, nl, id))
34
35def set_left_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {MI.set_left_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setl_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:
36 match x:
37 case M.Free{f}:
38 {==}
39 case M.N{c, a, b, q, k}:
40 {==}
41
42def set_left_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat) -> {MI.set_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setl(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:
43 set_left_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))
44
45def setl_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setl(K, nl, 1n+i, v), 1n+i) == M.N{c, v, b, q, k} : M.Node<K>}:
46 %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setl_n(K, nl, 1n+i, v, _), 1n+i) == M.N{c, v, b, q, k} : M.Node<K>}
47 FR.nd_wr_same(K, nl, i, M.N{c, v, b, q, k}, hi)
48
49def setl_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {SC.length(M.Node<K>, setl_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:
50 match x:
51 case M.Free{f}:
52 {==}
53 case M.N{+c, +a, +b, +q, +k}:
54 FR.len_wr(K, nl, id, M.N{c, v, b, q, k})
55
56def setl_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {SC.length(M.Node<K>, setl(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:
57 setl_n_len(K, nl, id, v, ST.nd(K, nl, id))
58
59def setl_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setl_n(K, nl, id, v, x)) == True{} : Bool}:
60 match x:
61 case M.Free{f}:
62 AG.agr_refl(~K, ~cmp, ~o, xs, nl)
63 case M.N{+c, +a, +b, +q, +k}:
64 AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{c, v, b, q, k}, hn)
65
66# agreement off the written id
67def setl_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setl(K, nl, id, v)) == True{} : Bool}:
68 setl_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)
69
70# ---- right ----
71
72def setr_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, x: M.Node<K>) -> List<&2, M.Node<K>>:
73 match x:
74 case M.Free{f}:
75 nl
76 case M.N{+c, +a, +b, +q, +k}:
77 PR.wr_nl(K, nl, id, M.N{c, a, v, q, k})
78
79def setr(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> List<&2, M.Node<K>>:
80 setr_n(K, nl, id, v, ST.nd(K, nl, id))
81
82def set_right_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {MI.set_right_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setr_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:
83 match x:
84 case M.Free{f}:
85 {==}
86 case M.N{c, a, b, q, k}:
87 {==}
88
89def set_right_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat) -> {MI.set_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setr(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:
90 set_right_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))
91
92def setr_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setr(K, nl, 1n+i, v), 1n+i) == M.N{c, a, v, q, k} : M.Node<K>}:
93 %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setr_n(K, nl, 1n+i, v, _), 1n+i) == M.N{c, a, v, q, k} : M.Node<K>}
94 FR.nd_wr_same(K, nl, i, M.N{c, a, v, q, k}, hi)
95
96def setr_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {SC.length(M.Node<K>, setr_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:
97 match x:
98 case M.Free{f}:
99 {==}
100 case M.N{+c, +a, +b, +q, +k}:
101 FR.len_wr(K, nl, id, M.N{c, a, v, q, k})
102
103def setr_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {SC.length(M.Node<K>, setr(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:
104 setr_n_len(K, nl, id, v, ST.nd(K, nl, id))
105
106def setr_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setr_n(K, nl, id, v, x)) == True{} : Bool}:
107 match x:
108 case M.Free{f}:
109 AG.agr_refl(~K, ~cmp, ~o, xs, nl)
110 case M.N{+c, +a, +b, +q, +k}:
111 AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{c, a, v, q, k}, hn)
112
113# agreement off the written id
114def setr_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setr(K, nl, id, v)) == True{} : Bool}:
115 setr_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)
116
117# ---- parent ----
118
119def setp_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, x: M.Node<K>) -> List<&2, M.Node<K>>:
120 match x:
121 case M.Free{f}:
122 nl
123 case M.N{+c, +a, +b, +q, +k}:
124 PR.wr_nl(K, nl, id, M.N{c, a, b, v, k})
125
126def setp(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> List<&2, M.Node<K>>:
127 setp_n(K, nl, id, v, ST.nd(K, nl, id))
128
129def set_parent_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {MI.set_parent_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setp_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:
130 match x:
131 case M.Free{f}:
132 {==}
133 case M.N{c, a, b, q, k}:
134 {==}
135
136def set_parent_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat) -> {MI.set_parent(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setp(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:
137 set_parent_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))
138
139def setp_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setp(K, nl, 1n+i, v), 1n+i) == M.N{c, a, b, v, k} : M.Node<K>}:
140 %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setp_n(K, nl, 1n+i, v, _), 1n+i) == M.N{c, a, b, v, k} : M.Node<K>}
141 FR.nd_wr_same(K, nl, i, M.N{c, a, b, v, k}, hi)
142
143def setp_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {SC.length(M.Node<K>, setp_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:
144 match x:
145 case M.Free{f}:
146 {==}
147 case M.N{+c, +a, +b, +q, +k}:
148 FR.len_wr(K, nl, id, M.N{c, a, b, v, k})
149
150def setp_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {SC.length(M.Node<K>, setp(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:
151 setp_n_len(K, nl, id, v, ST.nd(K, nl, id))
152
153def setp_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setp_n(K, nl, id, v, x)) == True{} : Bool}:
154 match x:
155 case M.Free{f}:
156 AG.agr_refl(~K, ~cmp, ~o, xs, nl)
157 case M.N{+c, +a, +b, +q, +k}:
158 AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{c, a, b, v, k}, hn)
159
160# agreement off the written id
161def setp_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setp(K, nl, id, v)) == True{} : Bool}:
162 setp_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)
163
164# ---- red ----
165
166def setc_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, x: M.Node<K>) -> List<&2, M.Node<K>>:
167 match x:
168 case M.Free{f}:
169 nl
170 case M.N{+c, +a, +b, +q, +k}:
171 PR.wr_nl(K, nl, id, M.N{v, a, b, q, k})
172
173def setc(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> List<&2, M.Node<K>>:
174 setc_n(K, nl, id, v, ST.nd(K, nl, id))
175
176def set_red_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Bool, +x: M.Node<K>) -> {MI.set_red_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setc_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:
177 match x:
178 case M.Free{f}:
179 {==}
180 case M.N{c, a, b, q, k}:
181 {==}
182
183def set_red_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Bool) -> {MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setc(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:
184 set_red_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))
185
186def setc_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Bool, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setc(K, nl, 1n+i, v), 1n+i) == M.N{v, a, b, q, k} : M.Node<K>}:
187 %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setc_n(K, nl, 1n+i, v, _), 1n+i) == M.N{v, a, b, q, k} : M.Node<K>}
188 FR.nd_wr_same(K, nl, i, M.N{v, a, b, q, k}, hi)
189
190def setc_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +x: M.Node<K>) -> {SC.length(M.Node<K>, setc_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:
191 match x:
192 case M.Free{f}:
193 {==}
194 case M.N{+c, +a, +b, +q, +k}:
195 FR.len_wr(K, nl, id, M.N{v, a, b, q, k})
196
197def setc_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {SC.length(M.Node<K>, setc(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:
198 setc_n_len(K, nl, id, v, ST.nd(K, nl, id))
199
200def setc_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setc_n(K, nl, id, v, x)) == True{} : Bool}:
201 match x:
202 case M.Free{f}:
203 AG.agr_refl(~K, ~cmp, ~o, xs, nl)
204 case M.N{+c, +a, +b, +q, +k}:
205 AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{v, a, b, q, k}, hn)
206
207# agreement off the written id
208def setc_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setc(K, nl, id, v)) == True{} : Bool}:
209 setc_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)
210
211# ---- every id's node after a setter ----
212
213def fn_c(-K: Data, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +e: {M.Free{0n} == M.N{c, a, b, q, k} : M.Node<K>}) -> Empty:
214 L.true_false(L.subst(M.Node<K>, z => {ST.is_free(K, M.Free{0n}, 0n) == ST.is_free(K, z, 0n) : Bool}, M.Free{0n}, M.N{c, a, b, q, k}, e, {==}))
215
216def nr_c(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +t: Bool, +ht: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == t : Bool}) -> {t == True{} : Bool}:
217 match t:
218 case True{}:
219 {==}
220 case False{}:
221 +e = Equal.trans(M.Node<K>, M.Free{0n}, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.Free{0n}, PR.nth_hi(M.Node<K>, nl, i, M.Free{0n}, ht)), hx)
222 Empty.absurd({False{} == True{} : Bool}, fn_c(K, c, a, b, q, k, e))
223
224def nd_n_range(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}) -> {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}:
225 nr_c(K, nl, i, c, a, b, q, k, hx, Nat.is_lt(i, SC.length(M.Node<K>, nl)), {==})
226
227def modl(-K: Data, x: M.Node<K>, +v: Nat) -> M.Node<K>:
228 match x:
229 case M.Free{+f}:
230 M.Free{f}
231 case M.N{+c, +a, +b, +q, +k}:
232 M.N{c, v, b, q, k}
233
234def wsame_l(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, v, b, q, k}), id) == M.N{c, v, b, q, k} : M.Node<K>}:
235 match id:
236 case 0n:
237 Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{c, v, b, q, k}), 0n) == M.N{c, v, b, q, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))
238 case 1n+i:
239 FR.nd_wr_same(K, nl, i, M.N{c, v, b, q, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))
240
241def ndl_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setl_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
242 match x e:
243 case M.Free{f} True{}:
244 +ej = N.eq_from_is_eq(id, j, he)
245 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modl(K, ST.nd(K, nl, _), v) : M.Node<K>}
246 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modl(K, _, v) : M.Node<K>}
247 {==}
248 case M.Free{f} False{}:
249 {==}
250 case M.N{+c, +a, +b, +q, +k} True{}:
251 +ej = N.eq_from_is_eq(id, j, he)
252 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, v, b, q, k}), _) == modl(K, ST.nd(K, nl, _), v) : M.Node<K>}
253 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, v, b, q, k}), id) == modl(K, _, v) : M.Node<K>}
254 wsame_l(K, nl, id, v, c, a, b, q, k, hx)
255 case M.N{+c, +a, +b, +q, +k} False{}:
256 FR.nd_wr_other(K, nl, id, M.N{c, v, b, q, k}, j, he)
257
258# the node at j after setting id: modified when j is id
259def ndl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.nd(K, setl(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
260 ndl_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})
261
262def modr(-K: Data, x: M.Node<K>, +v: Nat) -> M.Node<K>:
263 match x:
264 case M.Free{+f}:
265 M.Free{f}
266 case M.N{+c, +a, +b, +q, +k}:
267 M.N{c, a, v, q, k}
268
269def wsame_r(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, v, q, k}), id) == M.N{c, a, v, q, k} : M.Node<K>}:
270 match id:
271 case 0n:
272 Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{c, a, v, q, k}), 0n) == M.N{c, a, v, q, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))
273 case 1n+i:
274 FR.nd_wr_same(K, nl, i, M.N{c, a, v, q, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))
275
276def ndr_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setr_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
277 match x e:
278 case M.Free{f} True{}:
279 +ej = N.eq_from_is_eq(id, j, he)
280 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modr(K, ST.nd(K, nl, _), v) : M.Node<K>}
281 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modr(K, _, v) : M.Node<K>}
282 {==}
283 case M.Free{f} False{}:
284 {==}
285 case M.N{+c, +a, +b, +q, +k} True{}:
286 +ej = N.eq_from_is_eq(id, j, he)
287 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, v, q, k}), _) == modr(K, ST.nd(K, nl, _), v) : M.Node<K>}
288 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, v, q, k}), id) == modr(K, _, v) : M.Node<K>}
289 wsame_r(K, nl, id, v, c, a, b, q, k, hx)
290 case M.N{+c, +a, +b, +q, +k} False{}:
291 FR.nd_wr_other(K, nl, id, M.N{c, a, v, q, k}, j, he)
292
293# the node at j after setting id: modified when j is id
294def ndr(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.nd(K, setr(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
295 ndr_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})
296
297def modp(-K: Data, x: M.Node<K>, +v: Nat) -> M.Node<K>:
298 match x:
299 case M.Free{+f}:
300 M.Free{f}
301 case M.N{+c, +a, +b, +q, +k}:
302 M.N{c, a, b, v, k}
303
304def wsame_p(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, b, v, k}), id) == M.N{c, a, b, v, k} : M.Node<K>}:
305 match id:
306 case 0n:
307 Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{c, a, b, v, k}), 0n) == M.N{c, a, b, v, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))
308 case 1n+i:
309 FR.nd_wr_same(K, nl, i, M.N{c, a, b, v, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))
310
311def ndp_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setp_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
312 match x e:
313 case M.Free{f} True{}:
314 +ej = N.eq_from_is_eq(id, j, he)
315 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modp(K, ST.nd(K, nl, _), v) : M.Node<K>}
316 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modp(K, _, v) : M.Node<K>}
317 {==}
318 case M.Free{f} False{}:
319 {==}
320 case M.N{+c, +a, +b, +q, +k} True{}:
321 +ej = N.eq_from_is_eq(id, j, he)
322 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, b, v, k}), _) == modp(K, ST.nd(K, nl, _), v) : M.Node<K>}
323 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, b, v, k}), id) == modp(K, _, v) : M.Node<K>}
324 wsame_p(K, nl, id, v, c, a, b, q, k, hx)
325 case M.N{+c, +a, +b, +q, +k} False{}:
326 FR.nd_wr_other(K, nl, id, M.N{c, a, b, v, k}, j, he)
327
328# the node at j after setting id: modified when j is id
329def ndp(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.nd(K, setp(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
330 ndp_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})
331
332def modc(-K: Data, x: M.Node<K>, +v: Bool) -> M.Node<K>:
333 match x:
334 case M.Free{+f}:
335 M.Free{f}
336 case M.N{+c, +a, +b, +q, +k}:
337 M.N{v, a, b, q, k}
338
339def wsame_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{v, a, b, q, k}), id) == M.N{v, a, b, q, k} : M.Node<K>}:
340 match id:
341 case 0n:
342 Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{v, a, b, q, k}), 0n) == M.N{v, a, b, q, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))
343 case 1n+i:
344 FR.nd_wr_same(K, nl, i, M.N{v, a, b, q, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))
345
346def ndc_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setc_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
347 match x e:
348 case M.Free{f} True{}:
349 +ej = N.eq_from_is_eq(id, j, he)
350 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modc(K, ST.nd(K, nl, _), v) : M.Node<K>}
351 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modc(K, _, v) : M.Node<K>}
352 {==}
353 case M.Free{f} False{}:
354 {==}
355 case M.N{+c, +a, +b, +q, +k} True{}:
356 +ej = N.eq_from_is_eq(id, j, he)
357 %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{v, a, b, q, k}), _) == modc(K, ST.nd(K, nl, _), v) : M.Node<K>}
358 %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{v, a, b, q, k}), id) == modc(K, _, v) : M.Node<K>}
359 wsame_c(K, nl, id, v, c, a, b, q, k, hx)
360 case M.N{+c, +a, +b, +q, +k} False{}:
361 FR.nd_wr_other(K, nl, id, M.N{v, a, b, q, k}, j, he)
362
363# the node at j after setting id: modified when j is id
364def ndc(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat) -> {ST.nd(K, setc(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:
365 ndc_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})
366
367# ---- what setters keep everywhere ----
368
369
370def ent_modl(-K: Data, -V: Data, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, modl(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
371 match x m:
372 case M.Free{f} +m:
373 {==}
374 case M.N{c, a, b, q, k} None{}:
375 {==}
376 case M.N{c, a, b, q, k} Some{w}:
377 {==}
378
379def free_modl(-K: Data, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, modl(K, x, v), q) == ST.is_free(K, x, q) : Bool}:
380 match x:
381 case M.Free{f}:
382 {==}
383 case M.N{c, a, b, q2, k}:
384 {==}
385
386def ent_pkl(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modl(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
387 match e:
388 case True{}:
389 ent_modl(K, V, x, v, m)
390 case False{}:
391 {==}
392
393def free_pkl(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modl(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:
394 match e:
395 case True{}:
396 free_modl(K, x, v, q)
397 case False{}:
398 {==}
399
400def ent_setl(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setl(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:
401 %Equal.sym(M.Node<K>, ST.nd(K, setl(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndl(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}
402 ent_pkl(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)
403
404# a setter keeps every entry
405def ents_setl(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {ST.ents(~K, ~V, xs, setl(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
406 match xs:
407 case Nil{}:
408 {==}
409 case Con{+j, +t}:
410 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setl(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setl(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setl(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
411 %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setl(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setl(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
412 {==}
413
414def oks_setl(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {EN.oks(~K, ~V, xs, setl(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
415 match xs:
416 case Nil{}:
417 {==}
418 case Con{+j, +t}:
419 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setl(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setl(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setl(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
420 %Equal.sym(Bool, EN.oks(~K, ~V, t, setl(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setl(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
421 {==}
422
423# a setter keeps the free chain
424def fll_setl(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {ST.fll(~K, setl(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:
425 match fl:
426 case Nil{}:
427 {==}
428 case Con{+f, +t}:
429 %Equal.sym(M.Node<K>, ST.nd(K, setl(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modl(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndl(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setl(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
430 %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modl(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkl(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setl(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
431 %Equal.sym(Bool, ST.fll(~K, setl(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setl(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}
432 {==}
433
434def ent_modr(-K: Data, -V: Data, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, modr(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
435 match x m:
436 case M.Free{f} +m:
437 {==}
438 case M.N{c, a, b, q, k} None{}:
439 {==}
440 case M.N{c, a, b, q, k} Some{w}:
441 {==}
442
443def free_modr(-K: Data, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, modr(K, x, v), q) == ST.is_free(K, x, q) : Bool}:
444 match x:
445 case M.Free{f}:
446 {==}
447 case M.N{c, a, b, q2, k}:
448 {==}
449
450def ent_pkr(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modr(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
451 match e:
452 case True{}:
453 ent_modr(K, V, x, v, m)
454 case False{}:
455 {==}
456
457def free_pkr(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modr(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:
458 match e:
459 case True{}:
460 free_modr(K, x, v, q)
461 case False{}:
462 {==}
463
464def ent_setr(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setr(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:
465 %Equal.sym(M.Node<K>, ST.nd(K, setr(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndr(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}
466 ent_pkr(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)
467
468# a setter keeps every entry
469def ents_setr(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {ST.ents(~K, ~V, xs, setr(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
470 match xs:
471 case Nil{}:
472 {==}
473 case Con{+j, +t}:
474 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setr(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setr(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setr(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
475 %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setr(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setr(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
476 {==}
477
478def oks_setr(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {EN.oks(~K, ~V, xs, setr(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
479 match xs:
480 case Nil{}:
481 {==}
482 case Con{+j, +t}:
483 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setr(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setr(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setr(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
484 %Equal.sym(Bool, EN.oks(~K, ~V, t, setr(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setr(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
485 {==}
486
487# a setter keeps the free chain
488def fll_setr(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {ST.fll(~K, setr(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:
489 match fl:
490 case Nil{}:
491 {==}
492 case Con{+f, +t}:
493 %Equal.sym(M.Node<K>, ST.nd(K, setr(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modr(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndr(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setr(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
494 %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modr(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkr(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setr(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
495 %Equal.sym(Bool, ST.fll(~K, setr(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setr(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}
496 {==}
497
498def ent_modp(-K: Data, -V: Data, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, modp(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
499 match x m:
500 case M.Free{f} +m:
501 {==}
502 case M.N{c, a, b, q, k} None{}:
503 {==}
504 case M.N{c, a, b, q, k} Some{w}:
505 {==}
506
507def free_modp(-K: Data, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, modp(K, x, v), q) == ST.is_free(K, x, q) : Bool}:
508 match x:
509 case M.Free{f}:
510 {==}
511 case M.N{c, a, b, q2, k}:
512 {==}
513
514def ent_pkp(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modp(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
515 match e:
516 case True{}:
517 ent_modp(K, V, x, v, m)
518 case False{}:
519 {==}
520
521def free_pkp(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modp(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:
522 match e:
523 case True{}:
524 free_modp(K, x, v, q)
525 case False{}:
526 {==}
527
528def ent_setp(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setp(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:
529 %Equal.sym(M.Node<K>, ST.nd(K, setp(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndp(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}
530 ent_pkp(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)
531
532# a setter keeps every entry
533def ents_setp(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {ST.ents(~K, ~V, xs, setp(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
534 match xs:
535 case Nil{}:
536 {==}
537 case Con{+j, +t}:
538 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setp(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setp(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setp(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
539 %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setp(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setp(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
540 {==}
541
542def oks_setp(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {EN.oks(~K, ~V, xs, setp(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
543 match xs:
544 case Nil{}:
545 {==}
546 case Con{+j, +t}:
547 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setp(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setp(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setp(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
548 %Equal.sym(Bool, EN.oks(~K, ~V, t, setp(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setp(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
549 {==}
550
551# a setter keeps the free chain
552def fll_setp(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {ST.fll(~K, setp(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:
553 match fl:
554 case Nil{}:
555 {==}
556 case Con{+f, +t}:
557 %Equal.sym(M.Node<K>, ST.nd(K, setp(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modp(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndp(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setp(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
558 %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modp(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkp(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setp(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
559 %Equal.sym(Bool, ST.fll(~K, setp(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setp(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}
560 {==}
561
562def ent_modc(-K: Data, -V: Data, +x: M.Node<K>, +v: Bool, +m: Maybe<&2, V>) -> {ST.ent(K, V, modc(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
563 match x m:
564 case M.Free{f} +m:
565 {==}
566 case M.N{c, a, b, q, k} None{}:
567 {==}
568 case M.N{c, a, b, q, k} Some{w}:
569 {==}
570
571def free_modc(-K: Data, +x: M.Node<K>, +v: Bool, +q: Nat) -> {ST.is_free(K, modc(K, x, v), q) == ST.is_free(K, x, q) : Bool}:
572 match x:
573 case M.Free{f}:
574 {==}
575 case M.N{c, a, b, q2, k}:
576 {==}
577
578def ent_pkc(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Bool, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modc(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:
579 match e:
580 case True{}:
581 ent_modc(K, V, x, v, m)
582 case False{}:
583 {==}
584
585def free_pkc(-K: Data, +e: Bool, +x: M.Node<K>, +v: Bool, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modc(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:
586 match e:
587 case True{}:
588 free_modc(K, x, v, q)
589 case False{}:
590 {==}
591
592def ent_setc(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setc(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:
593 %Equal.sym(M.Node<K>, ST.nd(K, setc(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndc(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}
594 ent_pkc(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)
595
596# a setter keeps every entry
597def ents_setc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Bool) -> {ST.ents(~K, ~V, xs, setc(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:
598 match xs:
599 case Nil{}:
600 {==}
601 case Con{+j, +t}:
602 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setc(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setc(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setc(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
603 %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setc(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setc(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}
604 {==}
605
606def oks_setc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Bool) -> {EN.oks(~K, ~V, xs, setc(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:
607 match xs:
608 case Nil{}:
609 {==}
610 case Con{+j, +t}:
611 %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setc(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setc(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setc(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
612 %Equal.sym(Bool, EN.oks(~K, ~V, t, setc(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setc(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}
613 {==}
614
615# a setter keeps the free chain
616def fll_setc(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {ST.fll(~K, setc(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:
617 match fl:
618 case Nil{}:
619 {==}
620 case Con{+f, +t}:
621 %Equal.sym(M.Node<K>, ST.nd(K, setc(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modc(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndc(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setc(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
622 %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modc(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkc(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setc(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}
623 %Equal.sym(Bool, ST.fll(~K, setc(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setc(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}
624 {==}
625
626# ---- recolouring keeps every link ----
627
628
629def isn_modc(-K: Data, +x: M.Node<K>, +v: Bool, +a: Nat, +b: Nat, +q: Nat) -> {ST.is_node(K, modc(K, x, v), a, b, q) == ST.is_node(K, x, a, b, q) : Bool}:
630 match x:
631 case M.Free{f}:
632 {==}
633 case M.N{c, x1, x2, x3, k}:
634 {==}
635
636def isn_pkc(-K: Data, +e: Bool, +x: M.Node<K>, +v: Bool, +a: Nat, +b: Nat, +q: Nat) -> {ST.is_node(K, ST.pk(M.Node<K>, e, modc(K, x, v), x), a, b, q) == ST.is_node(K, x, a, b, q) : Bool}:
637 match e:
638 case True{}:
639 isn_modc(K, x, v, a, b, q)
640 case False{}:
641 {==}
642
643def isn_setc(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat, +a: Nat, +b: Nat, +q: Nat) -> {ST.is_node(K, ST.nd(K, setc(K, nl, id, v), j), a, b, q) == ST.is_node(K, ST.nd(K, nl, j), a, b, q) : Bool}:
644 %Equal.sym(M.Node<K>, ST.nd(K, setc(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndc(K, nl, id, v, j)) : {ST.is_node(K, _, a, b, q) == ST.is_node(K, ST.nd(K, nl, j), a, b, q) : Bool}
645 isn_pkc(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v, a, b, q)
646
647def rep_setc(~K: Data, +t: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {ST.rep(~K, t, p, setc(K, nl, id, v)) == ST.rep(~K, t, p, nl) : Bool}:
648 match t:
649 case ST.TE{}:
650 {==}
651 case ST.TN{+i, +l, +r}:
652 %Equal.sym(Bool, ST.is_node(K, ST.nd(K, setc(K, nl, id, v), i), ST.rid(l), ST.rid(r), p), ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), isn_setc(K, nl, id, v, i, ST.rid(l), ST.rid(r), p)) : {Bool.and(Nat.is_lt(0n, i), Bool.and(_, Bool.and(ST.rep(~K, l, i, setc(K, nl, id, v)), ST.rep(~K, r, i, setc(K, nl, id, v))))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}
653 %Equal.sym(Bool, ST.rep(~K, l, i, setc(K, nl, id, v)), ST.rep(~K, l, i, nl), rep_setc(~K, l, i, nl, id, v)) : {Bool.and(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, r, i, setc(K, nl, id, v))))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}
654 %Equal.sym(Bool, ST.rep(~K, r, i, setc(K, nl, id, v)), ST.rep(~K, r, i, nl), rep_setc(~K, r, i, nl, id, v)) : {Bool.and(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, ST.TN{i, l, r}, p, nl) : Bool}
655 {==}
656
657def ctx_setc(~K: Data, +c: List<&2, P.Fr>, +x: Nat, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {P.ctxok(~K, c, x, setc(K, nl, id, v)) == P.ctxok(~K, c, x, nl) : Bool}:
658 match c:
659 case Nil{}:
660 {==}
661 case Con{P.FR{+p, +lft, +s}, +u}:
662 %Equal.sym(Bool, ST.is_node(K, ST.nd(K, setc(K, nl, id, v), p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), isn_setc(K, nl, id, v, p, ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u))) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(_, ST.rep(~K, s, p, setc(K, nl, id, v)))), P.ctxok(~K, u, p, setc(K, nl, id, v))) == P.ctxok(~K, Con{P.FR{p, lft, s}, u}, x, nl) : Bool}
663 %Equal.sym(Bool, ST.rep(~K, s, p, setc(K, nl, id, v)), ST.rep(~K, s, p, nl), rep_setc(~K, s, p, nl, id, v)) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), _)), P.ctxok(~K, u, p, setc(K, nl, id, v))) == P.ctxok(~K, Con{P.FR{p, lft, s}, u}, x, nl) : Bool}
664 %Equal.sym(Bool, P.ctxok(~K, u, p, setc(K, nl, id, v)), P.ctxok(~K, u, p, nl), ctx_setc(~K, u, p, nl, id, v)) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, p, nl))), _) == P.ctxok(~K, Con{P.FR{p, lft, s}, u}, x, nl) : Bool}
665 {==}
666
667# the recoloured node's colour
668def red_modc(-K: Data, +x: M.Node<K>, +v: Bool, +h: {ST.is_red(K, x) == ST.is_red(K, x) : Bool}) -> {ST.is_red(K, modc(K, x, False{})) == False{} : Bool}:
669 match x:
670 case M.Free{f}:
671 {==}
672 case M.N{c, a, b, q, k}:
673 {==}
674
675# ---- link setters keep every colour ----
676
677def red_modl(-K: Data, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, modl(K, x, v)) == ST.is_red(K, x) : Bool}:
678 match x:
679 case M.Free{f}:
680 {==}
681 case M.N{c, a, b, q, k}:
682 {==}
683
684def red_pkl(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, ST.pk(M.Node<K>, e, modl(K, x, v), x)) == ST.is_red(K, x) : Bool}:
685 match e:
686 case True{}:
687 red_modl(K, x, v)
688 case False{}:
689 {==}
690
691def red_setl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.is_red(K, ST.nd(K, setl(K, nl, id, v), j)) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}:
692 %Equal.sym(M.Node<K>, ST.nd(K, setl(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndl(K, nl, id, v, j)) : {ST.is_red(K, _) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}
693 red_pkl(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v)
694
695def red_modr(-K: Data, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, modr(K, x, v)) == ST.is_red(K, x) : Bool}:
696 match x:
697 case M.Free{f}:
698 {==}
699 case M.N{c, a, b, q, k}:
700 {==}
701
702def red_pkr(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, ST.pk(M.Node<K>, e, modr(K, x, v), x)) == ST.is_red(K, x) : Bool}:
703 match e:
704 case True{}:
705 red_modr(K, x, v)
706 case False{}:
707 {==}
708
709def red_setr(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.is_red(K, ST.nd(K, setr(K, nl, id, v), j)) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}:
710 %Equal.sym(M.Node<K>, ST.nd(K, setr(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndr(K, nl, id, v, j)) : {ST.is_red(K, _) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}
711 red_pkr(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v)
712
713def red_modp(-K: Data, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, modp(K, x, v)) == ST.is_red(K, x) : Bool}:
714 match x:
715 case M.Free{f}:
716 {==}
717 case M.N{c, a, b, q, k}:
718 {==}
719
720def red_pkp(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, ST.pk(M.Node<K>, e, modp(K, x, v), x)) == ST.is_red(K, x) : Bool}:
721 match e:
722 case True{}:
723 red_modp(K, x, v)
724 case False{}:
725 {==}
726
727def red_setp(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.is_red(K, ST.nd(K, setp(K, nl, id, v), j)) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}:
728 %Equal.sym(M.Node<K>, ST.nd(K, setp(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndp(K, nl, id, v, j)) : {ST.is_red(K, _) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}
729 red_pkp(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v)