leads_to_always_tla_forall

vstd_extra::temporal_logic::rules

Function leads_to_always_tla_forall 

Source 
pub proof fn leads_to_always_tla_forall<T, A>(
    spec: TempPred<T>,
    p: TempPred<T>,
    a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
    domain: Set<A>,
)
Expand description
requires
forall |a: A| spec.entails(p.leads_to(always(#[trigger] a_to_temp_pred(a)))),
domain.finite(),
domain.len() > 0,
forall |a: A| #[trigger] domain.contains(a),
ensures
spec.entails(p.leads_to(always(tla_forall(a_to_temp_pred)))),

Leads to □tla_forall(a_to_temp_pred) if forall a, it leads to □a_to_temp_pred(a).

§Preconditions

  • forall |a: A|, spec ⊧ p ⇝ □a_to_temp_pred(a)
  • forall |a: A|, a \in domain
  • domain.is_finite() && domain.len() > 0

§Postconditions

  • spec ⊧ □tla_forall(a_to_temp_pred)

The domain set assist in showing type A contains finite elements.