PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 23 lem 0 1 2 1 1 1

1. P: Prop
2. n:
3. k:{n...}. P(k) (i:k. P(i))
4. m:
5. P(m)
6. m < n

l:(m-0+1). P(l)

By: Witness m

Generated subgoals:

None


About:
existsnatural_numberaddsubtractapply
functionpropallimpliesless_than