always_to_always_later

vstd_extra::temporal_logic::rules

Function always_to_always_later 

Source 
pub broadcast proof fn always_to_always_later<T>(spec: TempPred<T>, p: TempPred<T>)
Expand description
requires
spec.entails(always(p)),
ensures
#[trigger] spec.entails(always(later(p))),

If entails □p, then entails □(later(p)).

§Preconditions

  • spec ⊧ □p

§Postconditions

  • spec ⊧ □p'