Behavior would be similar to that of next(...) in JTLV. Implementation should be straightforward, basically an extra parsing step in which primes are pushed into subformulae until they act directly on variables. For instance, one could write
[](x | y | z)'
which would be semantically equivalent to
[](x' | y' | z')
Behavior would be similar to that of next(...) in JTLV. Implementation should be straightforward, basically an extra parsing step in which primes are pushed into subformulae until they act directly on variables. For instance, one could write
[](x | y | z)'
which would be semantically equivalent to
[](x' | y' | z')