Nuprl - Pf lang_auto_compute 1 1 2 1

PrintForm Definitions automata 4 Sections AutomataTheory Doc

1. Alph: Type
2. L: LangOver(Alph)
3. EquivRel x,y:Alph*. x L-induced Equiv y
4. L Alph*Prop
5. g: (x,y:Alph*//(x L-induced Equiv y))
6. l: Alph*

(Result(A(g))l) = l x,y:Alph*//(x L-induced Equiv y)

By: ListInd 6

Generated subgoals:

1 (Result(A(g))nil) = nil

2 7. u: Alph
8. v: Alph*
9. (Result(A(g))v) = v x,y:Alph*//(x L-induced Equiv y)
(Result(A(g))u.v) = u.v x,y:Alph*//(x L-induced Equiv y)

About:

1	`(Result(A(g))nil) = nil`
2	7. `u:` `Alph` 8. `v:` `Alph` 9. `(Result(A(g))v) = v x,y:Alph//(x L-induced Equiv y)` `(Result(A(g))u.v) = u.v x,y:Alph*//(x L-induced Equiv y)`