entails_or_temp

vstd_extra::temporal_logic::rules

Function entails_or_temp 

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

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

If ⊧ p or ⊧ q, then ⊧ p ∨ q.

§Preconditions

  • spec ⊧ p or spec ⊧ q

§Postconditions

  • spec ⊧ p ∨ q

NOTE: The other direction does not hold in general.