lift_state_implies_equality

vstd_extra::temporal_logic::rules

Function lift_state_implies_equality 

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

StatePred::implies distributes over lift_state.

§Postconditions

  • lift_state(p ⇒ q) == lift_state(p) ⇒ lift_state(q)