PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd auto eq auto 1 1 2 1 1 1 1 1 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)
7. g: St
8. t:St. I(NDA) = t g(t)
9. f: St

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

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

About:
existsandassertapplylambda
universeallequalfunctionbool