tla_forall_always_equality

vstd_extra::temporal_logic::rules

Function tla_forall_always_equality 

Source 
pub proof fn tla_forall_always_equality<T, A>(
    a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
)
Expand description
ensures
tla_forall(|a: A| always(a_to_temp_pred(a))) == always(tla_forall(a_to_temp_pred)),

Lift the □ outside tla_forall if the function is previously wrapped by an □.

§Postconditions

  • ∀ a:A. □P(a) == □(∀ a:A. P(a)))

NOTE: Verus may not able to infer that (|a| func(a))(a) equals func(a). Please turn to lemma tla_forall_always_equality_variant for troubleshooting.