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

PrintForm Definitions finite sets Sections AutomataTheory Doc

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

1. n:
2. m:
3. a3:
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

0a3m+a4

By: Analyze 2

Generated subgoal:

1 2. m:
3. 0 < m
4. a3:
5. 0a3
6. a3 < n
7. a4:
8. 0a4
9. a4 < m
10. a5:
11. 0a5
12. a5 < n
13. a6:
14. 0a6
15. a6 < m
0a3m+a4

About: