vacuous_leads_to

vstd_extra::temporal_logic::rules

Function vacuous_leads_to 

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

Proving p ⇝ q vacuously.

§Preconditions

  • spec ⊧ □r
  • p ∧ r == false

§Postconditions

  • spec ⊧ p ⇝ q