1	import Base
2	import ../storage/arith.bend as Arith
3	import ../shape/core.bend as Shape
4	import ./word_injective.bend as Injective
5	import ../storage/model.bend as Model
6	import ../shape/nat_proofs.bend as NatProof
7	
8	def word_has_zero(width: Nat, word: Word(width)) -> Bool:
9	  match width:
10	    case 0n:
11	      False{}
12	    case 1n+p:
13	      match word:
14	        case WCon{False{}, tail}:
15	          True{}
16	        case WCon{True{}, tail}:
17	          word_has_zero(p, tail)
18	
19	def greater_low_bit_tail(comparison: Cmp, +bit: Bool,
20	  accepted: {Cmp.is_lt(Word.cmp.fin(True{}, bit, comparison)) == True{} : Bool}) ->
21	  {Cmp.is_lt(comparison) == True{} : Bool}:
22	  match comparison:
23	    case LT{}:
24	      {==}
25	    case EQ{}:
26	      match bit:
27	        case False{}:
28	          Empty.absurd({False{} == True{} : Bool}, Arith.clash(accepted))
29	        case True{}:
30	          Empty.absurd({False{} == True{} : Bool}, Arith.clash(accepted))
31	    case GT{}:
32	      Empty.absurd({False{} == True{} : Bool}, Arith.clash(accepted))
33	
34	def word_lt_has_zero(+width: Nat, +left: Word(width), +right: Word(width),
35	  accepted: {Cmp.is_lt(Word.cmp(width, left, right)) == True{} : Bool}) ->
36	  {word_has_zero(width, left) == True{} : Bool}:
37	  match width:
38	    case 0n:
39	      Empty.absurd({False{} == True{} : Bool}, Arith.clash(accepted))
40	    case 1n+p:
41	      match left right:
42	        case WCon{False{}, lt} WCon{rb, rt}:
43	          {==}
44	        case WCon{True{}, +lt} WCon{+rb, +rt}:
45	          word_lt_has_zero(p, lt, rt, greater_low_bit_tail(Word.cmp(p, lt, rt), rb, accepted))
46	
47	def word_increment_exact(+width: Nat, +word: Word(width), zero: {word_has_zero(width, word) == True{} : Bool}) ->
48	  {Word.to_nat(width, Word.inc(width, word)) == 1n+Word.to_nat(width, word) : Nat}:
49	  match width:
50	    case 0n:
51	      Empty.absurd({0n == 1n : Nat}, Arith.clash(zero))
52	    case 1n+p:
53	      match word:
54	        case WCon{False{}, tail}:
55	          {==}
56	        case WCon{True{}, +tail}:
57	          Equal.cong(Nat, Nat, Nat.double, Word.to_nat(p, Word.inc(p, tail)), 1n+Word.to_nat(p, tail),
58	            word_increment_exact(p, tail, zero))
59	
60	def increment_below_exact(+word: U32, +limit: U32, below: {U32.is_lt(word, limit) == True{} : Bool}) ->
61	  {U32.to_nat(U32.inc(word)) == 1n+U32.to_nat(word) : Nat}:
62	  match word limit:
63	    case U32{+w} U32{+upper}:
64	      word_increment_exact(32n, w, word_lt_has_zero(32n, w, upper, below))
65	
66	def le_predecessor(+number: Nat, +bound: Nat, within: {Nat.is_le(1n+number, bound) == True{} : Bool}) ->
67	  {Nat.is_le(number, bound) == True{} : Bool}:
68	  match bound:
69	    case 0n:
70	      Empty.absurd({Nat.is_le(number, 0n) == True{} : Bool}, Arith.clash(within))
71	    case 1n+p:
72	      Arith.le_succ(number, p, within)
73	
74	def le_successor_lt(+number: Nat, +bound: Nat, within: {Nat.is_le(1n+number, bound) == True{} : Bool}) ->
75	  {Nat.is_lt(number, bound) == True{} : Bool}:
76	  match bound:
77	    case 0n:
78	      Empty.absurd({Nat.is_lt(number, 0n) == True{} : Bool}, Arith.clash(within))
79	    case 1n+p:
80	      Arith.lt_succ(number, p, within)
81	
82	def natural_word_exact(+number: Nat, +limit: U32, +within: {Nat.is_le(number, U32.to_nat(limit)) == True{} : Bool}) ->
83	  {U32.to_nat(U32.from_nat(number)) == number : Nat}:
84	  match number:
85	    case 0n:
86	      {==}
87	    case 1n+p:
88	      Equal.trans(Nat, U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p,
89	        increment_below_exact(U32.from_nat(p), limit,
90	          %Arith.u32_lt(U32.from_nat(p), limit) : {_ == True{} : Bool}
91	          %Equal.sym(Nat, U32.to_nat(U32.from_nat(p)), p,
92	            natural_word_exact(p, limit, le_predecessor(p, U32.to_nat(limit), within))) :
93	              {Nat.is_lt(_, U32.to_nat(limit)) == True{} : Bool}
94	          le_successor_lt(p, U32.to_nat(limit), within)),
95	        Equal.cong(Nat, Nat, n => 1n+n, U32.to_nat(U32.from_nat(p)), p,
96	          natural_word_exact(p, limit, le_predecessor(p, U32.to_nat(limit), within))))
97	
98	def le_reflexive(+number: Nat) -> {Nat.is_le(number, number) == True{} : Bool}:
99	  match number:
100	    case 0n:
101	      {==}
102	    case 1n+p:
103	      le_reflexive(p)
104	
105	def word_natural_exact(+word: U32) -> {U32.from_nat(U32.to_nat(word)) == word : U32}:
106	  Injective.u32_natural_injective(U32.from_nat(U32.to_nat(word)), word)(
107	    natural_word_exact(U32.to_nat(word), word, le_reflexive(U32.to_nat(word))))
108	
109	def double_le(+left: Nat, +right: Nat, bound: {Nat.is_le(left, right) == True{} : Bool}) ->
110	  {Nat.is_le(Nat.double(left), Nat.double(right)) == True{} : Bool}:
111	  match left right:
112	    case 0n 0n:
113	      {==}
114	    case 0n 1n+r:
115	      {==}
116	    case 1n+l 0n:
117	      Empty.absurd({Nat.is_le(2n+Nat.double(l), 0n) == True{} : Bool}, Arith.clash(bound))
118	    case 1n+l 1n+r:
119	      double_le(l, r, bound)
120	
121	def le_trans(+left: Nat, +middle: Nat, +right: Nat,
122	  first: {Nat.is_le(left, middle) == True{} : Bool},
123	  second: {Nat.is_le(middle, right) == True{} : Bool}) ->
124	  {Nat.is_le(left, right) == True{} : Bool}:
125	  match left:
126	    case 0n:
127	      Arith.le_zero(right)
128	    case 1n+l:
129	      match middle:
130	        case 0n:
131	          Empty.absurd({Nat.is_le(1n+l, right) == True{} : Bool}, Arith.clash(first))
132	        case 1n+m:
133	          match right:
134	            case 0n:
135	              Empty.absurd({Nat.is_le(1n+l, 0n) == True{} : Bool}, Arith.clash(second))
136	            case 1n+r:
137	              le_trans(l, m, r, first, second)
138	
139	def word_increment_le(+width: Nat, +word: Word(width)) ->
140	  {Nat.is_le(Word.to_nat(width, Word.inc(width, word)), 1n+Word.to_nat(width, word)) == True{} : Bool}:
141	  match width:
142	    case 0n:
143	      {==}
144	    case 1n+p:
145	      match word:
146	        case WCon{False{}, +tail}:
147	          le_reflexive(1n+Nat.double(Word.to_nat(p, tail)))
148	        case WCon{True{}, +tail}:
149	          double_le(Word.to_nat(p, Word.inc(p, tail)), 1n+Word.to_nat(p, tail), word_increment_le(p, tail))
150	
151	def increment_le(+word: U32) ->
152	  {Nat.is_le(U32.to_nat(U32.inc(word)), 1n+U32.to_nat(word)) == True{} : Bool}:
153	  match word:
154	    case U32{+bits}:
155	      word_increment_le(32n, bits)
156	
157	def natural_word_le(+number: Nat) ->
158	  {Nat.is_le(U32.to_nat(U32.from_nat(number)), number) == True{} : Bool}:
159	  match number:
160	    case 0n:
161	      {==}
162	    case 1n+p:
163	      le_trans(U32.to_nat(U32.inc(U32.from_nat(p))), 1n+U32.to_nat(U32.from_nat(p)), 1n+p,
164	        increment_le(U32.from_nat(p)), natural_word_le(p))
165	
166	def lt_le(+number: Nat, +bound: Nat, below: {Nat.is_lt(number, bound) == True{} : Bool}) ->
167	  {Nat.is_le(number, bound) == True{} : Bool}:
168	  match number bound:
169	    case 0n 0n:
170	      Empty.absurd({Nat.is_le(0n, 0n) == True{} : Bool}, Arith.clash(below))
171	    case 0n 1n+p:
172	      {==}
173	    case 1n+n 0n:
174	      Empty.absurd({Nat.is_le(1n+n, 0n) == True{} : Bool}, Arith.clash(below))
175	    case 1n+n 1n+p:
176	      lt_le(n, p, below)
177	
178	def naturals_words_fitting(+dims: List<&2, U32>, +values: List<&2, Nat>,
179	  +fit: {True{} == Shape.fit(Shape.naturals(dims), values) : Bool}) ->
180	  {Shape.naturals(Shape.words(values)) == values : List<&2, Nat>}:
181	  match dims values:
182	    case Nil{} Nil{}:
183	      {==}
184	    case +dim <> +dt +head <> +tail:
185	      %Equal.sym(Nat, U32.to_nat(U32.from_nat(head)), head,
186	        natural_word_exact(head, dim, lt_le(head, U32.to_nat(dim),
187	          Arith.and_left(Nat.is_lt(head, U32.to_nat(dim)), Shape.fit(Shape.naturals(dt), tail),
188	            Equal.sym(Bool, True{}, Shape.fit(Shape.naturals(dim <> dt), head <> tail), fit))))) :
189	            {_ <> Shape.naturals(Shape.words(tail)) == head <> tail : List<&2, Nat>}
190	      %Equal.sym(List<&2, Nat>, Shape.naturals(Shape.words(tail)), tail,
191	        naturals_words_fitting(dt, tail,
192	          Equal.sym(Bool, Shape.fit(Shape.naturals(dt), tail), True{},
193	            Arith.and_right(Nat.is_lt(head, U32.to_nat(dim)), Shape.fit(Shape.naturals(dt), tail),
194	              Equal.sym(Bool, True{}, Shape.fit(Shape.naturals(dim <> dt), head <> tail), fit))))) :
195	              {head <> _ == head <> tail : List<&2, Nat>}
196	      {==}
197	    case Nil{} head <> tail:
198	      Empty.absurd({Shape.naturals(Shape.words(head <> tail)) == head <> tail : List<&2, Nat>},
199	        Arith.clash(Equal.sym(Bool, True{}, False{}, fit)))
200	    case dim <> dt Nil{}:
201	      Empty.absurd({Nil{} == Nil{} : List<&2, Nat>}, Arith.clash(Equal.sym(Bool, True{}, False{}, fit)))
202	
203	def add_zero(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
204	  match number:
205	    case 0n:
206	      {==}
207	    case 1n+p:
208	      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero(p))
209	
210	def capacity_product(+left: Nat, +right: Nat) ->
211	  {Model.capacity(Nat.add(left, right)) == Nat.mul(Model.capacity(left), Model.capacity(right)) : Nat}:
212	  match left:
213	    case 0n:
214	      Equal.sym(Nat, Nat.add(Model.capacity(right), 0n), Model.capacity(right), add_zero(Model.capacity(right)))
215	    case 1n+p:
216	      Equal.trans(Nat, Nat.add(Model.capacity(Nat.add(p, right)), Model.capacity(Nat.add(p, right))),
217	        Nat.add(Nat.mul(Model.capacity(p), Model.capacity(right)), Nat.mul(Model.capacity(p), Model.capacity(right))),
218	        Nat.mul(Nat.add(Model.capacity(p), Model.capacity(p)), Model.capacity(right)),
219	        Equal.cong(Nat, Nat, n => Nat.add(n, n), Model.capacity(Nat.add(p, right)),
220	          Nat.mul(Model.capacity(p), Model.capacity(right)), capacity_product(p, right)),
221	        Equal.sym(Nat, Nat.mul(Nat.add(Model.capacity(p), Model.capacity(p)), Model.capacity(right)),
222	          Nat.add(Nat.mul(Model.capacity(p), Model.capacity(right)), Nat.mul(Model.capacity(p), Model.capacity(right))),
223	          NatProof.mul_add_right(Model.capacity(p), Model.capacity(p), Model.capacity(right))))
224	
225	def small_power() -> {Model.capacity(8n) == 256n : Nat}:
226	  {==}
227	
228	def chunk_power() -> {Model.capacity(12n) == 4096n : Nat}:
229	  {==}
230	
231	def add4096(-tail: Nat) -> {Nat.add(4096n, tail) == 4096n+tail : Nat}:
232	  {==}
233	
234	def literal_product_step(-count: Nat, -previous: Nat, -value: Nat,
235	  product: {Nat.mul(count, 4096n) == previous : Nat},
236	  chunk: {Nat.add(4096n, previous) == value : Nat}) ->
237	  {Nat.mul(1n+count, 4096n) == value : Nat}:
238	  Equal.trans(Nat, Nat.add(4096n, Nat.mul(count, 4096n)), Nat.add(4096n, previous), value,
239	    Equal.cong(Nat, Nat, n => Nat.add(4096n, n), Nat.mul(count, 4096n), previous, product), chunk)
240	
241	def literal_product_zero() -> {Nat.mul(0n, 4096n) == 0n : Nat}:
242	  {==}
243	
244	def literal_product_16() -> {Nat.mul(16n, 4096n) == 65536n : Nat}:
245	  literal_product_step(15n, 61440n, 65536n,
246	      literal_product_step(14n, 57344n, 61440n,
247	      literal_product_step(13n, 53248n, 57344n,
248	      literal_product_step(12n, 49152n, 53248n,
249	      literal_product_step(11n, 45056n, 49152n,
250	      literal_product_step(10n, 40960n, 45056n,
251	      literal_product_step(9n, 36864n, 40960n,
252	      literal_product_step(8n, 32768n, 36864n,
253	      literal_product_step(7n, 28672n, 32768n,
254	      literal_product_step(6n, 24576n, 28672n,
255	      literal_product_step(5n, 20480n, 24576n,
256	      literal_product_step(4n, 16384n, 20480n,
257	      literal_product_step(3n, 12288n, 16384n,
258	      literal_product_step(2n, 8192n, 12288n,
259	      literal_product_step(1n, 4096n, 8192n,
260	      literal_product_step(0n, 0n, 4096n,
261	      literal_product_zero(), add4096(0n)), add4096(4096n)), add4096(8192n)), add4096(12288n)), add4096(16384n)), add4096(20480n)), add4096(24576n)), add4096(28672n)), add4096(32768n)), add4096(36864n)), add4096(40960n)), add4096(45056n)), add4096(49152n)), add4096(53248n)), add4096(57344n)), add4096(61440n))
262	
263	def literal_product_32() -> {Nat.mul(32n, 4096n) == 131072n : Nat}:
264	  literal_product_step(31n, 126976n, 131072n,
265	      literal_product_step(30n, 122880n, 126976n,
266	      literal_product_step(29n, 118784n, 122880n,
267	      literal_product_step(28n, 114688n, 118784n,
268	      literal_product_step(27n, 110592n, 114688n,
269	      literal_product_step(26n, 106496n, 110592n,
270	      literal_product_step(25n, 102400n, 106496n,
271	      literal_product_step(24n, 98304n, 102400n,
272	      literal_product_step(23n, 94208n, 98304n,
273	      literal_product_step(22n, 90112n, 94208n,
274	      literal_product_step(21n, 86016n, 90112n,
275	      literal_product_step(20n, 81920n, 86016n,
276	      literal_product_step(19n, 77824n, 81920n,
277	      literal_product_step(18n, 73728n, 77824n,
278	      literal_product_step(17n, 69632n, 73728n,
279	      literal_product_step(16n, 65536n, 69632n,
280	      literal_product_16(), add4096(65536n)), add4096(69632n)), add4096(73728n)), add4096(77824n)), add4096(81920n)), add4096(86016n)), add4096(90112n)), add4096(94208n)), add4096(98304n)), add4096(102400n)), add4096(106496n)), add4096(110592n)), add4096(114688n)), add4096(118784n)), add4096(122880n)), add4096(126976n))
281	
282	def literal_product_48() -> {Nat.mul(48n, 4096n) == 196608n : Nat}:
283	  literal_product_step(47n, 192512n, 196608n,
284	      literal_product_step(46n, 188416n, 192512n,
285	      literal_product_step(45n, 184320n, 188416n,
286	      literal_product_step(44n, 180224n, 184320n,
287	      literal_product_step(43n, 176128n, 180224n,
288	      literal_product_step(42n, 172032n, 176128n,
289	      literal_product_step(41n, 167936n, 172032n,
290	      literal_product_step(40n, 163840n, 167936n,
291	      literal_product_step(39n, 159744n, 163840n,
292	      literal_product_step(38n, 155648n, 159744n,
293	      literal_product_step(37n, 151552n, 155648n,
294	      literal_product_step(36n, 147456n, 151552n,
295	      literal_product_step(35n, 143360n, 147456n,
296	      literal_product_step(34n, 139264n, 143360n,
297	      literal_product_step(33n, 135168n, 139264n,
298	      literal_product_step(32n, 131072n, 135168n,
299	      literal_product_32(), add4096(131072n)), add4096(135168n)), add4096(139264n)), add4096(143360n)), add4096(147456n)), add4096(151552n)), add4096(155648n)), add4096(159744n)), add4096(163840n)), add4096(167936n)), add4096(172032n)), add4096(176128n)), add4096(180224n)), add4096(184320n)), add4096(188416n)), add4096(192512n))
300	
301	def literal_product_64() -> {Nat.mul(64n, 4096n) == 262144n : Nat}:
302	  literal_product_step(63n, 258048n, 262144n,
303	      literal_product_step(62n, 253952n, 258048n,
304	      literal_product_step(61n, 249856n, 253952n,
305	      literal_product_step(60n, 245760n, 249856n,
306	      literal_product_step(59n, 241664n, 245760n,
307	      literal_product_step(58n, 237568n, 241664n,
308	      literal_product_step(57n, 233472n, 237568n,
309	      literal_product_step(56n, 229376n, 233472n,
310	      literal_product_step(55n, 225280n, 229376n,
311	      literal_product_step(54n, 221184n, 225280n,
312	      literal_product_step(53n, 217088n, 221184n,
313	      literal_product_step(52n, 212992n, 217088n,
314	      literal_product_step(51n, 208896n, 212992n,
315	      literal_product_step(50n, 204800n, 208896n,
316	      literal_product_step(49n, 200704n, 204800n,
317	      literal_product_step(48n, 196608n, 200704n,
318	      literal_product_48(), add4096(196608n)), add4096(200704n)), add4096(204800n)), add4096(208896n)), add4096(212992n)), add4096(217088n)), add4096(221184n)), add4096(225280n)), add4096(229376n)), add4096(233472n)), add4096(237568n)), add4096(241664n)), add4096(245760n)), add4096(249856n)), add4096(253952n)), add4096(258048n))
319	
320	def literal_product_80() -> {Nat.mul(80n, 4096n) == 327680n : Nat}:
321	  literal_product_step(79n, 323584n, 327680n,
322	      literal_product_step(78n, 319488n, 323584n,
323	      literal_product_step(77n, 315392n, 319488n,
324	      literal_product_step(76n, 311296n, 315392n,
325	      literal_product_step(75n, 307200n, 311296n,
326	      literal_product_step(74n, 303104n, 307200n,
327	      literal_product_step(73n, 299008n, 303104n,
328	      literal_product_step(72n, 294912n, 299008n,
329	      literal_product_step(71n, 290816n, 294912n,
330	      literal_product_step(70n, 286720n, 290816n,
331	      literal_product_step(69n, 282624n, 286720n,
332	      literal_product_step(68n, 278528n, 282624n,
333	      literal_product_step(67n, 274432n, 278528n,
334	      literal_product_step(66n, 270336n, 274432n,
335	      literal_product_step(65n, 266240n, 270336n,
336	      literal_product_step(64n, 262144n, 266240n,
337	      literal_product_64(), add4096(262144n)), add4096(266240n)), add4096(270336n)), add4096(274432n)), add4096(278528n)), add4096(282624n)), add4096(286720n)), add4096(290816n)), add4096(294912n)), add4096(299008n)), add4096(303104n)), add4096(307200n)), add4096(311296n)), add4096(315392n)), add4096(319488n)), add4096(323584n))
338	
339	def literal_product_96() -> {Nat.mul(96n, 4096n) == 393216n : Nat}:
340	  literal_product_step(95n, 389120n, 393216n,
341	      literal_product_step(94n, 385024n, 389120n,
342	      literal_product_step(93n, 380928n, 385024n,
343	      literal_product_step(92n, 376832n, 380928n,
344	      literal_product_step(91n, 372736n, 376832n,
345	      literal_product_step(90n, 368640n, 372736n,
346	      literal_product_step(89n, 364544n, 368640n,
347	      literal_product_step(88n, 360448n, 364544n,
348	      literal_product_step(87n, 356352n, 360448n,
349	      literal_product_step(86n, 352256n, 356352n,
350	      literal_product_step(85n, 348160n, 352256n,
351	      literal_product_step(84n, 344064n, 348160n,
352	      literal_product_step(83n, 339968n, 344064n,
353	      literal_product_step(82n, 335872n, 339968n,
354	      literal_product_step(81n, 331776n, 335872n,
355	      literal_product_step(80n, 327680n, 331776n,
356	      literal_product_80(), add4096(327680n)), add4096(331776n)), add4096(335872n)), add4096(339968n)), add4096(344064n)), add4096(348160n)), add4096(352256n)), add4096(356352n)), add4096(360448n)), add4096(364544n)), add4096(368640n)), add4096(372736n)), add4096(376832n)), add4096(380928n)), add4096(385024n)), add4096(389120n))
357	
358	def literal_product_112() -> {Nat.mul(112n, 4096n) == 458752n : Nat}:
359	  literal_product_step(111n, 454656n, 458752n,
360	      literal_product_step(110n, 450560n, 454656n,
361	      literal_product_step(109n, 446464n, 450560n,
362	      literal_product_step(108n, 442368n, 446464n,
363	      literal_product_step(107n, 438272n, 442368n,
364	      literal_product_step(106n, 434176n, 438272n,
365	      literal_product_step(105n, 430080n, 434176n,
366	      literal_product_step(104n, 425984n, 430080n,
367	      literal_product_step(103n, 421888n, 425984n,
368	      literal_product_step(102n, 417792n, 421888n,
369	      literal_product_step(101n, 413696n, 417792n,
370	      literal_product_step(100n, 409600n, 413696n,
371	      literal_product_step(99n, 405504n, 409600n,
372	      literal_product_step(98n, 401408n, 405504n,
373	      literal_product_step(97n, 397312n, 401408n,
374	      literal_product_step(96n, 393216n, 397312n,
375	      literal_product_96(), add4096(393216n)), add4096(397312n)), add4096(401408n)), add4096(405504n)), add4096(409600n)), add4096(413696n)), add4096(417792n)), add4096(421888n)), add4096(425984n)), add4096(430080n)), add4096(434176n)), add4096(438272n)), add4096(442368n)), add4096(446464n)), add4096(450560n)), add4096(454656n))
376	
377	def literal_product_128() -> {Nat.mul(128n, 4096n) == 524288n : Nat}:
378	  literal_product_step(127n, 520192n, 524288n,
379	      literal_product_step(126n, 516096n, 520192n,
380	      literal_product_step(125n, 512000n, 516096n,
381	      literal_product_step(124n, 507904n, 512000n,
382	      literal_product_step(123n, 503808n, 507904n,
383	      literal_product_step(122n, 499712n, 503808n,
384	      literal_product_step(121n, 495616n, 499712n,
385	      literal_product_step(120n, 491520n, 495616n,
386	      literal_product_step(119n, 487424n, 491520n,
387	      literal_product_step(118n, 483328n, 487424n,
388	      literal_product_step(117n, 479232n, 483328n,
389	      literal_product_step(116n, 475136n, 479232n,
390	      literal_product_step(115n, 471040n, 475136n,
391	      literal_product_step(114n, 466944n, 471040n,
392	      literal_product_step(113n, 462848n, 466944n,
393	      literal_product_step(112n, 458752n, 462848n,
394	      literal_product_112(), add4096(458752n)), add4096(462848n)), add4096(466944n)), add4096(471040n)), add4096(475136n)), add4096(479232n)), add4096(483328n)), add4096(487424n)), add4096(491520n)), add4096(495616n)), add4096(499712n)), add4096(503808n)), add4096(507904n)), add4096(512000n)), add4096(516096n)), add4096(520192n))
395	
396	def literal_product_144() -> {Nat.mul(144n, 4096n) == 589824n : Nat}:
397	  literal_product_step(143n, 585728n, 589824n,
398	      literal_product_step(142n, 581632n, 585728n,
399	      literal_product_step(141n, 577536n, 581632n,
400	      literal_product_step(140n, 573440n, 577536n,
401	      literal_product_step(139n, 569344n, 573440n,
402	      literal_product_step(138n, 565248n, 569344n,
403	      literal_product_step(137n, 561152n, 565248n,
404	      literal_product_step(136n, 557056n, 561152n,
405	      literal_product_step(135n, 552960n, 557056n,
406	      literal_product_step(134n, 548864n, 552960n,
407	      literal_product_step(133n, 544768n, 548864n,
408	      literal_product_step(132n, 540672n, 544768n,
409	      literal_product_step(131n, 536576n, 540672n,
410	      literal_product_step(130n, 532480n, 536576n,
411	      literal_product_step(129n, 528384n, 532480n,
412	      literal_product_step(128n, 524288n, 528384n,
413	      literal_product_128(), add4096(524288n)), add4096(528384n)), add4096(532480n)), add4096(536576n)), add4096(540672n)), add4096(544768n)), add4096(548864n)), add4096(552960n)), add4096(557056n)), add4096(561152n)), add4096(565248n)), add4096(569344n)), add4096(573440n)), add4096(577536n)), add4096(581632n)), add4096(585728n))
414	
415	def literal_product_160() -> {Nat.mul(160n, 4096n) == 655360n : Nat}:
416	  literal_product_step(159n, 651264n, 655360n,
417	      literal_product_step(158n, 647168n, 651264n,
418	      literal_product_step(157n, 643072n, 647168n,
419	      literal_product_step(156n, 638976n, 643072n,
420	      literal_product_step(155n, 634880n, 638976n,
421	      literal_product_step(154n, 630784n, 634880n,
422	      literal_product_step(153n, 626688n, 630784n,
423	      literal_product_step(152n, 622592n, 626688n,
424	      literal_product_step(151n, 618496n, 622592n,
425	      literal_product_step(150n, 614400n, 618496n,
426	      literal_product_step(149n, 610304n, 614400n,
427	      literal_product_step(148n, 606208n, 610304n,
428	      literal_product_step(147n, 602112n, 606208n,
429	      literal_product_step(146n, 598016n, 602112n,
430	      literal_product_step(145n, 593920n, 598016n,
431	      literal_product_step(144n, 589824n, 593920n,
432	      literal_product_144(), add4096(589824n)), add4096(593920n)), add4096(598016n)), add4096(602112n)), add4096(606208n)), add4096(610304n)), add4096(614400n)), add4096(618496n)), add4096(622592n)), add4096(626688n)), add4096(630784n)), add4096(634880n)), add4096(638976n)), add4096(643072n)), add4096(647168n)), add4096(651264n))
433	
434	def literal_product_176() -> {Nat.mul(176n, 4096n) == 720896n : Nat}:
435	  literal_product_step(175n, 716800n, 720896n,
436	      literal_product_step(174n, 712704n, 716800n,
437	      literal_product_step(173n, 708608n, 712704n,
438	      literal_product_step(172n, 704512n, 708608n,
439	      literal_product_step(171n, 700416n, 704512n,
440	      literal_product_step(170n, 696320n, 700416n,
441	      literal_product_step(169n, 692224n, 696320n,
442	      literal_product_step(168n, 688128n, 692224n,
443	      literal_product_step(167n, 684032n, 688128n,
444	      literal_product_step(166n, 679936n, 684032n,
445	      literal_product_step(165n, 675840n, 679936n,
446	      literal_product_step(164n, 671744n, 675840n,
447	      literal_product_step(163n, 667648n, 671744n,
448	      literal_product_step(162n, 663552n, 667648n,
449	      literal_product_step(161n, 659456n, 663552n,
450	      literal_product_step(160n, 655360n, 659456n,
451	      literal_product_160(), add4096(655360n)), add4096(659456n)), add4096(663552n)), add4096(667648n)), add4096(671744n)), add4096(675840n)), add4096(679936n)), add4096(684032n)), add4096(688128n)), add4096(692224n)), add4096(696320n)), add4096(700416n)), add4096(704512n)), add4096(708608n)), add4096(712704n)), add4096(716800n))
452	
453	def literal_product_192() -> {Nat.mul(192n, 4096n) == 786432n : Nat}:
454	  literal_product_step(191n, 782336n, 786432n,
455	      literal_product_step(190n, 778240n, 782336n,
456	      literal_product_step(189n, 774144n, 778240n,
457	      literal_product_step(188n, 770048n, 774144n,
458	      literal_product_step(187n, 765952n, 770048n,
459	      literal_product_step(186n, 761856n, 765952n,
460	      literal_product_step(185n, 757760n, 761856n,
461	      literal_product_step(184n, 753664n, 757760n,
462	      literal_product_step(183n, 749568n, 753664n,
463	      literal_product_step(182n, 745472n, 749568n,
464	      literal_product_step(181n, 741376n, 745472n,
465	      literal_product_step(180n, 737280n, 741376n,
466	      literal_product_step(179n, 733184n, 737280n,
467	      literal_product_step(178n, 729088n, 733184n,
468	      literal_product_step(177n, 724992n, 729088n,
469	      literal_product_step(176n, 720896n, 724992n,
470	      literal_product_176(), add4096(720896n)), add4096(724992n)), add4096(729088n)), add4096(733184n)), add4096(737280n)), add4096(741376n)), add4096(745472n)), add4096(749568n)), add4096(753664n)), add4096(757760n)), add4096(761856n)), add4096(765952n)), add4096(770048n)), add4096(774144n)), add4096(778240n)), add4096(782336n))
471	
472	def literal_product_208() -> {Nat.mul(208n, 4096n) == 851968n : Nat}:
473	  literal_product_step(207n, 847872n, 851968n,
474	      literal_product_step(206n, 843776n, 847872n,
475	      literal_product_step(205n, 839680n, 843776n,
476	      literal_product_step(204n, 835584n, 839680n,
477	      literal_product_step(203n, 831488n, 835584n,
478	      literal_product_step(202n, 827392n, 831488n,
479	      literal_product_step(201n, 823296n, 827392n,
480	      literal_product_step(200n, 819200n, 823296n,
481	      literal_product_step(199n, 815104n, 819200n,
482	      literal_product_step(198n, 811008n, 815104n,
483	      literal_product_step(197n, 806912n, 811008n,
484	      literal_product_step(196n, 802816n, 806912n,
485	      literal_product_step(195n, 798720n, 802816n,
486	      literal_product_step(194n, 794624n, 798720n,
487	      literal_product_step(193n, 790528n, 794624n,
488	      literal_product_step(192n, 786432n, 790528n,
489	      literal_product_192(), add4096(786432n)), add4096(790528n)), add4096(794624n)), add4096(798720n)), add4096(802816n)), add4096(806912n)), add4096(811008n)), add4096(815104n)), add4096(819200n)), add4096(823296n)), add4096(827392n)), add4096(831488n)), add4096(835584n)), add4096(839680n)), add4096(843776n)), add4096(847872n))
490	
491	def literal_product_224() -> {Nat.mul(224n, 4096n) == 917504n : Nat}:
492	  literal_product_step(223n, 913408n, 917504n,
493	      literal_product_step(222n, 909312n, 913408n,
494	      literal_product_step(221n, 905216n, 909312n,
495	      literal_product_step(220n, 901120n, 905216n,
496	      literal_product_step(219n, 897024n, 901120n,
497	      literal_product_step(218n, 892928n, 897024n,
498	      literal_product_step(217n, 888832n, 892928n,
499	      literal_product_step(216n, 884736n, 888832n,
500	      literal_product_step(215n, 880640n, 884736n,
501	      literal_product_step(214n, 876544n, 880640n,
502	      literal_product_step(213n, 872448n, 876544n,
503	      literal_product_step(212n, 868352n, 872448n,
504	      literal_product_step(211n, 864256n, 868352n,
505	      literal_product_step(210n, 860160n, 864256n,
506	      literal_product_step(209n, 856064n, 860160n,
507	      literal_product_step(208n, 851968n, 856064n,
508	      literal_product_208(), add4096(851968n)), add4096(856064n)), add4096(860160n)), add4096(864256n)), add4096(868352n)), add4096(872448n)), add4096(876544n)), add4096(880640n)), add4096(884736n)), add4096(888832n)), add4096(892928n)), add4096(897024n)), add4096(901120n)), add4096(905216n)), add4096(909312n)), add4096(913408n))
509	
510	def literal_product_240() -> {Nat.mul(240n, 4096n) == 983040n : Nat}:
511	  literal_product_step(239n, 978944n, 983040n,
512	      literal_product_step(238n, 974848n, 978944n,
513	      literal_product_step(237n, 970752n, 974848n,
514	      literal_product_step(236n, 966656n, 970752n,
515	      literal_product_step(235n, 962560n, 966656n,
516	      literal_product_step(234n, 958464n, 962560n,
517	      literal_product_step(233n, 954368n, 958464n,
518	      literal_product_step(232n, 950272n, 954368n,
519	      literal_product_step(231n, 946176n, 950272n,
520	      literal_product_step(230n, 942080n, 946176n,
521	      literal_product_step(229n, 937984n, 942080n,
522	      literal_product_step(228n, 933888n, 937984n,
523	      literal_product_step(227n, 929792n, 933888n,
524	      literal_product_step(226n, 925696n, 929792n,
525	      literal_product_step(225n, 921600n, 925696n,
526	      literal_product_step(224n, 917504n, 921600n,
527	      literal_product_224(), add4096(917504n)), add4096(921600n)), add4096(925696n)), add4096(929792n)), add4096(933888n)), add4096(937984n)), add4096(942080n)), add4096(946176n)), add4096(950272n)), add4096(954368n)), add4096(958464n)), add4096(962560n)), add4096(966656n)), add4096(970752n)), add4096(974848n)), add4096(978944n))
528	
529	def literal_product_256() -> {Nat.mul(256n, 4096n) == 1048576n : Nat}:
530	  literal_product_step(255n, 1044480n, 1048576n,
531	      literal_product_step(254n, 1040384n, 1044480n,
532	      literal_product_step(253n, 1036288n, 1040384n,
533	      literal_product_step(252n, 1032192n, 1036288n,
534	      literal_product_step(251n, 1028096n, 1032192n,
535	      literal_product_step(250n, 1024000n, 1028096n,
536	      literal_product_step(249n, 1019904n, 1024000n,
537	      literal_product_step(248n, 1015808n, 1019904n,
538	      literal_product_step(247n, 1011712n, 1015808n,
539	      literal_product_step(246n, 1007616n, 1011712n,
540	      literal_product_step(245n, 1003520n, 1007616n,
541	      literal_product_step(244n, 999424n, 1003520n,
542	      literal_product_step(243n, 995328n, 999424n,
543	      literal_product_step(242n, 991232n, 995328n,
544	      literal_product_step(241n, 987136n, 991232n,
545	      literal_product_step(240n, 983040n, 987136n,
546	      literal_product_240(), add4096(983040n)), add4096(987136n)), add4096(991232n)), add4096(995328n)), add4096(999424n)), add4096(1003520n)), add4096(1007616n)), add4096(1011712n)), add4096(1015808n)), add4096(1019904n)), add4096(1024000n)), add4096(1028096n)), add4096(1032192n)), add4096(1036288n)), add4096(1040384n)), add4096(1044480n))
547	
548	def capacity_word_bits() -> {1048576 == U32{Arith.unit(32n, 20n)} : U32}:
549	  {==}
550	
551	def u32_unit_nat(+bit: Nat, below: {Nat.is_lt(bit, 32n) == True{} : Bool}) ->
552	  {Model.capacity(bit) == U32.to_nat(U32{Arith.unit(32n, bit)}) : Nat}:
553	  Arith.unit_nat(32n, bit, below)
554	
555	def capacity_word_model() -> {U32.to_nat(1048576) == Model.capacity(20n) : Nat}:
556	  Equal.trans(Nat, U32.to_nat(1048576), U32.to_nat(U32{Arith.unit(32n, 20n)}), Model.capacity(20n),
557	    Equal.cong(U32, Nat, U32.to_nat, 1048576, U32{Arith.unit(32n, 20n)}, capacity_word_bits()),
558	    Equal.sym(Nat, Model.capacity(20n), U32.to_nat(U32{Arith.unit(32n, 20n)}), u32_unit_nat(20n, {==})))
559	
560	def capacity_product_at(+left: Nat, +right: Nat, +sum: Nat, equal: {Nat.add(left, right) == sum : Nat}) ->
561	  {Model.capacity(sum) == Nat.mul(Model.capacity(left), Model.capacity(right)) : Nat}:
562	  Equal.trans(Nat, Model.capacity(sum), Model.capacity(Nat.add(left, right)), Nat.mul(Model.capacity(left), Model.capacity(right)),
563	    Equal.sym(Nat, Model.capacity(Nat.add(left, right)), Model.capacity(sum),
564	      Equal.cong(Nat, Nat, Model.capacity, Nat.add(left, right), sum, equal)),
565	    capacity_product(left, right))
566	
567	def capacity_model_product() -> {Model.capacity(20n) == Nat.mul(256n, 4096n) : Nat}:
568	  Equal.trans(Nat, Model.capacity(20n), Nat.mul(Model.capacity(8n), Model.capacity(12n)), Nat.mul(256n, 4096n),
569	    capacity_product_at(8n, 12n, 20n, {==}),
570	    Equal.trans(Nat, Nat.mul(Model.capacity(8n), Model.capacity(12n)), Nat.mul(256n, Model.capacity(12n)), Nat.mul(256n, 4096n),
571	      Equal.cong(Nat, Nat, n => Nat.mul(n, Model.capacity(12n)), Model.capacity(8n), 256n, small_power()),
572	      Equal.cong(Nat, Nat, n => Nat.mul(256n, n), Model.capacity(12n), 4096n, chunk_power())))
573	
574	def capacity_word_nat() -> {U32.to_nat(1048576) == 1048576n : Nat}:
575	  Equal.trans(Nat, U32.to_nat(1048576), Model.capacity(20n), 1048576n, capacity_word_model(),
576	    Equal.trans(Nat, Model.capacity(20n), Nat.mul(256n, 4096n), 1048576n,
577	      capacity_model_product(), literal_product_256()))
578	
579	def capacity_within(+number: Nat, within: Shape.LE(number, 1048576n)) ->
580	  {Nat.is_le(number, U32.to_nat(1048576)) == True{} : Bool}:
581	  Equal.trans(Bool, Nat.is_le(number, U32.to_nat(1048576)), Nat.is_le(number, 1048576n), True{},
582	    Equal.cong(Nat, Bool, n => Nat.is_le(number, n), U32.to_nat(1048576), 1048576n, capacity_word_nat()),
583	    Equal.sym(Bool, True{}, Nat.is_le(number, 1048576n), NatProof.le_true(number, 1048576n, within)))
584	
585	def capacity_natural_word_exact(+number: Nat, within: Shape.LE(number, 1048576n)) ->
586	  {U32.to_nat(U32.from_nat(number)) == number : Nat}:
587	  natural_word_exact(number, 1048576, capacity_within(number, within))
588	
589	def shape_capacity(+shape: Shape.Shape) -> Shape.LE(Shape.elements(shape), 1048576n):
590	  match shape:
591	    case Shape.SShape{+dims, +size, +exact, rank_bound, capacity_bound}:
592	      %Equal.sym(Nat, size, Shape.logical_numel(dims), exact) : Shape.LE(_, 1048576n)
593	      capacity_bound
594	
595	def shape_count_exact(+shape: Shape.Shape) -> {U32.to_nat(Shape.count(shape)) == Shape.elements(shape) : Nat}:
596	  capacity_natural_word_exact(Shape.elements(shape), shape_capacity(shape))
597	
598	def shape_count_within(+shape: Shape.Shape) -> {U32.is_le(Shape.count(shape), 1048576) == True{} : Bool}:
599	  %Arith.u32_le(Shape.count(shape), 1048576) : {_ == True{} : Bool}
600	  %Equal.sym(Nat, U32.to_nat(Shape.count(shape)), Shape.elements(shape), shape_count_exact(shape)) :
601	    {Nat.is_le(_, U32.to_nat(1048576)) == True{} : Bool}
602	  capacity_within(Shape.elements(shape), shape_capacity(shape))