PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
2
1
1
1
1
1
1
1.
n:
2.
m:
3.
z1:
4.
0
z1 < n
5.
z2:
6.
0
z2 < m
7.
z1
n-1
z1 < n-1+1
8.
z1
n-1
9.
m
z1
m
(n-1)
z1
m+z2 < n
m
By:
Inst
Thm*
i1,i2,j1,j2:
. i1 < j1
i2
j2
i1+i2 < j1+j2 [z2;m
z1;m;m
(n-1)]
Generated subgoal:
1
10.
z2+m
z1 < m+m
(n-1)
z1
m+z2 < n
m
About:
z1 < m+m(n-1)
z1m+z2 < nm
z1 < n z2 < mn-1 
z1 < n-1+1n-1z1m(n-1) z1m+z2 < nm
i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2
[z2;mz1;m;m(n-1)]z1 < m+m(n-1) z1m+z2 < nm
