entails_implies_leads_to

vstd_extra::temporal_logic::rules

Function entails_implies_leads_to 

Source 
pub proof fn entails_implies_leads_to<T>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
p.entails(q),
ensures
spec.entails(p.leads_to(q)),

If p ⇒ q for all executions, then p ⇝ q.

§Preconditions

  • p ⊧ q

§Postconditions

  • spec ⊧ p ⇝ q

NOTE: there is no constraint on spec, it can be true_pred().