tla_exists_leads_to_intro

vstd_extra::temporal_logic::rules

Function tla_exists_leads_to_intro 

Source 
pub broadcast proof fn tla_exists_leads_to_intro<T, A>(
    spec: TempPred<T>,
    a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
    q: TempPred<T>,
)
Expand description
requires
forall |a: A| #[trigger] spec.entails(a_to_temp_pred(a).leads_to(q)),
ensures
#[trigger] spec.entails(tla_exists(a_to_temp_pred).leads_to(q)),

If ⊧ P(a) ⇝ q for all a, then ⊧ exists a. P(a) leads_to q.

§Preconditions

  • forall a: A. spec ⊧ P(a) ⇝ q

§Postconditions

  • spec ⊧ (∃ a: A. P(a)) ⇝ q