Function leads_to_framed_by_or

pub broadcast proof fn leads_to_framed_by_or<T>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: TempPred<T>,
    r: TempPred<T>,
)

Expand description

requires

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

ensures

#[trigger] spec.entails(p.or(r).leads_to(q.or(r))),

Sandwich ⇝ with ∨ r.

leads_to_framed_by_or