leads_to_weaken

vstd_extra::temporal_logic::rules

Function leads_to_weaken 

Source 
pub proof fn leads_to_weaken<T>(
    spec: TempPred<T>,
    p1: TempPred<T>,
    q1: TempPred<T>,
    p2: TempPred<T>,
    q2: TempPred<T>,
)
Expand description
requires
spec.entails(always(p2.implies(p1))),
spec.entails(always(q1.implies(q2))),
spec.entails(p1.leads_to(q1)),
ensures
spec.entails(p2.leads_to(q2)),

Weaken ⇝ by ⇒.

§Preconditions

  • spec ⊧ □(p2 ⇒ p1)
  • spec ⊧ □(q1 ⇒ q2)
  • spec ⊧ p1 ⇝ q1

§Postconditions

  • spec ⊧ p2 ⇝ q2