unpack_conditions_from_spec

vstd_extra::temporal_logic::rules

Function unpack_conditions_from_spec 

Source 
pub proof fn unpack_conditions_from_spec<T>(
    spec: TempPred<T>,
    c: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
valid(stable(spec)),
spec.and(c).entails(p.leads_to(q)),
ensures
spec.entails(p.and(c).leads_to(q)),

Unpack the conditions from the left to the right side of ⊧

§Preconditions

  • ⊧ stable(spec)
  • spec ∧ c ⊧ p ⇝ q

§Postconditions

  • spec ⊧ p ∧ c ⇝ q