lift_state_and_equality

vstd_extra::temporal_logic::rules

Function lift_state_and_equality 

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

StatePred::and distributes over lift_state.

§Postconditions

  • lift_state(p ∧ q) == lift_state(p) ∧ lift_state(q)