leads_to_always_enhance

vstd_extra::temporal_logic::rules

Function leads_to_always_enhance 

Source 
pub proof fn leads_to_always_enhance<T>(
    spec: TempPred<T>,
    inv: TempPred<T>,
    p: TempPred<T>,
    q1: TempPred<T>,
    q2: TempPred<T>,
)
Expand description
requires
spec.entails(always(inv)),
spec.entails(p.leads_to(always(q1))),
q1.and(inv).entails(q2),
ensures
spec.entails(p.leads_to(always(q2))),

Enhance the conclusion of leads-to □ using invariant.

§Preconditions

  • spec ⊧ □inv
  • spec ⊧ p ⇝ □q1
  • q1 ∧ inv ⊧ q2

§Postconditions

  • spec ⊧ p ⇝ □q2