PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1
2
1
1
1
7
1
1
1
1.
n:
2.
m:
3.
b:
(n
m)
4.
a1:
5.
0
a1 < n
6.
a2:
7.
0
a2 < m
a1
m+a2 < n
m
By:
Inst Thm*
i,j:
. i
j
i < j+1 [a1;n-1]
THEN
Analyze 8
Generated subgoal:
1
8.
a1
n-1
a1 < n-1+1
9.
(a1
n-1)
(a1 < n-1+1)
a1
m+a2 < n
m
About:
n-1 
a1 < n-1+1n-1) 
(a1 < n-1+1)
a1
m+a2 < nm
(nm)
a1 < n a2 < m a1m+a2 < nm
i,j:. ij i < j+1 [a1;n-1]
n-1 a1 < n-1+1n-1) (a1 < n-1+1) a1m+a2 < nm
