PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: total back listify 1 1 2 2 1 2 1 2
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. 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
16. s: S.car
17. w: Alph*
18. mem_f(S.car;(S:ws);sL)
19. i:
20. 0 < i
21. i-1||w|| mem_f(S.car;(S:nth_tl(i-1;w)s);TBL)
22. i||w||

mem_f(S.car;(S:nth_tl(i;w)s);TBL)
By:
Analyze -2
THEN
RecUnfold `maction` -1
THEN
MoveToConcl -1
THEN
SplitOnConclITE
THEN
Analyze 0
Generated subgoals:

121. i||w||
22. nth_tl(i-1;w) = nil
23. mem_f(S.car;s;TBL)
mem_f(S.car;(S:nth_tl(i;w)s);TBL)
221. i||w||
22. nth_tl(i-1;w) = nil
23. mem_f(S.car;S.act(hd(nth_tl(i-1;w)),(S:tl(nth_tl(i-1;w))s));TBL)
mem_f(S.car;(S:nth_tl(i;w)s);TBL)

About:
universelistintless_thannatural_numberequalsubtract
allimpliesexistsfalseorapply