PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: auto3 lang


n:2. n = 0 (l:3*. LangOf(Auto)(l))

By: Inst Thm* Auto:Automata(Alph;St). Fin(Alph) & Fin(St) Dec(l:Alph*. LangOf(Auto)(l)) [3;3;Auto] THENA (Auto THEN BackThru Thm* n:. Fin(n))

Generated subgoal:

11. Dec(l:3*. LangOf(Auto)(l))
n:2. n = 0 (l:3*. LangOf(Auto)(l))


About:
existsnatural_numberequalintlistapply