leads_to_self_temp

vstd_extra::temporal_logic::rules

Function leads_to_self_temp 

Source 
pub broadcast proof fn leads_to_self_temp<T>(p: TempPred<T>)
Expand description
ensures
#[trigger] valid(p.leads_to(p)),

Obviously p ⇝ p is valid.

§Postconditions

  • ⊧ p ⇝ p