entails_implies_temp_reverse

vstd_extra::temporal_logic::rules

Function entails_implies_temp_reverse 

Source 
pub broadcast proof fn entails_implies_temp_reverse<T>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
#[trigger] spec.entails(p.implies(q)),
ensures
spec.entails(p) ==> spec.entails(q),

Lift entails TempPred::implies to Verus meta-level.

If ⊧ p ⇒ q, then ⊧ p implies ⊧ q.

§Preconditions

  • spec ⊧ (p ⇒ q)

§Postconditions

  • (spec ⊧ p) ⇒ (spec ⊧ q)

NOTE: The other direction does not hold in general.