always_p_is_stable

vstd_extra::temporal_logic::rules

Function always_p_is_stable 

Source 
pub broadcast proof fn always_p_is_stable<T>(p: TempPred<T>)
Expand description
ensures
#[trigger] valid(stable(always(p))),

An □ predicate is stable.

§Postconditions

  • ⊧ stable(□p)