PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1
1
1
1
1
1
1
1
1
1
1
3
1.
n:
2.
m:
3.
a3:
4.
0
a3
5.
a3 < n
6.
a4:
7.
0
a4
8.
a4 < m
9.
a5:
10.
0
a5
11.
a5 < n
12.
a6:
13.
0
a6
14.
a6 < m
a3
m+a4 < n
m
By:
Inst Thm*
i,j:
. i
j
i < j+1 [a3;n-1]
Generated subgoal:
1
15.
a3
n-1
a3 < n-1+1
a3
m+a4 < n
m
About:
n-1 
a3 < n-1+1
a3
m+a4 < nm
a3a4a5a6 a3m+a4 < nm
i,j:. ij i < j+1 [a3;n-1]n-1 a3 < n-1+1 a3m+a4 < nm
