At: reach lemma 1 1 2 2 2 1 1 2 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. g o f = Id
9. f o g = Id
10. k: 
11. 0 < k
12. k
nn
13. RLa: S.car*
14. 
i:{1..1
}, a:Alph. si = S.act(a,[si][i]) 
False mem_f(S.car;S.act(a,[si][i]);RLa)
15. a:Alph. g(a) < k-1 
si = S.act(a,si) False mem_f(S.car;S.act(a,si);RLa)
16. s:S.car. mem_f(S.car;s;RLa) (
w:Alph*. (S:w
si) = s)
17. a: Alph
18. g(a) < k
19. 
g(a) < k-1
20. g(a) = k-1 
nn
(f o g)(a) = a
By:
RWH (HypC 9) 0
THEN
Reduce 0
Generated subgoals:None
About:
