Hi Alexandre,
I've now worked out the proofs for the ## operator - there were a few (nice)
surprises. To summarise, ##[i:j] is SI if both operands are SI, j is in {0,1,$}, and
either:
* i=0, or
* i=1 and a is prefix-closed OR b is suffix-closed, or
* i=2 and a is prefix-closed AND b is suffix-closed.
Note that ##[0:1] does not need prefix/suffix-closedness as K:L catches some of the
un-stuttered words from K;L, and similarly for ##[0:$]. These operators mix fusion with
concatenation in a confusing way. Similarly, ##[2:$] was somewhat unexpected but nice :-)
- I had expected only 0,1,$ to be allowed.
Concerning the |=>, I hope we can lift the prefix/suffix-closedness idea to
omega-languages and handle it. I also hope this will handle some cases of X, which would
be really nice. E.g.: {a[+]} |=> Fx is si, and for the same reason {a[+]}|->XFx is
si.
Regards,
Victor.