- - - - CENAPAD-MGCO

A seguir: Equidade forte e fraca: Acima: Técnicas de Prova de Anterior: Prova de via com

Prova de $P \ensuremath{ \; leads\!{\small -}\!to\;}Q$ via $\gamma$ com equidade forte

Os seguintes pontos devem ser estabelecidos:

• por hipótese, $\gamma$ é executado com equidade forte;
• $P \Longrightarrow g$, onde g é a guarda de $\gamma$
  • ($\gamma$ sempre está habilitado enquanto P for válido)
• a execução de $\gamma$ leva à validação de Q
• a execução de qualquer outro comando $\delta= \in \Gamma, \delta \neq \gamma$,que esteja habilitado quando P for válido acarreta a validade de um predicado R tal que $R \ensuremath{ \; leads\!{\small -}\!to\;}(P \vee Q)$
  • (a execução de $\delta$ leva ou bem à validação futura de Q, ou bem à re-habilitação de $\gamma$).

Com o estabelecimento destes pontos, uma computação infinita que viole $P \ensuremath{ \; leads\!{\small -}\!to\;}Q$ está descartada:

• suponha a existência de uma computação em que P foi válido num instante i, e Q não se verifica para nenhum instante j maior ou igual a i;
• esta computação teria a guarda de $\gamma$ habilitada por um número ilimitado de vezes após o instante i, mas $\gamma$nunca teria sido executado, o que contradiz a hipótese de equidade forte.