1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/u32alg.bend as A
5	import ../../lib/list.bend as LL
6	import ../../../spec/lib/common.bend as SC
7	import ../../../spec/containers/doubly_linked_list.bend as S
8	import ./state.bend as ST
9	import ./rel.bend as RL
10	import ../../lib/nat_list.bend as NL
11	import ../../lib/words32.bend as W32
12	
13	# The value and generation lists: reads after writes, prefixes, and the
14	# invariant's live-listed and zero-generation components pointwise.
15	
16	
17	# ---- values ----
18	
19	def val_upd_same(-T: Data, +vl: List<&2, Maybe<&2, T>>, +i: Nat, +v: Maybe<&2, T>, +h: {Nat.is_lt(i, SC.length(Maybe<&2, T>, vl)) == True{} : Bool}) -> {S.val_of(T, SC.update(Maybe<&2, T>, vl, i, v), i) == v : Maybe<&2, T>}:
20	  match vl i:
21	    case Nil{} _:
22	      Empty.absurd({S.val_of(T, Nil{}, i) == v : Maybe<&2, T>}, N.lt_zero_absurd(i, h))
23	    case Con{m, t} 0n:
24	      {==}
25	    case Con{m, +t} 1n+p:
26	      val_upd_same(T, t, p, v, h)
27	
28	def val_upd_other(-T: Data, +vl: List<&2, Maybe<&2, T>>, +i: Nat, +j: Nat, +v: Maybe<&2, T>, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {S.val_of(T, SC.update(Maybe<&2, T>, vl, i, v), j) == S.val_of(T, vl, j) : Maybe<&2, T>}:
29	  match vl i j:
30	    case Nil{} _ _:
31	      {==}
32	    case Con{m, t} 0n 0n:
33	      Empty.absurd({v == m : Maybe<&2, T>}, L.true_false(ne))
34	    case Con{m, t} 0n 1n+q:
35	      {==}
36	    case Con{m, t} 1n+p 0n:
37	      {==}
38	    case Con{m, +t} 1n+p 1n+q:
39	      val_upd_other(T, t, p, q, v, ne)
40	
41	def val_take(-T: Data, +vl: List<&2, Maybe<&2, T>>, +n: Nat, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {S.val_of(T, SC.take(Maybe<&2, T>, vl, n), i) == S.val_of(T, vl, i) : Maybe<&2, T>}:
42	  match vl n i:
43	    case Nil{} _ _:
44	      {==}
45	    case Con{m, t} 0n _:
46	      Empty.absurd({S.val_of(T, Nil{}, i) == S.val_of(T, Con{m, t}, i) : Maybe<&2, T>}, N.lt_zero_absurd(i, h))
47	    case Con{m, t} 1n+p 0n:
48	      {==}
49	    case Con{m, +t} 1n+p 1n+q:
50	      val_take(T, t, p, q, h)
51	
52	def val_hi(-T: Data, +vl: List<&2, Maybe<&2, T>>, +i: Nat, +h: {Nat.is_le(SC.length(Maybe<&2, T>, vl), i) == True{} : Bool}) -> {S.val_of(T, vl, i) == None{} : Maybe<&2, T>}:
53	  match vl i:
54	    case Nil{} _:
55	      {==}
56	    case Con{m, t} 0n:
57	      Empty.absurd({m == None{} : Maybe<&2, T>}, L.false_true(h))
58	    case Con{m, +t} 1n+p:
59	      val_hi(T, t, p, h)
60	
61	# ---- generations ----
62	
63	def gen_nth0(+gl: List<&2, U32>, +i: Nat) -> {S.gen_of(gl, i) == W32.nth0(gl, i) : U32}:
64	  match gl i:
65	    case Nil{} _:
66	      {==}
67	    case Con{g, t} 0n:
68	      {==}
69	    case Con{g, +t} 1n+p:
70	      gen_nth0(t, p)
71	
72	def nth0_take(+gl: List<&2, U32>, +n: Nat, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {W32.nth0(SC.take(U32, gl, n), i) == W32.nth0(gl, i) : U32}:
73	  match gl n i:
74	    case Nil{} _ _:
75	      {==}
76	    case Con{g, t} 0n _:
77	      Empty.absurd({W32.nth0(Nil{}, i) == W32.nth0(Con{g, t}, i) : U32}, N.lt_zero_absurd(i, h))
78	    case Con{g, t} 1n+p 0n:
79	      {==}
80	    case Con{g, +t} 1n+p 1n+q:
81	      nth0_take(t, p, q, h)
82	
83	def gen_take(+gl: List<&2, U32>, +n: Nat, +i: Nat, +h: {Nat.is_lt(i, n) == True{} : Bool}) -> {S.gen_of(SC.take(U32, gl, n), i) == W32.nth0(gl, i) : U32}:
84	  Equal.trans(U32, S.gen_of(SC.take(U32, gl, n), i), W32.nth0(SC.take(U32, gl, n), i), W32.nth0(gl, i), gen_nth0(SC.take(U32, gl, n), i), nth0_take(gl, n, i, h))
85	
86	def gen_snoc(+gl: List<&2, U32>, +g: U32) -> {S.gen_of(SC.snoc(U32, gl, g), SC.length(U32, gl)) == g : U32}:
87	  match gl:
88	    case Nil{}:
89	      {==}
90	    case Con{x, +t}:
91	      gen_snoc(t, g)
92	
93	# ---- prefixes ----
94	
95	def take_upd_succ(-X: Data, +xs: List<&2, X>, +n: Nat, +v: X, +h: {Nat.is_lt(n, SC.length(X, xs)) == True{} : Bool}) -> {SC.take(X, SC.update(X, xs, n, v), 1n+n) == SC.snoc(X, SC.take(X, xs, n), v) : List<&2, X>}:
96	  match xs n:
97	    case Nil{} _:
98	      Empty.absurd({Nil{} == SC.snoc(X, Nil{}, v) : List<&2, X>}, N.lt_zero_absurd(n, h))
99	    case Con{x, +t} 0n:
100	      LL.cons_cong(X, v, SC.take(X, t, 0n), Nil{}, LL.sc_take_zero(X, t))
101	    case Con{x, +t} 1n+p:
102	      LL.cons_cong(X, x, SC.take(X, SC.update(X, t, p, v), 1n+p), SC.snoc(X, SC.take(X, t, p), v), take_upd_succ(X, t, p, v, h))
103	
104	def upd_snoc(-X: Data, +ys: List<&2, X>, +dv: X, +v: X) -> {SC.update(X, SC.snoc(X, ys, dv), SC.length(X, ys), v) == SC.snoc(X, ys, v) : List<&2, X>}:
105	  match ys:
106	    case Nil{}:
107	      {==}
108	    case Con{y, +t}:
109	      LL.cons_cong(X, y, SC.update(X, SC.snoc(X, t, dv), SC.length(X, t), v), SC.snoc(X, t, v), upd_snoc(X, t, dv, v))
110	
111	def take_succ_u(+xs: List<&2, U32>, +n: Nat, +h: {Nat.is_lt(n, SC.length(U32, xs)) == True{} : Bool}) -> {SC.take(U32, xs, 1n+n) == SC.snoc(U32, SC.take(U32, xs, n), W32.nth0(xs, n)) : List<&2, U32>}:
112	  match xs n:
113	    case Nil{} _:
114	      Empty.absurd({Nil{} == SC.snoc(U32, Nil{}, 0) : List<&2, U32>}, N.lt_zero_absurd(n, h))
115	    case Con{x, +t} 0n:
116	      LL.cons_cong(U32, x, SC.take(U32, t, 0n), Nil{}, LL.sc_take_zero(U32, t))
117	    case Con{x, +t} 1n+p:
118	      LL.cons_cong(U32, x, SC.take(U32, t, 1n+p), SC.snoc(U32, SC.take(U32, t, p), W32.nth0(t, p)), take_succ_u(t, p, h))
119	
120	# ---- the live-listed component, pointwise ----
121	
122	def or_nt(+b: Bool, +c: Bool, +h: {Bool.or(Bool.not(b), c) == True{} : Bool}, +hb: {b == True{} : Bool}) -> {c == True{} : Bool}:
123	  L.subst(Bool, z => {Bool.or(Bool.not(z), c) == True{} : Bool}, b, True{}, hb, h)
124	
125	# every live index x (from k) is the id k + x of sl
126	def lvin_elim(~T: Data, +vl: List<&2, Maybe<&2, T>>, +k: Nat, +sl: List<&2, Nat>, +h: {ST.lvin(~T, vl, k, sl) == True{} : Bool}, +x: Nat, +hx: {ST.some_b(T, S.val_of(T, vl, x)) == True{} : Bool}) -> {NL.memn(Nat.add(k, x), sl) == True{} : Bool}:
127	  match vl x:
128	    case Nil{} _:
129	      Empty.absurd({NL.memn(Nat.add(k, x), sl) == True{} : Bool}, L.false_true(hx))
130	    case Con{+m, +t} 0n:
131	      +h0 = L.and_left(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h)
132	      L.subst(Nat, z => {NL.memn(z, sl) == True{} : Bool}, k, Nat.add(k, 0n), Equal.sym(Nat, Nat.add(k, 0n), k, N.add_zero(k)), or_nt(ST.some_b(T, m), NL.memn(k, sl), h0, hx))
133	    case Con{+m, +t} 1n+p:
134	      +ih = lvin_elim(~T, t, 1n+k, sl, L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h), p, hx)
135	      L.subst(Nat, z => {NL.memn(z, sl) == True{} : Bool}, 1n+Nat.add(k, p), Nat.add(k, 1n+p), Equal.sym(Nat, Nat.add(k, 1n+p), 1n+Nat.add(k, p), N.add_succ(k, p)), ih)
136	
137	
138	def or_tr2(+a: Bool, +b: Bool, +h: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}:
139	  L.subst(Bool, z => {Bool.or(a, z) == True{} : Bool}, True{}, b, Equal.sym(Bool, b, True{}, h), NL.or_true_b(a))
140	
141	# a write of a value at a listed index
142	def lvin_upd(~T: Data, +vl: List<&2, Maybe<&2, T>>, +k: Nat, +sl: List<&2, Nat>, +j: Nat, +v: Maybe<&2, T>, +h: {ST.lvin(~T, vl, k, sl) == True{} : Bool}, +hm: {NL.memn(Nat.add(k, j), sl) == True{} : Bool}) -> {ST.lvin(~T, SC.update(Maybe<&2, T>, vl, j, v), k, sl) == True{} : Bool}:
143	  match vl j:
144	    case Nil{} _:
145	      {==}
146	    case Con{+m, +t} 0n:
147	      +hm0 = L.subst(Nat, z => {NL.memn(z, sl) == True{} : Bool}, Nat.add(k, 0n), k, N.add_zero(k), hm)
148	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, v)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), or_tr2(Bool.not(ST.some_b(T, v)), NL.memn(k, sl), hm0), L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h))
149	    case Con{+m, +t} 1n+p:
150	      +hm1 = L.subst(Nat, z => {NL.memn(z, sl) == True{} : Bool}, Nat.add(k, 1n+p), 1n+Nat.add(k, p), N.add_succ(k, p), hm)
151	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, SC.update(Maybe<&2, T>, t, p, v), 1n+k, sl), L.and_left(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h), lvin_upd(~T, t, 1n+k, sl, p, v, L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h), hm1))
152	
153	# a write of None
154	def lvin_none(~T: Data, +vl: List<&2, Maybe<&2, T>>, +k: Nat, +sl: List<&2, Nat>, +j: Nat, +h: {ST.lvin(~T, vl, k, sl) == True{} : Bool}) -> {ST.lvin(~T, SC.update(Maybe<&2, T>, vl, j, None{}), k, sl) == True{} : Bool}:
155	  match vl j:
156	    case Nil{} _:
157	      {==}
158	    case Con{+m, +t} 0n:
159	      L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h)
160	    case Con{+m, +t} 1n+p:
161	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, SC.update(Maybe<&2, T>, t, p, None{}), 1n+k, sl), L.and_left(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h), lvin_none(~T, t, 1n+k, sl, p, L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h)))
162	
163	# ---- ids of one list among another's ----
164	
165	def subn(xs: List<&2, Nat>, +ys: List<&2, Nat>) -> Bool:
166	  match xs:
167	    case Nil{}:
168	      True{}
169	    case Con{+x, t}:
170	      Bool.and(NL.memn(x, ys), subn(t, ys))
171	
172	def subn_c(+x: Nat, +y: Nat, +t: List<&2, Nat>, +ys: List<&2, Nat>, +hy: {NL.memn(y, ys) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(y, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hm2: {NL.memn(x, t) == True{} : Bool} -> {NL.memn(x, ys) == True{} : Bool}) -> {NL.memn(x, ys) == True{} : Bool}:
173	  match c:
174	    case True{}:
175	      L.subst(Nat, z => {NL.memn(z, ys) == True{} : Bool}, y, x, N.eq_from_is_eq(y, x, hc), hy)
176	    case False{}:
177	      rec(hm)
178	
179	def subn_mem(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +x: Nat, +h: {subn(xs, ys) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {NL.memn(x, ys) == True{} : Bool}:
180	  match xs:
181	    case Nil{}:
182	      Empty.absurd({NL.memn(x, ys) == True{} : Bool}, L.false_true(hm))
183	    case Con{+y, +t}:
184	      subn_c(x, y, t, ys, L.and_left(NL.memn(y, ys), subn(t, ys), h), Nat.is_eq(y, x), {==}, hm, hm2 => subn_mem(t, ys, x, L.and_right(NL.memn(y, ys), subn(t, ys), h), hm2))
185	
186	def subn_wk(+xs: List<&2, Nat>, +ys: List<&2, Nat>, +y: Nat, +h: {subn(xs, ys) == True{} : Bool}) -> {subn(xs, Con{y, ys}) == True{} : Bool}:
187	  match xs:
188	    case Nil{}:
189	      {==}
190	    case Con{+x, +t}:
191	      L.and_intro(NL.memn(x, Con{y, ys}), subn(t, Con{y, ys}), NL.or_tr(Nat.is_eq(y, x), NL.memn(x, ys), L.and_left(NL.memn(x, ys), subn(t, ys), h)), subn_wk(t, ys, y, L.and_right(NL.memn(x, ys), subn(t, ys), h)))
192	
193	def subn_refl(+xs: List<&2, Nat>) -> {subn(xs, xs) == True{} : Bool}:
194	  match xs:
195	    case Nil{}:
196	      {==}
197	    case Con{+x, +t}:
198	      L.and_intro(NL.memn(x, Con{x, t}), subn(t, Con{x, t}), RL.self_in(x, t), subn_wk(t, t, x, subn_refl(t)))
199	
200	def mem2_c(+x: Nat, +y: Nat, +z: Nat, +ys: List<&2, Nat>, +c: Bool, +h: {Bool.or(c, NL.memn(x, ys)) == True{} : Bool}) -> {Bool.or(c, Bool.or(Nat.is_eq(z, x), NL.memn(x, ys))) == True{} : Bool}:
201	  match c:
202	    case True{}:
203	      {==}
204	    case False{}:
205	      NL.or_tr(Nat.is_eq(z, x), NL.memn(x, ys), h)
206	
207	def subn_wk2(+xs: List<&2, Nat>, +y: Nat, +z: Nat, +ys: List<&2, Nat>, +h: {subn(xs, Con{y, ys}) == True{} : Bool}) -> {subn(xs, Con{y, Con{z, ys}}) == True{} : Bool}:
208	  match xs:
209	    case Nil{}:
210	      {==}
211	    case Con{+x, +t}:
212	      L.and_intro(NL.memn(x, Con{y, Con{z, ys}}), subn(t, Con{y, Con{z, ys}}), mem2_c(x, y, z, ys, Nat.is_eq(y, x), L.and_left(NL.memn(x, Con{y, ys}), subn(t, Con{y, ys}), h)), subn_wk2(t, y, z, ys, L.and_right(NL.memn(x, Con{y, ys}), subn(t, Con{y, ys}), h)))
213	
214	
215	# a ++ b among a ++ n :: b
216	def subn_ins(+a: List<&2, Nat>, +b: List<&2, Nat>, +n: Nat) -> {subn(SC.append(Nat, a, b), SC.append(Nat, a, Con{n, b})) == True{} : Bool}:
217	  match a:
218	    case Nil{}:
219	      subn_wk(b, b, n, subn_refl(b))
220	    case Con{+x, +t}:
221	      L.and_intro(NL.memn(x, Con{x, SC.append(Nat, t, Con{n, b})}), subn(SC.append(Nat, t, b), Con{x, SC.append(Nat, t, Con{n, b})}), RL.self_in(x, SC.append(Nat, t, Con{n, b})), subn_wk(SC.append(Nat, t, b), SC.append(Nat, t, Con{n, b}), x, subn_ins(t, b, n)))
222	
223	# a ++ s :: b among s :: a ++ b
224	def subn_rm(+a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>) -> {subn(SC.append(Nat, a, Con{s, b}), Con{s, SC.append(Nat, a, b)}) == True{} : Bool}:
225	  match a:
226	    case Nil{}:
227	      subn_refl(Con{s, b})
228	    case Con{+x, +t}:
229	      L.and_intro(NL.memn(x, Con{s, Con{x, SC.append(Nat, t, b)}}), subn(SC.append(Nat, t, Con{s, b}), Con{s, Con{x, SC.append(Nat, t, b)}}), NL.or_tr(Nat.is_eq(s, x), NL.memn(x, Con{x, SC.append(Nat, t, b)}), RL.self_in(x, SC.append(Nat, t, b))), subn_wk2(SC.append(Nat, t, Con{s, b}), s, x, SC.append(Nat, t, b), subn_rm(t, s, b)))
230	
231	def ornc(-T: Data, +m: Maybe<&2, T>, +c: Bool, +c0: Bool, +h: {Bool.or(Bool.not(ST.some_b(T, m)), c0) == True{} : Bool}, f: @hc: {c0 == True{} : Bool} -> {c == True{} : Bool}) -> {Bool.or(Bool.not(ST.some_b(T, m)), c) == True{} : Bool}:
232	  match m:
233	    case None{}:
234	      {==}
235	    case Some{v}:
236	      f(h)
237	
238	# a larger list of ids
239	def lvin_sub(~T: Data, +vl: List<&2, Maybe<&2, T>>, +k: Nat, +sl: List<&2, Nat>, +sl2: List<&2, Nat>, +h: {ST.lvin(~T, vl, k, sl) == True{} : Bool}, +hs: {subn(sl, sl2) == True{} : Bool}) -> {ST.lvin(~T, vl, k, sl2) == True{} : Bool}:
240	  match vl:
241	    case Nil{}:
242	      {==}
243	    case Con{+m, +t}:
244	      +h0 = ornc(T, m, NL.memn(k, sl2), NL.memn(k, sl), L.and_left(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h), hk => subn_mem(sl, sl2, k, hs, hk))
245	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl2)), ST.lvin(~T, t, 1n+k, sl2), h0, lvin_sub(~T, t, 1n+k, sl, sl2, L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h), hs))
246	
247	# indices from k are all above s: s can be dropped
248	def lvin_low(~T: Data, +vl: List<&2, Maybe<&2, T>>, +k: Nat, +s: Nat, +sl: List<&2, Nat>, +h: {ST.lvin(~T, vl, k, Con{s, sl}) == True{} : Bool}, +hlt: {Nat.is_lt(s, k) == True{} : Bool}) -> {ST.lvin(~T, vl, k, sl) == True{} : Bool}:
249	  match vl:
250	    case Nil{}:
251	      {==}
252	    case Con{+m, +t}:
253	      +hne = N.is_eq_lt(s, k, hlt)
254	      +h0 = ornc(T, m, NL.memn(k, sl), NL.memn(k, Con{s, sl}), L.and_left(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, Con{s, sl})), ST.lvin(~T, t, 1n+k, Con{s, sl}), h), hk => L.subst(Bool, z => {Bool.or(z, NL.memn(k, sl)) == True{} : Bool}, Nat.is_eq(s, k), False{}, hne, hk))
255	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h0, lvin_low(~T, t, 1n+k, s, sl, L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, Con{s, sl})), ST.lvin(~T, t, 1n+k, Con{s, sl}), h), N.lt_trans(s, k, 1n+k, hlt, N.lt_succ(k))))
256	
257	# the id s = k + j with a vacant value can be dropped
258	def lvin_skip(~T: Data, +vl: List<&2, Maybe<&2, T>>, +k: Nat, +j: Nat, +sl: List<&2, Nat>, +h: {ST.lvin(~T, vl, k, Con{Nat.add(k, j), sl}) == True{} : Bool}, +hv: {ST.some_b(T, S.val_of(T, vl, j)) == False{} : Bool}) -> {ST.lvin(~T, vl, k, sl) == True{} : Bool}:
259	  match vl j:
260	    case Nil{} _:
261	      {==}
262	    case Con{+m, +t} 0n:
263	      +h1 = L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, Con{Nat.add(k, 0n), sl})), ST.lvin(~T, t, 1n+k, Con{Nat.add(k, 0n), sl}), h)
264	      +h1b = L.subst(Nat, z => {ST.lvin(~T, t, 1n+k, Con{z, sl}) == True{} : Bool}, Nat.add(k, 0n), k, N.add_zero(k), h1)
265	      +h0 = L.subst(Bool, z => {Bool.or(Bool.not(z), NL.memn(k, sl)) == True{} : Bool}, False{}, ST.some_b(T, m), Equal.sym(Bool, ST.some_b(T, m), False{}, hv), {==})
266	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h0, lvin_low(~T, t, 1n+k, k, sl, h1b, N.lt_succ(k)))
267	    case Con{+m, +t} 1n+p:
268	      +e = N.add_succ(k, p)
269	      +hne = N.is_eq_lt(k, 1n+Nat.add(k, p), N.le_lt_succ(k, Nat.add(k, p), N.le_add_right(k, p)))
270	      +hne2 = L.subst(Nat, z => {Nat.is_eq(z, k) == False{} : Bool}, 1n+Nat.add(k, p), Nat.add(k, 1n+p), Equal.sym(Nat, Nat.add(k, 1n+p), 1n+Nat.add(k, p), e), N.is_eq_sym_false(k, 1n+Nat.add(k, p), hne))
271	      +h0 = ornc(T, m, NL.memn(k, sl), NL.memn(k, Con{Nat.add(k, 1n+p), sl}), L.and_left(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, Con{Nat.add(k, 1n+p), sl})), ST.lvin(~T, t, 1n+k, Con{Nat.add(k, 1n+p), sl}), h), hk => L.subst(Bool, z => {Bool.or(z, NL.memn(k, sl)) == True{} : Bool}, Nat.is_eq(Nat.add(k, 1n+p), k), False{}, hne2, hk))
272	      +h1 = L.and_right(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, Con{Nat.add(k, 1n+p), sl})), ST.lvin(~T, t, 1n+k, Con{Nat.add(k, 1n+p), sl}), h)
273	      +h1b = L.subst(Nat, z => {ST.lvin(~T, t, 1n+k, Con{z, sl}) == True{} : Bool}, Nat.add(k, 1n+p), Nat.add(1n+k, p), e, h1)
274	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, m)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h0, lvin_skip(~T, t, 1n+k, p, sl, h1b, hv))
275	
276	def lvin_rep(~T: Data, +m: Nat, +k: Nat, +sl: List<&2, Nat>) -> {ST.lvin(~T, SC.replicate(Maybe<&2, T>, m, None{}), k, sl) == True{} : Bool}:
277	  match m:
278	    case 0n:
279	      {==}
280	    case 1n+p:
281	      lvin_rep(~T, p, 1n+k, sl)
282	
283	# vacant slots appended
284	def lvin_grow(~T: Data, +vl: List<&2, Maybe<&2, T>>, +k: Nat, +sl: List<&2, Nat>, +m: Nat, +h: {ST.lvin(~T, vl, k, sl) == True{} : Bool}) -> {ST.lvin(~T, SC.append(Maybe<&2, T>, vl, SC.replicate(Maybe<&2, T>, m, None{})), k, sl) == True{} : Bool}:
285	  match vl:
286	    case Nil{}:
287	      lvin_rep(~T, m, k, sl)
288	    case Con{+x, +t}:
289	      L.and_intro(Bool.or(Bool.not(ST.some_b(T, x)), NL.memn(k, sl)), ST.lvin(~T, SC.append(Maybe<&2, T>, t, SC.replicate(Maybe<&2, T>, m, None{})), 1n+k, sl), L.and_left(Bool.or(Bool.not(ST.some_b(T, x)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h), lvin_grow(~T, t, 1n+k, sl, m, L.and_right(Bool.or(Bool.not(ST.some_b(T, x)), NL.memn(k, sl)), ST.lvin(~T, t, 1n+k, sl), h)))
290	
291	# ---- the zero-generation component ----
292	
293	def gz_at(+gl: List<&2, U32>, +fr: Nat, +h: {ST.gz(gl, fr) == True{} : Bool}, +hl: {Nat.is_lt(fr, SC.length(U32, gl)) == True{} : Bool}) -> {W32.nth0(gl, fr) == 0 : U32}:
294	  match gl fr:
295	    case Nil{} _:
296	      Empty.absurd({W32.nth0(Nil{}, fr) == 0 : U32}, N.lt_zero_absurd(fr, hl))
297	    case Con{+g, +t} 0n:
298	      A.eq_of(g, 0, L.and_left(U32.is_eq(g, 0), ST.gz(t, 0n), h))
299	    case Con{+g, +t} 1n+p:
300	      gz_at(t, p, h, hl)
301	
302	def gz_succ(+gl: List<&2, U32>, +fr: Nat, +h: {ST.gz(gl, fr) == True{} : Bool}) -> {ST.gz(gl, 1n+fr) == True{} : Bool}:
303	  match gl fr:
304	    case Nil{} _:
305	      {==}
306	    case Con{+g, +t} 0n:
307	      L.and_right(U32.is_eq(g, 0), ST.gz(t, 0n), h)
308	    case Con{+g, +t} 1n+p:
309	      gz_succ(t, p, h)
310	
311	def gz_upd(+gl: List<&2, U32>, +fr: Nat, +i: Nat, +v: U32, +h: {ST.gz(gl, fr) == True{} : Bool}, +hi: {Nat.is_lt(i, fr) == True{} : Bool}) -> {ST.gz(SC.update(U32, gl, i, v), fr) == True{} : Bool}:
312	  match gl fr i:
313	    case Nil{} _ _:
314	      {==}
315	    case Con{g, t} 0n _:
316	      Empty.absurd({ST.gz(SC.update(U32, Con{g, t}, i, v), 0n) == True{} : Bool}, N.lt_zero_absurd(i, hi))
317	    case Con{g, t} 1n+q 0n:
318	      h
319	    case Con{g, +t} 1n+q 1n+p:
320	      gz_upd(t, q, p, v, h, hi)
321	
322	def gz_rep(+m: Nat) -> {ST.gz(SC.replicate(U32, m, 0), 0n) == True{} : Bool}:
323	  match m:
324	    case 0n:
325	      {==}
326	    case 1n+p:
327	      gz_rep(p)
328	
329	def gz_grow(+gl: List<&2, U32>, +m: Nat) -> {ST.gz(SC.append(U32, gl, SC.replicate(U32, m, 0)), SC.length(U32, gl)) == True{} : Bool}:
330	  match gl:
331	    case Nil{}:
332	      gz_rep(m)
333	    case Con{g, +t}:
334	      gz_grow(t, m)