stable_and_temp

vstd_extra::temporal_logic::rules

Function stable_and_temp 

Source 
pub broadcast proof fn stable_and_temp<T>(p: TempPred<T>, q: TempPred<T>)
Expand description
requires
valid(stable(p)),
valid(stable(q)),
ensures
#[trigger] valid(stable(p.and(q))),

p ∧ q is stable if both p and q are stable.

§Preconditions

  • ⊧ stable(p)
  • ⊧ stable(q)

§Postconditions

  • ⊧ stable(p ∧ q)