entails_always_lift_state_and

vstd_extra::temporal_logic::rules

Function entails_always_lift_state_and 

Source 
pub broadcast proof fn entails_always_lift_state_and<T>(
    spec: TempPred<T>,
    p: StatePred<T>,
    q: StatePred<T>,
)
Expand description
requires
spec.entails(always(lift_state(p))),
spec.entails(always(lift_state(q))),
ensures
#[trigger] spec.entails(always(lift_state(p.and(q)))),

If ⊧ □(lift_state(p)) and ⊧ □(lift_state(q)), then ⊧ □(lift_state(p ∧ q)).

§Preconditions

  • spec ⊧ □lift_state(p)
  • spec ⊧ □lift_state(q)

§Postconditions

  • spec ⊧ □lift_state(p ∧ q)