inductive Relation.TraceReflGen {α : Sort u_1} {ε : Type u_2} [Monoid ε] (R : α → ε → α → Prop) : α → ε → α → Prop

• refl {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x : α} : TraceReflGen R x Trace.τ x
• single {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y : α} {a : ε} : R x a y → TraceReflGen R x a y

inductive Relation.TraceTransGen {α : Sort u_1} {ε : Type u_2} [Monoid ε] (R : α → ε → α → Prop) : α → ε → α → Prop

• single {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y : α} {a : ε} : R x a y → TraceTransGen R x a y
• head {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y z : α} {a a' : ε} : R x a y → TraceTransGen R y a' z → TraceTransGen R x (a * a') z

theorem Relation.TraceTransGen.no_rel {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y : α} {a : ε} (h : ∀ (y : α) (a : ε), ¬R x a y) : ¬TraceTransGen R x a y

theorem Relation.TraceTransGen.trans {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y z : α} {a a' : ε} : TraceTransGen R x a y → TraceTransGen R y a' z → TraceTransGen R x (a * a') z

inductive Relation.TraceReflTransGen {α : Sort u_1} {ε : Type u_2} [Monoid ε] (R : α → ε → α → Prop) : α → ε → α → Prop

• refl {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x : α} : TraceReflTransGen R x Trace.τ x
• head {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x : α} (y : α) {z : α} {a a' : ε} : R x a y → TraceReflTransGen R y a' z → TraceReflTransGen R x (a * a') z

theorem Relation.TraceReflTransGen.single {α : Sort u_1} {ε : Type u_2} [Monoid ε] (R : α → ε → α → Prop) {x : α} {a : ε} (y : α) : R x a y → TraceReflTransGen R x a y

theorem Relation.TraceReflTransGen.no_rel_to_eq {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y : α} {a : ε} (h₁ : ∀ (y : α) (a : ε), ¬R x a y) (h₂ : TraceReflTransGen R x a y) : x = y

theorem Relation.TraceReflTransGen.to_trans_gen {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y z : α} {a a' : ε} : R x a y → TraceReflTransGen R y a' z → TraceTransGen R x (a * a') z

theorem Relation.TraceReflTransGen.trans {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y z : α} {a a' : ε} : TraceReflTransGen R x a y → TraceReflTransGen R y a' z → TraceReflTransGen R x (a * a') z

theorem Relation.TraceTransGen.to_refl_trans_gen {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y : α} {a : ε} : TraceTransGen R x a y → TraceReflTransGen R x a y

theorem Relation.TraceReflTransGen.tail {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x y z : α} {a a' : ε} : TraceReflTransGen R x a y → R y a' z → TraceReflTransGen R x (a * a') z

theorem Relation.TraceReflTransGen.tail_induction_on {α : Sort u_1} {ε : Type u_2} [Monoid ε] {R : α → ε → α → Prop} {x : α} {motive : (z : α) → (e : ε) → TraceReflTransGen R x e z → Prop} {z : α} {e : ε} (h : TraceReflTransGen R x e z) (refl : motive x Trace.τ ⋯) (tail : ∀ {y z : α} {e₁ e₂ : ε} (h : TraceReflTransGen R x e₁ y) (h' : R y e₂ z), motive y e₁ h → motive z (e₁ * e₂) ⋯) : motive z e h

def Relation.iComp {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} {ι : Type u_4} {ι' : Type u_5} (R : ι → α → β → Prop) (R' : ι' → β → δ → Prop) : ι × ι' → α → δ → Prop

Equations

• Relation.iComp R R' (i, i') = R i ∘ᵣ R' i'

theorem Relation.flip_icomp {α : Sort u_1} {β : Sort u_2} {δ : Sort u_3} {ι : Type u_4} {ι' : Type u_5} {R : ι → α → β → Prop} {R' : ι' → β → δ → Prop} : flip ∘ iComp R R' = iComp (flip ∘ R') (flip ∘ R) ∘ Prod.swap

inductive Relation.Eventually {α : Type u_1} (R : α → Set α → Prop) : α → Set α → Prop

Eventually R x P is the proposition stating that:

• All possible R-chains from x are safe (do not get stuck).
• All possible R-chains from x eventually reach a value satisfying P.

• here {α : Type u_1} {R : α → Set α → Prop} {x : α} {P : Set α} : x ∈ P → Eventually R x P
• step {α : Type u_1} {R : α → Set α → Prop} {x : α} {P : Set α} (P' : Set α) : R x P' → (∀ x' ∈ P', Eventually R x' P) → Eventually R x P

theorem Relation.Eventually.wellformed {α : Type u_1} (R : α → Set α → Prop) (R_wf : ∀ (x : α) (P : Set α), R x P → P ≠ ∅) (x : α) (P : Set α) : Eventually R x P → P ≠ ∅

theorem Relation.Eventually.step_chained {α : Type u_1} {x : α} {R : α → Set α → Prop} {P : Set α} (h : R x {y : α | Eventually R y P}) : Eventually R x P

theorem Relation.Eventually.cut {α : Type u_1} {x : α} {P : Set α} (P' : Set α) {R : α → Set α → Prop} (h : Eventually R x P') (h' : ∀ y ∈ P', Eventually R y P) : Eventually R x P

theorem Relation.Eventually.cut_chained {α : Type u_1} {x : α} {R : α → Set α → Prop} {P : Set α} (h : Eventually R x {y : α | Eventually R y P}) : Eventually R x P

inductive Relation.Eventually? {α : Type u_1} (R : α → Set α → Prop) : α → Set α → Prop

Eventually? R x P is the proposition stating that:

• All possible R-chains from x that are R-safe eventually reach a value satisfying P.

• here {α : Type u_1} {R : α → Set α → Prop} {x : α} {P : Set α} : x ∈ P → Eventually? R x P
• step? {α : Type u_1} {R : α → Set α → Prop} {x : α} {P : Set α} (P' : Set α) (x' : α) : R x P' → x' ∈ P' → Eventually? R x' P → Eventually? R x P

theorem Relation.Eventually?.wellformed {α : Type u_1} (R : α → Set α → Prop) (x : α) (P : Set α) : Eventually? R x P → P ≠ ∅