PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: empty lang dec 1 1 1 1 1 1 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. n:
6. f:(nSt). Bij(n; St; f)

(l:Alph*. FinalState(Auto)(Result(Auto)l)) (k:(n+1), l:{l:(Alph*)| ||l|| = k }. FinalState(Auto)(Result(Auto)l))
By: RWH (LemmaC Thm* Auto:Automata(Alph;St), l:Alph*. (Result(Auto)l) = (Action(Auto):lInitialState(Auto))) 0
Generated subgoal:

1 (l:Alph*. FinalState(Auto)((Action(Auto):lInitialState(Auto)))) (k:(n+1), l:{l:(Alph*)| ||l|| = k }. FinalState(Auto)((Action(Auto):lInitialState(Auto))))

About:
impliesexistslistassertapplynatural_numberadd
setequalintuniverseallfunction