search

tlaplus / tlapm

The TLA Proof Manager
https://proofs.tlapl.us/
BSD 2-Clause "Simplified" License
65 stars 20 forks source link

ENABLED is not coalesced #75

Open muenchnerkindl opened 1 year ago

muenchnerkindl commented 1 year ago

The PTL backend easily proves

   THEOREM []([]F => <>G) <=> (<>[]F => []<>G)

but not

 THEOREM []([](ENABLED <<A>>_v) => <><<A>>_v) <=> ([]<>(ENABLED <<A>>_v) => []<><<A>>_v)

This appears to indicate that ENABLED formulas are not coalesced as they should be. (Issue reported by Leslie Lamport.)