leads_to_apply

vstd_extra::temporal_logic::rules

Function leads_to_apply 

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

If ⊧ p and ⊧ p ⇝ q, then ⊧ ◊q.

§Preconditions

  • spec ⊧ p
  • spec ⊧ p ⇝ q

§Postconditions

  • spec ⊧ ◊q