1	import Base
2	import ./model.bend as Model
3	
4	def falsity(value: Bool) -> Data:
5	  match value:
6	    case True{}:
7	      Empty
8	    case False{}:
9	      Unit
10	
11	def clash(equal: {False{} == True{} : Bool}) -> Empty:
12	  %equal : falsity(_)
13	  Unit{}
14	
15	def bit(b: Bool, x: Nat) -> Nat:
16	  match b:
17	    case False{}:
18	      Nat.double(x)
19	    case True{}:
20	      1n+Nat.double(x)
21	
22	def borrow(c: Bool) -> Nat:
23	  match c:
24	    case False{}:
25	      1n
26	    case True{}:
27	      0n
28	
29	def add_succ(a: Nat, -b: Nat) -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}:
30	  match a:
31	    case 0n:
32	      {==}
33	    case 1n+p:
34	      %add_succ(p, b) : {1n+Nat.add(p, 1n+b) == 1n+_ : Nat}
35	      {==}
36	
37	def double_add(a: Nat, -b: Nat) -> {Nat.add(Nat.double(a), Nat.double(b)) == Nat.double(Nat.add(a, b)) : Nat}:
38	  match a:
39	    case 0n:
40	      {==}
41	    case 1n+p:
42	      %double_add(p, b) : {2n+Nat.add(Nat.double(p), Nat.double(b)) == 2n+_ : Nat}
43	      {==}
44	
45	def double_self(+a: Nat) -> {Nat.add(a, a) == Nat.double(a) : Nat}:
46	  match a:
47	    case 0n:
48	      {==}
49	    case 1n+p:
50	      %double_self(p) : {1n+Nat.add(p, 1n+p) == 2n+_ : Nat}
51	      %add_succ(p, p) : {1n+Nat.add(p, 1n+p) == 1n+_ : Nat}
52	      {==}
53	
54	def eq_refl(+a: Nat) -> {Nat.is_eq(a, a) == True{} : Bool}:
55	  match a:
56	    case 0n:
57	      {==}
58	    case 1n+p:
59	      eq_refl(p)
60	
61	def eq_true(+a: Nat, +b: Nat, decided: {Nat.is_eq(a, b) == True{} : Bool}) -> {a == b : Nat}:
62	  match a b:
63	    case 0n 0n:
64	      {==}
65	    case 0n 1n+q:
66	      Empty.absurd({0n == 1n+q : Nat}, clash(decided))
67	    case 1n+p 0n:
68	      Empty.absurd({1n+p == 0n : Nat}, clash(decided))
69	    case 1n+p 1n+q:
70	      %eq_true(p, q, decided) : {1n+p == 1n+_ : Nat}
71	      {==}
72	
73	def cmp_bits(+x: Nat, +y: Nat, +a: Bool, +b: Bool) ->
74	  {Word.cmp.fin(a, b, Nat.cmp(x, y)) == Nat.cmp(bit(a, x), bit(b, y)) : Cmp}:
75	  match x y:
76	    case 0n 0n:
77	      match a b:
78	        case False{} False{}:
79	          {==}
80	        case False{} True{}:
81	          {==}
82	        case True{} False{}:
83	          {==}
84	        case True{} True{}:
85	          {==}
86	    case 0n 1n+q:
87	      match a b:
88	        case False{} False{}:
89	          {==}
90	        case False{} True{}:
91	          {==}
92	        case True{} False{}:
93	          {==}
94	        case True{} True{}:
95	          {==}
96	    case 1n+p 0n:
97	      match a b:
98	        case False{} False{}:
99	          {==}
100	        case False{} True{}:
101	          {==}
102	        case True{} False{}:
103	          {==}
104	        case True{} True{}:
105	          {==}
106	    case 1n+p 1n+q:
107	      match a b:
108	        case False{} False{}:
109	          cmp_bits(p, q, False{}, False{})
110	        case False{} True{}:
111	          cmp_bits(p, q, False{}, True{})
112	        case True{} False{}:
113	          cmp_bits(p, q, True{}, False{})
114	        case True{} True{}:
115	          cmp_bits(p, q, True{}, True{})
116	
117	def word_bit(-p: Nat, +b: Bool, -t: Word(p)) -> {bit(b, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
118	  match b:
119	    case False{}:
120	      {==}
121	    case True{}:
122	      {==}
123	
124	def word_cmp(+n: Nat, +a: Word(n), +b: Word(n)) ->
125	  {Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) == Word.cmp(n, a, b) : Cmp}:
126	  match n:
127	    case 0n:
128	      {==}
129	    case 1n+p:
130	      match a b:
131	        case WCon{+x, +xs} WCon{+y, +ys}:
132	          %word_bit(p, x, xs) : {Nat.cmp(_, Word.to_nat(1n+p, WCon{y, ys})) == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
133	          %word_bit(p, y, ys) : {Nat.cmp(bit(x, Word.to_nat(p, xs)), _) == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
134	          %cmp_bits(Word.to_nat(p, xs), Word.to_nat(p, ys), x, y) : {_ == Word.cmp.fin(x, y, Word.cmp(p, xs, ys)) : Cmp}
135	          %word_cmp(p, xs, ys) : {Word.cmp.fin(x, y, Nat.cmp(Word.to_nat(p, xs), Word.to_nat(p, ys))) == Word.cmp.fin(x, y, _) : Cmp}
136	          {==}
137	
138	def u32_lt(+a: U32, +b: U32) -> {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == U32.is_lt(a, b) : Bool}:
139	  match a b:
140	    case U32{x} U32{y}:
141	      %word_cmp(32n, x, y) : {Cmp.is_lt(Nat.cmp(Word.to_nat(32n, x), Word.to_nat(32n, y))) == Cmp.is_lt(_) : Bool}
142	      {==}
143	
144	def u32_le(+a: U32, +b: U32) -> {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == U32.is_le(a, b) : Bool}:
145	  match a b:
146	    case U32{x} U32{y}:
147	      %word_cmp(32n, x, y) : {Cmp.is_le(Nat.cmp(Word.to_nat(32n, x), Word.to_nat(32n, y))) == Cmp.is_le(_) : Bool}
148	      {==}
149	
150	def le_zero(+q: Nat) -> {Nat.is_le(0n, q) == True{} : Bool}:
151	  match q:
152	    case 0n:
153	      {==}
154	    case 1n+r:
155	      {==}
156	
157	def le_dd(+u: Nat, +v: Nat, h: {Nat.is_le(Nat.double(u), Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(u, v) == True{} : Bool}:
158	  match u v:
159	    case 0n 0n:
160	      {==}
161	    case 0n 1n+q:
162	      {==}
163	    case 1n+p 0n:
164	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, clash(h))
165	    case 1n+p 1n+q:
166	      le_dd(p, q, h)
167	
168	def le_sd(+u: Nat, +v: Nat, h: {Nat.is_le(1n+Nat.double(u), Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(1n+u, v) == True{} : Bool}:
169	  match u v:
170	    case 0n 0n:
171	      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, clash(h))
172	    case 0n 1n+q:
173	      le_zero(q)
174	    case 1n+p 0n:
175	      Empty.absurd({Nat.is_le(2n+p, 0n) == True{} : Bool}, clash(h))
176	    case 1n+p 1n+q:
177	      le_sd(p, q, h)
178	
179	def le_ds(+u: Nat, +v: Nat, h: {Nat.is_le(Nat.double(u), 1n+Nat.double(v)) == True{} : Bool}) -> {Nat.is_le(u, v) == True{} : Bool}:
180	  match u v:
181	    case 0n v:
182	      le_zero(v)
183	    case 1n+p 0n:
184	      Empty.absurd({Nat.is_le(1n+p, 0n) == True{} : Bool}, clash(h))
185	    case 1n+p 1n+q:
186	      le_ds(p, q, h)
187	
188	# Word.sub(a, b) is Word.adc(a, b, True, True): it adds the complement of b
189	# with an incoming carry, so a cleared carry is a borrow of one.
190	def sub_word(+n: Nat, +a: Word(n), +b: Word(n), +c: Bool,
191	  h: {Nat.is_le(Nat.add(borrow(c), Word.to_nat(n, b)), Word.to_nat(n, a)) == True{} : Bool}) ->
192	  {Nat.add(borrow(c), Nat.add(Word.to_nat(n, b), Word.to_nat(n, Word.adc(n, a, b, True{}, c)))) == Word.to_nat(n, a) : Nat}:
193	  match n:
194	    case 0n:
195	      match c:
196	        case False{}:
197	          Empty.absurd({1n == 0n : Nat}, clash(h))
198	        case True{}:
199	          {==}
200	    case 1n+p:
201	      match a:
202	        case WCon{+x, +xs}:
203	          match x:
204	            case False{}:
205	              match b:
206	                case WCon{+y, +ys}:
207	                  match y:
208	                    case False{}:
209	                      match c:
210	                        case False{}:
211	                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
212	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
213	                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
214	                          {==}
215	                        case True{}:
216	                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == Nat.double(_) : Nat}
217	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
218	                          {==}
219	                    case True{}:
220	                      match c:
221	                        case False{}:
222	                          %sub_word(p, xs, ys, False{}, le_dd(1n+Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
223	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
224	                          {==}
225	                        case True{}:
226	                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == Nat.double(_) : Nat}
227	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
228	                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+_ : Nat}
229	                          {==}
230	            case True{}:
231	              match b:
232	                case WCon{+y, +ys}:
233	                  match y:
234	                    case False{}:
235	                      match c:
236	                        case False{}:
237	                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
238	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
239	                          {==}
240	                        case True{}:
241	                          %sub_word(p, xs, ys, True{}, le_ds(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
242	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
243	                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) : {Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == _ : Nat}
244	                          {==}
245	                    case True{}:
246	                      match c:
247	                        case False{}:
248	                          %sub_word(p, xs, ys, False{}, le_sd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 1n+Nat.double(_) : Nat}
249	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{}))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 3n+_ : Nat}
250	                          %add_succ(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) : {2n+Nat.add(Nat.double(Word.to_nat(p, ys)), 1n+Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, False{})))) == 2n+_ : Nat}
251	                          {==}
252	                        case True{}:
253	                          %sub_word(p, xs, ys, True{}, le_dd(Word.to_nat(p, ys), Word.to_nat(p, xs), h)) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+Nat.double(_) : Nat}
254	                          %double_add(Word.to_nat(p, ys), Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{}))) : {1n+Nat.add(Nat.double(Word.to_nat(p, ys)), Nat.double(Word.to_nat(p, Word.adc(p, xs, ys, True{}, True{})))) == 1n+_ : Nat}
255	                          {==}
256	
257	def lt_le_trans(+a: Nat, +b: Nat, +c: Nat, ab: {Nat.is_lt(a, b) == True{} : Bool},
258	  bc: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_lt(a, c) == True{} : Bool}:
259	  match a:
260	    case 0n:
261	      match b:
262	        case 0n:
263	          Empty.absurd({Nat.is_lt(0n, c) == True{} : Bool}, clash(ab))
264	        case 1n+q:
265	          match c:
266	            case 0n:
267	              Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(bc))
268	            case 1n+r:
269	              {==}
270	    case 1n+p:
271	      match b:
272	        case 0n:
273	          Empty.absurd({Nat.is_lt(1n+p, c) == True{} : Bool}, clash(ab))
274	        case 1n+q:
275	          match c:
276	            case 0n:
277	              Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(bc))
278	            case 1n+r:
279	              lt_le_trans(p, q, r, ab, bc)
280	
281	def lt_succ(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_lt(a, 1n+b) == True{} : Bool}:
282	  match a:
283	    case 0n:
284	      {==}
285	    case 1n+p:
286	      match b:
287	        case 0n:
288	          Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, clash(h))
289	        case 1n+q:
290	          lt_succ(p, q, h)
291	
292	def lt_dd(+x: Nat, +c: Nat, h: {Nat.is_lt(Nat.double(x), Nat.double(c)) == True{} : Bool}) -> {Nat.is_lt(x, c) == True{} : Bool}:
293	  match x c:
294	    case 0n 0n:
295	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(h))
296	    case 0n 1n+q:
297	      {==}
298	    case 1n+p 0n:
299	      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(h))
300	    case 1n+p 1n+q:
301	      lt_dd(p, q, h)
302	
303	def lt_sd(+x: Nat, +c: Nat, h: {Nat.is_lt(1n+Nat.double(x), Nat.double(c)) == True{} : Bool}) -> {Nat.is_lt(x, c) == True{} : Bool}:
304	  match x c:
305	    case 0n 0n:
306	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, clash(h))
307	    case 0n 1n+q:
308	      {==}
309	    case 1n+p 0n:
310	      Empty.absurd({Nat.is_lt(1n+p, 0n) == True{} : Bool}, clash(h))
311	    case 1n+p 1n+q:
312	      lt_sd(p, q, h)
313	
314	def lt_doubled(+x: Nat, +c: Nat, h: {Nat.is_lt(x, Nat.add(c, c)) == True{} : Bool}) -> {Nat.is_lt(x, Nat.double(c)) == True{} : Bool}:
315	  %double_self(c) : {Nat.is_lt(x, _) == True{} : Bool}
316	  h
317	
318	def lt_half(+b: Bool, +x: Nat, +c: Nat, h: {Nat.is_lt(bit(b, x), Model.capacity(1n+c)) == True{} : Bool}) ->
319	  {Nat.is_lt(x, Model.capacity(c)) == True{} : Bool}:
320	  match b:
321	    case False{}:
322	      lt_dd(x, Model.capacity(c), lt_doubled(Nat.double(x), Model.capacity(c), h))
323	    case True{}:
324	      lt_sd(x, Model.capacity(c), lt_doubled(1n+Nat.double(x), Model.capacity(c), h))
325	
326	def lt_zero(+x: Nat, h: {Nat.is_lt(x, 0n) == True{} : Bool}) -> Empty:
327	  match x:
328	    case 0n:
329	      clash(h)
330	    case 1n+p:
331	      clash(h)
332	
333	def lt_one(+x: Nat, h: {Nat.is_lt(x, 1n) == True{} : Bool}) -> {0n == x : Nat}:
334	  match x:
335	    case 0n:
336	      {==}
337	    case 1n+p:
338	      Empty.absurd({0n == 1n+p : Nat}, lt_zero(p, h))
339	
340	def lt_d1(+x: Nat, h: {Nat.is_lt(Nat.double(x), 1n) == True{} : Bool}) -> {Nat.is_lt(x, 1n) == True{} : Bool}:
341	  match x:
342	    case 0n:
343	      {==}
344	    case 1n+p:
345	      Empty.absurd({Nat.is_lt(1n+p, 1n) == True{} : Bool}, clash(h))
346	
347	def low(m: Nat, +k: Nat) -> Word(m):
348	  match m:
349	    case 0n:
350	      WNil{}
351	    case 1n+q:
352	      match k:
353	        case 0n:
354	          WCon{False{}, low(q, 0n)}
355	        case 1n+r:
356	          WCon{True{}, low(q, r)}
357	
358	def mask_word(+m: Nat, +k: Nat, +w: Word(m), h: {Nat.is_lt(Word.to_nat(m, w), Model.capacity(k)) == True{} : Bool}) ->
359	  {w == Word.and(m, w, low(m, k)) : Word(m)}:
360	  match m:
361	    case 0n:
362	      match w:
363	        case WNil{}:
364	          {==}
365	    case 1n+q:
366	      match k:
367	        case 0n:
368	          match w:
369	            case WCon{+b, +t}:
370	              match b:
371	                case False{}:
372	                  %mask_word(q, 0n, t, lt_d1(Word.to_nat(q, t), h)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+q)}
373	                  {==}
374	                case True{}:
375	                  Empty.absurd({WCon{True{}, t} == Word.and(1n+q, WCon{True{}, t}, low(1n+q, 0n)) : Word(1n+q)}, lt_zero(Nat.double(Word.to_nat(q, t)), h))
376	        case 1n+r:
377	          match w:
378	            case WCon{+b, +t}:
379	              match b:
380	                case False{}:
381	                  %mask_word(q, r, t, lt_half(False{}, Word.to_nat(q, t), r, h)) : {WCon{False{}, t} == WCon{False{}, _} : Word(1n+q)}
382	                  {==}
383	                case True{}:
384	                  %mask_word(q, r, t, lt_half(True{}, Word.to_nat(q, t), r, h)) : {WCon{True{}, t} == WCon{True{}, _} : Word(1n+q)}
385	                  {==}
386	
387	def unit(m: Nat, +k: Nat) -> Word(m):
388	  match m:
389	    case 0n:
390	      WNil{}
391	    case 1n+q:
392	      match k:
393	        case 0n:
394	          WCon{True{}, Word.zero(q)}
395	        case 1n+r:
396	          WCon{False{}, unit(q, r)}
397	
398	def zero_nat(+q: Nat) -> {0n == Word.to_nat(q, Word.zero(q)) : Nat}:
399	  match q:
400	    case 0n:
401	      {==}
402	    case 1n+p:
403	      %zero_nat(p) : {0n == Nat.double(_) : Nat}
404	      {==}
405	
406	def unit_nat(+m: Nat, +k: Nat, h: {Nat.is_lt(k, m) == True{} : Bool}) -> {Model.capacity(k) == Word.to_nat(m, unit(m, k)) : Nat}:
407	  match m:
408	    case 0n:
409	      match k:
410	        case 0n:
411	          Empty.absurd({1n == 0n : Nat}, clash(h))
412	        case 1n+r:
413	          Empty.absurd({Model.capacity(1n+r) == 0n : Nat}, clash(h))
414	    case 1n+q:
415	      match k:
416	        case 0n:
417	          %zero_nat(q) : {1n == 1n+Nat.double(_) : Nat}
418	          {==}
419	        case 1n+r:
420	          %unit_nat(q, r, h) : {Model.capacity(1n+r) == Nat.double(_) : Nat}
421	          double_self(Model.capacity(r))
422	
423	def truth(value: Bool) -> Data:
424	  match value:
425	    case True{}:
426	      Unit
427	    case False{}:
428	      Empty
429	
430	def clash_true(equal: {True{} == False{} : Bool}) -> Empty:
431	  %equal : truth(_)
432	  Unit{}
433	
434	def le_succ(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(a, 1n+b) == True{} : Bool}:
435	  match a:
436	    case 0n:
437	      {==}
438	    case 1n+p:
439	      match b:
440	        case 0n:
441	          Empty.absurd({Nat.is_le(1n+p, 1n) == True{} : Bool}, clash(h))
442	        case 1n+q:
443	          le_succ(p, q, h)
444	
445	def not_lt_le(+a: Nat, +b: Nat, h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.is_le(b, a) == True{} : Bool}:
446	  match a:
447	    case 0n:
448	      match b:
449	        case 0n:
450	          {==}
451	        case 1n+q:
452	          Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, clash_true(h))
453	    case 1n+p:
454	      match b:
455	        case 0n:
456	          {==}
457	        case 1n+q:
458	          not_lt_le(p, q, h)
459	
460	def lt_add_cancel(+c: Nat, +j: Nat, +k: Nat, h: {Nat.is_lt(Nat.add(c, j), Nat.add(c, k)) == True{} : Bool}) ->
461	  {Nat.is_lt(j, k) == True{} : Bool}:
462	  match c:
463	    case 0n:
464	      h
465	    case 1n+r:
466	      lt_add_cancel(r, j, k, h)
467	
468	def and_left(+a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
469	  match a:
470	    case False{}:
471	      Empty.absurd({False{} == True{} : Bool}, clash(h))
472	    case True{}:
473	      {==}
474	
475	def and_right(+a: Bool, -b: Bool, h: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
476	  match a:
477	    case False{}:
478	      Empty.absurd({b == True{} : Bool}, clash(h))
479	    case True{}:
480	      h
481	
482	def sub_u32(+i: U32, +c: U32, h: {Nat.is_le(U32.to_nat(c), U32.to_nat(i)) == True{} : Bool}) ->
483	  {U32.to_nat(i) == Nat.add(U32.to_nat(c), U32.to_nat(U32.sub(i, c))) : Nat}:
484	  match i c:
485	    case U32{x} U32{y}:
486	      Equal.sym(Nat, Nat.add(Word.to_nat(32n, y), Word.to_nat(32n, Word.adc(32n, x, y, True{}, True{}))), Word.to_nat(32n, x),
487	        sub_word(32n, x, y, True{}, h))