lift_state_or_equality

vstd_extra::temporal_logic::rules

Function lift_state_or_equality 

Source 
pub broadcast proof fn lift_state_or_equality<T>(p: StatePred<T>, q: StatePred<T>)
Expand description
ensures
lift_state(p.or(q)) == lift_state(p).or(lift_state(q)),

StatePred::or distributes over lift_state.

§Postconditions

  • lift_state(p ∨ q) == lift_state(p) ∨ lift_state(q)