nat_order.bend
bend-kit-collections@0.1.3.0 · 899 lines · 0 definitions
1# Nat order and linear-form lemmas for the OMap weight-balance proofs.
2import Base
3import bend-mathlib@0.7.2.0/nat.bend as MNat
4import bend-mathlib@0.7.2.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))