leads_to_rank_step_one

vstd_extra::temporal_logic::rules

Function leads_to_rank_step_one 

Source 
pub proof fn leads_to_rank_step_one<T>(
    spec: TempPred<T>,
    p: FnSpec<(nat,), TempPred<T>>,
)
Expand description
requires
forall |n: nat| (n > 0 ==> spec.entails(p(n).leads_to(p((n - 1) as nat)))),
ensures
forall |n: nat| #[trigger] spec.entails(p(n).leads_to(p(0))),

Concluding p(n) ⇝ p(0) using ranking functions, with a step of one.

§Preconditions

  • forall |n: nat|, n > 0 ==> spec ⊧ p(n) ⇝ p(n - 1)

§Postconditions

  • forall |n: nat|, spec ⊧ p(n) ⇝ p(0)