state_pred_not_apply_equality

vstd_extra::temporal_logic::rules

Function state_pred_not_apply_equality 

Source 
pub broadcast proof fn state_pred_not_apply_equality<T>(p: StatePred<T>, s: T)
Expand description
ensures
#[trigger] p.not().apply(s) == !p.apply(s),

Lift StatePred::not to Verus meta-level.