PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
nd
comp
extend
wf
1
2
1
2
1
1
2
1.
Alph:
Type
2.
St:
Type
3.
C:
{C:{l:((St
Alph*)*)| ||l|| > 0 }|
i:
(||C||-1). ||2of(C[i])|| > 0 }
4.
a:
Alph
5.
q:
St
6.
i:
7.
0
i < ||map(
c. < 1of(c),a.2of(c) > ;C)||+1-1
||2of((
c. < 1of(c),a.2of(c) > )(C[i]))|| > 0
By:
Reduce 0
Generated subgoal:
1
||2of(C[i])||+1 > 0
About:
||2of(C[i])||+1 > 0
Alph*)*)| ||l|| > 0 }| 
i:
(||C||-1). ||2of(C[i])|| > 0 }
i < ||map(
c. < 1of(c),a.2of(c) > ;C)||+1-1 ||2of((c. < 1of(c),a.2of(c) > )(C[i]))|| > 0 ||2of(C[i])||+1 > 0
