lift_state_exists_leads_to_case_analysis

vstd_extra::temporal_logic::rules

Function lift_state_exists_leads_to_case_analysis 

Source 
pub proof fn lift_state_exists_leads_to_case_analysis<T, A>(
    spec: TempPred<T>,
    a_to_temp_pred: FnSpec<(A,), StatePred<T>>,
    p: StatePred<T>,
    q: TempPred<T>,
)
Expand description
requires
spec.entails(lift_state_exists(StatePred::absorb(a_to_temp_pred, p)).leads_to(q)),
spec.entails(lift_state_exists(StatePred::absorb(a_to_temp_pred, p.not())).leads_to(q)),
ensures
spec.entails(lift_state_exists(a_to_temp_pred).leads_to(q)),

Prove lift_state_exists leads to by case analysis on another StatePred.

§Preconditions

  • spec ⊧ lift_state_exists(absorb(a_to_temp_pred, p)) ⇝ q
  • spec ⊧ lift_state_exists(absorb(a_to_temp_pred, ~p)) ⇝ q

§Postconditions

  • spec ⊧ lift_state_exists(a_to_temp_pred) ⇝ q