use_tla_forall

vstd_extra::temporal_logic::rules

Function use_tla_forall 

Source 
pub proof fn use_tla_forall<T, A>(
    spec: TempPred<T>,
    a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
    a: A,
)
Expand description
requires
spec.entails(tla_forall(a_to_temp_pred)),
ensures
spec.entails(a_to_temp_pred(a)),

If ⊧ forall a. P(a), then ⊧ P(a) for any particular a.

§Preconditions

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

§Postconditions

  • spec ⊧ P(a)