Go backward to The Rules of Simple Temporal LogicGo up to TopGo forward to Additional Rules |

- TLA1.
*P**and*(*f*=*f'*)*=>**P'*`always`*P**<=>**P**and*`always`[*P**=>**P'*]_{f} - TLA2.
*P**and*<`A`>_{f}*=>**Q**and*[`A`]_{g}`always`*P**and*`always`<`A`>_{f}*=>*`always`*Q**and*`always`[`A`]_{g}

Additional Rules

- INV1.
*I**and*[`A`]_{f}*=>**I'**I**and*`always`[`A`]_{f}*=>*`always`*I* - INV2.
|- `always`*I**=>*(`always`[`A`]_{f}*<=>*`always`[`A`*and**I**and**I'*])_{f} - WF1.
*P**and*[`A`]_{f}*=>*(*P'**or**Q'*)*P**and*<`A`*and*`A`>_{f}*=>**Q'**P**=>*`Enabled`<`A`>_{f}`always`[`A`]_{f}*and*WF(_{f}`A`)*=>*(*P**|->**Q*)

Author: Wolfgang Schreiner

Last Modification: May 14, 1998