proofs/containers/doubly_linked_list/vals.bend
bend-collections-laws-containers@1.0.0.0 · 334 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/u32alg.bend as A
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
6import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
7import bend-collections-laws-containers@1.0.0.0/spec/containers/doubly_linked_list.bend as S
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/state.bend as ST
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/doubly_linked_list/rel.bend as RL
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
11import bend-collections-laws-containers@1.0.0.0/proofs/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
19def 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
28def 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
41def 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
52def 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
63def 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
72def 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
83def 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
86def 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
95def 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
104def 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
111def 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
122def 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
126def 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
138def 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
142def 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
154def 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
165def 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
172def 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
179def 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
186def 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
193def 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
200def 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
207def 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
216def 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
224def 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
231def 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
239def 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
248def 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
258def 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
276def 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
284def 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
293def 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
302def 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
311def 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
322def 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
329def 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)