PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
mn
23
lem
0
P:(
Prop), n:
. (
k:{n...}. P(k)
(
i:
k. P(i))) & (
m:
. P(m))
(
m:
n. P(m))
By:
UnivCD
THEN
Analyze 3
THEN
Analyze 4
Generated subgoal:
1
1.
P:
Prop
2.
n:
3.
k:{n...}. P(k)
(
i:
k. P(i))
4.
m:
5.
P(m)
m:
n. P(m)
About:
Prop
k:{n...}. P(k) 
(
i:k. P(i))
m:n. P(m) P:(Prop), n:. (k:{n...}. P(k) (i:k. P(i))) & (m:. P(m)) (m:n. P(m))Propk:{n...}. P(k) (i:k. P(i)) m:n. P(m)
