Go backward to The Rules of Simple Temporal Logic Go up to Top Go forward to Additional Rules |
P and (f = f') => P' |
always P <=> P and always [P => P']f |
P and <A>f => Q and [A]g |
always P and always <A>f => always Q and always [A]g |
Additional Rules
I and [A]f => I' |
I and always [A]f => always I |
|- always I => (always [A]f <=> always [A and I and I']f) |
| |||
always [A]f and WFf(A) => (P |-> Q) |