leads_to_by_borrowing_inv

vstd_extra::temporal_logic::rules

Function leads_to_by_borrowing_inv 

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

Proving p ⇝ q by borrowing the inv.

§Preconditions

  • spec ⊧ p ∧ inv ⇝ q
  • spec ⊧ □inv

§Postconditions

  • spec ⊧ p ⇝ q