PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
nd
ext
valcom
1
1
1
1
1
1.
Alph:
Type
2.
St:
Type
3.
NDA:
NDA(Alph;St)
4.
C:
(St
Alph*)*
5.
||C|| > 0
6.
i:
(||C||-1). ||2of(C[i])|| > 0
7.
q:
St
8.
a:
Alph
9.
p:
St
10.
NDA(C)
q
11.
NDA(q,a,p)
I(NDA) = 1of(hd(map(
c. < 1of(c),a.2of(c) > ;C)))
By:
RWH (LemmaC
Thm*
l:T*. ||l|| > 0
hd(l) = l[0]) 0
Generated subgoal:
1
I(NDA) = 1of(map(
c. < 1of(c),a.2of(c) > ;C)[0])
About:
I(NDA) = 1of(map(
c. < 1of(c),a.2of(c) > ;C)[0])
Alph*)*
i:
(||C||-1). ||2of(C[i])|| > 0 q
NDA(q,a,p) I(NDA) = 1of(hd(map(c. < 1of(c),a.2of(c) > ;C)))l:T*. ||l|| > 0 
hd(l) = l[0])
0 I(NDA) = 1of(map(c. < 1of(c),a.2of(c) > ;C)[0])
