eliminate_always

vstd_extra::temporal_logic::rules

Function eliminate_always 

Source 
pub proof fn eliminate_always<T>(spec: TempPred<T>, p: TempPred<T>)
Expand description
requires
spec.entails(always(p)),
ensures
spec.entails(p),

If ⊧ □p, then ⊧ p.

§Preconditions

  • spec ⊧ □p

§Postconditions

  • spec ⊧ p