Nuprl - Pf total_back_listify 1 1 2 2

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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 & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)))

TBL:S.car*. (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) ||TBL|| = n & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)))

By: ExRepD THEN ListInd 12 THEN Reduce 0 THEN RepD

Generated subgoals:

1 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. AL: S.car*
13. s:S.car. False (w:Alph*. mem_f(S.car;(S:ws);sL))
14. s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) False
15. s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) False
TBL:S.car*. (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) ||TBL|| = n & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)))

2 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. AL: S.car*
13. u: S.car
14. v: S.car*
15. (s:S.car. mem_f(S.car;s;v) (w:Alph*. mem_f(S.car;(S:ws);sL))) (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;v)) (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;v)) (TBL:S.car*. (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) ||TBL|| = n & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL))))
16. s:S.car. u = s mem_f(S.car;s;v) (w:Alph*. mem_f(S.car;(S:ws);sL))
17. s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) u = s mem_f(S.car;s;v)
18. 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)
TBL:S.car*. (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) ||TBL|| = n & (i:||TBL||, j:i. TBL[i] = TBL[j]) & (s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (AL:S.car*. (s:S.car. mem_f(S.car;s;AL) (w:Alph*. mem_f(S.car;(S:ws);sL))) & (s:S.car. mem_f(S.car;s;sL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. mem_f(S.car;S.act(a,s);TBL) mem_f(S.car;s;TBL) mem_f(S.car;s;AL)))

About: