Go backward to Additional Notation Go up to Top Go forward to The Basic Rules of TLA |
F provable by propositional logic |
always F |
|- always F => F |
|- always always F <=> always F |
F => G |
always F => always G |
|- always (F and G) <=> (always F) and (always G) |
|- (eventually always F) and (eventually always G) <=> eventually always (F and G) |
| ||
F => ((exists c in S: Hc) |-> G) |