2. S: ActionSet(Alph)
3. N:
4. s: S.car
5. #(S.car)=N
6. A: Alph*
7. N < ||A||
a,b,c:Alph*. 0 < ||b|| & A = ((a @ b) @ c) & (
k:. (S:(a @ (b
k)) @ c
s) = (S:As)) Alph:Type, S:ActionSet(Alph), N:, s:S.car.
#(S.car)=N 
(A:Alph*.
N < ||A|| (a,b,c:Alph*. 0 < ||b|| & A = ((a @ b) @ c) & (k:. (S:(a @ (bk)) @ cs) = (S:As))))| 1 | 1. Alph: Type 2. S: ActionSet(Alph) 3. N: 4. s: S.car 5. #(S.car)=N 6. A: Alph* 7. N < ||A|| a,b,c:Alph*. 0 < ||b|| & A = ((a @ b) @ c) & (k:. (S:(a @ (bk)) @ cs) = (S:As)) |
About:
 |  |  |  |  |
 |  |  |  |