PrintForm Definitions finite sets Sections AutomataTheory Doc

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

a3m+a4 = a5m+a6 (nm) < a3,a4 > = < a5,a6 > nm
By: Analyze 0
Generated subgoals:

111. a3m+a4 = a5m+a6 (nm)
< a3,a4 > = < a5,a6 > nm
24. 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
34. 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
a3m+a4 < nm
44. 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
54. 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
a5m+a6 < nm

About:
impliesequalnatural_numbermultiplyadd
productpairintless_than