entails_trans_by_simplify

vstd_extra::temporal_logic::rules

Function entails_trans_by_simplify 

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

Transitivity of ⊧ with simplification.

§Preconditions

  • spec ⊧ p
  • spec ∧ p ⊧ q

§Postconditions

  • spec ⊧ q