PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd auto eq auto 1 1 2 1 1
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)

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;y.I(NDA) = y] THENA Reduce 0
Generated subgoal:

17. g:(St). t:St. (y.I(NDA) = y)(t) g(t)
DA:Automata(Alph;St). L(NDA) = LangOf(DA)

About:
existsfunctionboollambdaequaluniverseallapply