or_leads_to_case_analysis

vstd_extra::temporal_logic::rules

Function or_leads_to_case_analysis 

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

Prove p ⇝ r by case analysis on q.

§Preconditions

  • spec ⊧ (p ∧ q) ⇝ r
  • spec ⊧ (p ∧ ~q) ⇝ r

§Postconditions

  • spec ⊧ p ⇝ r