leads_to_shortcut_temp

vstd_extra::temporal_logic::rules

Function leads_to_shortcut_temp 

Source 
pub proof fn leads_to_shortcut_temp<T>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
    r: TempPred<T>,
    s: TempPred<T>,
)
Expand description
requires
spec.entails(p.leads_to(q.or(s))),
spec.entails(q.leads_to(r.or(s))),
ensures
spec.entails(p.leads_to(r.or(s))),

Combine two ⇝ with a shortcut.

§Preconditions

  • spec ⊧ p ⇝ q ∨ s
  • spec ⊧ q ⇝ r ∨ s

§Postconditions

  • spec ⊧ p ⇝ r ∨ s