Fórmulas com apenas um operador

Nesta secção começamos por estudar métodos de prova para propriedades à espera de simples, cuja forma geral é

sendo p, q e r fórmulas de estado. Esta fórmula indica que um estado onde p se verifique é seguido por um intervalo onde q se verifica, podendo este ser terminado por um estado onde se verifica r ou extender-se até ao infinito. O intervalo onde q se verifica também pode ser vazio se no estado em que se verifica p também se verificar r.