PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 23 lem 0 1 2 1 1 2 1

1. P: Prop
2. n:
3. k:{n...}. P(k) (i:k. P(i))
4. m:
5. P(m)
6. m < n
7. i:
8. 0 < i
9. i < m-n+2
10. l: (m-(i-1)+1)
11. P(l)

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

By: Decide (l < m-i+1)

Generated subgoals:

112. l < m-i+1
l:(m-i+1). P(l)
212. l < m-i+1
l:(m-i+1). P(l)


About:
existsnatural_numberaddsubtractapplyless_than
functionpropallimpliesint