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
1
1
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
15.
a3
n-1
a3 < n-1+1
16.
a3
n-1
a3
m+a4 < n
m
By:
Inst
Thm*
a,b:
, n:
. a
b
n
a
n
b [a3;n-1;m]
Generated subgoal:
1
17.
m
a3
m
(n-1)
a3
m+a4 < n
m
About:
a3
m(n-1)
a3m+a4 < nm
a3a4a5a6n-1 
a3 < n-1+1n-1 a3m+a4 < nm
a,b:, n:. ab nanb
[a3;n-1;m]a3m(n-1) a3m+a4 < nm
