Nuprl - Pf rect_enumer 1 3 1 1 1 1 1 1 1 1 1 1 1 1 2 2 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 1 1

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
15. a3m+a4 = a5m+a6 (nm)
16. (a4 rem m) = a4

if 0a6 a6 else -a6 fi < if 0m m else -m fi

By: SplitOnConclITE THEN SplitOnConclITE

Generated subgoals:

None

About: