PrintForm
Definitions
det
automata
Sections
AutomataTheory
Doc
At:
reach
aux
1
1
1.
Alph:
Type
2.
S:
ActionSet(Alph)
3.
si:
S.car
4.
Fin(S.car)
5.
n:
6.
f:
n
Alph
7.
g:
Alph
n
8.
InvFuns(
n; Alph; f; g)
RL:S.car*.
s:S.car. (
w:Alph*. (S:w
si) = s)
mem_f(S.car;s;RL)
By:
Assert Fin(S.car) THENA NthHyp 4
Generated subgoal:
1
9.
Fin(S.car)
RL:S.car*.
s:S.car. (
w:Alph*. (S:w
si) = s)
mem_f(S.car;s;RL)
About:
RL:S.car*. 
s:S.car. (w:Alph*. (S:w
si) = s) 
mem_f(S.car;s;RL)
n
Alphnn; Alph; f; g) RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL) RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)
