Nuprl - Pf total_back_listify 1 1 2 2 2 2 1 2 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: total back listify 1 1 2 2 2 2 1 2 1

1. Alph: Type
2. S: ActionSet(Alph)
3. sL: S.car*
4. Fin(Alph)
5. Fin(S.car)
6. n:
7. 0 < n
8. TBL: S.car*
9. ||TBL|| = n-1
10. i:||TBL||, j:i. TBL[i] = TBL[j]
11. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))
12. u: S.car
13. v: S.car*
14. s:S.car. u = s mem_f(S.car;s;v) (w:Alph*. mem_f(S.car;(S:ws);sL))
15. s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) u = s mem_f(S.car;s;v)
16. s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) u = s mem_f(S.car;s;v)
17. mem_f(S.car;u;TBL)
18. i: (||TBL||+1)
19. j: i
20. j = 0
21. 0 < i

hd(nth_tl(i-1;TBL)) = hd(nth_tl(j;u.TBL))

By: RWH (AddrC [2] (FoldC `select`)) 0 THEN RecCaseSplit `nth_tl`

Generated subgoal:

1 22. 0 < j
TBL[(i-1)] = hd(nth_tl(j-1;TBL))

About: