always_implies_forall_intro

vstd_extra::temporal_logic::rules

Function always_implies_forall_intro 

Source 
pub broadcast proof fn always_implies_forall_intro<T, A>(
    spec: TempPred<T>,
    p: TempPred<T>,
    a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
)
Expand description
requires
forall |a: A| #[trigger] spec.entails(always(p.implies(a_to_temp_pred(a)))),
ensures
#[trigger] spec.entails(always(p.implies(tla_forall(a_to_temp_pred)))),

If ⊧ □(p ⇒ P(a)) for all a, then ⊧ □(p ⇒ forall a. P(a)).

§Preconditions

  • forall a: A. spec ⊧ □(p ⇒ P(a))

§Postconditions

  • spec ⊧ □(p ⇒ (∀ a: A. P(a)))