use_always_tla_forall

vstd_extra::temporal_logic::rules

Function use_always_tla_forall 

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

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

§Preconditions

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

§Postconditions

  • spec ⊧ □(P(a))