entails_and_temp

vstd_extra::temporal_logic::rules

Function entails_and_temp 

Source 
pub broadcast proof fn entails_and_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.and(q)),

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

If ⊧ p and ⊧ q, then ⊧ p ∧ q.

§Preconditions

  • spec ⊧ p
  • spec ⊧ q

§Postconditions

  • spec ⊧ p ∧ q