p_leads_to_q_is_stable

vstd_extra::temporal_logic::rules

Function p_leads_to_q_is_stable 

Source 
pub proof fn p_leads_to_q_is_stable<T>(p: TempPred<T>, q: TempPred<T>)
Expand description
ensures
valid(stable(p.leads_to(q))),

A ⇝ predicate is stable.

§Postconditions

  • ⊧ stable(p ⇝ q)