Handbook of Automated Reasoning

In the above picture, nodes satisfying φ are shown solid (or as a shaded area), whereas ψ nodes are indicated by a circle.

The operator A U⁺ can be expressed by E U⁺ and A F⁺ . This characterization is similar to the definition of the unless-operator in linear temporal logic, cf. page 1648:

$\mathbf{A}\left(\phi {\mathbf{U}}^{+}\psi \right)\leftrightarrow \left(\mathbf{A}\left(\phi {\mathbf{W}}^{+}\psi \right)\wedge \mathbf{A}{\mathbf{F}}^{+}\psi \right)=\left(\neg \mathbf{E}\left(\neg \psi {\mathbf{U}}^{+}\neg \left(\phi \vee \psi \right)\right)\wedge \mathbf{A}{\mathbf{F}}^{+}\psi \right).$

Therefore, it is sufficient to consider only the two basic operators E U ⁺ and A F⁺ in formal proofs and algorithms. Similarly, the formula E(φ W⁺ ψ) can be replaced by (E(φ U⁺ ψ) ∨ EG⁺ φ). However, there is no negation-free ...