Nuprl - Pf empty_lang_dec 1 1 1 1 1 1 1 1 1 1 4 1 1 1

PrintForm Definitions automata 7 Sections AutomataTheory Doc

At: empty lang dec 1 1 1 1 1 1 1 1 1 1 4 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)
7. l: Alph*
8. FinalState(Auto)((Action(Auto):lInitialState(Auto)))
9. l@0: Alph*
10. ||l@0||n & (Action(Auto):l@0InitialState(Auto)) = (Action(Auto):lInitialState(Auto))

FinalState(Auto)((Action(Auto):l@0InitialState(Auto)))

By: Analyze 10

Generated subgoal:

1 10. ||l@0||n
11. (Action(Auto):l@0InitialState(Auto)) = (Action(Auto):lInitialState(Auto))
FinalState(Auto)((Action(Auto):l@0InitialState(Auto)))

About: