PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
2
1
1
1.
n:
2.
m:
3.
z1:
4.
0
z1 < n
5.
z2:
6.
0
z2 < m
z1
m+z2 < n
m
By:
Inst Thm*
i,j:
. i
j
i < j+1 [z1;n-1]
Generated subgoal:
1
7.
z1
n-1
z1 < n-1+1
z1
m+z2 < n
m
About:
n-1 
z1 < n-1+1
z1
m+z2 < nm
z1 < n z2 < m z1m+z2 < nm
i,j:. ij i < j+1 [z1;n-1]n-1 z1 < n-1+1 z1m+z2 < nm
