always_lift_state_weaken

vstd_extra::temporal_logic::rules

Function always_lift_state_weaken 

Source 
pub proof fn always_lift_state_weaken<T>(
    spec: TempPred<T>,
    p: StatePred<T>,
    q: StatePred<T>,
)
Expand description
requires
forall |s: T| #[trigger] p.apply(s) ==> q.apply(s),
spec.entails(always(lift_state(p))),
ensures
spec.entails(always(lift_state(q))),

Weaken □ lifted state predicate by ⇒.

§Preconditions

  • ∀ s. p(s) ⇒ q(s)
  • spec ⊧ □lift_state(p)

§Postconditions

  • spec ⊧ □lift_state(q)