2. Alph: Type
3. S: ActionSet(Alph)
4. s: S.car
5. f: S.car
6. #(S.car)=n
7.
l:Alph*. (S:l
s) = f
l:Alph*. ||l||
n & (S:ls) = f 
n:, Alph:Type, S:ActionSet(Alph), s,f:S.car.
#(S.car)=n 
(l:Alph*. (S:ls) = f) (l:Alph*. ||l||n & (S:ls) = f)| 1 | 1. n: 2. Alph: Type 3. S: ActionSet(Alph) 4. s: S.car 5. f: S.car 6. #(S.car)=n 7. l:Alph*. (S:ls) = f l:Alph*. ||l||n & (S:ls) = f |
About:
 |  |  |  |  |  |  |