At: reach lemma 1 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. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||
0+1 }| y[(||y||-1)] = si }
10. k:
11. knn
12. RLa: S.car*
13. a: Alph
14. g(a) < k
||RL||
1
By:
Analyze 9
THEN
Analyze 9
THEN
UnhideSqStableHyp 11
Generated subgoals:None
About:
