spec_entails_always_tla_forall

vstd_extra::temporal_logic::rules

Function spec_entails_always_tla_forall 

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

If ⊧ □(P(a)) for all a, then ⊧ □(∀ a. P(a)).

§Preconditions

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

§Postconditions

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