Nuprl - Pf reach_lemma 1 2 2 1 1 1 2 3 2 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: {y:{x:(S.car*)| 0 < ||x|| & ||x||n-1+1 }| y[(||y||-1)] = si }
12. ||RL|| = n-1+1
13. i:||RL||, j:i. RL[i] = RL[j]
14. s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s)
15. 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)))
16. RLa: S.car*
17. 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)
18. 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)
19. s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)
20. La': S.car*
21. t:S.car. mem_f(S.car;t;RLa) mem_f(S.car;t;RL) mem_f(S.car;t;La')
22. t:S.car. mem_f(S.car;t;La') mem_f(S.car;t;RLa)
23. ||La'||1 mem_f(S.car;hd(La');RL)
24. ||La'||1
25. k:
26. 0 < k
27. knn
28. R1: S.car*
29. i:{1..(||RL||+1)}, a:Alph. hd(La') = S.act(a,(hd(La').RL)[i]) mem_f(S.car;S.act(a,(hd(La').RL)[i]);RL) mem_f(S.car;S.act(a,(hd(La').RL)[i]);R1)
30. a:Alph. g(a) < k-1 hd(La') = S.act(a,hd(La')) mem_f(S.car;S.act(a,hd(La'));RL) mem_f(S.car;S.act(a,hd(La'));R1)
31. s:S.car. mem_f(S.car;s;R1) (w:Alph*. (S:wsi) = s)

RLa:S.car*. (i:{1..(||RL||+1)}, a:Alph. hd(La') = S.act(a,(hd(La').RL)[i]) mem_f(S.car;S.act(a,(hd(La').RL)[i]);RL) mem_f(S.car;S.act(a,(hd(La').RL)[i]);RLa)) & (a:Alph. g(a) < k hd(La') = S.act(a,hd(La')) mem_f(S.car;S.act(a,hd(La'));RL) mem_f(S.car;S.act(a,hd(La'));RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s))

By: InstConcl [S.act(f(k-1),hd(La')).R1] THEN Reduce 0

Generated subgoals:

1 32. i: {1..(||RL||+1)}
33. a: Alph
hd(La') = S.act(a,(hd(La').RL)[i]) mem_f(S.car;S.act(a,(hd(La').RL)[i]);RL) S.act(f(k-1),hd(La')) = S.act(a,(hd(La').RL)[i]) mem_f(S.car;S.act(a,(hd(La').RL)[i]);R1)

2 32. a: Alph
33. g(a) < k
hd(La') = S.act(a,hd(La')) mem_f(S.car;S.act(a,hd(La'));RL) S.act(f(k-1),hd(La')) = S.act(a,hd(La')) mem_f(S.car;S.act(a,hd(La'));R1)

3 32. s: S.car
33. S.act(f(k-1),hd(La')) = s mem_f(S.car;s;R1)
w:Alph*. (S:wsi) = s

About:

1	32. `i:` `{1..(\|\|RL\|\|+1)}` 33. `a:` `Alph` `hd(La') = S.act(a,(hd(La').RL)[i]) mem_f(S.car;S.act(a,(hd(La').RL)[i]);RL) S.act(f(k-1),hd(La')) = S.act(a,(hd(La').RL)[i]) mem_f(S.car;S.act(a,(hd(La').RL)[i]);R1)`
2	32. `a:` `Alph` 33. `g(a) < k` `hd(La') = S.act(a,hd(La')) mem_f(S.car;S.act(a,hd(La'));RL) S.act(f(k-1),hd(La')) = S.act(a,hd(La')) mem_f(S.car;S.act(a,hd(La'));R1)`
3	32. `s:` `S.car` 33. `S.act(f(k-1),hd(La')) = s mem_f(S.car;s;R1)` `w:Alph*. (S:wsi) = s`