PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
fin
alph
list
quo
1
1
1
1
1.
Alph:
Type
2.
E:
Alph*
Alph*
Prop
3.
n:
4.
n ~ Alph
5.
EquivRel x,y:Alph*. x E y
6.
x,y:Alph*. Dec(x E y)
h:(Alph*
Alph*). (
x,y:Alph*. (x E y)
h(x) = h(y)) & (
x:Alph*. x E (h(x)))
By:
Analyze 4
THEN
Analyze 5
Generated subgoal:
1
4.
f:
n
Alph
5.
g:
Alph
n
6.
InvFuns(
n; Alph; f; g)
7.
EquivRel x,y:Alph*. x E y
8.
x,y:Alph*. Dec(x E y)
h:(Alph*
Alph*). (
x,y:Alph*. (x E y)
h(x) = h(y)) & (
x:Alph*. x E (h(x)))
About: