Nuprl - Pf mn_12 1 2 2 1 2 1 2 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. Alph: Type
2. L: LangOver(Alph)
3. Fin(Alph)
4. St: Type
5. Auto: Automata(Alph;St)
6. Fin(St)
7. L = LangOf(Auto)
8. EquivRel x,y:Alph*. (Result(Auto)x) = (Result(Auto)y)

Fin(x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)))

By: Inst Thm* f:(TS). Fin(S) & (s:S. Dec(t:T. f(t) = s)) Fin(x,y:T//(f(x) = f(y))) [Alph*;St;t.Result(Auto)t]

Generated subgoals:

1 Fin(St) & (s:St. Dec(t:Alph*. (t.Result(Auto)t)(t) = s))

2 9. Fin(x,y:Alph*//((t.Result(Auto)t)(x) = (t.Result(Auto)t)(y) St))
Fin(x,y:Alph*//((Result(Auto)x) = (Result(Auto)y)))

About:

1	`Fin(St) & (s:St. Dec(t:Alph*. (t.Result(Auto)t)(t) = s))`
2	9. `Fin(x,y:Alph//((t.Result(Auto)t)(x) = (t.Result(Auto)t)(y) St))` `Fin(x,y:Alph//((Result(Auto)x) = (Result(Auto)y)))`