inductive SnHeadRed : Term → Term → Prop

• beta {t : Term} {A : Ty} {b : Term} : LeanSubst.SN Red t → ((:λ[A] b) :@ t) ~>sn b[LeanSubst.su t::+0]
• app {f f' : Term} (a : Term) : f ~>sn f' → (f :@ a) ~>sn (f' :@ a)

def «term_~>sn_» : Lean.TrailingParserDescr

Equations

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

theorem SnHeadRed.red_compatible {t a b : Term} : t ~>sn a → t ~> b → a = b ∨ ∃ (z : Term), b ~>sn z ∧ LeanSubst.Star Red a z

theorem SN.subterm_app {f a : Term} : LeanSubst.SN Red (f :@ a) → LeanSubst.SN Red f ∧ LeanSubst.SN Red a

theorem SN.lam {t : Term} {A : Ty} : LeanSubst.SN Red t ↔ LeanSubst.SN Red (:λ[A] t)

theorem SN.neutral_app {f a : Term} : Neutral f → LeanSubst.SN Red f → LeanSubst.SN Red a → LeanSubst.SN Red (f :@ a)

theorem SN.weak_head_expansion {t b : Term} {A : Ty} : LeanSubst.SN Red t → LeanSubst.SN Red b[LeanSubst.su t::+0] → LeanSubst.SN Red ((:λ[A] b) :@ t)

theorem SN.red_app_preservation {f f' a : Term} : f ~>sn f' → LeanSubst.SN Red f → LeanSubst.SN Red a → LeanSubst.SN Red (f' :@ a) → LeanSubst.SN Red (f :@ a)

theorem SN.backward_closure {t' t : Term} : LeanSubst.SN Red t' → t ~>sn t' → LeanSubst.SN Red t

inductive SnVariant : Type

• neu : SnVariant
• nor : SnVariant
• red : SnVariant

@[reducible, inline]

abbrev SnIndices : SnVariant → Type

Equations

• SnIndices SnVariant.neu = Term
• SnIndices SnVariant.nor = Term
• SnIndices SnVariant.red = (Term × Term)

inductive SNi (v : SnVariant) : SnIndices v → Prop

• var {x : Nat} : SNi SnVariant.neu #x
• app {s : SnIndices SnVariant.neu} {t : SnIndices SnVariant.nor} : SNi SnVariant.neu s → SNi SnVariant.nor t → SNi SnVariant.neu (s :@ t)
• lam {t : SnIndices SnVariant.nor} {A : Ty} : SNi SnVariant.nor t → SNi SnVariant.nor (:λ[A] t)
• neu {t : SnIndices SnVariant.neu} : SNi SnVariant.neu t → SNi SnVariant.nor t
• red {t t' : Term} : SNi SnVariant.red (t, t') → SNi SnVariant.nor t' → SNi SnVariant.nor t
• beta {t : SnIndices SnVariant.nor} {A : Ty} {b : Term} : SNi SnVariant.nor t → SNi SnVariant.red ((:λ[A] b) :@ t, b[LeanSubst.su t::+0])
• step {s s' t : Term} : SNi SnVariant.red (s, s') → SNi SnVariant.red (s :@ t, s' :@ t)

@[reducible, inline]

abbrev SNi.SnRenameLemmaType (r : LeanSubst.Ren) (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnRenameLemmaType r SnVariant.neu t = SNi SnVariant.neu t[↑r]
• SNi.SnRenameLemmaType r SnVariant.nor t = SNi SnVariant.nor t[↑r]
• SNi.SnRenameLemmaType r SnVariant.red (t, t') = SNi SnVariant.red (t[↑r], t'[↑r])

theorem SNi.rename {v : SnVariant} {i : SnIndices v} (r : LeanSubst.Ren) : SNi v i → SnRenameLemmaType r v i

@[reducible, inline]

abbrev SNi.SnAntiRenameLemmaType (r : LeanSubst.Ren) (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnAntiRenameLemmaType r SnVariant.neu t = ∀ (z : SnIndices SnVariant.neu), t = z[↑r] → SNi SnVariant.neu z
• SNi.SnAntiRenameLemmaType r SnVariant.nor t = ∀ (z : SnIndices SnVariant.nor), t = z[↑r] → SNi SnVariant.nor z
• SNi.SnAntiRenameLemmaType r SnVariant.red (t, t') = ∀ (z : Term), t = z[↑r] → ∃ (z' : Term), t' = z'[↑r] ∧ SNi SnVariant.red (z, z')

theorem SNi.antirename {v : SnVariant} {i : SnIndices v} (r : LeanSubst.Ren) : SNi v i → SnAntiRenameLemmaType r v i

@[reducible, inline]

abbrev SNi.SnBetaVarLemmaType (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnBetaVarLemmaType SnVariant.neu s = ∀ (t : Term) (x : Nat), s = t :@ #x → SNi SnVariant.neu t
• SNi.SnBetaVarLemmaType SnVariant.nor s = ∀ (t : Term) (x : Nat), s = t :@ #x → SNi SnVariant.nor t
• SNi.SnBetaVarLemmaType SnVariant.red x_2 = True

theorem SNi.beta_var {v : SnVariant} {i : SnIndices v} : SNi v i → SnBetaVarLemmaType v i

@[reducible, inline]

abbrev SNi.SnPropertyWeakenLemmaType (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnPropertyWeakenLemmaType SnVariant.neu t = Neutral t
• SNi.SnPropertyWeakenLemmaType SnVariant.nor t = True
• SNi.SnPropertyWeakenLemmaType SnVariant.red (t, t') = t ~> t'

theorem SNi.property_weaken {v : SnVariant} {i : SnIndices v} : SNi v i → SnPropertyWeakenLemmaType v i

@[reducible, inline]

abbrev SNi.SnSoundLemmaType (v : SnVariant) (i : SnIndices v) : Prop

Equations

• SNi.SnSoundLemmaType SnVariant.neu t = LeanSubst.SN Red t
• SNi.SnSoundLemmaType SnVariant.nor t = LeanSubst.SN Red t
• SNi.SnSoundLemmaType SnVariant.red (t, t') = t ~>sn t'

theorem SNi.sound {v : SnVariant} {i : SnIndices v} : SNi v i → SnSoundLemmaType v i