leads_to_stable

vstd_extra::temporal_logic::rules

Function leads_to_stable 

Source 
pub proof fn leads_to_stable<T>(
    spec: TempPred<T>,
    next: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
spec.entails(always(q.and(next).implies(later(q)))),
spec.entails(always(next)),
spec.entails(p.leads_to(q)),
ensures
spec.entails(p.leads_to(always(q))),

Prove p ⇝ □q by showing that q is preserved.

§Preconditions

  • spec ⊧ □(q ∧ next ⇒ q')
  • spec ⊧ □next
  • spec ⊧ p ⇝ q

§Postconditions

  • spec ⊧ p ⇝ □q