PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd comp init wf 1 2

1. Alph: Type
2. St: Type
3. q: St

i:(||[ < q,nil > ]||-1). ||2of([ < q,nil > ][i])|| > 0

By: Assert (||[ < q,nil > ]|| )

Generated subgoals:

1 ||[ < q,nil > ]||
24. ||[ < q,nil > ]||
i:(||[ < q,nil > ]||-1). ||2of([ < q,nil > ][i])|| > 0


About:
allnatural_numbersubtractconspair
nilmemberintuniverse