Function wf1

pub proof fn wf1<T>(
    spec: TempPred<T>,
    next: ActionPred<T>,
    forward: ActionPred<T>,
    p: StatePred<T>,
    q: StatePred<T>,
)

Expand description

requires

forall |s, s_prime: T| {
    p.apply(s) && #[trigger] next.apply(s, s_prime)
        ==> p.apply(s_prime) || q.apply(s_prime)
},

forall |s, s_prime: T| {
    p.apply(s) && #[trigger] next.apply(s, s_prime) && forward.apply(s, s_prime)
        ==> q.apply(s_prime)
},

forall |s: T| #[trigger] p.apply(s) ==> enabled(forward).apply(s),

spec.entails(always(lift_action(next))),

spec.entails(weak_fairness(forward)),

ensures

spec.entails(lift_state(p).leads_to(lift_state(q))),

Get the initial ⇝ with a stronger wf assumption than wf1_variant_temp.

wf1