- - - - CENAPAD-MGCO

A seguir: Prova de via com Acima: Técnicas de Prova de Anterior: Técnicas de Prova de

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

É preciso estabelecer os seguintes pontos:

• por hipótese, $\gamma$ é executado com equidade fraca;
• $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 validação de $P \vee Q$
  • ($\delta$ ou bem provoca a ocorrência de Q, ou mantém $\gamma$ habilitado)

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 em todo instante $j \geq i$, o que contradiz a hipótese de equidade fraca para $\gamma$