Theorems · Theorem · logic and foundations

Computation.liftRel_def

∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β},
  Computation.LiftRel R ca cb ↔ (ca.Terminates ↔ cb.Terminates) ∧ ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b

Defined in

Mathlib.Data.Seq.Computation

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext