PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
rect
enumer
1
3
1
1
1
1
1
1
1
1
1
1
1
5
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
a5
m+a6 < n
m
By:
Inst Thm*
i,j:
. i
j
i < j+1 [a5;n-1]
Generated subgoal:
1
15.
a5
n-1
a5 < n-1+1
a5
m+a6 < n
m
About:
n-1 
a5 < n-1+1
a5
m+a6 < nm
a3a4a5a6 a5m+a6 < nm
i,j:. ij i < j+1 [a5;n-1]n-1 a5 < n-1+1 a5m+a6 < nm
