n)
n+(0 rem n)3. 0
n4. 0
(0 rem n) & (0 rem n) < n
(0 n) = 0 n)n+(0 rem n)3.
0n4. 0
(0 rem n) & (0 rem n) > n (0 n) = 0
(0 n) = 0
a:, n:. a = (a n)n+(a rem n)
[0;n])
THEN
(Decide (0n)))
THENL
[Inst
Thm* a:
, n:
. 0(a rem n) & (a rem n) < n
[0;n]
;Inst
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > n
[0;n]]
| 1 | 2. 0 = (0 n)n+(0 rem n) 3. 0 n4. 0 (0 rem n) & (0 rem n) < n (0 n) = 0 | 1 step |
| 2 | 2. 0 = (0 n)n+(0 rem n) 3. 0n4. 0 (0 rem n) & (0 rem n) > n (0 n) = 0 | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |  |