entails_preserved_by_always

vstd_extra::temporal_logic::rules

Function entails_preserved_by_always 

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

Introduce □ to both sides of ⊧.

§Preconditions

  • p ⊧ q

§Postconditions

  • □p ⊧ □q