entails_and_different_temp

vstd_extra::temporal_logic::rules

Function entails_and_different_temp 

Source 
pub broadcast proof fn entails_and_different_temp<T>(
    spec1: TempPred<T>,
    spec2: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
spec1.entails(p),
spec2.entails(q),
ensures
#[trigger] spec1.and(spec2).entails(p.and(q)),

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

§Preconditions

  • spec1 ⊧ p
  • spec2 ⊧ q

§Postconditions

  • spec1 ∧ spec2 ⊧ p ∧ q