PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
nd
auto
eq
auto
1
1
2
1
1
1
1
1
2
1
1.
Alph:
Type
2.
St:
Type
3.
NDA:
NDA(Alph;St)
4.
Fin(St)
5.
x,y:St, a:Alph. Dec(
NDA(x,a,y))
6.
y:St. Dec(I(NDA) = y)
7.
g:
St
8.
t:St. I(NDA) = t
g(t)
9.
f:(St
). Dec(
s:St. f(s) & F(NDA)(s))
t:(St
). Dec((
f.
s:St. f(s) & F(NDA)(s))(t))
By:
Reduce 0
Generated subgoals:
None
About:
x,y:St, a:Alph. Dec(
NDA(x,a,y))y:St. Dec(I(NDA) = y)
t:St. I(NDA) = t 
g(t)f:(St). Dec(
s:St. f(s) & F(NDA)(s))
t:(St). Dec((
f.s:St. f(s) & F(NDA)(s))(t))
