inductive Red : Term → Term → Prop

• beta {A : Ty} {b t : Term} : ((:λ[A] b) :@ t) ~> b[%t::LeanSubst.I]
• 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))

inductive RedSubstAction : LeanSubst.Subst.Action Term → LeanSubst.Subst.Action Term → Prop

• su {t t' : Term} : t ~> t' → %t ~s> %t'
• re {x : Nat} : #x ~s> #x

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'[%t'::LeanSubst.I]
• 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))

inductive ParRedSubstAction : LeanSubst.Subst.Action Term → LeanSubst.Subst.Action Term → Prop

• su {t t' : Term} : t ~p> t' → %t ~ps> %t'
• re {x : Nat} : #x ~ps> #x

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[%(ParRed.complete t)::LeanSubst.I]
• ParRed.complete (f :@ a) = ParRed.complete f :@ ParRed.complete a
• ParRed.complete (:λ[A] t) = :λ[A] ParRed.complete t
• ParRed.complete (Term.var x_1) = Term.var 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) : σ x ~ps> σ' x → (σ ∘ r.to) x ~ps> (σ' ∘ r.to) x

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

theorem ParRed.hsubst {t t' : Term} {σ σ' : LeanSubst.Subst Term} : (∀ (x : Nat), σ x ~ps> σ' 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) : σ x ~s> σ' x → (σ ∘ r.to) x ~s> (σ' ∘ r.to) x

theorem Red.subst_red_lift {σ σ' : LeanSubst.Subst Term} : (∀ (x : Nat), σ x ~s> σ' x) → ∀ (x : Nat), σ.lift x ~s> σ'.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 ParRedSubstAction %t %t'

theorem Red.seqs_action_lift {t t' : Term} : LeanSubst.Star Red t t' → LeanSubst.Star RedSubstAction %t %t'

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

theorem Red.pars_action_iff_seqs_action {t t' : LeanSubst.Subst.Action Term} : LeanSubst.Star ParRedSubstAction t t' ↔ LeanSubst.Star RedSubstAction t t'

theorem Red.subst_arg {t : Term} {σ σ' : LeanSubst.Subst Term} : (∀ (x : Nat), σ x ~s> σ' 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'