Nuprl - Pf auto

PrintForm Definitions automata 7 Sections AutomataTheory Doc

1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. l: Alph*

(Result(Auto)l) = (Action(Auto):lInitialState(Auto))

By: ListInd 4 THEN RecUnfold `compute_list` 0 THEN RecUnfold `maction` 0 THEN Reduce 0

Generated subgoals:

1 InitialState(Auto) = InitialState(Auto)

2 5. u: Alph
6. v: Alph*
7. (Result(Auto)v) = (Action(Auto):vInitialState(Auto))
Auto((Result(Auto)v),u) = Auto((Action(Auto):vInitialState(Auto)),u)

About:

1	`InitialState(Auto) = InitialState(Auto)`
2	5. `u:` `Alph` 6. `v:` `Alph*` 7. `(Result(Auto)v) = (Action(Auto):vInitialState(Auto))` `Auto((Result(Auto)v),u) = Auto((Action(Auto):vInitialState(Auto)),u)`