Nuprl - Pf action

PrintForm Definitions det automata Sections AutomataTheory Doc

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

( < St,l,s. Auto(s,l) > :lInitialState(Auto)) = (Result(Auto)l)

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

Generated subgoals:

1 InitialState(Auto) = InitialState(Auto)

2 5. u: Alph
6. v: Alph*
7. ( < St,l,s. Auto(s,l) > :vInitialState(Auto)) = (Result(Auto)v)
Auto(( < St,l,s. Auto(s,l) > :vInitialState(Auto)),u) = Auto((Result(Auto)v),u)

About:

1	`InitialState(Auto) = InitialState(Auto)`
2	5. `u:` `Alph` 6. `v:` `Alph*` 7. `( < St,l,s. Auto(s,l) > :vInitialState(Auto)) = (Result(Auto)v)` `Auto(( < St,l,s. Auto(s,l) > :vInitialState(Auto)),u) = Auto((Result(Auto)v),u)`