PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
list
quo
choice
2
1
1
1
1
1
1.
q:
2.
0 < q
3.
E:
q*
q*
Prop
4.
(EquivRel x,y:
q*. x E y) & (
x,y:
q*. Dec(x E y))
5.
q = 0
x,y:
q*. (x E y)
Id(x) = Id(y)
q*
By:
UnivCD
Generated subgoal:
1
6.
x:
q*
7.
y:
q*
(x E y)
Id(x) = Id(y)
q*
About:
q*q*
(x E y) 
Id(x) = Id(y) 
q*
0 < qq*
q*Propq*. x E y) & (
x,y:q*. Dec(x E y)) x,y:q*. (x E y) Id(x) = Id(y) q*q*q* (x E y) Id(x) = Id(y) q*
