PrintForm
Definitions
relation
autom
Sections
AutomataTheory
Doc
At:
quotient
of
nsubn
1
1
1
1
1
1.
E:
1
1
Prop
2.
EquivRel x,y:
1. x E y
3.
x,y:
1. Dec(x E y)
0
i,j:
1//(i E j)
By:
Assert (0
1)
Generated subgoal:
1
4.
0
1
0
i,j:
1//(i E j)
About:
1
0 i,j:1//(i E j)1
1Prop1. x E y
x,y:1. Dec(x E y) 0 i,j:1//(i E j) 1) 1 0 i,j:1//(i E j)
