RelItr

def Rel.iterate {α : Type u_1} (R : Rel α α) : ℕ → α → α → Prop

Imported declaration from the Incompleteness formalization.

Equations

• R.iterate 0 = fun (x1 x2 : α) => x1 = x2
• R.iterate n.succ = fun (x y : α) => ∃ (z : α), R x z ∧ R.iterate n z y

@[simp]

theorem Rel.iterate.iff_zero {α : Type u_1} {R : Rel α α} {x y : α} : R.iterate 0 x y ↔ x = y

@[simp]

theorem Rel.iterate.iff_succ {α : Type u_1} {R : Rel α α} {n : ℕ} {x y : α} : R.iterate (n + 1) x y ↔ ∃ (z : α), R x z ∧ R.iterate n z y

@[simp]

theorem Rel.iterate.eq {α : Type u_1} {n : ℕ} : iterate (fun (x1 x2 : α) => x1 = x2) n = fun (x1 x2 : α) => x1 = x2

theorem Rel.iterate.forward {α : Type u_1} {R : Rel α α} {n : ℕ} {x y : α} : R.iterate (n + 1) x y ↔ ∃ (z : α), R.iterate n x z ∧ R z y

theorem Rel.iterate.true_any {n : ℕ} {α✝ : Type u_1} {x y : α✝} (h : x = y) : iterate (fun (x x_1 : α✝) => True) n x y

theorem Rel.iterate.congr {α : Type u_1} {R : Rel α α} {n m : ℕ} {x y : α} (h : R.iterate n x y) (he : n = m) : R.iterate m x y

theorem Rel.iterate.comp {α : Type u_1} {R : Rel α α} {n m : ℕ} {x y : α} : (∃ (z : α), R.iterate n x z ∧ R.iterate m z y) ↔ R.iterate (n + m) x y