PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
incl
aux2
quo
1
1
1.
n:
{1...}
2.
m:
n
3.
E:
n
n
Prop
4.
EquivRel x,y:
n. x E y
5.
z:
x,y:
m//(x E y)
z = z
x,y:
n//(x E y)
By:
Analyze 5
Generated subgoal:
1
5.
z1:
m
6.
z2:
m
7.
z1 E z2
z1 = z2
x,y:
n//(x E y)
About:
mm
z1 = z2 
x,y:n//(x E y)nn
nPropn. x E ym//(x E y) z = z x,y:n//(x E y)mm z1 = z2 x,y:n//(x E y)
