Nuprl - Pf back_listify 1 1 2 1 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])))
12. mem_f(S.car;s;u2)
13. t: S.car
14. mem_f(S.car;t;BL)
15. i: ||v||
16. 1of(v[i]) = t
17. mem_f(S.car;s;2of(v[i]))

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

By: InstConcl [i+1] THEN Unfold `select` 0 THEN RecUnfold `nth_tl` 0 THEN SplitOnConclITE THEN Reduce 0

Generated subgoals:

1 18. 0 < i+1
1of(hd(nth_tl(i+1-1;v))) = t

2 18. 0 < i+1
mem_f(S.car;s;2of(hd(nth_tl(i+1-1;v))))

About:

1	18. `0 < i+1` `1of(hd(nth_tl(i+1-1;v))) = t`
2	18. `0 < i+1` `mem_f(S.car;s;2of(hd(nth_tl(i+1-1;v))))`