Nuprl - Pf total_back_listify 1 2 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. n:
6. f: nS.car
7. g: S.carn
8. InvFuns(n; S.car; f; g)
9. n:. 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)))
10. n = 0
11. TBL: S.car*
12. ||TBL|| = n+1
13. i:||TBL||, j:i. TBL[i] = TBL[j]
14. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))
15. AL: S.car*
16. s:S.car. mem_f(S.car;s;AL) (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) mem_f(S.car;s;AL)
18. 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))

By: Inst Thm* n:{1...}, f:((n+1)n). i:(n+1), j:i. f(i) = f(j) [n;x.g(TBL[x])] THEN ExRepD THEN Reduce -1

Generated subgoal:

1 19. i: (n+1)
20. j: i
21. g(TBL[i]) = g(TBL[j])
TBL:S.car*. s:S.car. mem_f(S.car;s;TBL) (w:Alph*. mem_f(S.car;(S:ws);sL))

About: