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

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 2 1 1 1 1 1

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
13. (a6 rem m) = a6
14. ((a4+a3m) rem m) = (a4 rem m)

((a4+a3m) rem m) = (a6 rem m)

By: Assert (a4+a3m = a3m+a4)

Generated subgoals:

1 a4+a3m = a3m+a4

2 15. a4+a3m = a3m+a4
((a4+a3m) rem m) = (a6 rem m)

About:

1	`a4+a3m = a3m+a4`
2	15. `a4+a3m = a3m+a4` `((a4+a3m) rem m) = (a6 rem m)`