Documentation

LeanSubst.Rewriting.Normal

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

T → Prop

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

Instances For

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

T → Prop

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

Instances For

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

SNPlus R t → SN R t

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

SNPlus R t → R t t' → SNPlus R t'

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

SNPlus R t → Star R t t' → SNPlus R t'

theorem LeanSubst.SN.preimage {T : Type} {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} {R : T → T → Prop} {t t' : T} :

SN R t → R t t' → SN R t'

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

SN R t → Star R t t' → SN R t'

theorem LeanSubst.SN.star {T : Type} {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} {R : T → T → Prop} {t : T} :

SN R t → SNPlus R t

theorem LeanSubst.SN.expansion_step {T : Type} {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} {R : T → T → Prop} {t t' : T} [Functional R] :

SN R t' → Star R t t' → SN R t

theorem LeanSubst.SN.equiv_acc {T : Type} {R : T → T → Prop} {t : T} :

SN R t ↔ Acc (flip R) t

theorem LeanSubst.SN.wellfounded {T : Type} {R : T → T → Prop} :

(∀ (t : T), SN R t) → WellFounded (flip R)