PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 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: n
8. a6: m

1of( < a3,a4 > )m+2of( < a3,a4 > ) = 1of( < a5,a6 > )m+2of( < a5,a6 > ) (nm) < a3,a4 > = < a5,a6 > nm

By: Analyze 7

Generated subgoal:

17. a5:
8. 0 a5 < n
9. a6: m
1of( < a3,a4 > )m+2of( < a3,a4 > ) = 1of( < a5,a6 > )m+2of( < a5,a6 > ) (nm) < a3,a4 > = < a5,a6 > nm


About:
impliesequalnatural_numbermultiplyaddpairproductint