PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
nd
auto
eq
auto
1
1
2
1
1
1
1
1
2
2
1
1
1
1
2
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))
10.
g1:
(St
)
11.
t:(St
). (
s:St. t(s) & F(NDA)(s))
g1(t)
12.
f:
St
13.
a:
Alph
14.
y:
St
15.
Dec(
t:St. (
s.f(s) &
NDA(s,a,y))(t))
Dec(
s:St. f(s) &
NDA(s,a,y))
By:
Reduce 15
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). (s:St. t(s) & F(NDA)(s)) g1(t)t:St. (
s.f(s) & NDA(s,a,y))(t))
Dec(s:St. f(s) & NDA(s,a,y))
