Nuprl - Pf nd_auto_eq_auto 1 1 2 1 1 1 1 1 2

PrintForm Definitions nfa 1 Sections AutomataTheory Doc

1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. Fin(St)
5. x,y:St, a:Alph. Dec(NDA(x,a,y))
6. y:St. Dec(I(NDA) = y)
7. g: St
8. t:St. I(NDA) = t g(t)
9. f:(St). Dec(s:St. f(s) & F(NDA)(s))

DA:Automata(Alph;St). L(NDA) = LangOf(DA)

By: Inst Thm* f:(TProp). (t:T. Dec(f(t))) (g:(T). t:T. f(t) g(t)) [St;f.s:St. f(s) & F(NDA)(s)]

Generated subgoals:

1 t:(St). Dec((f.s:St. f(s) & F(NDA)(s))(t))

2 10. g:((St)). t:(St). (f.s:St. f(s) & F(NDA)(s))(t) g(t)
DA:Automata(Alph;St). L(NDA) = LangOf(DA)

About:

1	`t:(St). Dec((f.s:St. f(s) & F(NDA)(s))(t))`
2	10. `g:((St)). t:(St). (f.s:St. f(s) & F(NDA)(s))(t) g(t)` `DA:Automata(Alph;St). L(NDA) = LangOf(DA)`