PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 1 1 1 1 1 1 1 1 1 1 1 4
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

0a5m+a6
By: Inst Thm* a,b:. 0ab [a5;m]
Generated subgoals:

None

About:
natural_numberaddmultiplyallintless_than