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