entails_not_temp_reverse

vstd_extra::temporal_logic::rules

Function entails_not_temp_reverse 

Source 
pub broadcast proof fn entails_not_temp_reverse<T>(spec: TempPred<T>, p: TempPred<T>)
Expand description
requires
#[trigger] spec.entails(not(p)),
spec != false_pred::<T>(),
ensures
!spec.entails(p),

Lift entails TempPred::not to Verus meta-level (reversed direction).

If ⊧ !p, then !(⊧ p).

§Preconditions

  • spec ⊧ !p

§Postconditions

  • !(spec ⊧ p)

NOTE: The other direction does not hold in general.