PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
quotient
of
nsubn
1
1
1
1
2
1
2
1
1.
E:
1
1
Prop
2.
EquivRel x,y:
1. x E y
3.
x,y:
1. Dec(x E y)
4.
0
i,j:
1//(i E j)
5.
x:
i,j:
1//(i E j)
0 = x
By:
Analyze 5
THEN
Analyze
Generated subgoal:
1
5.
x1:
1
6.
x2:
1
7.
x1 E x2
0 E x2
About:
11
0 E x21
1Prop1. x E y
x,y:1. Dec(x E y)
i,j:1//(i E j)1//(i E j) 0 = x11 0 E x2
