At: reach lemma 1 2 2 1 1 2 1 2 1 2 1 1 1 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. nn: 
5. f: nn
Alph
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:w
si) = 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' = nil
24. s: S.car
25. w: Alph*
26. u: Alph
27. v: Alph*
28. mem_f(S.car;(S:vsi);RL)
29. i: ||RL||
30. hd(RL) = (S:vsi)
31. i = 0
32. mem_f(S.car;S.act(u,hd(RL));RLa)
33. mem_f(S.car;S.act(u,hd(RL));La')
mem_f(S.car;S.act(u,hd(RL));RL)
By:
RWH (HypC 23) -1
THEN
Reduce -1
Generated subgoals:None
About:
