Nuprl - Pf reach_lemma 1 2 2 1 1 1 1 1

PrintForm Definitions det automata Sections AutomataTheory Doc

1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. nn:
5. f: nnAlph
6. g: Alphnn
7. Fin(S.car)
8. InvFuns(nn; Alph; f; g)
9. n:
10. 0 < n
11. RL: S.car*
12. 0 < ||RL||
13. ||RL||n-1+1
14. RL[(||RL||-1)] = si
15. ||RL|| = n-1+1
16. i:||RL||, j:i. RL[i] = RL[j]
17. s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s)
18. k:. knn (RLa:S.car*. (i:{1..||RL||}, a:Alph. mem_f(S.car;S.act(a,RL[i]);RL) mem_f(S.car;S.act(a,RL[i]);RLa)) & (a:Alph. g(a) < k mem_f(S.car;S.act(a,hd(RL));RL) mem_f(S.car;S.act(a,hd(RL));RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)))
19. RLa: S.car*
20. i:{1..||RL||}, a:Alph. mem_f(S.car;S.act(a,RL[i]);RL) mem_f(S.car;S.act(a,RL[i]);RLa)
21. a:Alph. g(a) < nn mem_f(S.car;S.act(a,hd(RL));RL) mem_f(S.car;S.act(a,hd(RL));RLa)
22. s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)
23. La': S.car*
24. t:S.car. mem_f(S.car;t;RLa) mem_f(S.car;t;RL) mem_f(S.car;t;La')
25. t:S.car. mem_f(S.car;t;La') mem_f(S.car;t;RLa)
26. ||La'||1 mem_f(S.car;hd(La');RL)
27. ||La'||1

(hd(La').RL)[(||RL||+1-1)] = si

By: ArithSimp 14 THEN Unfold `select` 0 THEN RecUnfold `nth_tl` 0 THEN Reduce 0

Generated subgoal:

1 14. RL[(-1+||RL||)] = si
15. ||RL|| = n-1+1
16. i:||RL||, j:i. RL[i] = RL[j]
17. s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s)
18. k:. knn (RLa:S.car*. (i:{1..||RL||}, a:Alph. mem_f(S.car;S.act(a,RL[i]);RL) mem_f(S.car;S.act(a,RL[i]);RLa)) & (a:Alph. g(a) < k mem_f(S.car;S.act(a,hd(RL));RL) mem_f(S.car;S.act(a,hd(RL));RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)))
19. RLa: S.car*
20. i:{1..||RL||}, a:Alph. mem_f(S.car;S.act(a,RL[i]);RL) mem_f(S.car;S.act(a,RL[i]);RLa)
21. a:Alph. g(a) < nn mem_f(S.car;S.act(a,hd(RL));RL) mem_f(S.car;S.act(a,hd(RL));RLa)
22. s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)
23. La': S.car*
24. t:S.car. mem_f(S.car;t;RLa) mem_f(S.car;t;RL) mem_f(S.car;t;La')
25. t:S.car. mem_f(S.car;t;La') mem_f(S.car;t;RLa)
26. ||La'||1 mem_f(S.car;hd(La');RL)
27. ||La'||1
hd(if ||RL||+1-10 hd(La').RL else nth_tl(||RL||+1-1-1;RL) fi) = si

About: