PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd comp init wf 1 2 2

1. Alph: Type
2. St: Type
3. q: St
4. ||[ < q,nil > ]||

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

By: Analyze 0

Generated subgoal:

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


About:
allnatural_numbersubtractconspair
niluniversememberint