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:

11. Alph: Type
2. St: Type
3. q: St
[ < q,nil > ] {C:{l:((StAlph*)*)| ||l|| > 0 }| i:(||C||-1). ||2of(C[i])|| > 0 }


About:
alluniversemembersetlistproduct
natural_numbersubtractconspairnil