PrintForm
Definitions
automata
5
Sections
AutomataTheory
Doc
At:
fin
alph
list
quo
1
1
1
1
1
3
1
1
1
1
1
1.
Alph:
Type
2.
E:
Alph*
Alph*
Prop
3.
n:
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)
9.
h:
n*
n*
10.
x,y:
n*. (map(f;x) E map(f;y))
h(x) = h(y)
11.
x:
n*. map(f;x) E map(f;h(x))
x,y:Alph*. (x E y)
map(f;h(map(g;x))) = map(f;h(map(g;y)))
By:
UnivCD
THEN
InstHyp [map(g;x);map(g;y)] 10
Generated subgoal:
1
12.
x:
Alph*
13.
y:
Alph*
14.
(map(f;map(g;x)) E map(f;map(g;y)))
h(map(g;x)) = h(map(g;y))
(x E y)
map(f;h(map(g;x))) = map(f;h(map(g;y)))
About: