proof_digits.bend
lawful-fields@0.1.1.0 · 795 lines · 48 definitions
1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-fields@0.1.1.0/defs.bend as F
5import lawful-fields@0.1.1.0/fields.bend as FC
6import lawful-bytes@0.1.1.0/proof_seq.bend as Q
7import lawful-bytes@0.1.1.0/proof_core.bend as C
8import lawful-bytes@0.1.1.0/proof_ops.bend as O
9import lawful-bytes@0.1.1.0/proof_same.bend as SM
10import lawful-bytes@0.1.1.0/proof_shift.bend as H
11import lawful-bytes@0.1.1.0/proof_grow.bend as G
12import lawful-words@0.1.0.0/proof_nat.bend as N
13import lawful-words@0.1.0.0/proof_u32.bend as U
14import lawful-arrays@0.1.0.0/proof_base.bend as AB
15import lawful-arrays@0.1.0.0/proof_tree.bend as P
16
17
18
19
20
21
22
23
24def alld(xs: List<&2, U32>) -> Bool:
25 match xs:
26 case Nil{}:
27 True{}
28 case Con{+x, t}:
29 Bool.and(Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57)), alld(t))
30
31law and_true:
32 for +a: Bool
33 {Bool.and(a, True{}) == a : Bool}
34
35def and_true(a):
36 match a:
37 case True{}:
38 {==}
39 case False{}:
40 {==}
41
42law push_some:
43 for +a: Nat
44 for +x: U32
45 for +b: Bool
46 {Maybe.is_some(&2, Nat, F.dec.push(Some{a}, F.digit.if(x, b))) == b : Bool}
47
48def push_some(a, x, b):
49 match b:
50 case True{}:
51 {==}
52 case False{}:
53 {==}
54
55law push_and:
56 for +m: Maybe<&2, Nat>
57 for +x: U32
58 for +r: Bool
59 {Bool.and(Maybe.is_some(&2, Nat, F.dec.push(m, F.digit(x))), r) == Bool.and(Bool.and(Maybe.is_some(&2, Nat, m), Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))), r) : Bool}
60
61def push_and(m, x, r):
62 match m:
63 case None{}:
64 {==}
65 case Some{+a}:
66 +isd = Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))
67 %Equal.sym(Bool, Maybe.is_some(&2, Nat, F.dec.push(Some{a}, F.digit.if(x, isd))), isd, push_some(a, x, isd)) :
68 {Bool.and(_, r) == Bool.and(Bool.and(True{}, isd), r) : Bool}
69 {==}
70
71
72law go_some:
73 for +ys: List<&2, U32>
74 for +m: Maybe<&2, Nat>
75 {Maybe.is_some(&2, Nat, F.dec.go(ys, m)) == Bool.and(Maybe.is_some(&2, Nat, m), alld(ys)) : Bool}
76
77def go_some(ys, m):
78 match ys:
79 case Nil{}:
80 Equal.sym(Bool, Bool.and(Maybe.is_some(&2, Nat, m), True{}), Maybe.is_some(&2, Nat, m), and_true(Maybe.is_some(&2, Nat, m)))
81 case Con{+x, t}:
82 +isd = Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))
83 +m2 = F.dec.push(m, F.digit(x))
84 %Equal.sym(Bool, Maybe.is_some(&2, Nat, F.dec.go(t, m2)), Bool.and(Maybe.is_some(&2, Nat, m2), alld(t)), go_some(t, m2)) :
85 {_ == Bool.and(Maybe.is_some(&2, Nat, m), Bool.and(isd, alld(t))) : Bool}
86 %SM.and_assoc(Maybe.is_some(&2, Nat, m), isd, alld(t)) :
87 {Bool.and(Maybe.is_some(&2, Nat, m2), alld(t)) == _ : Bool}
88 push_and(m, x, alld(t))
89
90law ne_dec:
91 for +ys: List<&2, U32>
92 for +h: {Nat.is_lt(0n, List.length(&2, U32, ys)) == True{} : Bool}
93 {Maybe.is_some(&2, Nat, F.dec(ys)) == alld(ys) : Bool}
94
95def ne_dec(ys, h):
96 match ys:
97 case Nil{}:
98 Empty.absurd({Maybe.is_some(&2, Nat, F.dec(Nil{})) == alld(Nil{}) : Bool}, AB.false_ne_true(h))
99 case Con{+y, t}:
100 go_some(y <> t, Some{0n})
101
102law dg_pair:
103 for +n: Nat
104 for +len: U32
105 for +t: P.Tree<U32>
106 for +j: U32
107 for +ok: Bool
108 {FC.digits.go(n, B.at(C.BT(len, t), j), j, ok) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits.go(n, B.at(C.BT(len, t), j), j, ok))) : D.Bytes & Bool}
109
110def dg_pair(n, len, t, j, ok):
111 match n:
112 case 0n:
113 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) :
114 {FC.digits.go(0n, _, j, ok) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits.go(0n, _, j, ok))) : D.Bytes & Bool}
115 {==}
116 case 1n+m:
117 +x = C.AT(len, t, j)
118 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) :
119 {FC.digits.go(1n+m, _, j, ok) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits.go(1n+m, _, j, ok))) : D.Bytes & Bool}
120 dg_pair(m, len, t, (j + 1 : U32), Bool.and(ok, Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))))
121
122law dg_view:
123 for +n: Nat
124 for +len: U32
125 for +t: P.Tree<U32>
126 for +d: Nat
127 for +j: U32
128 for +ok: Bool
129 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
130 for +hs: {Nat.is_le(Nat.add(U32.to_nat(j), n), U32.to_nat(len)) == True{} : Bool}
131 {Pair.snd(D.Bytes, Bool, FC.digits.go(n, B.at(C.BT(len, t), j), j, ok)) == Bool.and(ok, alld(D.slice(D.view(C.BT(len, t)), U32.to_nat(j), n))) : Bool}
132
133def dg_view(n, len, t, d, j, ok, h, hs):
134 match n:
135 case 0n:
136 +X = List.drop(&2, U32, D.view(C.BT(len, t)), U32.to_nat(j))
137 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), C.AT(len, t, j)), C.at_pair_t(len, t, j)) :
138 {Pair.snd(D.Bytes, Bool, FC.digits.go(0n, _, j, ok)) == Bool.and(ok, alld(List.take(&2, U32, X, 0n))) : Bool}
139 %Equal.sym(List<&2, U32>, List.take(&2, U32, X, 0n), Nil{}, Q.take_zero(X)) : {ok == Bool.and(ok, alld(_)) : Bool}
140 Equal.sym(Bool, Bool.and(ok, True{}), ok, and_true(ok))
141 case 1n+m:
142 +x = C.AT(len, t, j)
143 +j1 = (j + 1 : U32)
144 +isd = Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))
145 +xs = D.view(C.BT(len, t))
146 +RHS = Bool.and(ok, alld(D.slice(xs, U32.to_nat(j), 1n+m)))
147 %Equal.sym(D.Bytes & U32, B.at(C.BT(len, t), j), (C.BT(len, t), x), C.at_pair_t(len, t, j)) :
148 {Pair.snd(D.Bytes, Bool, FC.digits.go(1n+m, _, j, ok)) == RHS : Bool}
149 %Equal.sym(Bool, Pair.snd(D.Bytes, Bool, FC.digits.go(m, B.at(C.BT(len, t), j1), j1, Bool.and(ok, isd))),
150 Bool.and(Bool.and(ok, isd), alld(D.slice(xs, U32.to_nat(j1), m))),
151 dg_view(m, len, t, d, j1, Bool.and(ok, isd), h, SM.step_le(len, t, d, j, m, h, hs))) :
152 {_ == RHS : Bool}
153 %Equal.sym(List<&2, U32>, D.slice(xs, U32.to_nat(j), 1n+m), x <> D.slice(xs, Nat.add(U32.to_nat(j), 1n), m),
154 SM.slice_cons(xs, U32.to_nat(j), m, x, SM.step_val(len, t, d, j, m, h, hs))) :
155 {Bool.and(Bool.and(ok, isd), alld(D.slice(xs, U32.to_nat(j1), m))) == Bool.and(ok, alld(_)) : Bool}
156 %Equal.sym(Nat, U32.to_nat(j1), Nat.add(U32.to_nat(j), 1n), SM.step_inc(len, t, d, j, m, h, hs)) :
157 {Bool.and(Bool.and(ok, isd), alld(D.slice(xs, _, m))) == Bool.and(ok, Bool.and(isd, alld(D.slice(xs, Nat.add(U32.to_nat(j), 1n), m)))) : Bool}
158 SM.and_assoc(ok, isd, alld(D.slice(xs, Nat.add(U32.to_nat(j), 1n), m)))
159
160law digits_pair_t:
161 for +len: U32
162 for +t: P.Tree<U32>
163 for +from: U32
164 for +to: U32
165 {FC.digits(C.BT(len, t), from, to) == (C.BT(len, t), Pair.snd(D.Bytes, Bool, FC.digits(C.BT(len, t), from, to))) : D.Bytes & Bool}
166
167def digits_pair_t(len, t, from, to):
168 dg_pair(Nat.sub(U32.to_nat(to), U32.to_nat(from)), len, t, from, U32.is_lt(from, to))
169
170
171law dtop:
172 for +n: Nat
173 for +from: U32
174 for +to: U32
175 for +xs: List<&2, U32>
176 for +hn: {Nat.sub(U32.to_nat(to), U32.to_nat(from)) == n : Nat}
177 for +hle: {Nat.is_le(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
178 for +hlen: {Nat.is_le(Nat.add(U32.to_nat(from), n), List.length(&2, U32, xs)) == True{} : Bool}
179 {Bool.and(U32.is_lt(from, to), alld(D.slice(xs, U32.to_nat(from), n))) == Maybe.is_some(&2, Nat, F.dec(D.slice(xs, U32.to_nat(from), n))) : Bool}
180
181def dtop(n, from, to, xs, hn, hle, hlen):
182 match n:
183 case 0n:
184 +FF = U32.to_nat(from)
185 +TT = U32.to_nat(to)
186 +X = List.drop(&2, U32, xs, FF)
187 +e1 = AB.subst(Nat, y => {Nat.add(FF, y) == TT : Nat}, Nat.sub(TT, FF), 0n, hn, N.le_sub_add(FF, TT, hle))
188 +eFT = Equal.trans(Nat, FF, Nat.add(FF, 0n), TT, Equal.sym(Nat, Nat.add(FF, 0n), FF, N.add_zero(FF)), e1)
189 +hlt = Equal.trans(Bool, U32.is_lt(from, to), Nat.is_lt(FF, TT), False{}, U.is_lt_to_nat(from, to),
190 AB.subst(Nat, y => {Nat.is_lt(FF, y) == False{} : Bool}, FF, TT, eFT, N.lt_irrefl(FF)))
191 %Equal.sym(List<&2, U32>, List.take(&2, U32, X, 0n), Nil{}, Q.take_zero(X)) :
192 {Bool.and(U32.is_lt(from, to), alld(_)) == Maybe.is_some(&2, Nat, F.dec(_)) : Bool}
193 %Equal.sym(Bool, U32.is_lt(from, to), False{}, hlt) : {Bool.and(_, True{}) == False{} : Bool}
194 {==}
195 case 1n+k:
196 +FF = U32.to_nat(from)
197 +TT = U32.to_nat(to)
198 +X = List.drop(&2, U32, xs, FF)
199 +S = D.slice(xs, FF, 1n+k)
200 +e1 = AB.subst(Nat, y => {Nat.add(FF, y) == TT : Nat}, Nat.sub(TT, FF), 1n+k, hn, N.le_sub_add(FF, TT, hle))
201 +hlt = Equal.trans(Bool, U32.is_lt(from, to), Nat.is_lt(FF, TT), True{}, U.is_lt_to_nat(from, to),
202 SM.lt_of_le(FF, k, TT, AB.subst(Nat, y => {Nat.is_le(y, TT) == True{} : Bool}, TT, Nat.add(FF, 1n+k),
203 Equal.sym(Nat, Nat.add(FF, 1n+k), TT, e1), N.le_refl(TT))))
204 +hx = AB.subst(Nat, y => {Nat.is_le(1n+k, y) == True{} : Bool}, Nat.sub(List.length(&2, U32, xs), FF), List.length(&2, U32, X),
205 Equal.sym(Nat, List.length(&2, U32, X), Nat.sub(List.length(&2, U32, xs), FF), H.drop_length(xs, FF)),
206 N.le_sub_r(FF, 1n+k, List.length(&2, U32, xs), hlen))
207 +hne = AB.subst(Nat, y => {Nat.is_lt(0n, y) == True{} : Bool}, 1n+k, List.length(&2, U32, S),
208 Equal.sym(Nat, List.length(&2, U32, S), 1n+k, Q.take_length(X, 1n+k, hx)), {==})
209 %Equal.sym(Bool, U32.is_lt(from, to), True{}, hlt) : {Bool.and(_, alld(S)) == Maybe.is_some(&2, Nat, F.dec(S)) : Bool}
210 Equal.sym(Bool, Maybe.is_some(&2, Nat, F.dec(S)), alld(S), ne_dec(S, hne))
211
212law digits_view_t:
213 for +len: U32
214 for +t: P.Tree<U32>
215 for +d: Nat
216 for +from: U32
217 for +to: U32
218 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
219 for +hft: {U32.is_le(from, to) == True{} : Bool}
220 for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
221 {Pair.snd(D.Bytes, Bool, FC.digits(C.BT(len, t), from, to)) == F.all_digits(D.slice(D.view(C.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from)))) : Bool}
222
223def digits_view_t(len, t, d, from, to, h, hft, ht):
224 +FF = U32.to_nat(from)
225 +TT = U32.to_nat(to)
226 +NN = Nat.sub(TT, FF)
227 +xs = D.view(C.BT(len, t))
228 +hle = Equal.trans(Bool, Nat.is_le(FF, TT), U32.is_le(from, to), True{}, Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(FF, TT), U.is_le_to_nat(from, to)), hft)
229 +eFT = N.le_sub_add(FF, TT, hle)
230 +hs = AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(len)) == True{} : Bool}, TT, Nat.add(FF, NN), Equal.sym(Nat, Nat.add(FF, NN), TT, eFT), ht)
231 +hlen = AB.subst(Nat, y => {Nat.is_le(Nat.add(FF, NN), y) == True{} : Bool}, U32.to_nat(len), List.length(&2, U32, xs),
232 Equal.sym(Nat, List.length(&2, U32, xs), U32.to_nat(len), O.view_size_t(len, t, d, h)), hs)
233 Equal.trans(Bool, Pair.snd(D.Bytes, Bool, FC.digits(C.BT(len, t), from, to)), Bool.and(U32.is_lt(from, to), alld(D.slice(xs, FF, NN))),
234 Maybe.is_some(&2, Nat, F.dec(D.slice(xs, FF, NN))),
235 dg_view(NN, len, t, d, from, U32.is_lt(from, to), h, hs), dtop(NN, from, to, xs, {==}, hle, hlen))
236
237
238
239
240law eta_nn:
241 for p: Nat & Nat
242 {p == (Pair.fst(Nat, Nat, p), Pair.snd(Nat, Nat, p)) : Nat & Nat}
243
244def eta_nn(p):
245 (a, b) = p
246 {==}
247
248
249def DG(+x: Nat) -> U32:
250 U32.from_nat(Nat.add(48n, Nat.mod(x, 10n)))
251
252
253def lgo(f: Nat, +q: Nat, +d: U32, acc: List<&2, U32>) -> List<&2, U32>:
254 match f q:
255 case _ 0n:
256 d <> acc
257 case 0n 1n+p:
258 d <> acc
259 case 1n+g 1n+p:
260 lgo(g, Nat.div(1n+p, 10n), DG(1n+p), d <> acc)
261
262law show_fin:
263 for +g: Nat
264 for +q: Nat
265 for +d: U32
266 for +sacc: String
267 {F.codes(Nat.show.fin(g, sacc, (Chr{d}, q))) == lgo(g, q, d, F.codes(sacc)) : List<&2, U32>}
268
269def show_fin(g, q, d, sacc):
270 match g q:
271 case _ 0n:
272 {==}
273 case 0n 1n+p:
274 {==}
275 case 1n+h 1n+p:
276 +S = {SCon{Chr{d}, sacc} : String}
277 %Equal.sym(Nat & Nat, Nat.divmod(1n+p, 10n), (Nat.div(1n+p, 10n), Nat.mod(1n+p, 10n)), eta_nn(Nat.divmod(1n+p, 10n))) :
278 {F.codes(Nat.show.fin(h, S, Nat.show.put(_))) == lgo(1n+h, 1n+p, d, F.codes(sacc)) : List<&2, U32>}
279 show_fin(h, Nat.div(1n+p, 10n), DG(1n+p), S)
280
281law show_lgo:
282 for +m: Nat
283 {F.codes(Nat.show(m)) == lgo(m, Nat.div(m, 10n), DG(m), Nil{}) : List<&2, U32>}
284
285def show_lgo(m):
286 %Equal.sym(Nat & Nat, Nat.divmod(m, 10n), (Nat.div(m, 10n), Nat.mod(m, 10n)), eta_nn(Nat.divmod(m, 10n))) :
287 {F.codes(Nat.show.fin(m, SNil{}, Nat.show.put(_))) == lgo(m, Nat.div(m, 10n), DG(m), Nil{}) : List<&2, U32>}
288 show_fin(m, Nat.div(m, 10n), DG(m), SNil{})
289
290
291
292def BK(k: Nat) -> U32:
293 match k:
294 case 0n:
295 9
296 case 1n+a0:
297 match a0:
298 case 0n:
299 99
300 case 1n+a1:
301 match a1:
302 case 0n:
303 999
304 case 1n+a2:
305 match a2:
306 case 0n:
307 9999
308 case 1n+a3:
309 match a3:
310 case 0n:
311 99999
312 case 1n+a4:
313 match a4:
314 case 0n:
315 999999
316 case 1n+a5:
317 match a5:
318 case 0n:
319 9999999
320 case 1n+a6:
321 match a6:
322 case 0n:
323 99999999
324 case 1n+a7:
325 match a7:
326 case 0n:
327 999999999
328 case 1n+a8:
329 U32.not(0)
330
331law bk_step:
332 for +k: Nat
333 {U32.is_le(U32.div(BK(1n+k), 10), BK(k)) == True{} : Bool}
334
335def bk_step(k):
336 match k:
337 case 0n:
338 {==}
339 case 1n+a0:
340 match a0:
341 case 0n:
342 {==}
343 case 1n+a1:
344 match a1:
345 case 0n:
346 {==}
347 case 1n+a2:
348 match a2:
349 case 0n:
350 {==}
351 case 1n+a3:
352 match a3:
353 case 0n:
354 {==}
355 case 1n+a4:
356 match a4:
357 case 0n:
358 {==}
359 case 1n+a5:
360 match a5:
361 case 0n:
362 {==}
363 case 1n+a6:
364 match a6:
365 case 0n:
366 {==}
367 case 1n+a7:
368 match a7:
369 case 0n:
370 {==}
371 case 1n+a8:
372 {==}
373
374
375
376
377law s48:
378 for +r: Nat
379 for +hr: {Nat.is_lt(r, 10n) == True{} : Bool}
380 {Nat.is_le(Nat.add(r, 48n), Nat.pow(2n, 6n)) == True{} : Bool}
381
382def s48(r, hr):
383 %N.add_comm(48n, r) : {Nat.is_le(_, Nat.pow(2n, 6n)) == True{} : Bool}
384 N.le_trans(r, 10n, 16n, N.lt_to_le(r, 10n, hr), {==})
385
386
387law fits64:
388 for +x: Nat
389 for +hx: {Nat.is_le(x, Nat.pow(2n, 6n)) == True{} : Bool}
390 {Nat.is_lt(x, Nat.pow(2n, 32n)) == True{} : Bool}
391
392def fits64(x, hx):
393 N.le_lt_trans(x, Nat.pow(2n, 6n), Nat.pow(2n, 32n), hx, AB.pow_lt(6n, 32n, {==}))
394
395law dgv:
396 for +x: Nat
397 {U32.to_nat(DG(x)) == Nat.add(48n, Nat.mod(x, 10n)) : Nat}
398
399def dgv(x):
400 +X = Nat.add(48n, Nat.mod(x, 10n))
401 +hx = N.le_trans(Nat.mod(x, 10n), 10n, 16n, N.lt_to_le(Nat.mod(x, 10n), 10n, N.mod_lt(x, 10n, {==})), {==})
402 Equal.trans(Nat, U32.to_nat(U32.from_nat(X)), Nat.mod(X, Nat.pow(2n, 32n)), X, U.to_nat_from_nat_p(X), U.wrap_small_p(X, fits64(X, hx)))
403
404law dg_lt:
405 for +x: Nat
406 {U32.is_lt(DG(x), 256) == True{} : Bool}
407
408def dg_lt(x):
409 %Equal.sym(Bool, U32.is_lt(DG(x), 256), Nat.is_lt(U32.to_nat(DG(x)), U32.to_nat(256)), U.is_lt_to_nat(DG(x), 256)) : {_ == True{} : Bool}
410 %Equal.sym(Nat, U32.to_nat(DG(x)), Nat.add(48n, Nat.mod(x, 10n)), dgv(x)) : {Nat.is_lt(_, U32.to_nat(256)) == True{} : Bool}
411 N.lt_trans(Nat.mod(x, 10n), 10n, 208n, N.mod_lt(x, 10n, {==}), {==})
412
413law dg_eq_n:
414 for +n: U32
415 {U32.to_nat(U32.add(U32.mod(n, 10), 48)) == U32.to_nat(DG(U32.to_nat(n))) : Nat}
416
417def dg_eq_n(n):
418 +m = U32.to_nat(n)
419 +r = U32.to_nat(U32.mod(n, 10))
420 +er = U.to_nat_mod(n, 10)
421 +hr = AB.subst(Nat, y => {Nat.is_lt(y, 10n) == True{} : Bool}, Nat.mod(m, 10n), r, Equal.sym(Nat, r, Nat.mod(m, 10n), er), N.mod_lt(m, 10n, {==}))
422 +ea = U.to_nat_add_fits_p(U32.mod(n, 10), 48, fits64(Nat.add(U32.to_nat(U32.mod(n, 10)), U32.to_nat(48)), s48(r, hr)))
423 %Equal.sym(Nat, U32.to_nat(DG(m)), Nat.add(48n, Nat.mod(m, 10n)), dgv(m)) : {U32.to_nat(U32.add(U32.mod(n, 10), 48)) == _ : Nat}
424 %Equal.sym(Nat, U32.to_nat(U32.add(U32.mod(n, 10), 48)), Nat.add(r, U32.to_nat(48)), ea) : {_ == Nat.add(48n, Nat.mod(m, 10n)) : Nat}
425 %Equal.sym(Nat, r, Nat.mod(m, 10n), er) : {Nat.add(_, U32.to_nat(48)) == Nat.add(48n, Nat.mod(m, 10n)) : Nat}
426 N.add_comm(Nat.mod(m, 10n), 48n)
427
428
429law dg_eq:
430 for +n: U32
431 {U32.add(U32.mod(n, 10), 48) == DG(U32.to_nat(n)) : U32}
432
433def dg_eq(n):
434 U.to_nat_inj(U32.add(U32.mod(n, 10), 48), DG(U32.to_nat(n)), dg_eq_n(n))
435
436law lt10:
437 for +n: U32
438 for +hs: {U32.is_lt(n, 10) == True{} : Bool}
439 {Nat.is_lt(U32.to_nat(n), 10n) == True{} : Bool}
440
441def lt10(n, hs):
442 Equal.trans(Bool, Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U32.is_lt(n, 10), True{},
443 Equal.sym(Bool, U32.is_lt(n, 10), Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U.is_lt_to_nat(n, 10)), hs)
444
445law ge10:
446 for +n: U32
447 for +hs: {U32.is_lt(n, 10) == False{} : Bool}
448 {Nat.is_lt(U32.to_nat(n), 10n) == False{} : Bool}
449
450def ge10(n, hs):
451 Equal.trans(Bool, Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U32.is_lt(n, 10), False{},
452 Equal.sym(Bool, U32.is_lt(n, 10), Nat.is_lt(U32.to_nat(n), U32.to_nat(10)), U.is_lt_to_nat(n, 10)), hs)
453
454law dg_small_n:
455 for +n: U32
456 for +hs: {U32.is_lt(n, 10) == True{} : Bool}
457 {U32.to_nat(U32.add(n, 48)) == U32.to_nat(DG(U32.to_nat(n))) : Nat}
458
459def dg_small_n(n, hs):
460 +m = U32.to_nat(n)
461 +hm = lt10(n, hs)
462 +ea = U.to_nat_add_fits_p(n, 48, fits64(Nat.add(U32.to_nat(n), U32.to_nat(48)), s48(m, hm)))
463 %Equal.sym(Nat, U32.to_nat(DG(m)), Nat.add(48n, Nat.mod(m, 10n)), dgv(m)) : {U32.to_nat(U32.add(n, 48)) == _ : Nat}
464 %Equal.sym(Nat, U32.to_nat(U32.add(n, 48)), Nat.add(m, U32.to_nat(48)), ea) : {_ == Nat.add(48n, Nat.mod(m, 10n)) : Nat}
465 %Equal.sym(Nat, Nat.mod(m, 10n), m, N.mod_small(m, 10n, hm)) : {Nat.add(m, U32.to_nat(48)) == Nat.add(48n, _) : Nat}
466 N.add_comm(m, 48n)
467
468law dg_small:
469 for +n: U32
470 for +hs: {U32.is_lt(n, 10) == True{} : Bool}
471 {U32.add(n, 48) == DG(U32.to_nat(n)) : U32}
472
473def dg_small(n, hs):
474 U.to_nat_inj(U32.add(n, 48), DG(U32.to_nat(n)), dg_small_n(n, hs))
475
476
477
478
479law lt_add_succ:
480 for +p: Nat
481 for +y: Nat
482 {Nat.is_lt(p, Nat.add(p, 1n+y)) == True{} : Bool}
483
484def lt_add_succ(p, y):
485 %Equal.sym(Nat, Nat.add(p, 1n+y), 1n+Nat.add(p, y), N.add_succ(p, y)) : {Nat.is_lt(p, _) == True{} : Bool}
486 Equal.trans(Bool, Nat.is_lt(p, 1n+Nat.add(p, y)), Nat.is_le(p, Nat.add(p, y)), True{}, N.lt_succ_iff(p, Nat.add(p, y)), N.le_add_r(p, y))
487
488law dlt:
489 for +p: Nat
490 {Nat.is_le(Nat.div(1n+p, 10n), p) == True{} : Bool}
491
492def dlt(p):
493 +dl = N.div_lt(1n+p, 10n, 1n+p, {==}, lt_add_succ(p, Nat.add(p, Nat.mul(8n, 1n+p))))
494 Equal.trans(Bool, Nat.is_le(Nat.div(1n+p, 10n), p), Nat.is_lt(Nat.div(1n+p, 10n), 1n+p), True{},
495 Equal.sym(Bool, Nat.is_lt(Nat.div(1n+p, 10n), 1n+p), Nat.is_le(Nat.div(1n+p, 10n), p), N.lt_succ_iff(Nat.div(1n+p, 10n), p)), dl)
496
497law hdm:
498 for +m: Nat
499 {Nat.is_le(Nat.div(m, 10n), m) == True{} : Bool}
500
501def hdm(m):
502 match m:
503 case 0n:
504 {==}
505 case 1n+p:
506 N.le_trans(Nat.div(1n+p, 10n), p, 1n+p, dlt(p),
507 N.lt_to_le(p, 1n+p, Equal.trans(Bool, Nat.is_lt(p, 1n+p), Nat.is_le(p, p), True{}, N.lt_succ_iff(p, p), N.le_refl(p))))
508
509law div_mono10:
510 for +a: Nat
511 for +b: Nat
512 for +h: {Nat.is_le(a, b) == True{} : Bool}
513 {Nat.is_le(Nat.div(a, 10n), Nat.div(b, 10n)) == True{} : Bool}
514
515def div_mono10(a, b, h):
516 +x = Nat.div(b, 10n)
517 +r = Nat.mod(b, 10n)
518 +X = Nat.mul(x, 10n)
519 +hb = AB.subst(Nat, y => {Nat.is_lt(y, Nat.add(10n, X)) == True{} : Bool}, Nat.add(r, X), b,
520 Equal.trans(Nat, Nat.add(r, X), Nat.add(X, r), b, N.add_comm(r, X), N.div_mod(b, 10n)),
521 N.lt_add_mono_r(X, r, 10n, N.mod_lt(b, 10n, {==})))
522 +ha = N.le_lt_trans(a, b, Nat.add(10n, X), h, hb)
523 +h2 = AB.subst(Nat, y => {Nat.is_lt(a, y) == True{} : Bool}, Nat.mul(1n+x, 10n), Nat.mul(10n, 1n+x),
524 Equal.sym(Nat, Nat.mul(10n, 1n+x), Nat.mul(1n+x, 10n), N.mul_comm(10n, 1n+x)), ha)
525 +dl = N.div_lt(a, 10n, 1n+x, {==}, h2)
526 Equal.trans(Bool, Nat.is_le(Nat.div(a, 10n), x), Nat.is_lt(Nat.div(a, 10n), 1n+x), True{},
527 Equal.sym(Bool, Nat.is_lt(Nat.div(a, 10n), 1n+x), Nat.is_le(Nat.div(a, 10n), x), N.lt_succ_iff(Nat.div(a, 10n), x)), dl)
528
529
530law hk_step:
531 for +n: U32
532 for +j: Nat
533 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(1n+j))) == True{} : Bool}
534 {Nat.is_le(U32.to_nat(U32.div(n, 10)), U32.to_nat(BK(j))) == True{} : Bool}
535
536def hk_step(n, j, hk):
537 +m = U32.to_nat(n)
538 +Bv = U32.to_nat(BK(1n+j))
539 +bstep = Equal.trans(Bool, Nat.is_le(U32.to_nat(U32.div(BK(1n+j), 10)), U32.to_nat(BK(j))), U32.is_le(U32.div(BK(1n+j), 10), BK(j)), True{},
540 Equal.sym(Bool, U32.is_le(U32.div(BK(1n+j), 10), BK(j)), Nat.is_le(U32.to_nat(U32.div(BK(1n+j), 10)), U32.to_nat(BK(j))),
541 U.is_le_to_nat(U32.div(BK(1n+j), 10), BK(j))), bk_step(j))
542 %Equal.sym(Nat, U32.to_nat(U32.div(n, 10)), Nat.div(m, U32.to_nat(10)), U.to_nat_div(n, 10)) : {Nat.is_le(_, U32.to_nat(BK(j))) == True{} : Bool}
543 N.le_trans(Nat.div(m, 10n), Nat.div(Bv, 10n), U32.to_nat(BK(j)), div_mono10(m, Bv, hk),
544 AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(BK(j))) == True{} : Bool}, U32.to_nat(U32.div(BK(1n+j), 10)), Nat.div(Bv, 10n),
545 U.to_nat_div(BK(1n+j), 10), bstep))
546
547law ab0:
548 for +n: U32
549 for +hs: {U32.is_lt(n, 10) == False{} : Bool}
550 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(0n))) == True{} : Bool}
551 Empty
552
553def ab0(n, hs, hk):
554 AB.false_ne_true(N.le_trans(10n, U32.to_nat(n), U32.to_nat(BK(0n)), N.not_lt_le(U32.to_nat(n), 10n, ge10(n, hs)), hk))
555
556law lmax:
557 for +x: Nat
558 for +z: Nat
559 for +M: Nat
560 for +hx: {Nat.is_lt(x, M) == True{} : Bool}
561 for +hz: {z == Nat.sub(Nat.sub(M, 1n), U32.to_nat(0)) : Nat}
562 {Nat.is_le(x, z) == True{} : Bool}
563
564def lmax(x, z, M, hx, hz):
565 match M:
566 case 0n:
567 Empty.absurd({Nat.is_le(x, z) == True{} : Bool}, AB.lt_zero_absurd(x, hx))
568 case 1n+M1:
569 %Equal.sym(Nat, z, Nat.sub(Nat.sub(1n+M1, 1n), U32.to_nat(0)), hz) : {Nat.is_le(x, _) == True{} : Bool}
570 %Equal.sym(Nat, Nat.sub(Nat.sub(M1, 0n), 0n), Nat.sub(M1, 0n), N.sub_zero(Nat.sub(M1, 0n))) : {Nat.is_le(x, _) == True{} : Bool}
571 %Equal.sym(Nat, Nat.sub(M1, 0n), M1, N.sub_zero(M1)) : {Nat.is_le(x, _) == True{} : Bool}
572 Equal.trans(Bool, Nat.is_le(x, M1), Nat.is_lt(x, 1n+M1), True{}, Equal.sym(Bool, Nat.is_lt(x, 1n+M1), Nat.is_le(x, M1), N.lt_succ_iff(x, M1)), hx)
573
574
575law hkmax:
576 for +n: U32
577 {Nat.is_le(U32.to_nat(n), U32.to_nat(U32.not(0))) == True{} : Bool}
578
579def hkmax(n):
580 lmax(U32.to_nat(n), U32.to_nat(U32.not(0)), Nat.pow(2n, 32n), U.to_nat_lt_p(n), U.to_nat_not_p(0))
581
582
583
584
585
586law R:
587 for +k: Nat
588 for +small: Bool
589 for +q: Nat
590 for +f: Nat
591 for +n: U32
592 for +acc: List<&2, U32>
593 for +hs: {U32.is_lt(n, 10) == small : Bool}
594 for +hq: {Nat.div(U32.to_nat(n), 10n) == q : Nat}
595 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(k))) == True{} : Bool}
596 for +hf: {Nat.is_le(q, f) == True{} : Bool}
597 {FC.put_dec.digits(k, small, n, acc) == lgo(f, q, DG(U32.to_nat(n)), acc) : List<&2, U32>}
598
599def R(k, small, q, f, n, acc, hs, hq, hk, hf):
600 match k small q f:
601 case _ True{} 0n 0n:
602 %dg_small(n, hs) : {U32.add(n, 48) <> acc == _ <> acc : List<&2, U32>}
603 {==}
604 case _ True{} 0n 1n+g:
605 %dg_small(n, hs) : {U32.add(n, 48) <> acc == _ <> acc : List<&2, U32>}
606 {==}
607 case _ True{} 1n+p _:
608 +e0 = Equal.trans(Nat, 0n, Nat.div(U32.to_nat(n), 10n), 1n+p,
609 Equal.sym(Nat, Nat.div(U32.to_nat(n), 10n), 0n, N.div_small(U32.to_nat(n), 10n, lt10(n, hs))), hq)
610 Empty.absurd({FC.put_dec.digits(k, True{}, n, acc) == lgo(f, 1n+p, DG(U32.to_nat(n)), acc) : List<&2, U32>},
611 AB.succ_ne_zero(p, Equal.sym(Nat, 0n, 1n+p, e0)))
612 case 0n False{} _ _:
613 Empty.absurd({FC.put_dec.digits(0n, False{}, n, acc) == lgo(f, q, DG(U32.to_nat(n)), acc) : List<&2, U32>}, ab0(n, hs, hk))
614 case 1n+j False{} 0n _:
615 +m = U32.to_nat(n)
616 +edm = AB.subst(Nat, y => {Nat.add(Nat.mul(y, 10n), Nat.mod(m, 10n)) == m : Nat}, Nat.div(m, 10n), 0n, hq, N.div_mod(m, 10n))
617 +hm = AB.subst(Nat, y => {Nat.is_lt(y, 10n) == True{} : Bool}, Nat.mod(m, 10n), m, edm, N.mod_lt(m, 10n, {==}))
618 Empty.absurd({FC.put_dec.digits(1n+j, False{}, n, acc) == lgo(f, 0n, DG(m), acc) : List<&2, U32>},
619 AB.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(m, 10n), False{}, Equal.sym(Bool, Nat.is_lt(m, 10n), True{}, hm), ge10(n, hs))))
620 case 1n+j False{} 1n+p 0n:
621 Empty.absurd({FC.put_dec.digits(1n+j, False{}, n, acc) == lgo(0n, 1n+p, DG(U32.to_nat(n)), acc) : List<&2, U32>}, AB.false_ne_true(hf))
622 case 1n+j False{} 1n+p 1n+g:
623 +m = U32.to_nat(n)
624 +n1 = U32.div(n, 10)
625 +acc1 = {U32.add(U32.mod(n, 10), 48) <> acc : List<&2, U32>}
626 +e1 = Equal.trans(Nat, U32.to_nat(n1), Nat.div(m, 10n), 1n+p, U.to_nat_div(n, 10), hq)
627 +hf1 = AB.subst(Nat, y => {Nat.is_le(Nat.div(y, 10n), g) == True{} : Bool}, 1n+p, U32.to_nat(n1), Equal.sym(Nat, U32.to_nat(n1), 1n+p, e1),
628 N.le_trans(Nat.div(1n+p, 10n), p, g, dlt(p), hf))
629 +RHS = lgo(g, Nat.div(1n+p, 10n), DG(1n+p), DG(m) <> acc)
630 %Equal.sym(List<&2, U32>, FC.put_dec.digits(j, U32.is_lt(n1, 10), n1, acc1), lgo(g, Nat.div(U32.to_nat(n1), 10n), DG(U32.to_nat(n1)), acc1),
631 R(j, U32.is_lt(n1, 10), Nat.div(U32.to_nat(n1), 10n), g, n1, acc1, {==}, {==}, hk_step(n, j, hk), hf1)) :
632 {_ == RHS : List<&2, U32>}
633 %Equal.sym(Nat, U32.to_nat(n1), 1n+p, e1) : {lgo(g, Nat.div(_, 10n), DG(_), acc1) == RHS : List<&2, U32>}
634 %Equal.sym(U32, U32.add(U32.mod(n, 10), 48), DG(m), dg_eq(n)) : {lgo(g, Nat.div(1n+p, 10n), DG(1n+p), _ <> acc) == RHS : List<&2, U32>}
635 {==}
636
637law LN:
638 for +k: Nat
639 for +small: Bool
640 for +j: Nat
641 for +n: U32
642 for +acc: List<&2, U32>
643 for +hs: {U32.is_lt(n, 10) == small : Bool}
644 for +hk: {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(j))) == True{} : Bool}
645 for +hj: {Nat.is_le(j, k) == True{} : Bool}
646 {Nat.is_le(List.length(&2, U32, FC.put_dec.digits(k, small, n, acc)), Nat.add(1n+j, List.length(&2, U32, acc))) == True{} : Bool}
647
648def LN(k, small, j, n, acc, hs, hk, hj):
649 match k small j:
650 case _ True{} _:
651 N.le_add_l(List.length(&2, U32, acc), j)
652 case 0n False{} 0n:
653 Empty.absurd({Nat.is_le(List.length(&2, U32, FC.put_dec.digits(0n, False{}, n, acc)), Nat.add(1n, List.length(&2, U32, acc))) == True{} : Bool},
654 ab0(n, hs, hk))
655 case 0n False{} 1n+i:
656 Empty.absurd({Nat.is_le(List.length(&2, U32, FC.put_dec.digits(0n, False{}, n, acc)), Nat.add(1n+1n+i, List.length(&2, U32, acc))) == True{} : Bool},
657 AB.false_ne_true(hj))
658 case 1n+k1 False{} 0n:
659 Empty.absurd({Nat.is_le(List.length(&2, U32, FC.put_dec.digits(1n+k1, False{}, n, acc)), Nat.add(1n, List.length(&2, U32, acc))) == True{} : Bool},
660 ab0(n, hs, hk))
661 case 1n+k1 False{} 1n+i:
662 +n1 = U32.div(n, 10)
663 +acc1 = {U32.add(U32.mod(n, 10), 48) <> acc : List<&2, U32>}
664 +L = List.length(&2, U32, acc)
665 +len1 = List.length(&2, U32, FC.put_dec.digits(k1, U32.is_lt(n1, 10), n1, acc1))
666 AB.subst(Nat, y => {Nat.is_le(len1, 1n+y) == True{} : Bool}, Nat.add(i, 1n+L), 1n+Nat.add(i, L), N.add_succ(i, L),
667 LN(k1, U32.is_lt(n1, 10), i, n1, acc1, {==}, hk_step(n, i, hk), hj))
668
669law ab_cons:
670 for +n: U32
671 for +acc: List<&2, U32>
672 for +hacc: {D.all_bytes(acc) == True{} : Bool}
673 {D.all_bytes(U32.add(U32.mod(n, 10), 48) <> acc) == True{} : Bool}
674
675def ab_cons(n, acc, hacc):
676 %Equal.sym(U32, U32.add(U32.mod(n, 10), 48), DG(U32.to_nat(n)), dg_eq(n)) : {D.all_bytes(_ <> acc) == True{} : Bool}
677 %Equal.sym(Bool, U32.is_lt(DG(U32.to_nat(n)), 256), True{}, dg_lt(U32.to_nat(n))) : {Bool.and(_, D.all_bytes(acc)) == True{} : Bool}
678 hacc
679
680law AL:
681 for +k: Nat
682 for +small: Bool
683 for +n: U32
684 for +acc: List<&2, U32>
685 for +hs: {U32.is_lt(n, 10) == small : Bool}
686 for +hacc: {D.all_bytes(acc) == True{} : Bool}
687 {D.all_bytes(FC.put_dec.digits(k, small, n, acc)) == True{} : Bool}
688
689def AL(k, small, n, acc, hs, hacc):
690 match k small:
691 case _ True{}:
692 %Equal.sym(U32, U32.add(n, 48), DG(U32.to_nat(n)), dg_small(n, hs)) : {D.all_bytes(_ <> acc) == True{} : Bool}
693 %Equal.sym(Bool, U32.is_lt(DG(U32.to_nat(n)), 256), True{}, dg_lt(U32.to_nat(n))) : {Bool.and(_, D.all_bytes(acc)) == True{} : Bool}
694 hacc
695 case 0n False{}:
696 hacc
697 case 1n+k1 False{}:
698 AL(k1, U32.is_lt(U32.div(n, 10), 10), U32.div(n, 10), U32.add(U32.mod(n, 10), 48) <> acc, {==}, ab_cons(n, acc, hacc))
699
700
701
702
703law hkb:
704 for +n: U32
705 for +r: Nat
706 {Nat.is_le(U32.to_nat(n), U32.to_nat(BK(9n+r))) == True{} : Bool}
707
708def hkb(n, r):
709 AB.subst(U32, y => {Nat.is_le(U32.to_nat(n), U32.to_nat(y)) == True{} : Bool}, U32.not(0), BK(9n+r), {==}, hkmax(n))
710
711law list_show:
712 for +n: U32
713 {FC.put_dec.list(n) == F.show(n) : List<&2, U32>}
714
715def list_show(n):
716 +m = U32.to_nat(n)
717 Equal.trans(List<&2, U32>, FC.put_dec.list(n), lgo(m, Nat.div(m, 10n), DG(m), Nil{}), F.show(n),
718 R(10n, U32.is_lt(n, 10), Nat.div(m, 10n), m, n, Nil{}, {==}, {==}, hkb(n, 1n), hdm(m)),
719 Equal.sym(List<&2, U32>, F.show(n), lgo(m, Nat.div(m, 10n), DG(m), Nil{}), show_lgo(m)))
720
721law list_len:
722 for +n: U32
723 {Nat.is_le(List.length(&2, U32, FC.put_dec.list(n)), 10n) == True{} : Bool}
724
725def list_len(n):
726 LN(10n, U32.is_lt(n, 10), 9n, n, Nil{}, {==}, hkb(n, 0n), {==})
727
728law list_bytes:
729 for +n: U32
730 {D.all_bytes(FC.put_dec.list(n)) == True{} : Bool}
731
732def list_bytes(n):
733 AL(10n, U32.is_lt(n, 10), n, Nil{}, {==}, {==})
734
735law pd_eq:
736 for +xs: List<&2, U32>
737 for -b: D.Bytes
738 {FC.put_dec.go(xs, b) == B.of_list.go(xs, b) : D.Bytes}
739
740def pd_eq(xs, b):
741 match xs:
742 case Nil{}:
743 {==}
744 case Con{+x, t}:
745 pd_eq(t, B.push(b, x))
746
747law pd_room:
748 for +len: U32
749 for +t: P.Tree<U32>
750 for +d: Nat
751 for +n: U32
752 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
753 for +hc: {Nat.is_le(Nat.add(D.size(C.BT(len, t)), 10n), D.cap(C.BT(len, t))) == True{} : Bool}
754 {Nat.is_le(Nat.add(U32.to_nat(len), List.length(&2, U32, FC.put_dec.list(n))), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
755
756def pd_room(len, t, d, n, h, hc):
757 +M = Nat.mul(4n, Nat.pow(2n, d))
758 N.le_trans(Nat.add(U32.to_nat(len), List.length(&2, U32, FC.put_dec.list(n))), Nat.add(U32.to_nat(len), 10n), M,
759 N.le_add_mono_l(U32.to_nat(len), List.length(&2, U32, FC.put_dec.list(n)), 10n, list_len(n)),
760 AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat(len), 10n), y) == True{} : Bool}, D.cap(C.BT(len, t)), M, O.cap_ok_t(len, t, d, h), hc))
761
762law put_dec_view_t:
763 for +len: U32
764 for +t: P.Tree<U32>
765 for +d: Nat
766 for +n: U32
767 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
768 for +hc: {Nat.is_le(Nat.add(D.size(C.BT(len, t)), 10n), D.cap(C.BT(len, t))) == True{} : Bool}
769 {D.view(FC.put_dec(C.BT(len, t), n)) == List.append(&2, U32, D.view(C.BT(len, t)), F.show(n)) : List<&2, U32>}
770
771def put_dec_view_t(len, t, d, n, h, hc):
772 +L = FC.put_dec.list(n)
773 +V = D.view(C.BT(len, t))
774 %Equal.sym(D.Bytes, FC.put_dec.go(L, C.BT(len, t)), B.of_list.go(L, C.BT(len, t)), pd_eq(L, C.BT(len, t))) :
775 {D.view(_) == List.append(&2, U32, V, F.show(n)) : List<&2, U32>}
776 %Equal.sym(List<&2, U32>, D.view(B.of_list.go(L, C.BT(len, t))), List.append(&2, U32, V, L),
777 G.ol_go_view(L, len, t, d, h, list_bytes(n), pd_room(len, t, d, n, h, hc))) :
778 {_ == List.append(&2, U32, V, F.show(n)) : List<&2, U32>}
779 %list_show(n) : {List.append(&2, U32, V, L) == List.append(&2, U32, V, _) : List<&2, U32>}
780 {==}
781
782law put_dec_ok_t:
783 for +len: U32
784 for +t: P.Tree<U32>
785 for +d: Nat
786 for +n: U32
787 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
788 for +hc: {Nat.is_le(Nat.add(D.size(C.BT(len, t)), 10n), D.cap(C.BT(len, t))) == True{} : Bool}
789 {D.ok(FC.put_dec(C.BT(len, t), n), d) == True{} : Bool}
790
791def put_dec_ok_t(len, t, d, n, h, hc):
792 +L = FC.put_dec.list(n)
793 %Equal.sym(D.Bytes, FC.put_dec.go(L, C.BT(len, t)), B.of_list.go(L, C.BT(len, t)), pd_eq(L, C.BT(len, t))) :
794 {D.ok(_, d) == True{} : Bool}
795 G.ol_go_ok(L, len, t, d, h, pd_room(len, t, d, n, h, hc))