PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
nd
comp
init
wf
Alph,St:Type, q:St. [ < q,[] > ]
NComp(Alph;St)
By:
Unfold `nd_comp_init` 0
THEN
Unfold `nd_computation` 0
THEN
Unfold `list_p` 0
Generated subgoal:
1
1.
Alph:
Type
2.
St:
Type
3.
q:
St
[ < q,nil > ]
{C:{l:((St
Alph*)*)| ||l|| > 0 }|
i:
(||C||-1). ||2of(C[i])|| > 0 }
About: