class LeanSubst.Substitutive {T : Type u} [SubstMap T] (R : T → T → Prop) : Prop

• subst {t s : T} (σ : Subst T) : R t s → R (t[σ]) (s[σ])

class LeanSubst.HasTriangle {T : Type u} (R : T → T → Prop) : Type u

• complete : T → T
• triangle {t s : T} : R t s → R s (complete R t)

inductive LeanSubst.ActionRed {T : Type u} (R : T → T → Prop) : Subst.Action T → Subst.Action T → Prop

• su {T : Type u} {R : T → T → Prop} {x y : T} : R x y → ActionRed R %x %y
• re {T : Type u} {R : T → T → Prop} {x : Nat} : ActionRed R #x #x

inductive LeanSubst.Star {T : Type u} (R : T → T → Prop) : T → T → Prop

• refl {T : Type u} {R : T → T → Prop} {t : T} : Star R t t
• step {T : Type u} {R : T → T → Prop} {x y z : T} : Star R x y → R y z → Star R x z

inductive LeanSubst.Plus {T : Type u} (R : T → T → Prop) : T → T → Prop

• start {T : Type u} {R : T → T → Prop} {t s : T} : R t s → Plus R t s
• step {T : Type u} {R : T → T → Prop} {x y z : T} : Plus R x y → R y z → Plus R x z

inductive LeanSubst.Conv {T : Type u} (R : T → T → Prop) : T → T → Prop

• refl {T : Type u} {R : T → T → Prop} {x : T} : Conv R x x
• forward {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R x z → R x y → Conv R y z
• backward {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R y z → R x y → Conv R x z

class LeanSubst.HasConfluence {T : Type u} (R : T → T → Prop) : Prop

• confluence {s t1 t2 : T} : Star R s t1 → Star R s t2 → ∃ (t : T), Star R t1 t ∧ Star R t2 t

theorem LeanSubst.Star.trans {T : Type u} {R : T → T → Prop} {x y z : T} : Star R x y → Star R y z → Star R x z

theorem LeanSubst.Star.promote {T : Type u} {R1 R2 : T → T → Prop} {x y : T} (Rprm : ∀ {x y : T}, R1 x y → R2 x y) : Star R1 x y → Star R2 x y

theorem LeanSubst.Star.stepr {T : Type u} {R : T → T → Prop} {x y z : T} : R x y → Star R y z → Star R x z

theorem LeanSubst.Star.destruct {T : Type u} {R : T → T → Prop} {x z : T} : Star R x z → (∃ (y : T), R x y ∧ Star R y z) ∨ x = z

theorem LeanSubst.Star.congr3_1 {T : Type u} {R : T → T → Prop} {t1 t1' : T} (t2 t3 : T) (f : T → T → T → T) : (∀ {t1 t2 t3 t1' : T}, R t1 t1' → R (f t1 t2 t3) (f t1' t2 t3)) → Star R t1 t1' → Star R (f t1 t2 t3) (f t1' t2 t3)

theorem LeanSubst.Star.congr3_2 {T : Type u} {R : T → T → Prop} {t2 t2' : T} (t1 t3 : T) (f : T → T → T → T) : (∀ {t1 t2 t3 t2' : T}, R t2 t2' → R (f t1 t2 t3) (f t1 t2' t3)) → Star R t2 t2' → Star R (f t1 t2 t3) (f t1 t2' t3)

theorem LeanSubst.Star.congr3_3 {T : Type u} {R : T → T → Prop} {t3 t3' : T} (t1 t2 : T) (f : T → T → T → T) : (∀ {t1 t2 t3 t3' : T}, R t3 t3' → R (f t1 t2 t3) (f t1 t2 t3')) → Star R t3 t3' → Star R (f t1 t2 t3) (f t1 t2 t3')

theorem LeanSubst.Star.congr3 {T : Type u} {R : T → T → Prop} {t1 t1' t2 t2' t3 t3' : T} (f : T → T → T → T) : (∀ {t1 t2 t3 t1' : T}, R t1 t1' → R (f t1 t2 t3) (f t1' t2 t3)) → (∀ {t1 t2 t3 t2' : T}, R t2 t2' → R (f t1 t2 t3) (f t1 t2' t3)) → (∀ {t1 t2 t3 t3' : T}, R t3 t3' → R (f t1 t2 t3) (f t1 t2 t3')) → Star R t1 t1' → Star R t2 t2' → Star R t3 t3' → Star R (f t1 t2 t3) (f t1' t2' t3')

theorem LeanSubst.Star.congr2_1 {T : Type u} {R : T → T → Prop} {t1 t1' : T} (t2 : T) (f : T → T → T) : (∀ {t1 t2 t1' : T}, R t1 t1' → R (f t1 t2) (f t1' t2)) → Star R t1 t1' → Star R (f t1 t2) (f t1' t2)

theorem LeanSubst.Star.congr2_2 {T : Type u} {R : T → T → Prop} {t2 t2' : T} (t1 : T) (f : T → T → T) : (∀ {t1 t2 t2' : T}, R t2 t2' → R (f t1 t2) (f t1 t2')) → Star R t2 t2' → Star R (f t1 t2) (f t1 t2')

theorem LeanSubst.Star.congr2 {T : Type u} {R : T → T → Prop} {t1 t1' t2 t2' : T} (f : T → T → T) : (∀ {t1 t2 t1' : T}, R t1 t1' → R (f t1 t2) (f t1' t2)) → (∀ {t1 t2 t2' : T}, R t2 t2' → R (f t1 t2) (f t1 t2')) → Star R t1 t1' → Star R t2 t2' → Star R (f t1 t2) (f t1' t2')

theorem LeanSubst.Star.congr1 {T : Type u} {R : T → T → Prop} {t1 t1' : T} (f : T → T) : (∀ {t1 t1' : T}, R t1 t1' → R (f t1) (f t1')) → Star R t1 t1' → Star R (f t1) (f t1')

theorem LeanSubst.Star.strip {T : Type u} {R : T → T → Prop} [HasTriangle R] {s t1 t2 : T} : R s t1 → Star R s t2 → ∃ (t : T), Star R t1 t ∧ R t2 t

theorem LeanSubst.Star.confluence {T : Type u} {R : T → T → Prop} [HasTriangle R] {s t1 t2 : T} : Star R s t1 → Star R s t2 → ∃ (t : T), Star R t1 t ∧ Star R t2 t

theorem LeanSubst.Star.subst {T : Type u} {R : T → T → Prop} [SubstMap T] [Substitutive R] {x y : T} (σ : Subst T) : Star R x y → Star R (x[σ]) (y[σ])

instance LeanSubst.HasConfluence_from_HasTriangle {T : Type u} {R : T → T → Prop} [HasTriangle R] : HasConfluence R

theorem LeanSubst.Plus.destruct {T : Type u} {R : T → T → Prop} {x z : T} : Plus R x z → ∃ (y : T), R x y ∧ Star R y z

theorem LeanSubst.Plus.stepr {T : Type u} {R : T → T → Prop} {x y z : T} : R x y → Plus R y z → Plus R x z

theorem LeanSubst.Plus.stepr_from_star {T : Type u} {R : T → T → Prop} {x y z : T} : R x y → Star R y z → Plus R x z

theorem LeanSubst.Conv.forward_right {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R x y → R y z → Conv R x z

theorem LeanSubst.Conv.backward_right {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R x y → R z y → Conv R x z

theorem LeanSubst.Conv.sym {T : Type u} {R : T → T → Prop} {x y : T} : Conv R x y → Conv R y x

theorem LeanSubst.Conv.star_forward {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R x z → Star R x y → Conv R y z

theorem LeanSubst.Conv.star_backward {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R y z → Star R x y → Conv R x z

theorem LeanSubst.Conv.star_forward_right {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R x y → Star R y z → Conv R x z

theorem LeanSubst.Conv.star_backward_right {T : Type u} {R : T → T → Prop} {x y z : T} : Conv R x y → Star R z y → Conv R x z

theorem LeanSubst.Conv.star_equiv {T : Type u} {R : T → T → Prop} {x y : T} [HasConfluence R] : Conv R x y ↔ ∃ (t : T), Star R x t ∧ Star R y t

theorem LeanSubst.Conv.trans {T : Type u} {R : T → T → Prop} {x y z : T} [HasConfluence R] : Conv R x y → Conv R y z → Conv R x z

def LeanSubst.FunctionalTerm {T : Type u} (R : T → T → Prop) (t : T) : Prop

Equations

• LeanSubst.FunctionalTerm R t = ∀ {x y : T}, R t x → R t y → x = y

class LeanSubst.Functional {T : Type u} (R : T → T → Prop) : Prop

• functional {t : T} : FunctionalTerm R t