wf1_variant_temp

vstd_extra::temporal_logic::rules

Function wf1_variant_temp 

Source 
pub proof fn wf1_variant_temp<T>(
    spec: TempPred<T>,
    next: TempPred<T>,
    forward: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
)
Expand description
requires
spec.entails(always(p.and(next).implies(later(p).or(later(q))))),
spec.entails(always(p.and(next).and(forward).implies(later(q)))),
spec.entails(always(next)),
spec.entails(always(p).leads_to(forward)),
ensures
spec.entails(p.leads_to(q)),

Get the initial ⇝.

§Preconditions

  • spec ⊧ □(p ∧ next ⇒ p' ∨ q')
  • spec ⊧ □(p ∧ next ∧ forward ⇒ q')
  • spec ⊧ □next
  • spec ⊧ □p ⇝ forward

§Postconditions

  • spec ⊧ p ⇝ q