spec_entails_tla_forall

vstd_extra::temporal_logic::rules

Function spec_entails_tla_forall 

Source 
pub broadcast proof fn spec_entails_tla_forall<T, A>(
    spec: TempPred<T>,
    a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
)
Expand description
requires
forall |a: A| spec.entails(#[trigger] a_to_temp_pred(a)),
ensures
#[trigger] spec.entails(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)