PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
list
quo
choice
2
1
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
6.
x:
q*
7.
y:
q*
(x E y)
Id(x) = Id(y)
q*
By:
Reduce 0
THEN
RWH (LemmaC
Thm*
q:
, x:
q*. q = 0
x = nil) 0
Generated subgoal:
1
(nil E nil)
nil = nil
q*
About:
(nil E nil) 
nil = nil 
q*
0 < qq*
q*Propq*. x E y) & (
x,y:q*. Dec(x E y))q*q* (x E y) Id(x) = Id(y) q*q:, x:q*. q = 0 
x = nil)
0 (nil E nil) nil = nil q*
