entails_trans

vstd_extra::temporal_logic::rules

Function entails_trans 

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

Entails is transitive.

§Preconditions

  • p ⊧ q
  • q ⊧ r

§Postconditions

  • p ⊧ r