PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
incl
aux3
quo
1
2
1
1
1.
n:
{1...}
2.
m:
n
3.
E:
n
n
Prop
4.
EquivRel i,j:
n. i E j
5.
EquivRel i,j:
m. i E j
6.
x:
i,j:
m//(i E j)
7.
y:
i,j:
m//(i E j)
x
i,j:
n//(i E j)
By:
BackThru
Thm*
n:{1...}, m:
n, E:(
n
n
Prop). (EquivRel x,y:
n. x E y)
(
z:x,y:
m//(x E y). z
x,y:
n//(x E y))
Generated subgoals:
None
About:
nn
nPropn. i E jm. i E jm//(i E j)m//(i E j)
x 
i,j:n//(i E j)
n:{1...}, m:n, E:(nnProp).
(EquivRel x,y:n. x E y) 
(z:x,y:m//(x E y). z x,y:n//(x E y))