1	# Generated by gen/proof.py; do not edit by hand. The proofs of LAWS_div.bend:
2	# division.
3	import Base
4	import bend-osdev-u32@0.1.0.0/u32.bend as U
5	import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
6	import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
7	import ./word64.bend as W
8	import ./LAWS.bend as WB
9	import ./PROOF.bend as WBP
10	import ./proof_value.bend as P
11	import ./proof_shift.bend as PS
12	import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
13	import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
14	import ./LAWS_bits.bend as LB
15	import ./PROOF_bits.bend as LBP
16	import ./LAWS_div.bend as Laws
17	
18	# Bounds in the exact form a lemma takes them: a U32 value below 2^32, a W64
19	# value below 2^64
20	
21	def wu.ve(+w: Word(32n)) -> {Word.to_nat(32n, w) == U32.to_nat(U32{w}) : Nat}:
22	  {==}
23	
24	def wu.lt(+x: U32) -> {Nat.is_lt(U32.to_nat(x), U.U32Nat.dbl(32n, 1n)) == True{} : Bool}:
25	  match x:
26	    case U32{+w}:
27	      %wu.ve(w) : {Nat.is_lt(_, U.U32Nat.dbl(32n, 1n)) == True{} : Bool}
28	      UL.word_value_lt(32n, w)
29	
30	def wv.g(+n: Nat, +m: Nat, +h: Word(n), +l: Word(n), e: {Nat.add(n, n) == m : Nat}) -> {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(m, 1n)) == True{} : Bool}:
31	  %e : {Nat.is_lt(P.wv.V(n, h, l), U.U32Nat.dbl(_, 1n)) == True{} : Bool}
32	  %UL.dbl_dbl(n, n, 1n) : {Nat.is_lt(P.wv.V(n, h, l), _) == True{} : Bool}
33	  P.wv.val_lt2(n, Word.to_nat(n, l), Word.to_nat(n, h), UL.word_value_lt(n, l), UL.word_value_lt(n, h))
34	
35	def wv.ve(+h: Word(32n), +l: Word(32n)) -> {P.wv.V(32n, h, l) == W.W64.to_nat(W.W64{U32{h}, U32{l}}) : Nat}:
36	  {==}
37	
38	def wv.lt64(+x: W.W64) -> {Nat.is_lt(W.W64.to_nat(x), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}:
39	  match x:
40	    case W.W64{U32{+h}, U32{+l}}:
41	      %wv.ve(h, l) : {Nat.is_lt(_, U.U32Nat.dbl(64n, 1n)) == True{} : Bool}
42	      wv.g(32n, 64n, h, l, {==})
43	
44	def wn.sub0(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
45	  match x:
46	    case 0n:
47	      {==}
48	    case 1n+ +p:
49	      {==}
50	
51	def wn.le0(x: Nat) -> {Nat.is_le(0n, x) == True{} : Bool}:
52	  match x:
53	    case 0n:
54	      {==}
55	    case 1n+ +p:
56	      {==}
57	
58	def wn.ft(e: {False{} == True{} : Bool}) -> Empty:
59	  P.wn.ft(e)
60	
61	def wn.tf(e: {True{} == False{} : Bool}) -> Empty:
62	  PS.ns.tf(e)
63	
64	def wn.ge_lt(c: Cmp) -> {Cmp.is_ge(c) == Bool.not(Cmp.is_lt(c)) : Bool}:
65	  match c:
66	    case LT{}:
67	      {==}
68	    case EQ{}:
69	      {==}
70	    case GT{}:
71	      {==}
72	
73	def wm.fn(+h: Nat, +n: Nat, +x: Nat, +en: {Nat.add(h, h) == n : Nat}) -> {U.U32Nat.dbl(n, x) == U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)) : Nat}:
74	  Equal.trans(Nat, U.U32Nat.dbl(n, x), U.U32Nat.dbl(Nat.add(h, h), x), U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)), Equal.cong(Nat, Nat, zz => U.U32Nat.dbl(zz, x), n, Nat.add(h, h), Equal.sym(Nat, Nat.add(h, h), n, en)), Equal.sym(Nat, U.U32Nat.dbl(h, U.U32Nat.dbl(h, x)), U.U32Nat.dbl(Nat.add(h, h), x), UL.dbl_dbl(h, h, x)))
75	
76	# Division: W64.div.go reads the bits of a's two halves, most significant
77	# first (W64.div.bits), one W64.div.step a bit. Reading the m bits of w onto
78	# (q, r) with r < b gives (q', r') with q' b + r' = (q b + r) 2^m + w and
79	# r' < b (wd.bits, by induction on w), each step being bend-osdev-u32's
80	# divstep_value and divstep_lt at n = 64; the bound
81	# (q b + r) 2^m + w < 2^64 keeps q's shifts from wrapping.
82	
83	def wd.lt2(x: Nat, h: {Nat.is_lt(x, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {Nat.is_le(x, 1n) == True{} : Bool}:
84	  match x:
85	    case 0n:
86	      {==}
87	    case 1n+ +p:
88	      match p:
89	        case 0n:
90	          {==}
91	        case 1n+ +q:
92	          match q:
93	            case 0n:
94	              Empty.absurd({Nat.is_le(2n, 1n) == True{} : Bool}, wn.ft(h))
95	            case 1n+ +r:
96	              Empty.absurd({Nat.is_le(3n+r, 1n) == True{} : Bool}, wn.ft(h))
97	
98	def wd.bt(x: Nat, h: {Nat.is_lt(x, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}) -> {U.U32Nat.bit(Nat.is_eq(x, 1n)) == x : Nat}:
99	  match x:
100	    case 0n:
101	      {==}
102	    case 1n+ +p:
103	      match p:
104	        case 0n:
105	          {==}
106	        case 1n+ +q:
107	          match q:
108	            case 0n:
109	              Empty.absurd({U.U32Nat.bit(Nat.is_eq(2n, 1n)) == 2n : Nat}, wn.ft(h))
110	            case 1n+ +r:
111	              Empty.absurd({U.U32Nat.bit(Nat.is_eq(3n+r, 1n)) == 3n+r : Nat}, wn.ft(h))
112	
113	def wd.bv(g: Bool) -> {U32.to_nat(W.W64.bit(g)) == U.U32Nat.bit(g) : Nat}:
114	  match g:
115	    case True{}:
116	      {==}
117	    case False{}:
118	      {==}
119	
120	def wd.bl(g: Bool) -> {Nat.is_lt(U32.to_nat(W.W64.bit(g)), U.U32Nat.dbl(1n, 1n)) == True{} : Bool}:
121	  match g:
122	    case True{}:
123	      {==}
124	    case False{}:
125	      {==}
126	
127	# the top bit of a word, below 2
128	def wd.top(+x: W.W64) -> {Nat.is_lt(U32.to_nat(U32.shrn(W.W64.hi(x), 31n)), U.U32Nat.dbl(1n, 1n)) == True{} : Bool}:
129	  Equal.trans(Bool, Nat.is_lt(U32.to_nat(U32.shrn(W.W64.hi(x), 31n)), U.U32Nat.dbl(1n, 1n)), Nat.is_lt(U.U32Nat.high(31n, U32.to_nat(W.W64.hi(x))), U.U32Nat.dbl(1n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(1n, 1n)), U32.to_nat(U32.shrn(W.W64.hi(x), 31n)), U.U32Nat.high(31n, U32.to_nat(W.W64.hi(x))), Equal.sym(Nat, U.U32Nat.high(31n, U32.to_nat(W.W64.hi(x))), U32.to_nat(U32.shrn(W.W64.hi(x), 31n)), Equal.sym(Nat, U32.to_nat(U32.shrn(W.W64.hi(x), 31n)), U.U32Nat.high(31n, U32.to_nat(W.W64.hi(x))), UL.u32_shrn_value(W.W64.hi(x), 31n)))), UL.high_lt(31n, 1n, 32n, U32.to_nat(W.W64.hi(x)), {==}, wu.lt(W.W64.hi(x))))
130	
131	def wd.nz(x: Nat, e: {Nat.is_eq(x, 0n) == False{} : Bool}) -> {Nat.is_lt(0n, x) == True{} : Bool}:
132	  match x:
133	    case 0n:
134	      Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, wn.tf(e))
135	    case 1n+ +p:
136	      {==}
137	
138	# the value of a word one bit longer
139	def wd.wv(p: Nat, x: Bool, t: Word(p)) -> {Word.to_nat(1n+p, WCon{x, t}) == Nat.add(U.U32Nat.bit(x), Nat.double(Word.to_nat(p, t))) : Nat}:
140	  match x:
141	    case True{}:
142	      {==}
143	    case False{}:
144	      {==}
145	
146	# a pair is its two parts
147	def wd.eta(p: W.W64 & W.W64) -> {p == (W.W64.fst(p), W.W64.snd(p)) : W.W64 & W.W64}:
148	  (q, r) = p
149	  {==}
150	
151	def wd.p1(-x: Nat, -y: Nat, -c: Nat, -d: Nat, pr: {x == y : Nat} & {Nat.is_lt(c, d) == True{} : Bool}) -> {x == y : Nat}:
152	  (+u, +v) = pr
153	  u
154	
155	def wd.p2(-x: Nat, -y: Nat, -c: Nat, -d: Nat, pr: {x == y : Nat} & {Nat.is_lt(c, d) == True{} : Bool}) -> {Nat.is_lt(c, d) == True{} : Bool}:
156	  (+u, +v) = pr
157	  v
158	
159	def wr.d0(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(x2, x3)) == Nat.add(x1, Nat.add(x0, U.U32Nat.dbl(x2, x3))) : Nat}:
160	  %Equal.sym(Nat, Nat.add(Nat.add(x0, x1), U.U32Nat.dbl(x2, x3)), Nat.add(x0, Nat.add(x1, U.U32Nat.dbl(x2, x3))), UL.nat_add_assoc(x0, x1, U.U32Nat.dbl(x2, x3))) : {_ == Nat.add(x1, Nat.add(x0, U.U32Nat.dbl(x2, x3))) : Nat}
161	  %Equal.sym(Nat, Nat.add(x0, Nat.add(x1, U.U32Nat.dbl(x2, x3))), Nat.add(x1, Nat.add(x0, U.U32Nat.dbl(x2, x3))), Equal.sym(Nat, Nat.add(x1, Nat.add(x0, U.U32Nat.dbl(x2, x3))), Nat.add(x0, Nat.add(x1, U.U32Nat.dbl(x2, x3))), UL.nat_add_left_comm(x1, x0, U.U32Nat.dbl(x2, x3)))) : {_ == Nat.add(x1, Nat.add(x0, U.U32Nat.dbl(x2, x3))) : Nat}
162	  {==}
163	
164	def wr.d1(+x0: Nat, +x1: Nat, +x2: Nat) -> {Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}:
165	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2), x0)) : {_ == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
166	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x0)), UL.nat_add_assoc(Nat.mul(x0, x2), x2, x0)) : {Nat.add(Nat.mul(x0, x1), _) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
167	  %Equal.sym(Nat, Nat.add(x2, x0), Nat.add(x0, x2), UL.nat_add_comm(x2, x0)) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _)) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
168	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2)), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, x2)) : {Nat.add(Nat.mul(x0, x1), _) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
169	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(Nat.mul(x0, x2), x2))) : {_ == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
170	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2)), x2), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2)), x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.mul(x0, x2), x2))) : {Nat.add(x0, _) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
171	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2)), x2)), Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2))), x2), Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2))), x2), Nat.add(x0, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2)), x2)), UL.nat_add_assoc(x0, Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2)), x2))) : {_ == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
172	  %Equal.sym(Nat, x0, Nat.mul(1n, x0), Equal.sym(Nat, Nat.mul(1n, x0), x0, UL.nat_one_mul(x0))) : {Nat.add(Nat.add(_, Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2))), x2) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
173	  %Equal.sym(Nat, Nat.mul(1n, x0), Nat.mul(x0, 1n), Equal.sym(Nat, Nat.mul(x0, 1n), Nat.mul(1n, x0), UL.nat_mul_comm(x0, 1n))) : {Nat.add(Nat.add(_, Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2))), x2) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
174	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2)), Nat.mul(x0, Nat.add(x1, x2)), Equal.sym(Nat, Nat.mul(x0, Nat.add(x1, x2)), Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x2)), UL.nat_mul_add(x0, x1, x2))) : {Nat.add(Nat.add(Nat.mul(x0, 1n), _), x2) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
175	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, 1n), Nat.mul(x0, Nat.add(x1, x2))), Nat.mul(x0, Nat.add(1n, Nat.add(x1, x2))), Equal.sym(Nat, Nat.mul(x0, Nat.add(1n, Nat.add(x1, x2))), Nat.add(Nat.mul(x0, 1n), Nat.mul(x0, Nat.add(x1, x2))), UL.nat_mul_add(x0, 1n, Nat.add(x1, x2)))) : {Nat.add(_, x2) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
176	  %Equal.sym(Nat, Nat.add(1n, Nat.add(x1, x2)), Nat.add(x1, Nat.add(1n, x2)), Equal.sym(Nat, Nat.add(x1, Nat.add(1n, x2)), Nat.add(1n, Nat.add(x1, x2)), UL.nat_add_left_comm(x1, 1n, x2))) : {Nat.add(Nat.mul(x0, _), x2) == Nat.add(Nat.mul(x0, Nat.add(x1, 1n+x2)), x2) : Nat}
177	  {==}
178	
179	def wr.d2(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), x3), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}:
180	  %Equal.sym(Nat, Nat.double(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), UL.nat_double(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))) : {Nat.add(Nat.add(_, x3), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
181	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))) : {Nat.add(Nat.add(_, x3), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
182	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), UL.nat_add_assoc(Nat.mul(x0, x2), x2, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))) : {Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), _), x3), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
183	  %Equal.sym(Nat, Nat.add(x2, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), Nat.add(x2, Nat.add(Nat.mul(x0, x2), x2))), UL.nat_add_left_comm(x2, Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))) : {Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _)), x3), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
184	  %Equal.sym(Nat, Nat.add(x2, Nat.add(Nat.mul(x0, x2), x2)), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), UL.nat_add_left_comm(x2, Nat.mul(x0, x2), x2)) : {Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x1), _))), x3), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
185	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), UL.nat_add_left_comm(Nat.mul(x0, x2), Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))) : {Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), _), x3), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
186	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), x3), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3)) : {Nat.add(_, Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
187	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3)) : {Nat.add(Nat.add(Nat.mul(x0, x1), _), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
188	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3)), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3)) : {Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), _)), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
189	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(x2, x2), x3)), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.add(x2, x2), x3)) : {Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _))), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
190	  %Equal.sym(Nat, Nat.add(Nat.add(x2, x2), x3), Nat.add(x2, Nat.add(x2, x3)), UL.nat_add_assoc(x2, x2, x3)) : {Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), _)))), Nat.double(x0)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
191	  %Equal.sym(Nat, Nat.double(x0), Nat.add(x0, x0), UL.nat_double(x0)) : {Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))), _) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
192	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))), Nat.add(x0, x0)), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))), Nat.add(x0, x0))), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))), Nat.add(x0, x0))) : {_ == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
193	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))), Nat.add(x0, x0)), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))), Nat.add(x0, x0))), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))), Nat.add(x0, x0))) : {Nat.add(Nat.mul(x0, x1), _) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
194	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))), Nat.add(x0, x0)), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))), Nat.add(x0, x0))), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))), Nat.add(x0, x0))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), _)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
195	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))), Nat.add(x0, x0)), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(x2, Nat.add(x2, x3)), Nat.add(x0, x0))), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)), Nat.add(x0, x0))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
196	  %Equal.sym(Nat, Nat.add(Nat.add(x2, Nat.add(x2, x3)), Nat.add(x0, x0)), Nat.add(x2, Nat.add(Nat.add(x2, x3), Nat.add(x0, x0))), UL.nat_add_assoc(x2, Nat.add(x2, x3), Nat.add(x0, x0))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), _)))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
197	  %Equal.sym(Nat, Nat.add(Nat.add(x2, x3), Nat.add(x0, x0)), Nat.add(x2, Nat.add(x3, Nat.add(x0, x0))), UL.nat_add_assoc(x2, x3, Nat.add(x0, x0))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, _))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
198	  %Equal.sym(Nat, Nat.add(x3, Nat.add(x0, x0)), Nat.add(x0, Nat.add(x3, x0)), UL.nat_add_left_comm(x3, x0, x0)) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, _)))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
199	  %Equal.sym(Nat, Nat.add(x3, x0), Nat.add(x0, x3), UL.nat_add_comm(x3, x0)) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, Nat.add(x0, _))))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
200	  %Equal.sym(Nat, Nat.add(x2, Nat.add(x0, Nat.add(x0, x3))), Nat.add(x0, Nat.add(x2, Nat.add(x0, x3))), UL.nat_add_left_comm(x2, x0, Nat.add(x0, x3))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, _))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
201	  %Equal.sym(Nat, Nat.add(x2, Nat.add(x0, x3)), Nat.add(x0, Nat.add(x2, x3)), UL.nat_add_left_comm(x2, x0, x3)) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x0, _)))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
202	  %Equal.sym(Nat, Nat.add(x2, Nat.add(x0, Nat.add(x0, Nat.add(x2, x3)))), Nat.add(x0, Nat.add(x2, Nat.add(x0, Nat.add(x2, x3)))), UL.nat_add_left_comm(x2, x0, Nat.add(x0, Nat.add(x2, x3)))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), _)))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
203	  %Equal.sym(Nat, Nat.add(x2, Nat.add(x0, Nat.add(x2, x3))), Nat.add(x0, Nat.add(x2, Nat.add(x2, x3))), UL.nat_add_left_comm(x2, x0, Nat.add(x2, x3))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x0, _))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
204	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(x0, Nat.add(x2, Nat.add(x2, x3))))), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(x2, Nat.add(x2, x3))))), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, Nat.add(x0, Nat.add(x2, Nat.add(x2, x3))))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
205	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(x2, Nat.add(x2, x3)))), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, Nat.add(x2, Nat.add(x2, x3)))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x0, _)))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
206	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), _)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
207	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(x0, _))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
208	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))))) : {Nat.add(Nat.mul(x0, x1), _) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
209	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))) : {Nat.add(Nat.mul(x0, x1), Nat.add(x0, _)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
210	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3)))))))) : {_ == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
211	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x2, x3))))))) : {Nat.add(x0, _) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
212	  %Equal.sym(Nat, Nat.add(x2, Nat.add(x2, x3)), Nat.add(Nat.add(x2, x2), x3), Equal.sym(Nat, Nat.add(Nat.add(x2, x2), x3), Nat.add(x2, Nat.add(x2, x3)), UL.nat_add_assoc(x2, x2, x3))) : {Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), _)))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
213	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(x2, x2), x3)), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(x2, x2), x3)), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.add(x2, x2), x3))) : {Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _))))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
214	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3)), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3)), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), x3))) : {Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), _)))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
215	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))), x3))) : {Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), _))) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
216	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), x3), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), x3), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), x3))) : {Nat.add(x0, Nat.add(x0, _)) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
217	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), x3)), Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), x3), Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), x3), Nat.add(x0, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), x3)), UL.nat_add_assoc(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), x3))) : {Nat.add(x0, _) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
218	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), x3)), Nat.add(Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))))), x3), Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))))), x3), Nat.add(x0, Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), x3)), UL.nat_add_assoc(x0, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), x3))) : {_ == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
219	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))))) : {Nat.add(Nat.add(x0, _), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
220	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))), UL.nat_add_left_comm(Nat.mul(x0, x2), Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))) : {Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(x0, _))), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
221	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), Nat.add(x0, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2))))), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)))))) : {Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), _)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
222	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), Nat.add(x2, Nat.add(Nat.mul(x0, x2), x2)), Equal.sym(Nat, Nat.add(x2, Nat.add(Nat.mul(x0, x2), x2)), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x2)), UL.nat_add_left_comm(x2, Nat.mul(x0, x2), x2))) : {Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), _))))), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
223	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x2, Nat.add(Nat.mul(x0, x2), x2))), Nat.add(x2, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Equal.sym(Nat, Nat.add(x2, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), Nat.add(x2, Nat.add(Nat.mul(x0, x2), x2))), UL.nat_add_left_comm(x2, Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))) : {Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), Nat.add(x0, _)))), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
224	  %Equal.sym(Nat, Nat.add(x0, Nat.add(x2, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Nat.add(x2, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Equal.sym(Nat, Nat.add(x2, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Nat.add(x0, Nat.add(x2, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), UL.nat_add_left_comm(x2, x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))))) : {Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _))), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
225	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))))), Nat.add(Nat.add(Nat.mul(x0, x2), x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Nat.add(Nat.mul(x0, x2), Nat.add(x2, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))))), UL.nat_add_assoc(Nat.mul(x0, x2), x2, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))))) : {Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), _)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
226	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))))), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))))), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))))) : {Nat.add(Nat.add(x0, _), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
227	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))))), Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Equal.sym(Nat, Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))), Nat.add(x0, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))))), UL.nat_add_assoc(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)))))) : {Nat.add(_, x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
228	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2))), Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(Nat.mul(x0, x2), x2)))) : {Nat.add(Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), _), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
229	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2)), Nat.add(Nat.mul(x0, x2), Nat.add(x0, x2)), Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2)), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, x2))) : {Nat.add(Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), _)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
230	  %Equal.sym(Nat, Nat.add(x0, x2), Nat.add(x2, x0), Equal.sym(Nat, Nat.add(x2, x0), Nat.add(x0, x2), UL.nat_add_comm(x2, x0))) : {Nat.add(Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _))), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
231	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x2, x0)), Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x0)), UL.nat_add_assoc(Nat.mul(x0, x2), x2, x0))) : {Nat.add(Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), _)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
232	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2), x0))) : {Nat.add(Nat.add(Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), _), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
233	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2))), Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2))), Nat.add(x0, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2))), UL.nat_add_left_comm(Nat.mul(x0, x1), x0, Nat.add(Nat.mul(x0, x2), x2)))) : {Nat.add(Nat.add(_, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
234	  %Equal.sym(Nat, Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2)), Nat.add(Nat.mul(x0, x2), Nat.add(x0, x2)), Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x0, x2)), Nat.add(x0, Nat.add(Nat.mul(x0, x2), x2)), UL.nat_add_left_comm(Nat.mul(x0, x2), x0, x2))) : {Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), _), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
235	  %Equal.sym(Nat, Nat.add(x0, x2), Nat.add(x2, x0), Equal.sym(Nat, Nat.add(x2, x0), Nat.add(x0, x2), UL.nat_add_comm(x2, x0))) : {Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), _)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
236	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(x2, x0)), Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0), Nat.add(Nat.mul(x0, x2), Nat.add(x2, x0)), UL.nat_add_assoc(Nat.mul(x0, x2), x2, x0))) : {Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), _), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
237	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x2), x2), x0)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2), x0))) : {Nat.add(Nat.add(_, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
238	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), Equal.sym(Nat, Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), Nat.add(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), UL.nat_double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)))) : {Nat.add(_, x3) == Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x2), x2)), x0)), x3) : Nat}
239	  {==}
240	
241	def wr.d3(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.mul(Nat.add(Nat.double(x0), x1), x2), x3) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}:
242	  %Equal.sym(Nat, Nat.double(x0), Nat.add(x0, x0), UL.nat_double(x0)) : {Nat.add(Nat.mul(Nat.add(_, x1), x2), x3) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
243	  %Equal.sym(Nat, Nat.add(Nat.add(x0, x0), x1), Nat.add(x0, Nat.add(x0, x1)), UL.nat_add_assoc(x0, x0, x1)) : {Nat.add(Nat.mul(_, x2), x3) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
244	  %Equal.sym(Nat, Nat.mul(Nat.add(x0, Nat.add(x0, x1)), x2), Nat.add(Nat.mul(x0, x2), Nat.mul(Nat.add(x0, x1), x2)), UL.nat_add_mul(x0, Nat.add(x0, x1), x2)) : {Nat.add(_, x3) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
245	  %Equal.sym(Nat, Nat.mul(Nat.add(x0, x1), x2), Nat.add(Nat.mul(x0, x2), Nat.mul(x1, x2)), UL.nat_add_mul(x0, x1, x2)) : {Nat.add(Nat.add(Nat.mul(x0, x2), _), x3) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
246	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.mul(x1, x2))), x3), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.mul(x1, x2)), x3)), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.mul(x1, x2)), x3)) : {_ == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
247	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.mul(x1, x2)), x3), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x1, x2), x3)), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.mul(x1, x2), x3)) : {Nat.add(Nat.mul(x0, x2), _) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
248	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x1, x2), x3))), Nat.add(Nat.add(Nat.mul(x0, x2), Nat.mul(x0, x2)), Nat.add(Nat.mul(x1, x2), x3)), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x2), Nat.mul(x0, x2)), Nat.add(Nat.mul(x1, x2), x3)), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x0, x2), Nat.add(Nat.mul(x1, x2), x3))), UL.nat_add_assoc(Nat.mul(x0, x2), Nat.mul(x0, x2), Nat.add(Nat.mul(x1, x2), x3)))) : {_ == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
249	  %Equal.sym(Nat, Nat.add(Nat.mul(x1, x2), x3), Nat.add(x3, Nat.mul(x1, x2)), Equal.sym(Nat, Nat.add(x3, Nat.mul(x1, x2)), Nat.add(Nat.mul(x1, x2), x3), UL.nat_add_comm(x3, Nat.mul(x1, x2)))) : {Nat.add(Nat.add(Nat.mul(x0, x2), Nat.mul(x0, x2)), _) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
250	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x2), Nat.mul(x0, x2)), Nat.double(Nat.mul(x0, x2)), Equal.sym(Nat, Nat.double(Nat.mul(x0, x2)), Nat.add(Nat.mul(x0, x2), Nat.mul(x0, x2)), UL.nat_double(Nat.mul(x0, x2)))) : {Nat.add(_, Nat.add(x3, Nat.mul(x1, x2))) == Nat.add(Nat.double(Nat.mul(x0, x2)), Nat.add(x3, Nat.mul(x1, x2))) : Nat}
251	  {==}
252	
253	def wr.d4(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(Nat.double(Nat.mul(x0, x1)), Nat.add(x2, Nat.double(x3))) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}:
254	  %Equal.sym(Nat, Nat.double(Nat.mul(x0, x1)), Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x1)), UL.nat_double(Nat.mul(x0, x1))) : {Nat.add(_, Nat.add(x2, Nat.double(x3))) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
255	  %Equal.sym(Nat, Nat.double(x3), Nat.add(x3, x3), UL.nat_double(x3)) : {Nat.add(Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x1)), Nat.add(x2, _)) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
256	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.mul(x0, x1)), Nat.add(x2, Nat.add(x3, x3))), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(x2, Nat.add(x3, x3)))), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.mul(x0, x1), Nat.add(x2, Nat.add(x3, x3)))) : {_ == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
257	  %Equal.sym(Nat, Nat.add(x2, Nat.add(x3, x3)), Nat.add(x3, Nat.add(x2, x3)), Equal.sym(Nat, Nat.add(x3, Nat.add(x2, x3)), Nat.add(x2, Nat.add(x3, x3)), UL.nat_add_left_comm(x3, x2, x3))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), _)) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
258	  %Equal.sym(Nat, Nat.add(x2, x3), Nat.add(x3, x2), Equal.sym(Nat, Nat.add(x3, x2), Nat.add(x2, x3), UL.nat_add_comm(x3, x2))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(x3, _))) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
259	  %Equal.sym(Nat, Nat.add(x3, Nat.add(x3, x2)), Nat.add(Nat.add(x3, x3), x2), Equal.sym(Nat, Nat.add(Nat.add(x3, x3), x2), Nat.add(x3, Nat.add(x3, x2)), UL.nat_add_assoc(x3, x3, x2))) : {Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), _)) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
260	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(x3, x3), x2)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3)), x2), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3)), x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(x3, x3), x2)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(x3, x3), x2))) : {Nat.add(Nat.mul(x0, x1), _) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
261	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3)), x2)), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3))), x2), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3))), x2), Nat.add(Nat.mul(x0, x1), Nat.add(Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3)), x2)), UL.nat_add_assoc(Nat.mul(x0, x1), Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3)), x2))) : {_ == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
262	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3)), Nat.add(x3, Nat.add(Nat.mul(x0, x1), x3)), Equal.sym(Nat, Nat.add(x3, Nat.add(Nat.mul(x0, x1), x3)), Nat.add(Nat.mul(x0, x1), Nat.add(x3, x3)), UL.nat_add_left_comm(x3, Nat.mul(x0, x1), x3))) : {Nat.add(Nat.add(Nat.mul(x0, x1), _), x2) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
263	  %Equal.sym(Nat, Nat.add(Nat.mul(x0, x1), Nat.add(x3, Nat.add(Nat.mul(x0, x1), x3))), Nat.add(Nat.add(Nat.mul(x0, x1), x3), Nat.add(Nat.mul(x0, x1), x3)), Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), x3), Nat.add(Nat.mul(x0, x1), x3)), Nat.add(Nat.mul(x0, x1), Nat.add(x3, Nat.add(Nat.mul(x0, x1), x3))), UL.nat_add_assoc(Nat.mul(x0, x1), x3, Nat.add(Nat.mul(x0, x1), x3)))) : {Nat.add(_, x2) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
264	  %Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(x0, x1), x3), Nat.add(Nat.mul(x0, x1), x3)), Nat.double(Nat.add(Nat.mul(x0, x1), x3)), Equal.sym(Nat, Nat.double(Nat.add(Nat.mul(x0, x1), x3)), Nat.add(Nat.add(Nat.mul(x0, x1), x3), Nat.add(Nat.mul(x0, x1), x3)), UL.nat_double(Nat.add(Nat.mul(x0, x1), x3)))) : {Nat.add(_, x2) == Nat.add(Nat.double(Nat.add(Nat.mul(x0, x1), x3)), x2) : Nat}
265	  {==}
266	
267	def wd.k(+N: Nat, +Q: Nat, +B: Nat, +R: Nat, +tx: Nat, +Sr: Nat, +tr: Nat, +R2: Nat, +Sq: Nat, +tq: Nat, +Q1: Nat, +R1: Nat, +T: Bool, +L: Bool, +g: Bool, +hR: {Nat.is_lt(R, B) == True{} : Bool}, +hB: {Nat.is_lt(B, U.U32Nat.dbl(N, 1n)) == True{} : Bool}, +hX: {Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), U.U32Nat.dbl(N, 1n)) == True{} : Bool}, +fr: {Nat.add(Sr, U.U32Nat.dbl(N, tr)) == Nat.double(R) : Nat}, +fq: {Nat.add(Sq, U.U32Nat.dbl(N, tq)) == Nat.double(Q) : Nat}, +er2: {R2 == Nat.add(Sr, tx) : Nat}, +eq1: {Q1 == Nat.add(Sq, U.U32Nat.bit(g)) : Nat}, +htx: {Nat.is_lt(tx, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}, +htr: {Nat.is_lt(tr, U.U32Nat.dbl(1n, 1n)) == True{} : Bool}, +eT: {T == Nat.is_eq(tr, 1n) : Bool}, +eL: {Nat.is_lt(R2, B) == L : Bool}, +eg: {Bool.or(T, Bool.not(L)) == g : Bool}, +er1: {Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)) == Nat.add(R2, U.U32Nat.dbl(N, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(L)))) : Nat}) -> {Nat.add(Nat.mul(Q1, B), R1) == Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}:
268	  +bT = Equal.trans(Nat, U.U32Nat.bit(T), U.U32Nat.bit(Nat.is_eq(tr, 1n)), tr, Equal.cong(Bool, Nat, zz => U.U32Nat.bit(zz), T, Nat.is_eq(tr, 1n), eT), wd.bt(tr, htr))
269	  +eput = Equal.trans(Nat, Nat.add(R2, U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(tx, Nat.add(Sr, U.U32Nat.dbl(N, tr))), Nat.add(tx, Nat.double(R)), Equal.trans(Nat, Nat.add(R2, U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, tr)), Nat.add(tx, Nat.add(Sr, U.U32Nat.dbl(N, tr))), Equal.trans(Nat, Nat.add(R2, U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, U.U32Nat.bit(T))), Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, tr)), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(N, U.U32Nat.bit(T))), R2, Nat.add(Sr, tx), er2), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Sr, tx), U.U32Nat.dbl(N, zz)), U.U32Nat.bit(T), tr, bT)), wr.d0(Sr, tx, N, tr)), Equal.cong(Nat, Nat, zz => Nat.add(tx, zz), Nat.add(Sr, U.U32Nat.dbl(N, tr)), Nat.double(R), fr))
270	  +c1 = UL.divstep_value(N, R2, B, R, tx, R1, T, L, g, eput, eL, eg, er1, wd.lt2(tx, htx), hR, hB)
271	  +c2 = UL.divstep_lt(N, R2, B, R, tx, R1, T, L, g, eput, eL, eg, er1, wd.lt2(tx, htx), hR, hB)
272	  +qle = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R)), Q), Nat.add(Nat.mul(Q, Nat.add(Nat.sub(B, 1n+R), 1n+R)), R), Nat.add(Nat.mul(Q, B), R), wr.d1(Q, Nat.sub(B, 1n+R), R), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Q, zz), R), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, UL.nat_lt_witness(R, B, hR)))
273	  +hQ = UO.nat_le_lt_trans(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), U.U32Nat.dbl(N, 1n), Equal.trans(Bool, Nat.is_le(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx)), Nat.is_le(Nat.double(Q), Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q))), True{}, Equal.sym(Bool, Nat.is_le(Nat.double(Q), Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q))), Nat.is_le(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx)), Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.double(Q), zz), Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q)), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), Equal.trans(Nat, Nat.add(Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx), Nat.double(Q)), Nat.add(Nat.double(Nat.add(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R)), Q)), tx), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), wr.d2(Q, Nat.sub(B, 1n+R), R, tx), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(zz), tx), Nat.add(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R)), Q), Nat.add(Nat.mul(Q, B), R), qle)))), UL.nat_le_add(Nat.double(Q), Nat.add(Nat.double(Nat.add(Nat.mul(Q, Nat.sub(B, 1n+R)), Nat.add(Nat.mul(Q, R), R))), tx))), hX)
274	  +esq = UL.dbl_nowrap(N, tq, Sq, Nat.double(Q), Nat.double(Q), fq, UL.nat_le_refl(Nat.double(Q)), hQ)
275	  (Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(tx, Nat.double(R))), Nat.add(Nat.double(Nat.add(Nat.mul(Q, B), R)), tx), Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B))), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(tx, Nat.double(R))), Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.mul(Nat.add(Nat.double(Q), U.U32Nat.bit(g)), B), R1), Nat.add(Nat.double(Nat.mul(Q, B)), Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B))), Equal.trans(Nat, Nat.add(Nat.mul(Q1, B), R1), Nat.add(Nat.mul(Nat.add(Sq, U.U32Nat.bit(g)), B), R1), Nat.add(Nat.mul(Nat.add(Nat.double(Q), U.U32Nat.bit(g)), B), R1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(zz, B), R1), Q1, Nat.add(Sq, U.U32Nat.bit(g)), eq1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Nat.add(zz, U.U32Nat.bit(g)), B), R1), Sq, Nat.double(Q), esq)), wr.d3(Q, U.U32Nat.bit(g), B, R1)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.double(Nat.mul(Q, B)), zz), Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)), Nat.add(tx, Nat.double(R)), c1)), wr.d4(Q, B, tx, R)), c2)
276	
277	def wr.d5(+x0: Nat) -> {Nat.mul(1n, x0) == x0 : Nat}:
278	  %Equal.sym(Nat, Nat.mul(1n, x0), x0, UL.nat_one_mul(x0)) : {_ == x0 : Nat}
279	  {==}
280	
281	def wr.d6(+x0: Nat) -> {x0 == Nat.mul(1n, x0) : Nat}:
282	  %Equal.sym(Nat, x0, Nat.mul(1n, x0), Equal.sym(Nat, Nat.mul(1n, x0), x0, UL.nat_one_mul(x0))) : {_ == Nat.mul(1n, x0) : Nat}
283	  {==}
284	
285	def wr.d7(+x0: Nat, +x1: Nat, +x2: Nat) -> {Nat.add(x0, Nat.mul(0n, x1)) == Nat.add(x0, U.U32Nat.dbl(64n, Nat.mul(0n, x2))) : Nat}:
286	  %Equal.sym(Nat, Nat.add(x0, 0n), x0, UL.nat_add_zero(x0)) : {_ == Nat.add(x0, U.U32Nat.dbl(64n, Nat.mul(0n, x2))) : Nat}
287	  %Equal.sym(Nat, x0, Nat.add(x0, 0n), Equal.sym(Nat, Nat.add(x0, 0n), x0, UL.nat_add_zero(x0))) : {_ == Nat.add(x0, U.U32Nat.dbl(64n, Nat.mul(0n, x2))) : Nat}
288	  %Equal.sym(Nat, 0n, U.U32Nat.dbl(64n, 0n), Equal.sym(Nat, U.U32Nat.dbl(64n, 0n), 0n, UL.dbl_zero(64n))) : {Nat.add(x0, _) == Nat.add(x0, U.U32Nat.dbl(64n, Nat.mul(0n, x2))) : Nat}
289	  {==}
290	
291	def wd.sel(g: Bool, +r2: W.W64, +b: W.W64) -> {Nat.add(W.W64.to_nat(W.W64.sel(g, W.W64.sub(r2, b), r2)), Nat.mul(U.U32Nat.bit(g), W.W64.to_nat(b))) == Nat.add(W.W64.to_nat(r2), U.U32Nat.dbl(64n, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(W.W64.is_lt(r2, b))))) : Nat}:
292	  match g:
293	    case True{}:
294	      Equal.trans(Nat, Nat.add(W.W64.to_nat(W.W64.sub(r2, b)), Nat.mul(1n, W.W64.to_nat(b))), Nat.add(W.W64.to_nat(r2), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(r2, b)))), Nat.add(W.W64.to_nat(r2), U.U32Nat.dbl(64n, Nat.mul(1n, U.U32Nat.bit(W.W64.is_lt(r2, b))))), Equal.trans(Nat, Nat.add(W.W64.to_nat(W.W64.sub(r2, b)), Nat.mul(1n, W.W64.to_nat(b))), Nat.add(W.W64.to_nat(W.W64.sub(r2, b)), W.W64.to_nat(b)), Nat.add(W.W64.to_nat(r2), U.U32Nat.dbl(64n, U.U32Nat.bit(W.W64.is_lt(r2, b)))), Equal.cong(Nat, Nat, zz => Nat.add(W.W64.to_nat(W.W64.sub(r2, b)), zz), Nat.mul(1n, W.W64.to_nat(b)), W.W64.to_nat(b), wr.d5(W.W64.to_nat(b))), WB.sub_wrap(r2, b)), Equal.cong(Nat, Nat, zz => Nat.add(W.W64.to_nat(r2), U.U32Nat.dbl(64n, zz)), U.U32Nat.bit(W.W64.is_lt(r2, b)), Nat.mul(1n, U.U32Nat.bit(W.W64.is_lt(r2, b))), wr.d6(U.U32Nat.bit(W.W64.is_lt(r2, b)))))
295	    case False{}:
296	      wr.d7(W.W64.to_nat(r2), W.W64.to_nat(b), U.U32Nat.bit(W.W64.is_lt(r2, b)))
297	
298	def wd.st(+x: Bool, +b: W.W64, +q: W.W64, +r: W.W64, +hR: {Nat.is_lt(W.W64.to_nat(r), W.W64.to_nat(b)) == True{} : Bool}, +hb: {Nat.is_lt(W.W64.to_nat(b), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, +hX: {Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (q, r))))) == Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}:
299	  (Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U.U32Nat.bit(x)), wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.or(W.W64.shl(q, 1n), W.W64.from_u32(W.W64.bit(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), U32.to_nat(W.W64.bit(x))), W.W64.to_nat(W.W64.sel(Bool.or(U32.is_eq(U32.shrn(W.W64.hi(r), 31n), 1), W.W64.is_ge(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b)), W.W64.sub(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))), b), W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x))))), W.W64.to_nat(b), wd.k(64n, W.W64.to_nat(q), W.W64.to_nat(b), W.W64.to_nat(r), U32.to_nat(W.W64.bit(x)), W.W64.to_nat(W.W64.shl(r, 1n)), U32.to_nat(U32.shrn(W.W64.hi(r), 31n)), W.W64.to_nat(W.W64.or(W.W64.shl(r, 1n), W.W64.from_u32(W.W64.bit(x)))), W.W64.to_nat(W.W64.shl(q, 1n)), U32.to_nat(U32.shrn(W.W64.hi(q), 31n)), W.W64.to_nat(W.W6
300	
301	def wr.d8(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat, +x4: Nat, +x5: Nat) -> {Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}:
302	  %Equal.sym(Nat, Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), UL.nat_double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4))) : {Nat.add(_, x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
303	  %Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3)) : {Nat.add(Nat.add(Nat.add(_, x4), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
304	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(_, Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
305	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x4), Nat.add(x4, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
306	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, U.U32Nat.dbl(x0, x3))) : {Nat.add(Nat.add(_, Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
307	  %Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3)) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(_, x4)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
308	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), _), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
309	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x4), Nat.add(x4, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
310	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, U.U32Nat.dbl(x0, x3))) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), _), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
311	  %Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), UL.nat_add_assoc(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))) : {Nat.add(_, x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
312	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))) : {Nat.add(Nat.add(x4, _), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
313	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))) : {Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
314	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))) : {Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, _))), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
315	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))) : {Nat.add(Nat.add(x4, _), x5) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
316	  %Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), x5), Nat.add(x4, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5)), UL.nat_add_assoc(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5)) : {_ == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
317	  %Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5), Nat.add(x4, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5)), UL.nat_add_assoc(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5)) : {Nat.add(x4, _) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
318	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5)) : {Nat.add(x4, Nat.add(x4, _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
319	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5)) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
320	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, x3), x5)), UL.nat_add_assoc(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3), x5)) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
321	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x5), Nat.add(x5, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x5)) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), _))))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
322	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x5, U.U32Nat.dbl(x0, x3))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x5, U.U32Nat.dbl(x0, x3))) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
323	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
324	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))) : {Nat.add(x4, Nat.add(x4, _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
325	  %Equal.sym(Nat, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))) : {Nat.add(x4, Nat.add(x4, _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
326	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))))) : {Nat.add(x4, _) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
327	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))))) : {_ == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
328	  %Equal.sym(Nat, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x4, _))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
329	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
330	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
331	  %Equal.sym(Nat, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x5, U.U32Nat.dbl(x0, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x5, U.U32Nat.dbl(x0, x3))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x5, U.U32Nat.dbl(x0, x3)))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(x4, _)))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
332	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x5, U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x5, U.U32Nat.dbl(x0, x3)))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x5, U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x5, U.U32Nat.dbl(x0, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x4, Nat.add(x5, U.U32Nat.dbl(x0, x3))))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, _))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
333	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x5, U.U32Nat.dbl(x0, x3))))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, Nat.add(x5, U.U32Nat.dbl(x0, x3))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, Nat.add(x5, U.U32Nat.dbl(x0, x3))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x5, U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x4, Nat.add(x4, Nat.add(x5, U.U32Nat.dbl(x0, x3)))))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
334	  %Equal.sym(Nat, Nat.add(x5, U.U32Nat.dbl(x0, x3)), Nat.add(U.U32Nat.dbl(x0, x3), x5), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x5), Nat.add(x5, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x5))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, _))))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
335	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), x5)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, x5)), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, x5)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), x5)), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x4, x5))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, _)))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
336	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, x5))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, x5))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, x5))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, x5))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x4, Nat.add(x4, x5)))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), _))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
337	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, x5)))), Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(x4, x5))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(x4, x5))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, x5)))), UL.nat_add_assoc(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(x4, x5))))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
338	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(x4, x5)))), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(x4, x5))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(x4, x5))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(x4, x5)))), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(x4, x5))))) : {Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
339	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(x4, x5)))), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(x4, x5))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(x4, x5))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(x4, x5)))), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(x4, x5))))) : {_ == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
340	  %Equal.sym(Nat, Nat.add(x4, x5), Nat.add(x5, x4), Equal.sym(Nat, Nat.add(x5, x4), Nat.add(x4, x5), UL.nat_add_comm(x5, x4))) : {Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
341	  %Equal.sym(Nat, Nat.add(x4, Nat.add(x5, x4)), Nat.add(x5, Nat.add(x4, x4)), Equal.sym(Nat, Nat.add(x5, Nat.add(x4, x4)), Nat.add(x4, Nat.add(x5, x4)), UL.nat_add_left_comm(x5, x4, x4))) : {Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), _) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
342	  %Equal.sym(Nat, Nat.add(x4, x4), Nat.double(x4), Equal.sym(Nat, Nat.double(x4), Nat.add(x4, x4), UL.nat_double(x4))) : {Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(x5, _)) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
343	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))) : {Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _), Nat.add(x5, Nat.double(x4))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
344	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))) : {Nat.add(_, Nat.add(x5, Nat.double(x4))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
345	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3))) : {Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), _), Nat.add(x5, Nat.double(x4))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
346	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3))) : {Nat.add(Nat.add(_, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
347	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Equal.sym(Nat, Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), UL.nat_double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))))) : {Nat.add(_, Nat.add(x5, Nat.double(x4))) == Nat.add(Nat.double(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3))), Nat.add(x5, Nat.double(x4))) : Nat}
348	  {==}
349	
350	def wr.d9(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat, +x4: Nat, +x5: Nat) -> {Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4), x5), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}:
351	  %Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3)) : {Nat.add(Nat.add(Nat.add(_, x4), x5), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
352	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(_, x5), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
353	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x4), Nat.add(x4, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _), x5), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
354	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, U.U32Nat.dbl(x0, x3))) : {Nat.add(Nat.add(_, x5), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
355	  %Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), x5), Nat.add(x4, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x5)), UL.nat_add_assoc(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x5)) : {Nat.add(_, Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
356	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x5), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x5)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), x5)) : {Nat.add(Nat.add(x4, _), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
357	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x5), Nat.add(x5, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x5)) : {Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
358	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, U.U32Nat.dbl(x0, x3))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x5, U.U32Nat.dbl(x0, x3))) : {Nat.add(Nat.add(x4, _), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
359	  %Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3)) : {Nat.add(Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(_, x4)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
360	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), _) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
361	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x4), Nat.add(x4, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x4)) : {Nat.add(Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
362	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, U.U32Nat.dbl(x0, x3))) : {Nat.add(Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), _) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
363	  %Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), UL.nat_add_assoc(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))) : {_ == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
364	  %Equal.sym(Nat, Nat.add(Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x5, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), UL.nat_add_assoc(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))) : {Nat.add(x4, _) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
365	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))) : {Nat.add(x4, Nat.add(x5, _)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
366	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))) : {Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _))) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
367	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))) : {Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, _)))) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
368	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))) : {Nat.add(x4, Nat.add(x5, _)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
369	  %Equal.sym(Nat, Nat.add(x5, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), Nat.add(x4, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), UL.nat_add_left_comm(x5, x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))) : {Nat.add(x4, _) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
370	  %Equal.sym(Nat, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))) : {Nat.add(x4, Nat.add(x4, _)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
371	  %Equal.sym(Nat, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _))) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
372	  %Equal.sym(Nat, Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x5, U.U32Nat.dbl(x0, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x5, U.U32Nat.dbl(x0, x3))), Nat.add(x5, Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x5, U.U32Nat.dbl(x0, x3)))) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)))) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
373	  %Equal.sym(Nat, Nat.add(x5, U.U32Nat.dbl(x0, x3)), Nat.add(U.U32Nat.dbl(x0, x3), x5), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x5), Nat.add(x5, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x5))) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), _))))) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
374	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, x3), x5)), Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, x3), x5)), UL.nat_add_assoc(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3), x5))) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)))) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
375	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)), x5))) : {Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _))) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
376	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), x5))) : {Nat.add(x4, Nat.add(x4, _)) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
377	  %Equal.sym(Nat, Nat.add(x4, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5)), Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5), Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5), Nat.add(x4, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5)), UL.nat_add_assoc(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))), x5))) : {Nat.add(x4, _) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
378	  %Equal.sym(Nat, Nat.add(x4, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5)), Nat.add(Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), x5), Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))), x5), Nat.add(x4, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5)), UL.nat_add_assoc(x4, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), x5))) : {_ == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
379	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3)))))) : {Nat.add(Nat.add(x4, _), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
380	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))) : {Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, _))), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
381	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, x3), x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))) : {Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
382	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))))) : {Nat.add(Nat.add(x4, _), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
383	  %Equal.sym(Nat, Nat.add(x4, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Equal.sym(Nat, Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))), Nat.add(x4, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))))), UL.nat_add_assoc(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)))))) : {Nat.add(_, x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
384	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, U.U32Nat.dbl(x0, x3)))) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), _), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
385	  %Equal.sym(Nat, Nat.add(x4, U.U32Nat.dbl(x0, x3)), Nat.add(U.U32Nat.dbl(x0, x3), x4), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x4), Nat.add(x4, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x4))) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _)), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
386	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), x4))) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), _), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
387	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3))) : {Nat.add(Nat.add(Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(_, x4)), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
388	  %Equal.sym(Nat, Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(x4, U.U32Nat.dbl(x0, x3))), Nat.add(x4, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), x4, U.U32Nat.dbl(x0, x3)))) : {Nat.add(Nat.add(_, Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
389	  %Equal.sym(Nat, Nat.add(x4, U.U32Nat.dbl(x0, x3)), Nat.add(U.U32Nat.dbl(x0, x3), x4), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, x3), x4), Nat.add(x4, U.U32Nat.dbl(x0, x3)), UL.nat_add_comm(U.U32Nat.dbl(x0, x3), x4))) : {Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), _), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
390	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(x0, x3), x4)), UL.nat_add_assoc(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3), x4))) : {Nat.add(Nat.add(_, Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
391	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Equal.sym(Nat, U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(x0, Nat.mul(x1, x2)), U.U32Nat.dbl(x0, x3)), UL.dbl_add(x0, Nat.mul(x1, x2), x3))) : {Nat.add(Nat.add(Nat.add(_, x4), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
392	  %Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), Equal.sym(Nat, Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), Nat.add(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4), Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), UL.nat_double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)))) : {Nat.add(_, x5) == Nat.add(Nat.double(Nat.add(U.U32Nat.dbl(x0, Nat.add(Nat.mul(x1, x2), x3)), x4)), x5) : Nat}
393	  {==}
394	
395	def wd.bs(+p: Nat, +x: Bool, +hi: Word(p), +b: W.W64, +q: W.W64, +r: W.W64, +hb: {Nat.is_lt(W.W64.to_nat(b), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, +hX: {Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, ih: {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))) == Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r))))) == Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(1n+p, WCon{x, hi}, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}:
396	  (+e, +l) = ih
397	  %Equal.sym(W.W64 & W.W64, W.W64.div.bits(p, hi, b, (q, r)), (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))), wd.eta(W.W64.div.bits(p, hi, b, (q, r)))) : {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, _))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, _)))) == Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, _))), W.W64.to_nat(b)) == True{} : Bool}
398	  (Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))))), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), W.W64.to_nat(W.W64.snd(W.W64.div.step(x, b, (W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))))))), W.W64.to_nat(b), wd.st(x, b, W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))), W.W64.snd(W.W64.div.bits(p, hi, b, (q, r))), l, hb, Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(p, hi, b, (q, r)))))), U.U32Nat.bit(x)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(Nat.double(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(p, hi, b, (q, r))
399	
400	def wd.bits(m: Nat, w: Word(m), +b: W.W64, +q: W.W64, +r: W.W64, +hR: {Nat.is_lt(W.W64.to_nat(r), W.W64.to_nat(b)) == True{} : Bool}, +hb: {Nat.is_lt(W.W64.to_nat(b), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}, +hX: {Nat.is_lt(Nat.add(U.U32Nat.dbl(m, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(m, w)), U.U32Nat.dbl(64n, 1n)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(m, w, b, (q, r)))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(m, w, b, (q, r))))) == Nat.add(U.U32Nat.dbl(m, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(m, w)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(m, w, b, (q, r)))), W.W64.to_nat(b)) == True{} : Bool}:
401	  match m w:
402	    case 0n WNil{}:
403	      (Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)), 0n), Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)), UL.nat_add_zero(Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r)))), hR)
404	    case 1n+ +p WCon{+x, +hi}:
405	      wd.bs(p, x, hi, b, q, r, hb, hX, wd.bits(p, hi, b, q, r, hR, hb, UO.nat_le_lt_trans(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi})), U.U32Nat.dbl(64n, 1n), Equal.trans(Bool, Nat.is_le(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi}))), Nat.is_le(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)))), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), U.U32Nat.bit(x)), Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)))), Nat.is_le(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), Nat.add(U.U32Nat.dbl(1n+p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(1n+p, WCon{x, hi}))), Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), zz), Nat.add(Nat.add(Nat.add(U.U32Nat.dbl(p, Nat.add(Nat.mul(W.W64.to_nat(q), W.W64.to_nat(b)), W.W64.to_nat(r))), Word.to_nat(p, hi)), U.U32Nat.bit(x)),
406	
407	def wr.d10(+x0: Nat, +x1: Nat, +x2: Nat, +x3: Nat) -> {Nat.add(x0, U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3))) == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), x0) : Nat}:
408	  %Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3)), UL.dbl_add(32n, Nat.mul(x1, x2), x3)) : {Nat.add(x0, _) == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), x0) : Nat}
409	  %Equal.sym(Nat, Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3))), Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), Nat.add(x0, U.U32Nat.dbl(32n, x3))), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), Nat.add(x0, U.U32Nat.dbl(32n, x3))), Nat.add(x0, Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3))), UL.nat_add_left_comm(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), x0, U.U32Nat.dbl(32n, x3)))) : {_ == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), x0) : Nat}
410	  %Equal.sym(Nat, Nat.add(x0, U.U32Nat.dbl(32n, x3)), Nat.add(U.U32Nat.dbl(32n, x3), x0), Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, x3), x0), Nat.add(x0, U.U32Nat.dbl(32n, x3)), UL.nat_add_comm(U.U32Nat.dbl(32n, x3), x0))) : {Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), _) == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), x0) : Nat}
411	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(32n, x3), x0)), Nat.add(Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3)), x0), Equal.sym(Nat, Nat.add(Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3)), x0), Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), Nat.add(U.U32Nat.dbl(32n, x3), x0)), UL.nat_add_assoc(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3), x0))) : {_ == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), x0) : Nat}
412	  %Equal.sym(Nat, Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3)), U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), Equal.sym(Nat, U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), Nat.add(U.U32Nat.dbl(32n, Nat.mul(x1, x2)), U.U32Nat.dbl(32n, x3)), UL.dbl_add(32n, Nat.mul(x1, x2), x3))) : {Nat.add(_, x0) == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(x1, x2), x3)), x0) : Nat}
413	  {==}
414	
415	def wd.dz2(+hw: Word(32n), +lw: Word(32n), +b: W.W64, +h: {W.W64.is_zero(b) == False{} : Bool}, i1: {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))) == Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)) == True{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(False{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(False{}, W.W64{U32{hw}, U32{lw}}, b)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(False{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)) == True{} : Bool}:
416	  (+e1, +l1) = i1
417	  %Equal.sym(W.W64 & W.W64, W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())), (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), wd.eta(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))) : {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, lw, b, _))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, _)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, _))), W.W64.to_nat(b)) == True{} : Bool}
418	  (Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))))), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))))), Word.to_nat(32n, lw)), W.W64.to_nat(W.W64.snd(W.W64.div.bits(32n, lw, b, (W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))))))), W.W64.to_nat(b), wd.bits(32n, lw, b, W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), W.W64.snd(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero()))), l1, wv.lt64(b), Equal.trans(Bool, Nat.is_lt(Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.div.bits(32n, hw, b, (W.W64.zero(), W.W64.zero())))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.div.bit
419	
420	def wd.dz(+hw: Word(32n), +lw: Word(32n), +b: W.W64, z: Bool, ez: {W.W64.is_zero(b) == z : Bool}, +h: {W.W64.is_zero(b) == False{} : Bool}) -> {Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(z, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(z, W.W64{U32{hw}, U32{lw}}, b)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(z, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)) == True{} : Bool}:
421	  match z:
422	    case True{}:
423	      Empty.absurd({Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(True{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(True{}, W.W64{U32{hw}, U32{lw}}, b)))) == W.W64.to_nat(W.W64{U32{hw}, U32{lw}}) : Nat} & {Nat.is_lt(W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(True{}, W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)) == True{} : Bool}, wn.tf(Equal.trans(Bool, True{}, W.W64.is_zero(b), False{}, Equal.sym(Bool, W.W64.is_zero(b), True{}, ez), h)))
424	    case False{}:
425	      wd.dz2(hw, lw, b, h, wd.bits(32n, hw, b, W.W64.zero(), W.W64.zero(), Equal.trans(Bool, Nat.is_lt(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), Nat.is_lt(0n, W.W64.to_nat(b)), True{}, {==}, wd.nz(W.W64.to_nat(b), Equal.trans(Bool, Nat.is_eq(W.W64.to_nat(b), 0n), W.W64.is_zero(b), False{}, Equal.sym(Bool, W.W64.is_zero(b), Nat.is_eq(W.W64.to_nat(b), 0n), WB.eq_value(b, W.W64.zero())), h))), wv.lt64(b), Equal.trans(Bool, Nat.is_lt(Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), U.U32Nat.dbl(64n, 1n)), Nat.is_lt(Word.to_nat(32n, hw), U.U32Nat.dbl(64n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, U.U32Nat.dbl(64n, 1n)), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), Word.to_nat(32n, hw), Equal.sym(Nat, Word.to_nat(32n, hw), Nat.add(U.U32Nat.dbl(32n, Nat.add(Nat.mul(W.W64.to_nat(W.W64.zero()), W.W64.to_nat(b)), W.W64.to_nat(W.W64.zero()))), Word.to_nat(32n, hw)), {==})), UO.nat_lt_le_trans(Word.to_nat(32n, hw), U.U32Nat.dbl(32n, 1n), U.U32Nat.dbl(64n, 1n), UL.word_value_lt(32n, hw), UL.dbl_le_exp(32n, 64n, 1n, {==})))))
426	
427	
428	def Laws.divmod_value(a, b, h):
429	  match a:
430	    case W.W64{U32{+hw}, U32{+lw}}:
431	      wd.p1(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(W.W64.is_zero(b), W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(W.W64.is_zero(b), W.W64{U32{hw}, U32{lw}}, b)))), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(W.W64.is_zero(b), W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b), wd.dz(hw, lw, b, W.W64.is_zero(b), {==}, h))
432	
433	def Laws.mod_lt(a, b, h):
434	  match a:
435	    case W.W64{U32{+hw}, U32{+lw}}:
436	      wd.p2(Nat.add(Nat.mul(W.W64.to_nat(W.W64.fst(W.W64.divmod.pick(W.W64.is_zero(b), W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b)), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(W.W64.is_zero(b), W.W64{U32{hw}, U32{lw}}, b)))), W.W64.to_nat(W.W64{U32{hw}, U32{lw}}), W.W64.to_nat(W.W64.snd(W.W64.divmod.pick(W.W64.is_zero(b), W.W64{U32{hw}, U32{lw}}, b))), W.W64.to_nat(b), wd.dz(hw, lw, b, W.W64.is_zero(b), {==}, h))
437	
438	def Laws.div_zero(a):
439	  {==}
440	
441	def Laws.mod_zero(a):
442	  {==}