Nuprl - Pf rect_enumer 1 3 1 1 1 1 1 1 1 1 1 1 1 1 2 2

PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 1 1 1 1 1 1 1 1 1 1 1 1 2 2

1. n:
2. m:
3. a3:
4. 0 a3 < n
5. a4:
6. 0 a4 < m
7. a5:
8. 0 a5 < n
9. a6:
10. 0 a6 < m
11. a3m+a4 = a5m+a6 (nm)
12. (a4 rem m) = a4

a4 = a6 m

By: Inst Thm* a:, n:. |a| < |n| (a rem n) = a [a6;m]

Generated subgoals:

1 4. 0a3
5. a3 < n
6. a4:
7. 0a4
8. a4 < m
9. a5:
10. 0a5
11. a5 < n
12. a6:
13. 0a6
14. a6 < m
15. a3m+a4 = a5m+a6 (nm)
16. (a4 rem m) = a4
|a6| < |m|

2 13. (a6 rem m) = a6
a4 = a6 m

About:

1	4. `0a3` 5. `a3 < n` 6. `a4:` 7. `0a4` 8. `a4 < m` 9. `a5:` 10. `0a5` 11. `a5 < n` 12. `a6:` 13. `0a6` 14. `a6 < m` 15. `a3m+a4 = a5m+a6 (nm)` 16. `(a4 rem m) = a4` `\|a6\| < \|m\|`
2	13. `(a6 rem m) = a6` `a4 = a6 m`