At: reach lemma 1 2 1 4
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. 
s:S.car. (
w:Alph*. (S:w
si) = s) 
mem_f(S.car;s;RL)
13. R1: {y:{x:(S.car*)| 0 < ||x|| & ||x||n+1 }| y[(||y||-1)] = si }
14. k:
15. knn
16. RLa: S.car*
17. a: Alph
18. g(a) < k
||R1||
1
By:
Analyze 13
THEN
Analyze 13
THEN
UnhideSqStableHyp 15
Generated subgoals:None
About:
