Nuprl - Pf back_listify 1 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. Fin(Alph)
5. Fin(S.car)

LL:(S.carS.car*)*. BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:||LL||. 1of(LL[i]) = t & mem_f(S.car;s;2of(LL[i])))

By: Analyze 0 THEN ListInd -1

Generated subgoals:

1 6. LL: (S.carS.car*)*
BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:||nil||. 1of(nil[i]) = t & mem_f(S.car;s;2of(nil[i])))

2 6. LL: (S.carS.car*)*
7. u: S.carS.car*
8. v: (S.carS.car*)*
9. BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:||v||. 1of(v[i]) = t & mem_f(S.car;s;2of(v[i])))
BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:||u.v||. 1of((u.v)[i]) = t & mem_f(S.car;s;2of((u.v)[i])))

About:

1	6. `LL:` `(S.carS.car)` `BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:\|\|nil\|\|. 1of(nil[i]) = t & mem_f(S.car;s;2of(nil[i])))`
2	6. `LL:` `(S.carS.car)` 7. `u:` `S.carS.car` 8. `v:` `(S.carS.car)` 9. `BL:S.car. t:S.car. mem_f(S.car;t;BL) (i:\|\|v\|\|. 1of(v[i]) = t & mem_f(S.car;s;2of(v[i])))` `BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:\|\|u.v\|\|. 1of((u.v)[i]) = t & mem_f(S.car;s;2of((u.v)[i])))`