Go backward to Additional Notation Go up to Top Go forward to The Basic Rules of TLA

The Rules of Simple Temporal Logic

• STL1.

  F provable by propositional logic

  always F

• STL2.

  |- always F => F

• STL3.

  |- always always F <=> always F

• STL4.

  F => G

  always F => always G

• STL5.

  |- always (F and G) <=> (always F) and (always G)

• STL6.

  |- (eventually always F) and (eventually always G) <=> eventually always (F and G)

• LATTICE.
  

  F and (c in S) => (Hc |-> (G or exists d in S: (c > d) and Hd))

  F => ((exists c in S: Hc) |-> G)

  
  > a well-founded partial order on set S