PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
incl
aux4
quo
2
1.
n:
{1...}
2.
E:
n
n
Prop
3.
EquivRel i,j:
n. i E j
4.
x:
i,j:
n//(i E j)
n-1
i,j:
n//(i E j)
By:
Inst Thm*
T:Type, E:(T
T
Prop), x:T. (EquivRel x,y:T. x E y)
x
x,y:T//(x E y) [
n;E;n-1]
Generated subgoals:
None
About:
n
nPropn. i E jn//(i E j)
n-1 
i,j:n//(i E j)
T:Type, E:(TTProp), x:T. (EquivRel x,y:T. x E y) 
x x,y:T//(x E y) [n;E;n-1]