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

Equations

• LeanSubst.Reducible R t = ∃ (t' : T), R t t'

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

Equations

• LeanSubst.Normal R t = ¬LeanSubst.Reducible R t

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

Equations

• LeanSubst.NormalForm R t t' = (LeanSubst.Star R t t' ∧ LeanSubst.Normal R t')

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

Equations

• LeanSubst.WN R t = ∃ (t' : T), LeanSubst.NormalForm R t t'

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

• sn {T : Type u} {R : T → T → Prop} {x : T} : (∀ (y : T), R x y → SN R y) → SN R x

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

• sn {T : Type u} {R : T → T → Prop} {x : T} : (∀ (y : T), Plus R x y → SNPlus R y) → SNPlus R x

theorem LeanSubst.SNPlus.impies_sn {T : Type u} {R : T → T → Prop} {t : T} : SNPlus R t → SN R t

theorem LeanSubst.SNPlus.preservation_step {T : Type u} {R : T → T → Prop} {t t' : T} : SNPlus R t → R t t' → SNPlus R t'

theorem LeanSubst.SNPlus.preservation {T : Type u} {R : T → T → Prop} {t t' : T} : SNPlus R t → Star R t t' → SNPlus R t'

theorem LeanSubst.SN.preimage {T : Type u} {R : T → T → Prop} (f : T → T) (x : T) : (∀ (x y : T), R x y → R (f x) (f y)) → SN R (f x) → SN R x

theorem LeanSubst.SN.preservation_step {T : Type u} {R : T → T → Prop} {t t' : T} : SN R t → R t t' → SN R t'

theorem LeanSubst.SN.preservation {T : Type u} {R : T → T → Prop} {t t' : T} : SN R t → Star R t t' → SN R t'

theorem LeanSubst.SN.star {T : Type u} {R : T → T → Prop} {t : T} : (∀ (y : T), Star R t y → SN R y) → SN R t

theorem LeanSubst.SN.implies_snplus {T : Type u} {R : T → T → Prop} {t : T} : SN R t → SNPlus R t

theorem LeanSubst.SN.expansion_step {T : Type u} {R : T → T → Prop} {t t' : T} (f : FunctionalTerm R t) : SN R t' → R t t' → SN R t

theorem LeanSubst.SN.expansion {T : Type u} {R : T → T → Prop} {t t' : T} [Functional R] : SN R t' → Star R t t' → SN R t

theorem LeanSubst.SN.subst_preimage {T : Type u} {R : T → T → Prop} [SubstMap T] [Substitutive R] {σ : Subst T} {t : T} : SN R (t[σ]) → SN R t