In reply to a72:
But the following core assertion should work.
not((st==S1 ##1 st==S2) [*32]))
thanks.