I'm wondering if you could as part of the O operator list all the variables in consideration for the "next"-state asar as that operator is concerned.
like O[a,b,c]X in the next state which is determined by a change to any of a, b, or c, then X will be true. In the case where the set of variables is all of them they can be omitted and thus get the existing behaviour.
I also suspect that the O operator with with a subset of variables will behave identically to other instances with the same set.
However, I feel like this will still hit walls before practical limits, Beth would just need a non-trivial example
like O[a,b,c]X in the next state which is determined by a change to any of a, b, or c, then X will be true. In the case where the set of variables is all of them they can be omitted and thus get the existing behaviour.
I also suspect that the O operator with with a subset of variables will behave identically to other instances with the same set.
However, I feel like this will still hit walls before practical limits, Beth would just need a non-trivial example