Nuprl - Pf back_listify 1 1 2 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)
6. LL: (S.carS.car*)*
7. u1: S.car
8. u2: S.car*
9. v: (S.carS.car*)*
10. BL: S.car*
11. 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:|| < u1,u2 > .v||. 1of(( < u1,u2 > .v)[i]) = t & mem_f(S.car;s;2of(( < u1,u2 > .v)[i])))

By: Inst Thm* s:S, l:S*. Fin(S) Dec(mem_f(S;s;l)) [S.car;s;u2] THEN Analyze -1

Generated subgoals:

1 12. mem_f(S.car;s;u2)
BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:|| < u1,u2 > .v||. 1of(( < u1,u2 > .v)[i]) = t & mem_f(S.car;s;2of(( < u1,u2 > .v)[i])))

2 12. mem_f(S.car;s;u2)
BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:|| < u1,u2 > .v||. 1of(( < u1,u2 > .v)[i]) = t & mem_f(S.car;s;2of(( < u1,u2 > .v)[i])))

About:

1	12. `mem_f(S.car;s;u2)` `BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:\|\| < u1,u2 > .v\|\|. 1of(( < u1,u2 > .v)[i]) = t & mem_f(S.car;s;2of(( < u1,u2 > .v)[i])))`
2	12. `mem_f(S.car;s;u2)` `BL:S.car*. t:S.car. mem_f(S.car;t;BL) (i:\|\| < u1,u2 > .v\|\|. 1of(( < u1,u2 > .v)[i]) = t & mem_f(S.car;s;2of(( < u1,u2 > .v)[i])))`