leads_to_always_combine

vstd_extra::temporal_logic::rules

Function leads_to_always_combine 

Source 
pub broadcast proof fn leads_to_always_combine<T>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
    r: TempPred<T>,
)
Expand description
requires
spec.entails(p.leads_to(always(q))),
spec.entails(p.leads_to(always(r))),
ensures
spec.entails(p.leads_to(always(q.and(r)))),
spec.entails(p.leads_to(always(q).and(always(r)))),

Combine the conclusions of two ⇝ if the conclusions are stable.

§Preconditions

  • spec ⊧ p ⇝ □q
  • spec ⊧ p ⇝ □r

§Postconditions

  • spec ⊧ p ⇝ □(q ∧ r)