inductive Red : Term → Term → Prop

• beta {A : Ty} {b t : Term} : ((:λ[A] b) :@ t) ~> b[LeanSubst.su t::+0]
• app1 {f f' a : Term} : f ~> f' → (f :@ a) ~> (f' :@ a)
• app2 {a a' f : Term} : a ~> a' → (f :@ a) ~> (f :@ a')
• lam {A : Ty} {t t' : Term} : t ~> t' → (:λ[A] t) ~> :λ[A] t'

def «term_~>_» : Lean.TrailingParserDescr

Equations

• «term_~>_» = Lean.ParserDescr.trailingNode `«term_~>_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~> ") (Lean.ParserDescr.cat `term 81))

def «term_~>*_» : Lean.TrailingParserDescr

Equations

• «term_~>*_» = Lean.ParserDescr.trailingNode `«term_~>*_» 81 82 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~>* ") (Lean.ParserDescr.cat `term 82))

def «term_~s>_» : Lean.TrailingParserDescr

Equations

• «term_~s>_» = Lean.ParserDescr.trailingNode `«term_~s>_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~s> ") (Lean.ParserDescr.cat `term 81))

def «term_~s>*_» : Lean.TrailingParserDescr

Equations

• «term_~s>*_» = Lean.ParserDescr.trailingNode `«term_~s>*_» 81 82 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~s>* ") (Lean.ParserDescr.cat `term 82))

inductive ParRed : Term → Term → Prop

• var {x : Nat} : #x ~p> #x
• beta {A : Ty} {b b' t t' : Term} : b ~p> b' → t ~p> t' → ((:λ[A] b) :@ t) ~p> b'[LeanSubst.su t'::+0]
• app {f f' a a' : Term} : f ~p> f' → a ~p> a' → (f :@ a) ~p> (f' :@ a')
• lam {t t' : Term} {A : Ty} : t ~p> t' → (:λ[A] t) ~p> :λ[A] t'

def «term_~p>_» : Lean.TrailingParserDescr

Equations

• «term_~p>_» = Lean.ParserDescr.trailingNode `«term_~p>_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~p> ") (Lean.ParserDescr.cat `term 81))

def «term_~p>*_» : Lean.TrailingParserDescr

Equations

• «term_~p>*_» = Lean.ParserDescr.trailingNode `«term_~p>*_» 81 82 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~p>* ") (Lean.ParserDescr.cat `term 82))

def «term_~ps>_» : Lean.TrailingParserDescr

Equations

• «term_~ps>_» = Lean.ParserDescr.trailingNode `«term_~ps>_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ps> ") (Lean.ParserDescr.cat `term 81))

def «term_~ps>*_» : Lean.TrailingParserDescr

Equations

• «term_~ps>*_» = Lean.ParserDescr.trailingNode `«term_~ps>*_» 81 82 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~ps>* ") (Lean.ParserDescr.cat `term 82))

theorem ParRed.refl {t : Term} : t ~p> t

def ParRed.complete : Term → Term

Equations

• ParRed.complete ((:λ[a] b) :@ t) = (ParRed.complete b)[LeanSubst.su (ParRed.complete t)::+0]
• ParRed.complete (f :@ a) = ParRed.complete f :@ ParRed.complete a
• ParRed.complete (:λ[A] t) = :λ[A] ParRed.complete t
• ParRed.complete #x_1 = #x_1

theorem ParRed.subst {t t' : Term} (σ : LeanSubst.Subst Term) : t ~p> t' → t[σ] ~p> t'[σ]

theorem ParRed.subst_action {x : Nat} {σ σ' : LeanSubst.Subst Term} (r : LeanSubst.Ren) : LeanSubst.ActionRed ParRed (σ x) (σ' x) → LeanSubst.ActionRed ParRed ((σ ∘ ↑r) x) ((σ' ∘ ↑r) x)

theorem ParRed.subst_red_lift {σ σ' : LeanSubst.Subst Term} : (∀ (x : Nat), LeanSubst.ActionRed ParRed (σ x) (σ' x)) → ∀ (x : Nat), LeanSubst.ActionRed ParRed (σ.lift x) (σ'.lift x)

theorem ParRed.hsubst {t t' : Term} {σ σ' : LeanSubst.Subst Term} : (∀ (x : Nat), LeanSubst.ActionRed ParRed (σ x) (σ' x)) → t ~p> t' → t[σ] ~p> t'[σ']

theorem ParRed.triangle {t s : Term} : t ~p> s → s ~p> complete t

instance ParRed.instSubstitutiveTerm : LeanSubst.Substitutive ParRed

instance ParRed.instHasTriangleTerm : LeanSubst.HasTriangle ParRed

Equations

• ParRed.instHasTriangleTerm = { complete := ParRed.complete, triangle := ⋯ }

theorem Red.subst {t t' : Term} (σ : LeanSubst.Subst Term) : t ~> t' → t[σ] ~> t'[σ]

theorem Red.subst_action {x : Nat} {σ σ' : LeanSubst.Subst Term} (r : LeanSubst.Ren) : LeanSubst.ActionRed Red (σ x) (σ' x) → LeanSubst.ActionRed Red ((σ ∘ ↑r) x) ((σ' ∘ ↑r) x)

theorem Red.subst_red_lift {σ σ' : LeanSubst.Subst Term} : (∀ (x : Nat), LeanSubst.ActionRed Red (σ x) (σ' x)) → ∀ (x : Nat), LeanSubst.ActionRed Red (σ.lift x) (σ'.lift x)

theorem Red.seq_implies_par {t t' : Term} : t ~> t' → t ~p> t'

theorem Red.seqs_implies_pars {t t' : Term} : LeanSubst.Star Red t t' → LeanSubst.Star ParRed t t'

theorem Red.par_implies_seqs {t t' : Term} : t ~p> t' → LeanSubst.Star Red t t'

theorem Red.pars_implies_seqs {t t' : Term} : LeanSubst.Star ParRed t t' → LeanSubst.Star Red t t'

theorem Red.pars_action_lift {t t' : Term} : LeanSubst.Star ParRed t t' → LeanSubst.Star (LeanSubst.ActionRed ParRed) (LeanSubst.su t) (LeanSubst.su t')

theorem Red.seqs_action_lift {t t' : Term} : LeanSubst.Star Red t t' → LeanSubst.Star (LeanSubst.ActionRed Red) (LeanSubst.su t) (LeanSubst.su t')

theorem Red.seqs_action_destruct {a : LeanSubst.Subst.Action Term} {t' : Term} : LeanSubst.Star (LeanSubst.ActionRed Red) a (LeanSubst.su t') → ∃ (t : Term), a = LeanSubst.su t ∧ LeanSubst.Star Red t t'

theorem Red.pars_action_iff_seqs_action {t t' : LeanSubst.Subst.Action Term} : LeanSubst.Star (LeanSubst.ActionRed ParRed) t t' ↔ LeanSubst.Star (LeanSubst.ActionRed Red) t t'

theorem Red.subst_arg {t : Term} {σ σ' : LeanSubst.Subst Term} : (∀ (x : Nat), LeanSubst.ActionRed Red (σ x) (σ' x)) → LeanSubst.Star Red t[σ] t[σ']

theorem Red.confluence {s t1 t2 : Term} : LeanSubst.Star Red s t1 → LeanSubst.Star Red s t2 → ∃ (t : Term), LeanSubst.Star Red t1 t ∧ LeanSubst.Star Red t2 t

instance Red.instSubstitutiveTerm : LeanSubst.Substitutive Red

instance Red.instHasConfluenceTerm : LeanSubst.HasConfluence Red

theorem Red.preservation_of_neutral_step {t t' : Term} : Neutral t → t ~> t' → Neutral t'

theorem Red.preservation_of_neutral {t t' : Term} : Neutral t → LeanSubst.Star Red t t' → Neutral t'