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