always_implies_to_leads_to

vstd_extra::temporal_logic::rules

Function always_implies_to_leads_to 

Source 
pub broadcast proof fn always_implies_to_leads_to<T>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
#[trigger] spec.entails(always(p.implies(q))),
ensures
spec.entails(p.leads_to(q)),

If ⊧ □(p ⇒ q), then ⊧ p ⇝ q.

§Preconditions

  • spec ⊧ □(p ⇒ q)

§Postconditions

  • spec ⊧ p ⇝ q