PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: total back listify 1 1 2 2 2 2 3 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. BL: S.car*
19. t:S.car. mem_f(S.car;t;BL) (a:Alph. S.act(a,t) = u)

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) u = s mem_f(S.car;s;TBL) mem_f(S.car;s;AL)) & (s:S.car, a:Alph. u = S.act(a,s) mem_f(S.car;S.act(a,s);TBL) u = s mem_f(S.car;s;TBL) mem_f(S.car;s;AL))
By:
InstConcl [BL @ v]
THEN
RWH (LemmaC Thm* L1,L2:T*, t:T. mem_f(T;t;L1 @ L2) mem_f(T;t;L1) mem_f(T;t;L2)) 0
THEN
GenExRepD
Generated subgoals:

120. s: S.car
21. mem_f(S.car;s;BL)
w:Alph*. mem_f(S.car;(S:ws);sL)
220. s: S.car
21. mem_f(S.car;s;v)
w:Alph*. mem_f(S.car;(S:ws);sL)
320. s: S.car
21. mem_f(S.car;s;sL)
u = s mem_f(S.car;s;TBL) mem_f(S.car;s;BL) mem_f(S.car;s;v)
420. s: S.car
21. a: Alph
22. u = S.act(a,s)
u = s mem_f(S.car;s;TBL) mem_f(S.car;s;BL) mem_f(S.car;s;v)
520. s: S.car
21. a: Alph
22. mem_f(S.car;S.act(a,s);TBL)
u = s mem_f(S.car;s;TBL) mem_f(S.car;s;BL) mem_f(S.car;s;v)

About:
existslistandallimpliesorequal
applyuniverseintless_thannatural_numbersubtract