lift_state_exists_equality

vstd_extra::temporal_logic::rules

Function lift_state_exists_equality 

Source 
pub broadcast proof fn lift_state_exists_equality<T, A>(
    a_to_state_pred: FnSpec<(A,), StatePred<T>>,
)
Expand description
ensures
#[trigger] lift_state_exists(a_to_state_pred)
    == tla_exists(|a| lift_state(a_to_state_pred(a))),

Lift the exists outside lift_state.

§Postconditions

  • lift_state(∃ a: A. p(a)) == ∃ a: A. lift_state(p(a))