nat_order.bend

bend-kit-collections@0.1.4.1 · 899 lines · 127 definitions

1# Nat order and linear-form lemmas for the OMap weight-balance proofs.
2import Base
3import bend-mathlib@0.7.4.0/nat.bend as MNat
4import bend-mathlib@0.7.4.0/bool.bend as MBool
5
6def mul3(+a: Nat) -> Nat:
7  Nat.mul(3n, a)
8
9def wok(+wl: Nat, +wh: Nat) -> Bool:
10  Bool.and(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)))
11
12def wok_l(+wl: Nat, +wh: Nat, e: {wok(wl, wh) == True{} : Bool})
13  -> {Nat.is_le(wh, mul3(wl)) == True{} : Bool}:
14  MBool.eq_true_of_and_left(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), e)
15
16def wok_r(+wl: Nat, +wh: Nat, e: {wok(wl, wh) == True{} : Bool})
17  -> {Nat.is_le(wl, mul3(wh)) == True{} : Bool}:
18  MBool.eq_true_of_and_right(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), e)
19
20def wok_i(+wl: Nat, +wh: Nat, el: {Nat.is_le(wh, mul3(wl)) == True{} : Bool},
21  er: {Nat.is_le(wl, mul3(wh)) == True{} : Bool}) -> {wok(wl, wh) == True{} : Bool}:
22  MBool.and_eq_true(Nat.is_le(wh, mul3(wl)), Nat.is_le(wl, mul3(wh)), el, er)
23
24# --- sums ----------------------------------------------------------------------
25
26def LE(a: Nat, b: Nat) -> Data:
27  {Nat.is_le(a, b) == True{} : Bool}
28
29def tr(-a: Nat, -b: Nat, -c: Nat, e1: {a == b : Nat}, e2: {b == c : Nat}) -> {a == c : Nat}:
30  Equal.trans(Nat, a, b, c, e1, e2)
31
32def sy(-a: Nat, -b: Nat, e: {a == b : Nat}) -> {b == a : Nat}:
33  Equal.sym(Nat, a, b, e)
34
35def cong_add(-a: Nat, -a2: Nat, -b: Nat, -b2: Nat, e1: {a == a2 : Nat}, e2: {b == b2 : Nat})
36  -> {Nat.add(a, b) == Nat.add(a2, b2) : Nat}:
37  %e1 : {Nat.add(a, b) == Nat.add(_, b2) : Nat}
38  %e2 : {Nat.add(a, b) == Nat.add(a, _) : Nat}
39  {==}
40
41def step(+a: Nat, +b: Nat, +c: Nat, +d: Nat, -x: Nat, -y: Nat, e1: {Nat.add(a, c) == x : Nat},
42  e2: {Nat.add(b, d) == y : Nat}) -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(x, y) : Nat}:
43  tr(Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), Nat.add(x, y),
44    MNat.add_add_add_comm(a, b, c, d), cong_add(Nat.add(a, c), x, Nat.add(b, d), y, e1, e2))
45
46# --- linear forms c0 + c1*v1 + c2*v2 + c3*v3 + c4*v4 ----------------------------
47
48type Lin is Data:
49  L{c0: Nat, c1: Nat, c2: Nat, c3: Nat, c4: Nat}
50
51type Vs is Data:
52  VS{v1: Nat, v2: Nat, v3: Nat, v4: Nat}
53
54def F(p: Lin, v: Vs) -> Nat:
55  match p v:
56    case L{c0, c1, c2, c3, c4} VS{+v1, +v2, +v3, +v4}:
57      Nat.add(c0, Nat.add(Nat.mul(c1, v1), Nat.add(Nat.mul(c2, v2),
58        Nat.add(Nat.mul(c3, v3), Nat.mul(c4, v4)))))
59
60def ladd(p: Lin, q: Lin) -> Lin:
61  match p q:
62    case L{a0, a1, a2, a3, a4} L{b0, b1, b2, b3, b4}:
63      L{Nat.add(a0, b0), Nat.add(a1, b1), Nat.add(a2, b2), Nat.add(a3, b3), Nat.add(a4, b4)}
64
65def lsc(k: Nat, +p: Lin) -> Lin:
66  match k:
67    case 0n:
68      L{0n, 0n, 0n, 0n, 0n}
69    case 1n+j:
70      ladd(p, lsc(j, p))
71
72def lsuc(p: Lin) -> Lin:
73  match p:
74    case L{a0, a1, a2, a3, a4}:
75      L{1n+a0, a1, a2, a3, a4}
76
77def lle(p: Lin, q: Lin) -> Bool:
78  match p q:
79    case L{a0, a1, a2, a3, a4} L{b0, b1, b2, b3, b4}:
80      Bool.and(Nat.is_le(a0, b0), Bool.and(Nat.is_le(a1, b1), Bool.and(Nat.is_le(a2, b2),
81        Bool.and(Nat.is_le(a3, b3), Nat.is_le(a4, b4)))))
82
83def F_add(p: Lin, q: Lin, v: Vs) -> {Nat.add(F(p, v), F(q, v)) == F(ladd(p, q), v) : Nat}:
84  match p q v:
85    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
86      +x1 = Nat.mul(a1, v1)
87      +x2 = Nat.mul(a2, v2)
88      +x3 = Nat.mul(a3, v3)
89      +x4 = Nat.mul(a4, v4)
90      +y1 = Nat.mul(b1, v1)
91      +y2 = Nat.mul(b2, v2)
92      +y3 = Nat.mul(b3, v3)
93      +y4 = Nat.mul(b4, v4)
94      +z1 = Nat.mul(Nat.add(a1, b1), v1)
95      +z2 = Nat.mul(Nat.add(a2, b2), v2)
96      +z3 = Nat.mul(Nat.add(a3, b3), v3)
97      +z4 = Nat.mul(Nat.add(a4, b4), v4)
98      step(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))),
99        Nat.add(a0, b0), Nat.add(z1, Nat.add(z2, Nat.add(z3, z4))), {==},
100        step(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), z1,
101          Nat.add(z2, Nat.add(z3, z4)), MNat.add_mul_sym(a1, b1, v1),
102          step(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), z2, Nat.add(z3, z4), MNat.add_mul_sym(a2, b2, v2),
103            step(x3, x4, y3, y4, z3, z4, MNat.add_mul_sym(a3, b3, v3), MNat.add_mul_sym(a4, b4, v4)))))
104
105def comb(+p: Lin, +q: Lin, +r: Lin, +s: Lin, +v: Vs, e1: LE(F(p, v), F(q, v)), e2: LE(F(r, v), F(s, v)))
106  -> LE(F(ladd(p, r), v), F(ladd(q, s), v)):
107  %F_add(p, r, v) : LE(_, F(ladd(q, s), v))
108  %F_add(q, s, v) : LE(Nat.add(F(p, v), F(r, v)), _)
109  MNat.add_le_add(F(p, v), F(r, v), F(q, v), F(s, v), e1, e2)
110
111def scale(k: Nat, +p: Lin, +q: Lin, +v: Vs, +e: LE(F(p, v), F(q, v)))
112  -> LE(F(lsc(k, p), v), F(lsc(k, q), v)):
113  match k:
114    case 0n:
115      MNat.le_refl(F(L{0n, 0n, 0n, 0n, 0n}, v))
116    case 1n+ +j:
117      comb(p, q, lsc(j, p), lsc(j, q), v, e, scale(j, p, q, v, e))
118
119def and5_1(+a: Bool, +b: Bool, +c: Bool, +d: Bool, +f: Bool,
120  e: {Bool.and(a, Bool.and(b, Bool.and(c, Bool.and(d, f)))) == True{} : Bool}) -> {a == True{} : Bool}:
121  MBool.eq_true_of_and_left(a, Bool.and(b, Bool.and(c, Bool.and(d, f))), e)
122
123def and5_r(+a: Bool, +b: Bool, +c: Bool, +d: Bool, +f: Bool,
124  e: {Bool.and(a, Bool.and(b, Bool.and(c, Bool.and(d, f)))) == True{} : Bool})
125  -> {Bool.and(b, Bool.and(c, Bool.and(d, f))) == True{} : Bool}:
126  MBool.eq_true_of_and_right(a, Bool.and(b, Bool.and(c, Bool.and(d, f))), e)
127
128def F_mono(p: Lin, q: Lin, v: Vs, +h: {lle(p, q) == True{} : Bool}) -> LE(F(p, v), F(q, v)):
129  match p q v:
130    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
131      +l0 = Nat.is_le(a0, b0)
132      +l1 = Nat.is_le(a1, b1)
133      +l2 = Nat.is_le(a2, b2)
134      +l3 = Nat.is_le(a3, b3)
135      +l4 = Nat.is_le(a4, b4)
136      +r1 = and5_r(l0, l1, l2, l3, l4, h)
137      +r2 = MBool.eq_true_of_and_right(l1, Bool.and(l2, Bool.and(l3, l4)), r1)
138      +r3 = MBool.eq_true_of_and_right(l2, Bool.and(l3, l4), r2)
139      +x1 = Nat.mul(a1, v1)
140      +x2 = Nat.mul(a2, v2)
141      +x3 = Nat.mul(a3, v3)
142      +x4 = Nat.mul(a4, v4)
143      +y1 = Nat.mul(b1, v1)
144      +y2 = Nat.mul(b2, v2)
145      +y3 = Nat.mul(b3, v3)
146      +y4 = Nat.mul(b4, v4)
147      MNat.add_le_add(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))), and5_1(l0, l1, l2, l3, l4, h), MNat.add_le_add(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), MNat.mul_le_mul_right(a1, b1, v1, MBool.eq_true_of_and_left(l1, Bool.and(l2, Bool.and(l3, l4)), r1)), MNat.add_le_add(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), MNat.mul_le_mul_right(a2, b2, v2, MBool.eq_true_of_and_left(l2, Bool.and(l3, l4), r2)), MNat.add_le_add(x3, x4, y3, y4, MNat.mul_le_mul_right(a3, b3, v3, MBool.eq_true_of_and_left(l3, l4, r3)), MNat.mul_le_mul_right(a4, b4, v4, MBool.eq_true_of_and_right(l3, l4, r3))))))
148
149def le_succ_false(x: Nat, e: LE(1n+x, x)) -> Empty:
150  match x:
151    case 0n:
152      MBool.false_ne_true()(e)
153    case 1n+p:
154      le_succ_false(p, e)
155
156# A combined hypothesis F(p) <= F(q) with q < p term by term is false.
157def contra(+p: Lin, q: Lin, v: Vs, e: LE(F(p, v), F(q, v)), h: {lle(lsuc(q), p) == True{} : Bool}) -> Empty:
158  match q v:
159    case L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
160      +vs = {VS{v1, v2, v3, v4} : Vs}
161      +fq = F(L{b0, b1, b2, b3, b4}, vs)
162      le_succ_false(fq, MNat.le_trans(1n+fq, F(p, vs), fq, F_mono(L{1n+b0, b1, b2, b3, b4}, p, vs, h), e))
163
164# --- from terms to linear forms ------------------------------------------------
165
166def F0(v: Vs) -> {F(L{0n, 0n, 0n, 0n, 0n}, v) == 0n : Nat}:
167  match v:
168    case VS{v1, v2, v3, v4}:
169      {==}
170
171def cv_c(+n: Nat, v: Vs) -> {n == F(L{n, 0n, 0n, 0n, 0n}, v) : Nat}:
172  match v:
173    case VS{v1, v2, v3, v4}:
174      sy(Nat.add(n, 0n), n, MNat.add_zero(n))
175
176def az2(+a: Nat) -> {a == Nat.add(Nat.add(a, 0n), 0n) : Nat}:
177  sy(Nat.add(Nat.add(a, 0n), 0n), a,
178    tr(Nat.add(Nat.add(a, 0n), 0n), Nat.add(a, 0n), a, MNat.add_zero(Nat.add(a, 0n)), MNat.add_zero(a)))
179
180def cv_1(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {a == F(L{0n, 1n, 0n, 0n, 0n}, VS{a, b, c, d}) : Nat}:
181  az2(a)
182
183def cv_2(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {b == F(L{0n, 0n, 1n, 0n, 0n}, VS{a, b, c, d}) : Nat}:
184  az2(b)
185
186def cv_3(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {c == F(L{0n, 0n, 0n, 1n, 0n}, VS{a, b, c, d}) : Nat}:
187  az2(c)
188
189def cv_4(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {d == F(L{0n, 0n, 0n, 0n, 1n}, VS{a, b, c, d}) : Nat}:
190  sy(Nat.add(d, 0n), d, MNat.add_zero(d))
191
192def cv_add(-A: Nat, -B: Nat, +p: Lin, +q: Lin, +v: Vs, eA: {A == F(p, v) : Nat}, eB: {B == F(q, v) : Nat})
193  -> {Nat.add(A, B) == F(ladd(p, q), v) : Nat}:
194  tr(Nat.add(A, B), Nat.add(F(p, v), F(q, v)), F(ladd(p, q), v),
195    cong_add(A, F(p, v), B, F(q, v), eA, eB), F_add(p, q, v))
196
197def cv_mul(k: Nat, +A: Nat, +p: Lin, +v: Vs, +eA: {A == F(p, v) : Nat})
198  -> {Nat.mul(k, A) == F(lsc(k, p), v) : Nat}:
199  match k:
200    case 0n:
201      sy(F(L{0n, 0n, 0n, 0n, 0n}, v), 0n, F0(v))
202    case 1n+ +j:
203      cv_add(A, Nat.mul(j, A), p, lsc(j, p), v, eA, cv_mul(j, A, p, v, eA))
204
205def cvle(-A: Nat, -B: Nat, -p: Lin, -q: Lin, -v: Vs, eA: {A == F(p, v) : Nat}, eB: {B == F(q, v) : Nat},
206  h: LE(A, B)) -> LE(F(p, v), F(q, v)):
207  %eA : LE(_, F(q, v))
208  %eB : LE(A, _)
209  h
210
211# --- from comparisons to <= ----------------------------------------------------
212
213def gt_le(a: Nat, b: Nat, e: {Nat.is_gt(a, b) == True{} : Bool}) -> LE(1n+b, a):
214  match a b:
215    case 0n 0n:
216      Empty.absurd(LE(1n, 0n), MBool.false_ne_true()(e))
217    case 0n 1n+bp:
218      Empty.absurd(LE(1n+1n+bp, 0n), MBool.false_ne_true()(e))
219    case 1n+ap 0n:
220      MNat.zero_le(ap)
221    case 1n+ap 1n+bp:
222      gt_le(ap, bp, e)
223
224def ngt_le(a: Nat, b: Nat, e: {Nat.is_gt(a, b) == False{} : Bool}) -> LE(a, b):
225  match a b:
226    case 0n b:
227      MNat.zero_le(b)
228    case 1n+ap 0n:
229      Empty.absurd(LE(1n+ap, 0n), MBool.true_ne_false()(e))
230    case 1n+ap 1n+bp:
231      ngt_le(ap, bp, e)
232
233# Proves x <= y from a refutation of y < x.
234def by_contra(x: Nat, y: Nat, k: LE(1n+y, x) -> Empty) -> LE(x, y):
235  match x y:
236    case 0n y:
237      MNat.zero_le(y)
238    case 1n+xp 0n:
239      Empty.absurd(LE(1n+xp, 0n), k(MNat.zero_le(xp)))
240    case 1n+xp 1n+yp:
241      by_contra(xp, yp, k)
242
243# --- weight-balance arithmetic -------------------------------------------------
244# Machine-written certificates. Each lemma refutes its negated goal: it adds the
245# hypotheses as linear forms, each times a small factor, and contra shows the
246# sum is false. rls/rld: single/double rotation toward lo; rhs/rhd: toward hi.
247
248def alm(+wl: Nat, +wh: Nat) -> Bool:
249  Bool.and(Nat.is_le(wh, Nat.add(3n, mul3(wl))), Nat.is_le(wl, Nat.add(3n, mul3(wh))))
250
251def near(+a: Nat, +b: Nat) -> Bool:
252  Bool.and(Nat.is_le(a, 1n+b), Nat.is_le(b, 1n+a))
253
254def rls.c0a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), a), h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> Empty:
255  +v = {VS{l, a, b, 0n} : Vs}
256  +f_ng = cvle(1n+Nat.mul(3n, l), a, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
257    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
258    cv_2(l, a, b, 0n), ng)
259  +f_h4 = cvle(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v,
260    cv_add(a, b, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, a, b, 0n), cv_3(l, a, b, 0n)),
261    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))), h4)
262  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
263    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
264    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
265  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
266    cv_c(1n, v),
267    cv_1(l, a, b, 0n), pl)
268  contra(L{7n, 9n, 3n, 2n, 0n}, L{6n, 9n, 3n, 2n, 0n}, v,
269    comb(L{3n, 9n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{4n, 0n, 3n, 2n, 0n}, L{6n, 9n, 0n, 2n, 0n}, v, scale(3n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
270    comb(L{0n, 0n, 2n, 2n, 0n}, L{6n, 6n, 0n, 0n, 0n}, L{4n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 2n, 0n}, v, scale(2n, L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
271    comb(L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, f_hs,
272    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl)))), {==})
273def rls.c0a(+l: Nat, +a: Nat, +b: Nat, h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> LE(a, Nat.mul(3n, l)):
274  by_contra(a, Nat.mul(3n, l), ng => rls.c0a.k(l, a, b, ng, h4, hs, pl))
275
276def rls.c0b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, a), l), h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b))) -> Empty:
277  +v = {VS{l, a, b, 0n} : Vs}
278  +f_ng = cvle(1n+Nat.mul(3n, a), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
279    cv_add(1n, Nat.mul(3n, a), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n))),
280    cv_1(l, a, b, 0n), ng)
281  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
282    cv_3(l, a, b, 0n),
283    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
284  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(a, b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
285    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
286    cv_add(a, b, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, a, b, 0n), cv_3(l, a, b, 0n)), h3)
287  contra(L{3n, 3n, 6n, 1n, 0n}, L{0n, 2n, 4n, 1n, 0n}, v,
288    comb(L{2n, 0n, 6n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{1n, 3n, 0n, 1n, 0n}, L{0n, 0n, 4n, 1n, 0n}, v, scale(2n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
289    comb(L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v, f_h2,
290    f_h3)), {==})
291def rls.c0b(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b))) -> LE(l, Nat.mul(3n, a)):
292  by_contra(l, Nat.mul(3n, a), ng => rls.c0b.k(l, a, b, ng, h2, h3))
293
294def rls.w0(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), +h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(l, a) == True{} : Bool}:
295  MBool.and_eq_true(Nat.is_le(a, Nat.mul(3n, l)), Nat.is_le(l, Nat.mul(3n, a)), rls.c0a(l, a, b, h4, hs, pl), rls.c0b(l, a, b, h2, h3))
296
297def rls.c1a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(l, a)), b), h2: LE(b, Nat.mul(3n, a))) -> Empty:
298  +v = {VS{l, a, b, 0n} : Vs}
299  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(l, a)), b, L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
300    cv_add(1n, Nat.mul(3n, Nat.add(l, a)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(l, a), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(l, a, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, a, b, 0n), cv_2(l, a, b, 0n)))),
301    cv_3(l, a, b, 0n), ng)
302  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
303    cv_3(l, a, b, 0n),
304    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
305  contra(L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 3n, 1n, 0n}, v,
306    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_ng,
307    f_h2), {==})
308def rls.c1a(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a))) -> LE(b, Nat.mul(3n, Nat.add(l, a))):
309  by_contra(b, Nat.mul(3n, Nat.add(l, a)), ng => rls.c1a.k(l, a, b, ng, h2))
310
311def rls.c1b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), Nat.add(l, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), hs: LE(1n+a, Nat.mul(2n, b))) -> Empty:
312  +v = {VS{l, a, b, 0n} : Vs}
313  +f_ng = cvle(1n+Nat.mul(3n, b), Nat.add(l, a), L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v,
314    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n))),
315    cv_add(l, a, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, a, b, 0n), cv_2(l, a, b, 0n)), ng)
316  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(a, b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
317    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
318    cv_add(a, b, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, a, b, 0n), cv_3(l, a, b, 0n)), h3)
319  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
320    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
321    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
322  contra(L{8n, 3n, 4n, 9n, 0n}, L{0n, 3n, 4n, 9n, 0n}, v,
323    comb(L{3n, 0n, 0n, 9n, 0n}, L{0n, 3n, 3n, 0n, 0n}, L{5n, 3n, 4n, 0n, 0n}, L{0n, 0n, 1n, 9n, 0n}, v, scale(3n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
324    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{4n, 0n, 4n, 0n, 0n}, L{0n, 0n, 0n, 8n, 0n}, v, f_h3,
325    scale(4n, L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v, f_hs))), {==})
326def rls.c1b(+l: Nat, +a: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), hs: LE(1n+a, Nat.mul(2n, b))) -> LE(Nat.add(l, a), Nat.mul(3n, b)):
327  by_contra(Nat.add(l, a), Nat.mul(3n, b), ng => rls.c1b.k(l, a, b, ng, h3, hs))
328
329def rls.w1(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(a, b)), +h4: LE(Nat.add(a, b), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(Nat.add(l, a), b) == True{} : Bool}:
330  MBool.and_eq_true(Nat.is_le(b, Nat.mul(3n, Nat.add(l, a))), Nat.is_le(Nat.add(l, a), Nat.mul(3n, b)), rls.c1a(l, a, b, h2), rls.c1b(l, a, b, h3, hs))
331
332def rhs.c0a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), Nat.add(a, l)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), hs: LE(1n+a, Nat.mul(2n, b))) -> Empty:
333  +v = {VS{l, a, b, 0n} : Vs}
334  +f_ng = cvle(1n+Nat.mul(3n, b), Nat.add(a, l), L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v,
335    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n))),
336    cv_add(a, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, a, b, 0n), cv_1(l, a, b, 0n)), ng)
337  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, a), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
338    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
339    cv_add(b, a, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, a, b, 0n), cv_2(l, a, b, 0n)), h3)
340  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
341    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
342    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
343  contra(L{8n, 3n, 4n, 9n, 0n}, L{0n, 3n, 4n, 9n, 0n}, v,
344    comb(L{3n, 0n, 0n, 9n, 0n}, L{0n, 3n, 3n, 0n, 0n}, L{5n, 3n, 4n, 0n, 0n}, L{0n, 0n, 1n, 9n, 0n}, v, scale(3n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
345    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{4n, 0n, 4n, 0n, 0n}, L{0n, 0n, 0n, 8n, 0n}, v, f_h3,
346    scale(4n, L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v, f_hs))), {==})
347def rhs.c0a(+l: Nat, +a: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), hs: LE(1n+a, Nat.mul(2n, b))) -> LE(Nat.add(a, l), Nat.mul(3n, b)):
348  by_contra(Nat.add(a, l), Nat.mul(3n, b), ng => rhs.c0a.k(l, a, b, ng, h3, hs))
349
350def rhs.c0b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(a, l)), b), h2: LE(b, Nat.mul(3n, a))) -> Empty:
351  +v = {VS{l, a, b, 0n} : Vs}
352  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(a, l)), b, L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
353    cv_add(1n, Nat.mul(3n, Nat.add(a, l)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(a, l), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(a, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, a, b, 0n), cv_1(l, a, b, 0n)))),
354    cv_3(l, a, b, 0n), ng)
355  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
356    cv_3(l, a, b, 0n),
357    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
358  contra(L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 3n, 1n, 0n}, v,
359    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_ng,
360    f_h2), {==})
361def rhs.c0b(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a))) -> LE(b, Nat.mul(3n, Nat.add(a, l))):
362  by_contra(b, Nat.mul(3n, Nat.add(a, l)), ng => rhs.c0b.k(l, a, b, ng, h2))
363
364def rhs.w0(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), +h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(b, Nat.add(a, l)) == True{} : Bool}:
365  MBool.and_eq_true(Nat.is_le(Nat.add(a, l), Nat.mul(3n, b)), Nat.is_le(b, Nat.mul(3n, Nat.add(a, l))), rhs.c0a(l, a, b, h3, hs), rhs.c0b(l, a, b, h2))
366
367def rhs.c1a.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, a), l), h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a))) -> Empty:
368  +v = {VS{l, a, b, 0n} : Vs}
369  +f_ng = cvle(1n+Nat.mul(3n, a), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
370    cv_add(1n, Nat.mul(3n, a), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n))),
371    cv_1(l, a, b, 0n), ng)
372  +f_h2 = cvle(b, Nat.mul(3n, a), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
373    cv_3(l, a, b, 0n),
374    cv_mul(3n, a, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, a, b, 0n)), h2)
375  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, a), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
376    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
377    cv_add(b, a, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, a, b, 0n), cv_2(l, a, b, 0n)), h3)
378  contra(L{3n, 3n, 6n, 1n, 0n}, L{0n, 2n, 4n, 1n, 0n}, v,
379    comb(L{2n, 0n, 6n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{1n, 3n, 0n, 1n, 0n}, L{0n, 0n, 4n, 1n, 0n}, v, scale(2n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
380    comb(L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v, f_h2,
381    f_h3)), {==})
382def rhs.c1a(+l: Nat, +a: Nat, +b: Nat, h2: LE(b, Nat.mul(3n, a)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a))) -> LE(l, Nat.mul(3n, a)):
383  by_contra(l, Nat.mul(3n, a), ng => rhs.c1a.k(l, a, b, ng, h2, h3))
384
385def rhs.c1b.k(+l: Nat, +a: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), a), h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> Empty:
386  +v = {VS{l, a, b, 0n} : Vs}
387  +f_ng = cvle(1n+Nat.mul(3n, l), a, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
388    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))),
389    cv_2(l, a, b, 0n), ng)
390  +f_h4 = cvle(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v,
391    cv_add(b, a, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, a, b, 0n), cv_2(l, a, b, 0n)),
392    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, a, b, 0n))), h4)
393  +f_hs = cvle(1n+a, Nat.mul(2n, b), L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, v,
394    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(l, a, b, 0n)),
395    cv_mul(2n, b, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, a, b, 0n)), hs)
396  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
397    cv_c(1n, v),
398    cv_1(l, a, b, 0n), pl)
399  contra(L{7n, 9n, 3n, 2n, 0n}, L{6n, 9n, 3n, 2n, 0n}, v,
400    comb(L{3n, 9n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{4n, 0n, 3n, 2n, 0n}, L{6n, 9n, 0n, 2n, 0n}, v, scale(3n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
401    comb(L{0n, 0n, 2n, 2n, 0n}, L{6n, 6n, 0n, 0n, 0n}, L{4n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 2n, 0n}, v, scale(2n, L{0n, 0n, 1n, 1n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
402    comb(L{1n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, f_hs,
403    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl)))), {==})
404def rhs.c1b(+l: Nat, +a: Nat, +b: Nat, h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), hs: LE(1n+a, Nat.mul(2n, b)), pl: LE(1n, l)) -> LE(a, Nat.mul(3n, l)):
405  by_contra(a, Nat.mul(3n, l), ng => rhs.c1b.k(l, a, b, ng, h4, hs, pl))
406
407def rhs.w1(+l: Nat, +a: Nat, +b: Nat, +h1: LE(a, Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, a)), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, a)), +h4: LE(Nat.add(b, a), Nat.add(3n, Nat.mul(3n, l))), +hs: LE(1n+a, Nat.mul(2n, b)), +pl: LE(1n, l), +pa: LE(1n, a), +pb: LE(1n, b)) -> {wok(a, l) == True{} : Bool}:
408  MBool.and_eq_true(Nat.is_le(l, Nat.mul(3n, a)), Nat.is_le(a, Nat.mul(3n, l)), rhs.c1a(l, a, b, h2, h3), rhs.c1b(l, a, b, h4, hs, pl))
409
410def rld.c0a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(l, x)), Nat.add(y, b)), h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> Empty:
411  +v = {VS{l, x, y, b} : Vs}
412  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(l, x)), Nat.add(y, b), L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, v,
413    cv_add(1n, Nat.mul(3n, Nat.add(l, x)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(l, x), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(l, x, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, x, y, b), cv_2(l, x, y, b)))),
414    cv_add(y, b, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_3(l, x, y, b), cv_4(l, x, y, b)), ng)
415  +f_h4 = cvle(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
416    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)),
417    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
418  +f_px = cvle(1n, x, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
419    cv_c(1n, v),
420    cv_2(l, x, y, b), px)
421  contra(L{4n, 3n, 4n, 1n, 1n}, L{3n, 3n, 3n, 1n, 1n}, v,
422    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, L{3n, 0n, 1n, 1n, 1n}, L{3n, 3n, 3n, 0n, 0n}, v, f_ng,
423    comb(L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h4,
424    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_px))), {==})
425def rld.c0a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> LE(Nat.add(y, b), Nat.mul(3n, Nat.add(l, x))):
426  by_contra(Nat.add(y, b), Nat.mul(3n, Nat.add(l, x)), ng => rld.c0a.k(l, x, y, b, ng, h4, px))
427
428def rld.c0b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(y, b)), Nat.add(l, x)), h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), h5: LE(x, Nat.mul(3n, y))) -> Empty:
429  +v = {VS{l, x, y, b} : Vs}
430  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(y, b)), Nat.add(l, x), L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v,
431    cv_add(1n, Nat.mul(3n, Nat.add(y, b)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 3n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(y, b), L{0n, 0n, 0n, 1n, 1n}, v, cv_add(y, b, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_3(l, x, y, b), cv_4(l, x, y, b)))),
432    cv_add(l, x, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(l, x, y, b), cv_2(l, x, y, b)), ng)
433  +f_h1 = cvle(Nat.add(x, y), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
434    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)),
435    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
436  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
437    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
438    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)), h3)
439  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
440    cv_2(l, x, y, b),
441    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
442  contra(L{3n, 3n, 3n, 7n, 6n}, L{0n, 2n, 3n, 7n, 4n}, v,
443    comb(L{2n, 0n, 0n, 6n, 6n}, L{0n, 2n, 2n, 0n, 0n}, L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 1n, 7n, 4n}, v, scale(2n, L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
444    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{1n, 3n, 2n, 0n, 0n}, L{0n, 0n, 1n, 7n, 1n}, v, f_h1,
445    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 2n, 0n, 0n}, L{0n, 0n, 0n, 6n, 0n}, v, f_h3,
446    scale(2n, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_h5)))), {==})
447def rld.c0b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), h5: LE(x, Nat.mul(3n, y))) -> LE(Nat.add(l, x), Nat.mul(3n, Nat.add(y, b))):
448  by_contra(Nat.add(l, x), Nat.mul(3n, Nat.add(y, b)), ng => rld.c0b.k(l, x, y, b, ng, h1, h3, h5))
449
450def rld.w0(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(x, y), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(x, y))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), +h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(x, y)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(Nat.add(l, x), Nat.add(y, b)) == True{} : Bool}:
451  MBool.and_eq_true(Nat.is_le(Nat.add(y, b), Nat.mul(3n, Nat.add(l, x))), Nat.is_le(Nat.add(l, x), Nat.mul(3n, Nat.add(y, b))), rld.c0a(l, x, y, b, h4, px), rld.c0b(l, x, y, b, h1, h3, h5))
452
453def rld.c1a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), x), h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> Empty:
454  +v = {VS{l, x, y, b} : Vs}
455  +f_ng = cvle(1n+Nat.mul(3n, l), x, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
456    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
457    cv_2(l, x, y, b), ng)
458  +f_h1 = cvle(Nat.add(x, y), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
459    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)),
460    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
461  +f_h4 = cvle(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
462    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)),
463    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
464  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
465    cv_c(1n, v),
466    cv_1(l, x, y, b), pl)
467  +f_py = cvle(1n, y, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
468    cv_c(1n, v),
469    cv_3(l, x, y, b), py)
470  contra(L{10n, 12n, 4n, 4n, 3n}, L{9n, 11n, 4n, 4n, 3n}, v,
471    comb(L{4n, 12n, 0n, 0n, 0n}, L{0n, 0n, 4n, 0n, 0n}, L{6n, 0n, 4n, 4n, 3n}, L{9n, 11n, 0n, 4n, 3n}, v, scale(4n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
472    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{6n, 0n, 3n, 3n, 3n}, L{9n, 11n, 0n, 4n, 0n}, v, f_h1,
473    comb(L{0n, 0n, 3n, 3n, 3n}, L{9n, 9n, 0n, 0n, 0n}, L{6n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 4n, 0n}, v, scale(3n, L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
474    comb(L{2n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{4n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl),
475    scale(4n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, f_py))))), {==})
476def rld.c1a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(x, y), Nat.mul(3n, b)), h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> LE(x, Nat.mul(3n, l)):
477  by_contra(x, Nat.mul(3n, l), ng => rld.c1a.k(l, x, y, b, ng, h1, h4, pl, py))
478
479def rld.c1b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, x), l), h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h6: LE(y, Nat.mul(3n, x))) -> Empty:
480  +v = {VS{l, x, y, b} : Vs}
481  +f_ng = cvle(1n+Nat.mul(3n, x), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
482    cv_add(1n, Nat.mul(3n, x), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b))),
483    cv_1(l, x, y, b), ng)
484  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
485    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
486    cv_add(Nat.add(x, y), b, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), cv_4(l, x, y, b)), h3)
487  +f_hd = cvle(Nat.mul(2n, b), Nat.add(x, y), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
488    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
489    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), hd)
490  +f_h6 = cvle(y, Nat.mul(3n, x), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
491    cv_3(l, x, y, b),
492    cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b)), h6)
493  contra(L{4n, 3n, 9n, 2n, 2n}, L{0n, 3n, 8n, 2n, 1n}, v,
494    comb(L{3n, 0n, 9n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{1n, 3n, 0n, 2n, 2n}, L{0n, 0n, 8n, 2n, 1n}, v, scale(3n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
495    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 0n, 2n, 2n}, L{0n, 0n, 7n, 1n, 0n}, v, f_h3,
496    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{0n, 0n, 6n, 0n, 0n}, v, f_hd,
497    scale(2n, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h6)))), {==})
498def rld.c1b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h6: LE(y, Nat.mul(3n, x))) -> LE(l, Nat.mul(3n, x)):
499  by_contra(l, Nat.mul(3n, x), ng => rld.c1b.k(l, x, y, b, ng, h3, hd, h6))
500
501def rld.w1(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(x, y), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(x, y))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), +h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(x, y)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(l, x) == True{} : Bool}:
502  MBool.and_eq_true(Nat.is_le(x, Nat.mul(3n, l)), Nat.is_le(l, Nat.mul(3n, x)), rld.c1a(l, x, y, b, h1, h4, pl, py), rld.c1b(l, x, y, b, h3, hd, h6))
503
504def rld.c2a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, y), b), hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h5: LE(x, Nat.mul(3n, y))) -> Empty:
505  +v = {VS{l, x, y, b} : Vs}
506  +f_ng = cvle(1n+Nat.mul(3n, y), b, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v,
507    cv_add(1n, Nat.mul(3n, y), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b))),
508    cv_4(l, x, y, b), ng)
509  +f_hd = cvle(Nat.mul(2n, b), Nat.add(x, y), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
510    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
511    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)), hd)
512  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
513    cv_2(l, x, y, b),
514    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
515  contra(L{2n, 0n, 1n, 6n, 2n}, L{0n, 0n, 1n, 4n, 2n}, v,
516    comb(L{2n, 0n, 0n, 6n, 0n}, L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 0n, 2n}, L{0n, 0n, 1n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, f_ng),
517    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_hd,
518    f_h5)), {==})
519def rld.c2a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, hd: LE(Nat.mul(2n, b), Nat.add(x, y)), h5: LE(x, Nat.mul(3n, y))) -> LE(b, Nat.mul(3n, y)):
520  by_contra(b, Nat.mul(3n, y), ng => rld.c2a.k(l, x, y, b, ng, hd, h5))
521
522def rld.c2b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), y), h1: LE(Nat.add(x, y), Nat.mul(3n, b))) -> Empty:
523  +v = {VS{l, x, y, b} : Vs}
524  +f_ng = cvle(1n+Nat.mul(3n, b), y, L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, v,
525    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b))),
526    cv_3(l, x, y, b), ng)
527  +f_h1 = cvle(Nat.add(x, y), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
528    cv_add(x, y, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(l, x, y, b), cv_3(l, x, y, b)),
529    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
530  contra(L{1n, 0n, 1n, 1n, 3n}, L{0n, 0n, 0n, 1n, 3n}, v,
531    comb(L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, f_ng,
532    f_h1), {==})
533def rld.c2b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(x, y), Nat.mul(3n, b))) -> LE(y, Nat.mul(3n, b)):
534  by_contra(y, Nat.mul(3n, b), ng => rld.c2b.k(l, x, y, b, ng, h1))
535
536def rld.w2(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(x, y), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(x, y))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(Nat.add(x, y), b)), +h4: LE(Nat.add(Nat.add(x, y), b), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(x, y)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(y, b) == True{} : Bool}:
537  MBool.and_eq_true(Nat.is_le(b, Nat.mul(3n, y)), Nat.is_le(y, Nat.mul(3n, b)), rld.c2a(l, x, y, b, hd, h5), rld.c2b(l, x, y, b, h1))
538
539def rhd.c0a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(b, y)), Nat.add(x, l)), h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), h5: LE(x, Nat.mul(3n, y))) -> Empty:
540  +v = {VS{l, x, y, b} : Vs}
541  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(b, y)), Nat.add(x, l), L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v,
542    cv_add(1n, Nat.mul(3n, Nat.add(b, y)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 3n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(b, y), L{0n, 0n, 0n, 1n, 1n}, v, cv_add(b, y, L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_4(l, x, y, b), cv_3(l, x, y, b)))),
543    cv_add(x, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, x, y, b), cv_1(l, x, y, b)), ng)
544  +f_h1 = cvle(Nat.add(y, x), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
545    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)),
546    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
547  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x)), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
548    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
549    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))), h3)
550  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
551    cv_2(l, x, y, b),
552    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
553  contra(L{3n, 3n, 3n, 7n, 6n}, L{0n, 2n, 3n, 7n, 4n}, v,
554    comb(L{2n, 0n, 0n, 6n, 6n}, L{0n, 2n, 2n, 0n, 0n}, L{1n, 3n, 3n, 1n, 0n}, L{0n, 0n, 1n, 7n, 4n}, v, scale(2n, L{1n, 0n, 0n, 3n, 3n}, L{0n, 1n, 1n, 0n, 0n}, v, f_ng),
555    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{1n, 3n, 2n, 0n, 0n}, L{0n, 0n, 1n, 7n, 1n}, v, f_h1,
556    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 2n, 0n, 0n}, L{0n, 0n, 0n, 6n, 0n}, v, f_h3,
557    scale(2n, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_h5)))), {==})
558def rhd.c0a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), h5: LE(x, Nat.mul(3n, y))) -> LE(Nat.add(x, l), Nat.mul(3n, Nat.add(b, y))):
559  by_contra(Nat.add(x, l), Nat.mul(3n, Nat.add(b, y)), ng => rhd.c0a.k(l, x, y, b, ng, h1, h3, h5))
560
561def rhd.c0b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, Nat.add(x, l)), Nat.add(b, y)), h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> Empty:
562  +v = {VS{l, x, y, b} : Vs}
563  +f_ng = cvle(1n+Nat.mul(3n, Nat.add(x, l)), Nat.add(b, y), L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, v,
564    cv_add(1n, Nat.mul(3n, Nat.add(x, l)), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, Nat.add(x, l), L{0n, 1n, 1n, 0n, 0n}, v, cv_add(x, l, L{0n, 0n, 1n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_2(l, x, y, b), cv_1(l, x, y, b)))),
565    cv_add(b, y, L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_4(l, x, y, b), cv_3(l, x, y, b)), ng)
566  +f_h4 = cvle(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
567    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))),
568    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
569  +f_px = cvle(1n, x, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
570    cv_c(1n, v),
571    cv_2(l, x, y, b), px)
572  contra(L{4n, 3n, 4n, 1n, 1n}, L{3n, 3n, 3n, 1n, 1n}, v,
573    comb(L{1n, 3n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 1n}, L{3n, 0n, 1n, 1n, 1n}, L{3n, 3n, 3n, 0n, 0n}, v, f_ng,
574    comb(L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h4,
575    scale(3n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_px))), {==})
576def rhd.c0b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), px: LE(1n, x)) -> LE(Nat.add(b, y), Nat.mul(3n, Nat.add(x, l))):
577  by_contra(Nat.add(b, y), Nat.mul(3n, Nat.add(x, l)), ng => rhd.c0b.k(l, x, y, b, ng, h4, px))
578
579def rhd.w0(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(y, x), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(y, x))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), +h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(y, x)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(Nat.add(b, y), Nat.add(x, l)) == True{} : Bool}:
580  MBool.and_eq_true(Nat.is_le(Nat.add(x, l), Nat.mul(3n, Nat.add(b, y))), Nat.is_le(Nat.add(b, y), Nat.mul(3n, Nat.add(x, l))), rhd.c0a(l, x, y, b, h1, h3, h5), rhd.c0b(l, x, y, b, h4, px))
581
582def rhd.c1a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, b), y), h1: LE(Nat.add(y, x), Nat.mul(3n, b))) -> Empty:
583  +v = {VS{l, x, y, b} : Vs}
584  +f_ng = cvle(1n+Nat.mul(3n, b), y, L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, v,
585    cv_add(1n, Nat.mul(3n, b), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, cv_c(1n, v), cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b))),
586    cv_3(l, x, y, b), ng)
587  +f_h1 = cvle(Nat.add(y, x), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
588    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)),
589    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
590  contra(L{1n, 0n, 1n, 1n, 3n}, L{0n, 0n, 0n, 1n, 3n}, v,
591    comb(L{1n, 0n, 0n, 0n, 3n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v, f_ng,
592    f_h1), {==})
593def rhd.c1a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(y, x), Nat.mul(3n, b))) -> LE(y, Nat.mul(3n, b)):
594  by_contra(y, Nat.mul(3n, b), ng => rhd.c1a.k(l, x, y, b, ng, h1))
595
596def rhd.c1b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, y), b), hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h5: LE(x, Nat.mul(3n, y))) -> Empty:
597  +v = {VS{l, x, y, b} : Vs}
598  +f_ng = cvle(1n+Nat.mul(3n, y), b, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v,
599    cv_add(1n, Nat.mul(3n, y), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b))),
600    cv_4(l, x, y, b), ng)
601  +f_hd = cvle(Nat.mul(2n, b), Nat.add(y, x), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
602    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
603    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)), hd)
604  +f_h5 = cvle(x, Nat.mul(3n, y), L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v,
605    cv_2(l, x, y, b),
606    cv_mul(3n, y, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(l, x, y, b)), h5)
607  contra(L{2n, 0n, 1n, 6n, 2n}, L{0n, 0n, 1n, 4n, 2n}, v,
608    comb(L{2n, 0n, 0n, 6n, 0n}, L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 0n, 2n}, L{0n, 0n, 1n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 3n, 0n}, L{0n, 0n, 0n, 0n, 1n}, v, f_ng),
609    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, f_hd,
610    f_h5)), {==})
611def rhd.c1b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h5: LE(x, Nat.mul(3n, y))) -> LE(b, Nat.mul(3n, y)):
612  by_contra(b, Nat.mul(3n, y), ng => rhd.c1b.k(l, x, y, b, ng, hd, h5))
613
614def rhd.w1(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(y, x), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(y, x))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), +h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(y, x)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(b, y) == True{} : Bool}:
615  MBool.and_eq_true(Nat.is_le(y, Nat.mul(3n, b)), Nat.is_le(b, Nat.mul(3n, y)), rhd.c1a(l, x, y, b, h1), rhd.c1b(l, x, y, b, hd, h5))
616
617def rhd.c2a.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, x), l), h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h6: LE(y, Nat.mul(3n, x))) -> Empty:
618  +v = {VS{l, x, y, b} : Vs}
619  +f_ng = cvle(1n+Nat.mul(3n, x), l, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
620    cv_add(1n, Nat.mul(3n, x), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b))),
621    cv_1(l, x, y, b), ng)
622  +f_h3 = cvle(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x)), L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, v,
623    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
624    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))), h3)
625  +f_hd = cvle(Nat.mul(2n, b), Nat.add(y, x), L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, v,
626    cv_mul(2n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)),
627    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)), hd)
628  +f_h6 = cvle(y, Nat.mul(3n, x), L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
629    cv_3(l, x, y, b),
630    cv_mul(3n, x, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(l, x, y, b)), h6)
631  contra(L{4n, 3n, 9n, 2n, 2n}, L{0n, 3n, 8n, 2n, 1n}, v,
632    comb(L{3n, 0n, 9n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{1n, 3n, 0n, 2n, 2n}, L{0n, 0n, 8n, 2n, 1n}, v, scale(3n, L{1n, 0n, 3n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_ng),
633    comb(L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 1n}, L{0n, 0n, 0n, 2n, 2n}, L{0n, 0n, 7n, 1n, 0n}, v, f_h3,
634    comb(L{0n, 0n, 0n, 0n, 2n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 2n, 0n}, L{0n, 0n, 6n, 0n, 0n}, v, f_hd,
635    scale(2n, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, f_h6)))), {==})
636def rhd.c2a(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), hd: LE(Nat.mul(2n, b), Nat.add(y, x)), h6: LE(y, Nat.mul(3n, x))) -> LE(l, Nat.mul(3n, x)):
637  by_contra(l, Nat.mul(3n, x), ng => rhd.c2a.k(l, x, y, b, ng, h3, hd, h6))
638
639def rhd.c2b.k(+l: Nat, +x: Nat, +y: Nat, +b: Nat, ng: LE(1n+Nat.mul(3n, l), x), h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> Empty:
640  +v = {VS{l, x, y, b} : Vs}
641  +f_ng = cvle(1n+Nat.mul(3n, l), x, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
642    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))),
643    cv_2(l, x, y, b), ng)
644  +f_h1 = cvle(Nat.add(y, x), Nat.mul(3n, b), L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, v,
645    cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b)),
646    cv_mul(3n, b, L{0n, 0n, 0n, 0n, 1n}, v, cv_4(l, x, y, b)), h1)
647  +f_h4 = cvle(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l)), L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v,
648    cv_add(b, Nat.add(y, x), L{0n, 0n, 0n, 0n, 1n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_4(l, x, y, b), cv_add(y, x, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_3(l, x, y, b), cv_2(l, x, y, b))),
649    cv_add(3n, Nat.mul(3n, l), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, x, y, b))), h4)
650  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
651    cv_c(1n, v),
652    cv_1(l, x, y, b), pl)
653  +f_py = cvle(1n, y, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
654    cv_c(1n, v),
655    cv_3(l, x, y, b), py)
656  contra(L{10n, 12n, 4n, 4n, 3n}, L{9n, 11n, 4n, 4n, 3n}, v,
657    comb(L{4n, 12n, 0n, 0n, 0n}, L{0n, 0n, 4n, 0n, 0n}, L{6n, 0n, 4n, 4n, 3n}, L{9n, 11n, 0n, 4n, 3n}, v, scale(4n, L{1n, 3n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, f_ng),
658    comb(L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 0n, 0n, 3n}, L{6n, 0n, 3n, 3n, 3n}, L{9n, 11n, 0n, 4n, 0n}, v, f_h1,
659    comb(L{0n, 0n, 3n, 3n, 3n}, L{9n, 9n, 0n, 0n, 0n}, L{6n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 4n, 0n}, v, scale(3n, L{0n, 0n, 1n, 1n, 1n}, L{3n, 3n, 0n, 0n, 0n}, v, f_h4),
660    comb(L{2n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, L{4n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 4n, 0n}, v, scale(2n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pl),
661    scale(4n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, f_py))))), {==})
662def rhd.c2b(+l: Nat, +x: Nat, +y: Nat, +b: Nat, h1: LE(Nat.add(y, x), Nat.mul(3n, b)), h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), pl: LE(1n, l), py: LE(1n, y)) -> LE(x, Nat.mul(3n, l)):
663  by_contra(x, Nat.mul(3n, l), ng => rhd.c2b.k(l, x, y, b, ng, h1, h4, pl, py))
664
665def rhd.w2(+l: Nat, +x: Nat, +y: Nat, +b: Nat, +h1: LE(Nat.add(y, x), Nat.mul(3n, b)), +h2: LE(b, Nat.mul(3n, Nat.add(y, x))), +h3: LE(1n+Nat.mul(3n, l), Nat.add(b, Nat.add(y, x))), +h4: LE(Nat.add(b, Nat.add(y, x)), Nat.add(3n, Nat.mul(3n, l))), +hd: LE(Nat.mul(2n, b), Nat.add(y, x)), +h5: LE(x, Nat.mul(3n, y)), +h6: LE(y, Nat.mul(3n, x)), +pl: LE(1n, l), +px: LE(1n, x), +py: LE(1n, y), +pb: LE(1n, b)) -> {wok(x, l) == True{} : Bool}:
666  MBool.and_eq_true(Nat.is_le(l, Nat.mul(3n, x)), Nat.is_le(x, Nat.mul(3n, l)), rhd.c2a(l, x, y, b, h3, hd, h6), rhd.c2b(l, x, y, b, h1, h4, pl, py))
667
668def tiph(+l: Nat, h: LE(1n+Nat.mul(3n, l), 1n), pl: LE(1n, l)) -> Empty:
669  +v = {VS{l, 0n, 0n, 0n} : Vs}
670  +f_h = cvle(1n+Nat.mul(3n, l), 1n, L{1n, 3n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v,
671    cv_add(1n, Nat.mul(3n, l), L{1n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_mul(3n, l, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(l, 0n, 0n, 0n))),
672    cv_c(1n, v), h)
673  +f_pl = cvle(1n, l, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
674    cv_c(1n, v),
675    cv_1(l, 0n, 0n, 0n), pl)
676  contra(L{2n, 3n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
677    comb(L{1n, 3n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_h,
678    f_pl), {==})
679
680def dtip(+b: Nat, h: LE(Nat.mul(2n, b), 1n), pb: LE(1n, b)) -> Empty:
681  +v = {VS{b, 0n, 0n, 0n} : Vs}
682  +f_h = cvle(Nat.mul(2n, b), 1n, L{0n, 2n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v,
683    cv_mul(2n, b, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(b, 0n, 0n, 0n)),
684    cv_c(1n, v), h)
685  +f_pb = cvle(1n, b, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
686    cv_c(1n, v),
687    cv_1(b, 0n, 0n, 0n), pb)
688  contra(L{2n, 2n, 0n, 0n, 0n}, L{1n, 2n, 0n, 0n, 0n}, v,
689    comb(L{0n, 2n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, L{2n, 0n, 0n, 0n, 0n}, L{0n, 2n, 0n, 0n, 0n}, v, f_h,
690    scale(2n, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, f_pb)), {==})
691
692def almlo.c0a.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, w2)), wh), o1: LE(wh, Nat.mul(3n, wl)), n1: LE(wl, 1n+w2)) -> Empty:
693  +v = {VS{wl, wh, w2, 0n} : Vs}
694  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, w2)), wh, L{4n, 0n, 0n, 3n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v,
695    cv_add(1n, Nat.add(3n, Nat.mul(3n, w2)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, w2), L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(3n, v), cv_mul(3n, w2, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(wl, wh, w2, 0n)))),
696    cv_2(wl, wh, w2, 0n), ng)
697  +f_o1 = cvle(wh, Nat.mul(3n, wl), L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v,
698    cv_2(wl, wh, w2, 0n),
699    cv_mul(3n, wl, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(wl, wh, w2, 0n)), o1)
700  +f_n1 = cvle(wl, 1n+w2, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v,
701    cv_1(wl, wh, w2, 0n),
702    cv_add(1n, w2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_3(wl, wh, w2, 0n)), n1)
703  contra(L{4n, 3n, 1n, 3n, 0n}, L{3n, 3n, 1n, 3n, 0n}, v,
704    comb(L{4n, 0n, 0n, 3n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 1n, 0n, 0n}, L{3n, 3n, 0n, 3n, 0n}, v, f_ng,
705    comb(L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, f_o1,
706    scale(3n, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v, f_n1))), {==})
707def almlo.c0a(+wl: Nat, +wh: Nat, +w2: Nat, o1: LE(wh, Nat.mul(3n, wl)), n1: LE(wl, 1n+w2)) -> LE(wh, Nat.add(3n, Nat.mul(3n, w2))):
708  by_contra(wh, Nat.add(3n, Nat.mul(3n, w2)), ng => almlo.c0a.k(wl, wh, w2, ng, o1, n1))
709
710def almlo.c0b.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, wh)), w2), o2: LE(wl, Nat.mul(3n, wh)), n2: LE(w2, 1n+wl)) -> Empty:
711  +v = {VS{wl, wh, w2, 0n} : Vs}
712  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, wh)), w2, L{4n, 0n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
713    cv_add(1n, Nat.add(3n, Nat.mul(3n, wh)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 0n, 3n, 0n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, wh), L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, wh, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(wl, wh, w2, 0n)))),
714    cv_3(wl, wh, w2, 0n), ng)
715  +f_o2 = cvle(wl, Nat.mul(3n, wh), L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
716    cv_1(wl, wh, w2, 0n),
717    cv_mul(3n, wh, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(wl, wh, w2, 0n)), o2)
718  +f_n2 = cvle(w2, 1n+wl, L{0n, 0n, 0n, 1n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
719    cv_3(wl, wh, w2, 0n),
720    cv_add(1n, wl, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(wl, wh, w2, 0n)), n2)
721  contra(L{4n, 1n, 3n, 1n, 0n}, L{1n, 1n, 3n, 1n, 0n}, v,
722    comb(L{4n, 0n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 1n, 0n, 1n, 0n}, L{1n, 1n, 3n, 0n, 0n}, v, f_ng,
723    comb(L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, f_o2,
724    f_n2)), {==})
725def almlo.c0b(+wl: Nat, +wh: Nat, +w2: Nat, o2: LE(wl, Nat.mul(3n, wh)), n2: LE(w2, 1n+wl)) -> LE(w2, Nat.add(3n, Nat.mul(3n, wh))):
726  by_contra(w2, Nat.add(3n, Nat.mul(3n, wh)), ng => almlo.c0b.k(wl, wh, w2, ng, o2, n2))
727
728def almlo.w0(+wl: Nat, +wh: Nat, +w2: Nat, +o1: LE(wh, Nat.mul(3n, wl)), +o2: LE(wl, Nat.mul(3n, wh)), +n1: LE(wl, 1n+w2), +n2: LE(w2, 1n+wl)) -> {alm(w2, wh) == True{} : Bool}:
729  MBool.and_eq_true(Nat.is_le(wh, Nat.add(3n, Nat.mul(3n, w2))), Nat.is_le(w2, Nat.add(3n, Nat.mul(3n, wh))), almlo.c0a(wl, wh, w2, o1, n1), almlo.c0b(wl, wh, w2, o2, n2))
730
731def almhi.c0a.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, wl)), w2), o1: LE(wh, Nat.mul(3n, wl)), n2: LE(w2, 1n+wh)) -> Empty:
732  +v = {VS{wl, wh, w2, 0n} : Vs}
733  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, wl)), w2, L{4n, 3n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v,
734    cv_add(1n, Nat.add(3n, Nat.mul(3n, wl)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 3n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, wl), L{3n, 0n, 0n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v, cv_c(3n, v), cv_mul(3n, wl, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(wl, wh, w2, 0n)))),
735    cv_3(wl, wh, w2, 0n), ng)
736  +f_o1 = cvle(wh, Nat.mul(3n, wl), L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, v,
737    cv_2(wl, wh, w2, 0n),
738    cv_mul(3n, wl, L{0n, 1n, 0n, 0n, 0n}, v, cv_1(wl, wh, w2, 0n)), o1)
739  +f_n2 = cvle(w2, 1n+wh, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v,
740    cv_3(wl, wh, w2, 0n),
741    cv_add(1n, wh, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(wl, wh, w2, 0n)), n2)
742  contra(L{4n, 3n, 1n, 1n, 0n}, L{1n, 3n, 1n, 1n, 0n}, v,
743    comb(L{4n, 3n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{1n, 3n, 1n, 0n, 0n}, v, f_ng,
744    comb(L{0n, 0n, 1n, 0n, 0n}, L{0n, 3n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v, f_o1,
745    f_n2)), {==})
746def almhi.c0a(+wl: Nat, +wh: Nat, +w2: Nat, o1: LE(wh, Nat.mul(3n, wl)), n2: LE(w2, 1n+wh)) -> LE(w2, Nat.add(3n, Nat.mul(3n, wl))):
747  by_contra(w2, Nat.add(3n, Nat.mul(3n, wl)), ng => almhi.c0a.k(wl, wh, w2, ng, o1, n2))
748
749def almhi.c0b.k(+wl: Nat, +wh: Nat, +w2: Nat, ng: LE(1n+Nat.add(3n, Nat.mul(3n, w2)), wl), o2: LE(wl, Nat.mul(3n, wh)), n1: LE(wh, 1n+w2)) -> Empty:
750  +v = {VS{wl, wh, w2, 0n} : Vs}
751  +f_ng = cvle(1n+Nat.add(3n, Nat.mul(3n, w2)), wl, L{4n, 0n, 0n, 3n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
752    cv_add(1n, Nat.add(3n, Nat.mul(3n, w2)), L{1n, 0n, 0n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, cv_c(1n, v), cv_add(3n, Nat.mul(3n, w2), L{3n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 3n, 0n}, v, cv_c(3n, v), cv_mul(3n, w2, L{0n, 0n, 0n, 1n, 0n}, v, cv_3(wl, wh, w2, 0n)))),
753    cv_1(wl, wh, w2, 0n), ng)
754  +f_o2 = cvle(wl, Nat.mul(3n, wh), L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, v,
755    cv_1(wl, wh, w2, 0n),
756    cv_mul(3n, wh, L{0n, 0n, 1n, 0n, 0n}, v, cv_2(wl, wh, w2, 0n)), o2)
757  +f_n1 = cvle(wh, 1n+w2, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v,
758    cv_2(wl, wh, w2, 0n),
759    cv_add(1n, w2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_3(wl, wh, w2, 0n)), n1)
760  contra(L{4n, 1n, 3n, 3n, 0n}, L{3n, 1n, 3n, 3n, 0n}, v,
761    comb(L{4n, 0n, 0n, 3n, 0n}, L{0n, 1n, 0n, 0n, 0n}, L{0n, 1n, 3n, 0n, 0n}, L{3n, 0n, 3n, 3n, 0n}, v, f_ng,
762    comb(L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{0n, 0n, 3n, 0n, 0n}, L{3n, 0n, 0n, 3n, 0n}, v, f_o2,
763    scale(3n, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v, f_n1))), {==})
764def almhi.c0b(+wl: Nat, +wh: Nat, +w2: Nat, o2: LE(wl, Nat.mul(3n, wh)), n1: LE(wh, 1n+w2)) -> LE(wl, Nat.add(3n, Nat.mul(3n, w2))):
765  by_contra(wl, Nat.add(3n, Nat.mul(3n, w2)), ng => almhi.c0b.k(wl, wh, w2, ng, o2, n1))
766
767def almhi.w0(+wl: Nat, +wh: Nat, +w2: Nat, +o1: LE(wh, Nat.mul(3n, wl)), +o2: LE(wl, Nat.mul(3n, wh)), +n1: LE(wh, 1n+w2), +n2: LE(w2, 1n+wh)) -> {alm(wl, w2) == True{} : Bool}:
768  MBool.and_eq_true(Nat.is_le(w2, Nat.add(3n, Nat.mul(3n, wl))), Nat.is_le(wl, Nat.add(3n, Nat.mul(3n, w2))), almhi.c0a(wl, wh, w2, o1, n2), almhi.c0b(wl, wh, w2, o2, n1))
769
770def nearlo.c0a.k(+a: Nat, +a2: Nat, +c: Nat, ng: LE(1n+1n+Nat.add(a2, c), Nat.add(a, c)), n1: LE(a, 1n+a2)) -> Empty:
771  +v = {VS{a, a2, c, 0n} : Vs}
772  +f_ng = cvle(1n+1n+Nat.add(a2, c), Nat.add(a, c), L{2n, 0n, 1n, 1n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v,
773    cv_add(1n, 1n+Nat.add(a2, c), L{1n, 0n, 0n, 0n, 0n}, L{1n, 0n, 1n, 1n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a2, c), L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v, cv_c(1n, v), cv_add(a2, c, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(a, a2, c, 0n), cv_3(a, a2, c, 0n)))),
774    cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, a2, c, 0n), cv_3(a, a2, c, 0n)), ng)
775  +f_n1 = cvle(a, 1n+a2, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v,
776    cv_1(a, a2, c, 0n),
777    cv_add(1n, a2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(a, a2, c, 0n)), n1)
778  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
779    comb(L{2n, 0n, 1n, 1n, 0n}, L{0n, 1n, 0n, 1n, 0n}, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v, f_ng,
780    f_n1), {==})
781def nearlo.c0a(+a: Nat, +a2: Nat, +c: Nat, n1: LE(a, 1n+a2)) -> LE(Nat.add(a, c), 1n+Nat.add(a2, c)):
782  by_contra(Nat.add(a, c), 1n+Nat.add(a2, c), ng => nearlo.c0a.k(a, a2, c, ng, n1))
783
784def nearlo.c0b.k(+a: Nat, +a2: Nat, +c: Nat, ng: LE(1n+1n+Nat.add(a, c), Nat.add(a2, c)), n2: LE(a2, 1n+a)) -> Empty:
785  +v = {VS{a, a2, c, 0n} : Vs}
786  +f_ng = cvle(1n+1n+Nat.add(a, c), Nat.add(a2, c), L{2n, 1n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, v,
787    cv_add(1n, 1n+Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, a2, c, 0n), cv_3(a, a2, c, 0n)))),
788    cv_add(a2, c, L{0n, 0n, 1n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_2(a, a2, c, 0n), cv_3(a, a2, c, 0n)), ng)
789  +f_n2 = cvle(a2, 1n+a, L{0n, 0n, 1n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
790    cv_2(a, a2, c, 0n),
791    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, a2, c, 0n)), n2)
792  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
793    comb(L{2n, 1n, 0n, 1n, 0n}, L{0n, 0n, 1n, 1n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, f_ng,
794    f_n2), {==})
795def nearlo.c0b(+a: Nat, +a2: Nat, +c: Nat, n2: LE(a2, 1n+a)) -> LE(Nat.add(a2, c), 1n+Nat.add(a, c)):
796  by_contra(Nat.add(a2, c), 1n+Nat.add(a, c), ng => nearlo.c0b.k(a, a2, c, ng, n2))
797
798def nearlo.w0(+a: Nat, +a2: Nat, +c: Nat, +n1: LE(a, 1n+a2), +n2: LE(a2, 1n+a)) -> {near(Nat.add(a, c), Nat.add(a2, c)) == True{} : Bool}:
799  MBool.and_eq_true(Nat.is_le(Nat.add(a, c), 1n+Nat.add(a2, c)), Nat.is_le(Nat.add(a2, c), 1n+Nat.add(a, c)), nearlo.c0a(a, a2, c, n1), nearlo.c0b(a, a2, c, n2))
800
801def nearhi.c0a.k(+a: Nat, +c: Nat, +c2: Nat, ng: LE(1n+1n+Nat.add(a, c2), Nat.add(a, c)), n1: LE(c, 1n+c2)) -> Empty:
802  +v = {VS{a, c, c2, 0n} : Vs}
803  +f_ng = cvle(1n+1n+Nat.add(a, c2), Nat.add(a, c), L{2n, 1n, 0n, 1n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v,
804    cv_add(1n, 1n+Nat.add(a, c2), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, c2), L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_add(a, c2, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, c, c2, 0n), cv_3(a, c, c2, 0n)))),
805    cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(a, c, c2, 0n), cv_2(a, c, c2, 0n)), ng)
806  +f_n1 = cvle(c, 1n+c2, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v,
807    cv_2(a, c, c2, 0n),
808    cv_add(1n, c2, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_c(1n, v), cv_3(a, c, c2, 0n)), n1)
809  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
810    comb(L{2n, 1n, 0n, 1n, 0n}, L{0n, 1n, 1n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, L{1n, 0n, 0n, 1n, 0n}, v, f_ng,
811    f_n1), {==})
812def nearhi.c0a(+a: Nat, +c: Nat, +c2: Nat, n1: LE(c, 1n+c2)) -> LE(Nat.add(a, c), 1n+Nat.add(a, c2)):
813  by_contra(Nat.add(a, c), 1n+Nat.add(a, c2), ng => nearhi.c0a.k(a, c, c2, ng, n1))
814
815def nearhi.c0b.k(+a: Nat, +c: Nat, +c2: Nat, ng: LE(1n+1n+Nat.add(a, c), Nat.add(a, c2)), n2: LE(c2, 1n+c)) -> Empty:
816  +v = {VS{a, c, c2, 0n} : Vs}
817  +f_ng = cvle(1n+1n+Nat.add(a, c), Nat.add(a, c2), L{2n, 1n, 1n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, v,
818    cv_add(1n, 1n+Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, c), L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_add(a, c, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_1(a, c, c2, 0n), cv_2(a, c, c2, 0n)))),
819    cv_add(a, c2, L{0n, 1n, 0n, 0n, 0n}, L{0n, 0n, 0n, 1n, 0n}, v, cv_1(a, c, c2, 0n), cv_3(a, c, c2, 0n)), ng)
820  +f_n2 = cvle(c2, 1n+c, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v,
821    cv_3(a, c, c2, 0n),
822    cv_add(1n, c, L{1n, 0n, 0n, 0n, 0n}, L{0n, 0n, 1n, 0n, 0n}, v, cv_c(1n, v), cv_2(a, c, c2, 0n)), n2)
823  contra(L{2n, 1n, 1n, 1n, 0n}, L{1n, 1n, 1n, 1n, 0n}, v,
824    comb(L{2n, 1n, 1n, 0n, 0n}, L{0n, 1n, 0n, 1n, 0n}, L{0n, 0n, 0n, 1n, 0n}, L{1n, 0n, 1n, 0n, 0n}, v, f_ng,
825    f_n2), {==})
826def nearhi.c0b(+a: Nat, +c: Nat, +c2: Nat, n2: LE(c2, 1n+c)) -> LE(Nat.add(a, c2), 1n+Nat.add(a, c)):
827  by_contra(Nat.add(a, c2), 1n+Nat.add(a, c), ng => nearhi.c0b.k(a, c, c2, ng, n2))
828
829def nearhi.w0(+a: Nat, +c: Nat, +c2: Nat, +n1: LE(c, 1n+c2), +n2: LE(c2, 1n+c)) -> {near(Nat.add(a, c), Nat.add(a, c2)) == True{} : Bool}:
830  MBool.and_eq_true(Nat.is_le(Nat.add(a, c), 1n+Nat.add(a, c2)), Nat.is_le(Nat.add(a, c2), 1n+Nat.add(a, c)), nearhi.c0a(a, c, c2, n1), nearhi.c0b(a, c, c2, n2))
831
832def nearrf.c0a.k(+a: Nat, ng: LE(1n+1n+a, a)) -> Empty:
833  +v = {VS{a, 0n, 0n, 0n} : Vs}
834  +f_ng = cvle(1n+1n+a, a, L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
835    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
836    cv_1(a, 0n, 0n, 0n), ng)
837  contra(L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
838    f_ng, {==})
839def nearrf.c0a(+a: Nat) -> LE(a, 1n+a):
840  by_contra(a, 1n+a, ng => nearrf.c0a.k(a, ng))
841
842def nearrf.c0b.k(+a: Nat, ng: LE(1n+1n+a, a)) -> Empty:
843  +v = {VS{a, 0n, 0n, 0n} : Vs}
844  +f_ng = cvle(1n+1n+a, a, L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
845    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
846    cv_1(a, 0n, 0n, 0n), ng)
847  contra(L{2n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
848    f_ng, {==})
849def nearrf.c0b(+a: Nat) -> LE(a, 1n+a):
850  by_contra(a, 1n+a, ng => nearrf.c0b.k(a, ng))
851
852def nearrf.w0(+a: Nat) -> {near(a, a) == True{} : Bool}:
853  MBool.and_eq_true(Nat.is_le(a, 1n+a), Nat.is_le(a, 1n+a), nearrf.c0a(a), nearrf.c0b(a))
854
855def nearpm.c0a.k(+a: Nat, ng: LE(1n+1n+a, 1n+a)) -> Empty:
856  +v = {VS{a, 0n, 0n, 0n} : Vs}
857  +f_ng = cvle(1n+1n+a, 1n+a, L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
858    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
859    cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n)), ng)
860  contra(L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
861    f_ng, {==})
862def nearpm.c0a(+a: Nat) -> LE(1n+a, 1n+a):
863  by_contra(1n+a, 1n+a, ng => nearpm.c0a.k(a, ng))
864
865def nearpm.c0b.k(+a: Nat, ng: LE(1n+1n+1n+a, a)) -> Empty:
866  +v = {VS{a, 0n, 0n, 0n} : Vs}
867  +f_ng = cvle(1n+1n+1n+a, a, L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
868    cv_add(1n, 1n+1n+a, L{1n, 0n, 0n, 0n, 0n}, L{2n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n)))),
869    cv_1(a, 0n, 0n, 0n), ng)
870  contra(L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
871    f_ng, {==})
872def nearpm.c0b(+a: Nat) -> LE(a, 1n+1n+a):
873  by_contra(a, 1n+1n+a, ng => nearpm.c0b.k(a, ng))
874
875def nearpm.w0(+a: Nat) -> {near(1n+a, a) == True{} : Bool}:
876  MBool.and_eq_true(Nat.is_le(1n+a, 1n+a), Nat.is_le(a, 1n+1n+a), nearpm.c0a(a), nearpm.c0b(a))
877
878def neargt.c0a.k(+a: Nat, ng: LE(1n+1n+a, Nat.add(a, 1n))) -> Empty:
879  +v = {VS{a, 0n, 0n, 0n} : Vs}
880  +f_ng = cvle(1n+1n+a, Nat.add(a, 1n), L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
881    cv_add(1n, 1n+a, L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, a, L{1n, 0n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_1(a, 0n, 0n, 0n))),
882    cv_add(a, 1n, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v, cv_1(a, 0n, 0n, 0n), cv_c(1n, v)), ng)
883  contra(L{2n, 1n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v,
884    f_ng, {==})
885def neargt.c0a(+a: Nat) -> LE(Nat.add(a, 1n), 1n+a):
886  by_contra(Nat.add(a, 1n), 1n+a, ng => neargt.c0a.k(a, ng))
887
888def neargt.c0b.k(+a: Nat, ng: LE(1n+1n+Nat.add(a, 1n), a)) -> Empty:
889  +v = {VS{a, 0n, 0n, 0n} : Vs}
890  +f_ng = cvle(1n+1n+Nat.add(a, 1n), a, L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
891    cv_add(1n, 1n+Nat.add(a, 1n), L{1n, 0n, 0n, 0n, 0n}, L{2n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(1n, Nat.add(a, 1n), L{1n, 0n, 0n, 0n, 0n}, L{1n, 1n, 0n, 0n, 0n}, v, cv_c(1n, v), cv_add(a, 1n, L{0n, 1n, 0n, 0n, 0n}, L{1n, 0n, 0n, 0n, 0n}, v, cv_1(a, 0n, 0n, 0n), cv_c(1n, v)))),
892    cv_1(a, 0n, 0n, 0n), ng)
893  contra(L{3n, 1n, 0n, 0n, 0n}, L{0n, 1n, 0n, 0n, 0n}, v,
894    f_ng, {==})
895def neargt.c0b(+a: Nat) -> LE(a, 1n+Nat.add(a, 1n)):
896  by_contra(a, 1n+Nat.add(a, 1n), ng => neargt.c0b.k(a, ng))
897
898def neargt.w0(+a: Nat) -> {near(Nat.add(a, 1n), a) == True{} : Bool}:
899  MBool.and_eq_true(Nat.is_le(Nat.add(a, 1n), 1n+a), Nat.is_le(a, 1n+Nat.add(a, 1n)), neargt.c0a(a), neargt.c0b(a))