always_lift_state_and_equality

vstd_extra::temporal_logic::rules

Function always_lift_state_and_equality 

Source 
pub broadcast proof fn always_lift_state_and_equality<T>(p: StatePred<T>, q: StatePred<T>)
Expand description
ensures
#[trigger] always(lift_state(p.and(q)))
    == always(lift_state(p)).and(always(lift_state(q))),

StatePred::and distributes over □ and lift_state.

§Postconditions

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