Hello,
1. It is mentioned in section 8.9.4 of Specifying Systems that substitution does not distribute over ENABLED, and hence it does not distribute over WF or SF. Could someone give an example where it is indeed the case?
I believe this is covered in A science of concurrent programming (https://lamport.azurewebsites.net/tla/science.pdf) under section 5.4.4 (A Closer Look at E).
2. It is recommended in the same section that "you don't have to depend on this. You can instead expand the definitions of WF and SF [..] (and) compute the enabled predicates "by hand" and then perform the substitution." Are there conditions under which one could be sure that substitution distributes over entire specification formula so that there is no need to prove it "by hands"?
Thank you,
Dmitry