tla_forall_always_equality_variant

vstd_extra::temporal_logic::rules

Function tla_forall_always_equality_variant 

Source 
pub proof fn tla_forall_always_equality_variant<T, A>(
    a_to_always: FnSpec<(A,), TempPred<T>>,
    a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
)
Expand description
requires
forall |a: A| {
    a_to_always(a).entails((|a: A| always(a_to_temp_pred(a)))(a))
        && ((|a: A| always(a_to_temp_pred(a)))(a)).entails(a_to_always(a))
},
ensures
tla_forall(a_to_always) == always(tla_forall(a_to_temp_pred)),