proof_list.bend

lawful-fields@0.1.1.0 · 472 lines · 28 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-fields@0.1.1.0/defs.bend as F
4import lawful-words@0.1.0.0/proof_nat.bend as N
5import lawful-words@0.1.0.0/proof_u32.bend as U
6import lawful-arrays@0.1.0.0/proof_base.bend as AB
7
8# The laws about lists, text and decb, restated with every variable reusable
9# (same names and statements as in LAWS.bend).
10
11# Lists
12# =====
13
14law append_nil:
15  for +xs: List<&2, U32>
16  {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}
17
18def append_nil(xs):
19  match xs:
20    case Nil{}:
21      {==}
22    case Con{+x, t}:
23      %append_nil(t) : {x <> List.append(&2, U32, t, Nil{}) == x <> _ : List<&2, U32>}
24      {==}
25
26law append_assoc:
27  for +xs: List<&2, U32>
28  for +ys: List<&2, U32>
29  for +zs: List<&2, U32>
30  {List.append(&2, U32, List.append(&2, U32, xs, ys), zs) == List.append(&2, U32, xs, List.append(&2, U32, ys, zs)) : List<&2, U32>}
31
32def append_assoc(xs, ys, zs):
33  match xs:
34    case Nil{}:
35      {==}
36    case Con{+x, t}:
37      %append_assoc(t, ys, zs) :
38        {x <> List.append(&2, U32, List.append(&2, U32, t, ys), zs) == x <> _ : List<&2, U32>}
39      {==}
40
41law take_zero2:
42  for +ps: List<&2, List<&2, U32>>
43  {List.take(&2, List<&2, U32>, ps, 0n) == Nil{} : List<&2, List<&2, U32>>}
44
45def take_zero2(ps):
46  match ps:
47    case Nil{}:
48      {==}
49    case Con{p, t}:
50      {==}
51
52# split
53# =====
54
55law sl_fin:
56  for +x: U32
57  for +r: List<&2, List<&2, U32>>
58  for +b: Bool
59  for +c: Nat
60  for +hr: {List.length(&2, List<&2, U32>, r) == Nat.add(c, 1n) : Nat}
61  {List.length(&2, List<&2, U32>, F.split.fin(x, r, b)) == Nat.add(F.count.if(b, c), 1n) : Nat}
62
63def sl_fin(x, r, b, c, hr):
64  match r b:
65    case Nil{} True{}:
66      %hr : {1n+0n == 1n+_ : Nat}
67      {==}
68    case Nil{} False{}:
69      Empty.absurd({1n == Nat.add(c, 1n) : Nat},
70        AB.succ_ne_zero(c, Equal.sym(Nat, 0n, 1n+c, Equal.trans(Nat, 0n, Nat.add(c, 1n), 1n+c, hr, N.add_one(c)))))
71    case Con{h, t} True{}:
72      %hr : {1n+List.length(&2, List<&2, U32>, h <> t) == 1n+_ : Nat}
73      {==}
74    case Con{h, t} False{}:
75      hr
76
77law split_length:
78  for +xs: List<&2, U32>
79  for +sep: U32
80  {List.length(&2, List<&2, U32>, F.split(xs, sep)) == Nat.add(F.count(xs, sep), 1n) : Nat}
81
82def split_length(xs, sep):
83  match xs:
84    case Nil{}:
85      {==}
86    case Con{+x, t}:
87      sl_fin(x, F.split(t, sep), U32.is_eq(x, sep), F.count(t, sep), split_length(t, sep))
88
89# join.go of the pieces of split is the separator, then their join.
90law jg_fin:
91  for +y: U32
92  for +r: List<&2, List<&2, U32>>
93  for +b: Bool
94  for +sep: U32
95  {F.join.go(F.split.fin(y, r, b), sep) == sep <> F.join(F.split.fin(y, r, b), sep) : List<&2, U32>}
96
97def jg_fin(y, r, b, sep):
98  match r b:
99    case Nil{} True{}:
100      {==}
101    case Nil{} False{}:
102      {==}
103    case Con{h, t} True{}:
104      {==}
105    case Con{h, t} False{}:
106      {==}
107
108law jg:
109  for +t: List<&2, U32>
110  for +sep: U32
111  {F.join.go(F.split(t, sep), sep) == sep <> F.join(F.split(t, sep), sep) : List<&2, U32>}
112
113def jg(t, sep):
114  match t:
115    case Nil{}:
116      {==}
117    case Con{+y, t2}:
118      jg_fin(y, F.split(t2, sep), U32.is_eq(y, sep), sep)
119
120law join_push:
121  for +x: U32
122  for +r: List<&2, List<&2, U32>>
123  for +sep: U32
124  {F.join(F.split.push(x, r), sep) == x <> F.join(r, sep) : List<&2, U32>}
125
126def join_push(x, r, sep):
127  match r:
128    case Nil{}:
129      {==}
130    case Con{h, t}:
131      {==}
132
133law sj_fin:
134  for +x: U32
135  for +t: List<&2, U32>
136  for +sep: U32
137  for +b: Bool
138  for +hb: {U32.is_eq(x, sep) == b : Bool}
139  for +ih: {F.join(F.split(t, sep), sep) == t : List<&2, U32>}
140  for +hg: {F.join.go(F.split(t, sep), sep) == sep <> F.join(F.split(t, sep), sep) : List<&2, U32>}
141  {F.join(F.split.fin(x, F.split(t, sep), b), sep) == x <> t : List<&2, U32>}
142
143def sj_fin(x, t, sep, b, hb, ih, hg):
144  match b:
145    case True{}:
146      %Equal.sym(List<&2, U32>, F.join.go(F.split(t, sep), sep), sep <> F.join(F.split(t, sep), sep), hg) :
147        {_ == x <> t : List<&2, U32>}
148      %Equal.sym(List<&2, U32>, F.join(F.split(t, sep), sep), t, ih) : {sep <> _ == x <> t : List<&2, U32>}
149      %Equal.sym(U32, x, sep, U.is_eq_true(x, sep, hb)) : {sep <> t == _ <> t : List<&2, U32>}
150      {==}
151    case False{}:
152      %Equal.sym(List<&2, U32>, F.join(F.split.push(x, F.split(t, sep)), sep), x <> F.join(F.split(t, sep), sep),
153        join_push(x, F.split(t, sep), sep)) :
154        {_ == x <> t : List<&2, U32>}
155      %Equal.sym(List<&2, U32>, F.join(F.split(t, sep), sep), t, ih) : {x <> _ == x <> t : List<&2, U32>}
156      {==}
157
158law split_join:
159  for +xs: List<&2, U32>
160  for +sep: U32
161  {F.join(F.split(xs, sep), sep) == xs : List<&2, U32>}
162
163def split_join(xs, sep):
164  match xs:
165    case Nil{}:
166      {==}
167    case Con{+x, t}:
168      sj_fin(x, t, sep, U32.is_eq(x, sep), {==}, split_join(t, sep), jg(t, sep))
169
170# Text
171# ====
172
173law text_codes:
174  for +s: String
175  {F.text(F.codes(s)) == s : String}
176
177def text_codes(s):
178  match s:
179    case SNil{}:
180      {==}
181    case SCon{Chr{x}, t}:
182      %text_codes(t) : {SCon{Chr{x}, F.text(F.codes(t))} == SCon{Chr{x}, _} : String}
183      {==}
184
185law st_fin:
186  for +x: U32
187  for +r: List<&2, List<&2, U32>>
188  for +b: Bool
189  {String.split.fin(Chr{x}, F.texts(r), b) == F.texts(F.split.fin(x, r, b)) : List<&2, String>}
190
191def st_fin(x, r, b):
192  match r b:
193    case Nil{} True{}:
194      {==}
195    case Nil{} False{}:
196      {==}
197    case Con{h, t} True{}:
198      {==}
199    case Con{h, t} False{}:
200      {==}
201
202law split_text:
203  for +xs: List<&2, U32>
204  for +sep: U32
205  {String.split(F.text(xs), Chr{sep}) == F.texts(F.split(xs, sep)) : List<&2, String>}
206
207def split_text(xs, sep):
208  match xs:
209    case Nil{}:
210      {==}
211    case Con{+x, t}:
212      %Equal.sym(List<&2, String>, String.split(F.text(t), Chr{sep}), F.texts(F.split(t, sep)), split_text(t, sep)) :
213        {String.split.fin(Chr{x}, _, U32.is_eq(x, sep)) == F.texts(F.split.fin(x, F.split(t, sep), U32.is_eq(x, sep))) : List<&2, String>}
214      st_fin(x, F.split(t, sep), U32.is_eq(x, sep))
215
216law text_app:
217  for +a: List<&2, U32>
218  for +b: List<&2, U32>
219  {F.text(List.append(&2, U32, a, b)) == String.append(F.text(a), F.text(b)) : String}
220
221def text_app(a, b):
222  match a:
223    case Nil{}:
224      {==}
225    case Con{+x, t}:
226      %text_app(t, b) : {SCon{Chr{x}, F.text(List.append(&2, U32, t, b))} == SCon{Chr{x}, _} : String}
227      {==}
228
229law jt:
230  for +t: List<&2, List<&2, U32>>
231  for +p: List<&2, U32>
232  for +sep: U32
233  {F.text(List.append(&2, U32, p, F.join.go(t, sep))) == String.join.go(F.texts(t), F.text(p), F.text([sep])) : String}
234
235def jt(t, p, sep):
236  match t:
237    case Nil{}:
238      %Equal.sym(List<&2, U32>, List.append(&2, U32, p, Nil{}), p, append_nil(p)) : {F.text(_) == F.text(p) : String}
239      {==}
240    case Con{+h2, t2}:
241      +X = {sep <> List.append(&2, U32, h2, F.join.go(t2, sep)) : List<&2, U32>}
242      %Equal.sym(String, F.text(List.append(&2, U32, p, X)), String.append(F.text(p), F.text(X)), text_app(p, X)) :
243        {_ == String.join.go(F.texts(h2 <> t2), F.text(p), F.text([sep])) : String}
244      %jt(t2, h2, sep) :
245        {String.append(F.text(p), SCon{Chr{sep}, F.text(List.append(&2, U32, h2, F.join.go(t2, sep)))}) == String.append(F.text(p), SCon{Chr{sep}, _}) : String}
246      {==}
247
248law join_text:
249  for +ps: List<&2, List<&2, U32>>
250  for +sep: U32
251  {F.text(F.join(ps, sep)) == String.join(F.texts(ps), F.text([sep])) : String}
252
253def join_text(ps, sep):
254  match ps:
255    case Nil{}:
256      {==}
257    case Con{p, t}:
258      jt(t, p, sep)
259
260# Joining at piece k
261# ==================
262
263law ja0:
264  for +q: List<&2, U32>
265  for +t2: List<&2, List<&2, U32>>
266  for +sep: U32
267  for +h: {Nat.is_lt(1n, List.length(&2, List<&2, U32>, q <> t2)) == True{} : Bool}
268  {F.join.go(q <> t2, sep) == List.append(&2, U32, F.join.go(List.take(&2, List<&2, U32>, q <> t2, 1n), sep), sep <> F.join(List.drop(&2, List<&2, U32>, q <> t2, 1n), sep)) : List<&2, U32>}
269
270def ja0(q, t2, sep, h):
271  match t2:
272    case Nil{}:
273      Empty.absurd({F.join.go([q], sep) == List.append(&2, U32, F.join.go([q], sep), [sep]) : List<&2, U32>}, AB.false_ne_true(h))
274    case Con{+r, t3}:
275      +Z = {sep <> List.append(&2, U32, r, F.join.go(t3, sep)) : List<&2, U32>}
276      %Equal.sym(List<&2, U32>, List.append(&2, U32, q, Nil{}), q, append_nil(q)) :
277        {sep <> List.append(&2, U32, q, Z) == sep <> List.append(&2, U32, _, Z) : List<&2, U32>}
278      {==}
279
280law ja_go:
281  for +t: List<&2, List<&2, U32>>
282  for +sep: U32
283  for +k: Nat
284  for +h: {Nat.is_lt(Nat.add(k, 1n), List.length(&2, List<&2, U32>, t)) == True{} : Bool}
285  {F.join.go(t, sep) == List.append(&2, U32, F.join.go(List.take(&2, List<&2, U32>, t, Nat.add(k, 1n)), sep), sep <> F.join(List.drop(&2, List<&2, U32>, t, Nat.add(k, 1n)), sep)) : List<&2, U32>}
286
287def ja_go(t, sep, k, h):
288  match t k:
289    case Nil{} _:
290      Empty.absurd({F.join.go(Nil{}, sep) == List.append(&2, U32, F.join.go(List.take(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep), sep <> F.join(List.drop(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep)) : List<&2, U32>},
291        AB.lt_zero_absurd(Nat.add(k, 1n), h))
292    case Con{+q, t2} 0n:
293      ja0(q, t2, sep, h)
294    case Con{+q, t2} 1n+k2:
295      +JT = F.join.go(List.take(&2, List<&2, U32>, t2, Nat.add(k2, 1n)), sep)
296      +Z = {sep <> F.join(List.drop(&2, List<&2, U32>, t2, Nat.add(k2, 1n)), sep) : List<&2, U32>}
297      %Equal.sym(List<&2, U32>, F.join.go(t2, sep), List.append(&2, U32, JT, Z), ja_go(t2, sep, k2, h)) :
298        {sep <> List.append(&2, U32, q, _) == sep <> List.append(&2, U32, List.append(&2, U32, q, JT), Z) : List<&2, U32>}
299      %Equal.sym(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, q, JT), Z), List.append(&2, U32, q, List.append(&2, U32, JT, Z)), append_assoc(q, JT, Z)) :
300        {sep <> List.append(&2, U32, q, List.append(&2, U32, JT, Z)) == sep <> _ : List<&2, U32>}
301      {==}
302
303law jat0:
304  for +p: List<&2, U32>
305  for +t: List<&2, List<&2, U32>>
306  for +sep: U32
307  for +h: {Nat.is_lt(1n, List.length(&2, List<&2, U32>, p <> t)) == True{} : Bool}
308  {F.join(p <> t, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, p <> t, 1n), sep), sep <> F.join(List.drop(&2, List<&2, U32>, p <> t, 1n), sep)) : List<&2, U32>}
309
310def jat0(p, t, sep, h):
311  match t:
312    case Nil{}:
313      Empty.absurd({F.join([p], sep) == List.append(&2, U32, F.join([p], sep), [sep]) : List<&2, U32>}, AB.false_ne_true(h))
314    case Con{+r, t3}:
315      +Z = {sep <> List.append(&2, U32, r, F.join.go(t3, sep)) : List<&2, U32>}
316      %Equal.sym(List<&2, U32>, List.append(&2, U32, p, Nil{}), p, append_nil(p)) :
317        {List.append(&2, U32, p, Z) == List.append(&2, U32, _, Z) : List<&2, U32>}
318      {==}
319
320law join_at:
321  for +ps: List<&2, List<&2, U32>>
322  for +sep: U32
323  for +k: Nat
324  for +h: {Nat.is_lt(Nat.add(k, 1n), List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
325  {F.join(ps, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep), Con{sep, F.join(List.drop(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)}) : List<&2, U32>}
326
327def join_at(ps, sep, k, h):
328  match ps k:
329    case Nil{} _:
330      Empty.absurd({F.join(Nil{}, sep) == List.append(&2, U32, F.join(List.take(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep), sep <> F.join(List.drop(&2, List<&2, U32>, Nil{}, Nat.add(k, 1n)), sep)) : List<&2, U32>},
331        AB.lt_zero_absurd(Nat.add(k, 1n), h))
332    case Con{+p, t} 0n:
333      jat0(p, t, sep, h)
334    case Con{+p, t} 1n+k2:
335      +JT = F.join.go(List.take(&2, List<&2, U32>, t, Nat.add(k2, 1n)), sep)
336      +Z = {sep <> F.join(List.drop(&2, List<&2, U32>, t, Nat.add(k2, 1n)), sep) : List<&2, U32>}
337      %Equal.sym(List<&2, U32>, F.join.go(t, sep), List.append(&2, U32, JT, Z), ja_go(t, sep, k2, h)) :
338        {List.append(&2, U32, p, _) == List.append(&2, U32, List.append(&2, U32, p, JT), Z) : List<&2, U32>}
339      %Equal.sym(List<&2, U32>, List.append(&2, U32, List.append(&2, U32, p, JT), Z), List.append(&2, U32, p, List.append(&2, U32, JT, Z)), append_assoc(p, JT, Z)) :
340        {List.append(&2, U32, p, List.append(&2, U32, JT, Z)) == _ : List<&2, U32>}
341      {==}
342
343# Ends
344# ====
345
346law ends_arith:
347  for +from: Nat
348  for +lp: Nat
349  for +lj: Nat
350  {Nat.add(Nat.add(Nat.add(from, lp), 1n), lj) == Nat.add(from, Nat.add(lp, 1n+lj)) : Nat}
351
352def ends_arith(from, lp, lj):
353  %Equal.sym(Nat, Nat.add(Nat.add(from, lp), 1n), 1n+Nat.add(from, lp), N.add_one(Nat.add(from, lp))) :
354    {Nat.add(_, lj) == Nat.add(from, Nat.add(lp, 1n+lj)) : Nat}
355  %Equal.sym(Nat, Nat.add(lp, 1n+lj), 1n+Nat.add(lp, lj), N.add_succ(lp, lj)) :
356    {Nat.add(1n+Nat.add(from, lp), lj) == Nat.add(from, _) : Nat}
357  %Equal.sym(Nat, Nat.add(from, 1n+Nat.add(lp, lj)), 1n+Nat.add(from, Nat.add(lp, lj)), N.add_succ(from, Nat.add(lp, lj))) :
358    {Nat.add(1n+Nat.add(from, lp), lj) == _ : Nat}
359  %N.add_assoc(from, lp, lj) : {1n+Nat.add(Nat.add(from, lp), lj) == 1n+_ : Nat}
360  {==}
361
362# One step of ej, with the induction hypothesis for the rest (t is not empty).
363law ej_step:
364  for +p: List<&2, U32>
365  for +t: List<&2, List<&2, U32>>
366  for +sep: U32
367  for +from: Nat
368  for +k2: Nat
369  for +h: {Nat.is_lt(1n+k2, List.length(&2, List<&2, U32>, p <> t)) == True{} : Bool}
370  for +ih: {List.get(&2, Nat, F.ends(t, Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n)), k2) == Some{Nat.add(Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n), List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, t, 1n+k2), sep)))} : Maybe<&2, Nat>}
371  {List.get(&2, Nat, F.ends(p <> t, from), 1n+k2) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, p <> t, 1n+1n+k2), sep)))} : Maybe<&2, Nat>}
372
373def ej_step(p, t, sep, from, k2, h, ih):
374  match t:
375    case Nil{}:
376      Empty.absurd({List.get(&2, Nat, F.ends([p], from), 1n+k2) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, [p], 1n+1n+k2), sep)))} : Maybe<&2, Nat>}, AB.lt_zero_absurd(k2, h))
377    case Con{+q, t2}:
378      +lp = List.length(&2, U32, p)
379      +f1 = Nat.add(Nat.add(from, lp), 1n)
380      +J = F.join(List.take(&2, List<&2, U32>, q <> t2, 1n+k2), sep)
381      +RHS = {Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, p <> q <> t2, 1n+1n+k2), sep)))} : Maybe<&2, Nat>}
382      %Equal.sym(Maybe<&2, Nat>, List.get(&2, Nat, F.ends(q <> t2, f1), k2), Some{Nat.add(f1, List.length(&2, U32, J))}, ih) :
383        {_ == RHS : Maybe<&2, Nat>}
384      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, p, sep <> J)), Nat.add(lp, List.length(&2, U32, sep <> J)),
385        AB.length_append(U32, p, sep <> J)) :
386        {Some{Nat.add(f1, List.length(&2, U32, J))} == Some{Nat.add(from, _)} : Maybe<&2, Nat>}
387      %ends_arith(from, lp, List.length(&2, U32, J)) :
388        {Some{Nat.add(f1, List.length(&2, U32, J))} == Some{_} : Maybe<&2, Nat>}
389      {==}
390
391law ej:
392  for +ps: List<&2, List<&2, U32>>
393  for +sep: U32
394  for +from: Nat
395  for +k: Nat
396  for +h: {Nat.is_lt(k, List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
397  {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, 1n+k), sep)))} : Maybe<&2, Nat>}
398
399def ej(ps, sep, from, k, h):
400  match ps k:
401    case Nil{} _:
402      Empty.absurd({List.get(&2, Nat, F.ends(Nil{}, from), k) == Some{Nat.add(from, 0n)} : Maybe<&2, Nat>}, AB.lt_zero_absurd(k, h))
403    case Con{+p, t} 0n:
404      %Equal.sym(List<&2, List<&2, U32>>, List.take(&2, List<&2, U32>, t, 0n), Nil{}, take_zero2(t)) :
405        {Some{Nat.add(from, List.length(&2, U32, p))} == Some{Nat.add(from, List.length(&2, U32, F.join(p <> _, sep)))} : Maybe<&2, Nat>}
406      %Equal.sym(List<&2, U32>, List.append(&2, U32, p, Nil{}), p, append_nil(p)) :
407        {Some{Nat.add(from, List.length(&2, U32, p))} == Some{Nat.add(from, List.length(&2, U32, _))} : Maybe<&2, Nat>}
408      {==}
409    case Con{+p, t} 1n+k2:
410      ej_step(p, t, sep, from, k2, h, ej(t, sep, Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n), k2, h))
411
412law ends_join:
413  for +ps: List<&2, List<&2, U32>>
414  for +sep: U32
415  for +from: Nat
416  for +k: Nat
417  for +h: {Nat.is_lt(k, List.length(&2, List<&2, U32>, ps)) == True{} : Bool}
418  {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, Nat.add(k, 1n)), sep)))} : Maybe<&2, Nat>}
419
420def ends_join(ps, sep, from, k, h):
421  %Equal.sym(Nat, Nat.add(k, 1n), 1n+k, N.add_one(k)) :
422    {List.get(&2, Nat, F.ends(ps, from), k) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, ps, _), sep)))} : Maybe<&2, Nat>}
423  ej(ps, sep, from, k, h)
424
425law pieces_length:
426  for +es: List<&2, U32>
427  for +xs: List<&2, U32>
428  for +from: Nat
429  {List.length(&2, List<&2, U32>, F.pieces(es, xs, from)) == List.length(&2, U32, es) : Nat}
430
431def pieces_length(es, xs, from):
432  match es:
433    case Nil{}:
434      {==}
435    case Con{+e, t}:
436      %pieces_length(t, xs, Nat.add(U32.to_nat(e), 1n)) :
437        {1n+List.length(&2, List<&2, U32>, F.pieces(t, xs, Nat.add(U32.to_nat(e), 1n))) == 1n+_ : Nat}
438      {==}
439
440# decb
441# ====
442
443# 2^32 must never take part in a conversion (the checker would expand it), so
444# the bound stays a variable M and the law instantiates it.
445def decb_if(+n: Nat, b: Bool, hb: {b == True{} : Bool}) -> {F.decb.if(n, b) == Some{n} : Maybe<&2, Nat>}:
446  match b:
447    case True{}:
448      {==}
449    case False{}:
450      Empty.absurd({F.decb.if(n, False{}) == Some{n} : Maybe<&2, Nat>}, AB.false_ne_true(hb))
451
452law decb_fits_m:
453  for +xs: List<&2, U32>
454  for +n: Nat
455  for +m: Nat
456  for +h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
457  for +hn: {Nat.is_lt(n, m) == True{} : Bool}
458  {F.decb(xs, m) == Some{n} : Maybe<&2, Nat>}
459
460def decb_fits_m(xs, n, m, h, hn):
461  %Equal.sym(Maybe<&2, Nat>, F.dec(xs), Some{n}, h) : {F.decb.of(_, m) == Some{n} : Maybe<&2, Nat>}
462  decb_if(n, Nat.is_lt(n, m), hn)
463
464law decb_fits:
465  for +xs: List<&2, U32>
466  for +n: Nat
467  for +h: {F.dec(xs) == Some{n} : Maybe<&2, Nat>}
468  for +hn: {Nat.is_lt(n, Nat.pow(2n, 32n)) == True{} : Bool}
469  {F.decb(xs, Nat.pow(2n, 32n)) == Some{n} : Maybe<&2, Nat>}
470
471def decb_fits(xs, n, h, hn):
472  decb_fits_m(xs, n, Nat.pow(2n, 32n), h, hn)