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

PrintForm Definitions automata 7 Sections AutomataTheory Doc

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)))

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

By: Inst Thm* n:, Alph:Type, S:ActionSet(Alph), s,f:S.car. #(S.car)=n (l:Alph*. (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f) [n;Alph;Action(Auto);InitialState(Auto);(Action(Auto):lInitialState(Auto))]

Generated subgoals:

1 0 < n

2 #(Action(Auto).car)=n

3 l@0:Alph*. (Action(Auto):l@0InitialState(Auto)) = (Action(Auto):lInitialState(Auto))

4 9. l@0:Alph*. ||l@0||n & (Action(Auto):l@0InitialState(Auto)) = (Action(Auto):lInitialState(Auto))
k:(n+1), l:{l:(Alph*)| ||l|| = k }. FinalState(Auto)((Action(Auto):lInitialState(Auto)))

About:

1	`0 < n`
2	`#(Action(Auto).car)=n`
3	`l@0:Alph*. (Action(Auto):l@0InitialState(Auto)) = (Action(Auto):lInitialState(Auto))`
4	9. `l@0:Alph. \|\|l@0\|\|n & (Action(Auto):l@0InitialState(Auto)) = (Action(Auto):lInitialState(Auto))` `k:(n+1), l:{l:(Alph)\| \|\|l\|\| = k }. FinalState(Auto)((Action(Auto):lInitialState(Auto)))`