1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/order.bend as O
5	import ../../../spec/lib/common.bend as SC
6	import ../../../src/containers/balanced_search_tree.bend as M
7	import ./state.bend as ST
8	import ./prim.bend as PR
9	import ./mirror.bend as MI
10	import ./frame.bend as FR
11	import ./agree.bend as AG
12	import ../../../spec/containers/balanced_search_tree/main.bend as S
13	import ./ends.bend as EN
14	import ./path.bend as P
15	import ../../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	
25	def 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	
32	def 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	
35	def 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	
42	def 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	
45	def 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	
49	def 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	
56	def 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	
59	def 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
67	def 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	
72	def 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	
79	def 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	
82	def 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	
89	def 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	
92	def 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	
96	def 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	
103	def 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	
106	def 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
114	def 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	
119	def 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	
126	def 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	
129	def 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	
136	def 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	
139	def 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	
143	def 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	
150	def 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	
153	def 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
161	def 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	
166	def 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	
173	def 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	
176	def 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	
183	def 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	
186	def 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	
190	def 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	
197	def 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	
200	def 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
208	def 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	
213	def 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	
216	def 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	
224	def 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	
227	def 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	
234	def 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	
241	def 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
259	def 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	
262	def 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	
269	def 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	
276	def 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
294	def 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	
297	def 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	
304	def 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	
311	def 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
329	def 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	
332	def 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	
339	def 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	
346	def 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
364	def 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	
370	def 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	
379	def 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	
386	def 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	
393	def 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	
400	def 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
405	def 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	
414	def 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
424	def 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	
434	def 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	
443	def 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	
450	def 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	
457	def 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	
464	def 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
469	def 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	
478	def 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
488	def 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	
498	def 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	
507	def 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	
514	def 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	
521	def 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	
528	def 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
533	def 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	
542	def 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
552	def 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	
562	def 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	
571	def 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	
578	def 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	
585	def 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	
592	def 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
597	def 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	
606	def 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
616	def 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	
629	def 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	
636	def 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	
643	def 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	
647	def 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	
657	def 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
668	def 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	
677	def 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	
684	def 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	
691	def 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	
695	def 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	
702	def 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	
709	def 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	
713	def 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	
720	def 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	
727	def 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)