structure GeachConfluent.Taple : Type

• i : ℕ
• j : ℕ
• m : ℕ
• n : ℕ

def GeachConfluent {α : Type u_1} (t : GeachConfluent.Taple) (R : Rel α α) : Prop

Equations

• GeachConfluent t R = ∀ {x y z : α}, R.iterate t.i x y ∧ R.iterate t.j x z → ∃ (u : α), R.iterate t.m y u ∧ R.iterate t.n z u

theorem GeachConfluent.serial_def {α : Type u_1} {rel : Rel α α} : Serial rel ↔ GeachConfluent { i := 0, j := 0, m := 1, n := 1 } rel

theorem GeachConfluent.reflexive_def {α : Type u_1} {rel : Rel α α} : Reflexive rel ↔ GeachConfluent { i := 0, j := 0, m := 1, n := 0 } rel

theorem GeachConfluent.symmetric_def {α : Type u_1} {rel : Rel α α} : Symmetric rel ↔ GeachConfluent { i := 0, j := 1, m := 0, n := 1 } rel

theorem GeachConfluent.transitive_def {α : Type u_1} {rel : Rel α α} : Transitive rel ↔ GeachConfluent { i := 0, j := 2, m := 1, n := 0 } rel

theorem GeachConfluent.euclidean_def {α : Type u_1} {rel : Rel α α} : Euclidean rel ↔ GeachConfluent { i := 1, j := 1, m := 0, n := 1 } rel

theorem GeachConfluent.confluent_def {α : Type u_1} {rel : Rel α α} : Confluent rel ↔ GeachConfluent { i := 1, j := 1, m := 1, n := 1 } rel

theorem GeachConfluent.extensive_def {α : Type u_1} {rel : Rel α α} : Coreflexive rel ↔ GeachConfluent { i := 0, j := 1, m := 0, n := 0 } rel

theorem GeachConfluent.functional_def {α : Type u_1} {rel : Rel α α} : Functional rel ↔ GeachConfluent { i := 1, j := 1, m := 0, n := 0 } rel

theorem GeachConfluent.dense_def {α : Type u_1} {rel : Rel α α} : Dense rel ↔ GeachConfluent { i := 0, j := 1, m := 2, n := 0 } rel

@[simp]

theorem GeachConfluent.satisfies_eq {α : Type u_1} {t : Taple} : GeachConfluent t fun (x1 x2 : α) => x1 = x2

def MultiGeachConfluent {α : Type u_1} (ts : List GeachConfluent.Taple) (rel : Rel α α) : Prop

Equations

• MultiGeachConfluent [] rel = True
• MultiGeachConfluent [t] rel = GeachConfluent t rel
• MultiGeachConfluent (t :: ts_2) rel = (GeachConfluent t rel ∧ MultiGeachConfluent ts_2 rel)

@[simp]

theorem MultiGeachConfluent.iff_nil {α : Type u_1} {rel : Rel α α} : MultiGeachConfluent [] rel

@[simp]

theorem MultiGeachConfluent.iff_singleton {α : Type u_1} {rel : Rel α α} {t : GeachConfluent.Taple} : MultiGeachConfluent [t] rel ↔ GeachConfluent t rel

theorem MultiGeachConfluent.iff_cons {α : Type u_1} {rel : Rel α α} {ts : List GeachConfluent.Taple} {t : GeachConfluent.Taple} (h : ts ≠ []) : MultiGeachConfluent (t :: ts) rel ↔ GeachConfluent t rel ∧ MultiGeachConfluent ts rel

@[simp]

theorem MultiGeachConfluent.satisfies_eq {α : Type u_1} {ts : List GeachConfluent.Taple} : MultiGeachConfluent ts fun (x1 x2 : α) => x1 = x2