PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 2 1 1 1 1

1. n:
2. m:
3. z1:
4. 0 z1 < n
5. z2:
6. 0 z2 < m
7. z1n-1 z1 < n-1+1
8. (z1n-1) (z1 < n-1+1)

z1m+z2 < nm

By: Analyze 8

Generated subgoal:

18. z1n-1
z1m+z2 < nm


About:
less_thanaddmultiplyintnatural_numberimpliessubtract