From 5393822ad3f1caee98e34b35e6cf3d06ae5ddd04 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 12:44:33 -0600
Subject: [PATCH 01/18] add reference

---
 references.bib | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/references.bib b/references.bib
index 18281428d..c7b00e4d1 100644
--- a/references.bib
+++ b/references.bib
@@ -483,4 +483,12 @@ @book{Sipser2013
   edition   = {3rd},
   publisher = {Cengage Learning},
   year      = {2013}
+}
+
+@mastersthesis{Copes2018,
+  author       = {Copes, Martín},
+  title        = {A machine-checked proof of the Standardization Theorem 
+                  in Lambda Calculus using multiple substitution},
+  school       = {Universidad ORT Uruguay},
+  year         = {2018}
 }
\ No newline at end of file

From 096ca56f16df410fb59f5d0810eb858b26d05e3d Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 13:00:13 -0600
Subject: [PATCH 02/18] update Cslib

---
 Cslib.lean                                    |  1 +
 .../Untyped/LeftmostReduction.lean            | 35 +++++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean

diff --git a/Cslib.lean b/Cslib.lean
index 43c374ae7..d99833bb9 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -138,6 +138,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
new file mode 100644
index 000000000..79ac307fb
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Maximiliano Onofre Martínez. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Maximiliano Onofre Martínez
+-/
+
+module
+
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
+
+/-! # The Leftmost Reduction Theorem
+
+## Reference
+
+* [M. Copes, *A machine-checked proof of the Standardization Theorem in λ-calculus*][Copes2018]
+
+-/
+
+@[expose] public section
+
+set_option linter.unusedDecidableInType false
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.LocallyNameless.Untyped.Term
+
+
+
+end LambdaCalculus.LocallyNameless.Untyped.Term
+
+end Cslib

From 8582753d6be847ba82ca10c0c48af2e377d23ea4 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 13:58:27 -0600
Subject: [PATCH 03/18] add leftmost reduction definitions

---
 .../Untyped/LeftmostReduction.lean            | 36 ++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 79ac307fb..a70478575 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -28,7 +28,41 @@ variable {Var : Type u}
 
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
-
+/-- The number of β-redexes occurring in a term. -/
+def countRedexes : Term Var → Nat
+| fvar _        => 0
+| bvar _        => 0
+| abs m         => countRedexes m
+| app (abs m) n => (countRedexes (abs m) + countRedexes n) + 1
+| app m n       => countRedexes m + countRedexes n
+
+/-- A term is in normal form when it contains no β-redexes. -/
+def NormalForm (m : Term Var) : Prop := countRedexes m = 0
+
+/-- `IsAbs m` holds when `m` is an abstraction. -/
+inductive IsAbs : Term Var → Prop
+| abs (m : Term Var) : IsAbs (abs m)
+
+/-- `BetaAt M N i` reduces the redex at position `i` of `M` to obtain `N`;
+    positions are counted from left to right. -/
+inductive BetaAt : Term Var → Term Var → Nat → Prop
+/-- The outermost redex sits at position `0`. -/
+| outer : LC (abs M) → LC N → BetaAt (app (abs M) N) (M ^ N) 0
+/-- Reducing a non-abstraction operator keeps the position. -/
+| appNoAbsL : BetaAt M M' i → ¬ IsAbs M → BetaAt (app M N) (app M' N) i
+/-- Reducing an abstraction operator advances the position by one. -/
+| appAbsL : BetaAt M M' i → IsAbs M → BetaAt (app M N) (app M' N) (i + 1)
+/-- Reducing the operand adds the redex count of a non-abstraction operator. -/
+| appNoAbsR : BetaAt M M' i → ¬ IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N)
+/-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
+| appAbsR : BetaAt M M' i → IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N + 1)
+/-- Reducing under a binder keeps the position. -/
+| abs (xs : Finset Var) :
+    (∀ x ∉ xs, BetaAt (M ^ fvar x) (M' ^ fvar x) i) → BetaAt (abs M) (abs M') i
+
+/-- Leftmost reduction: a β-reduction contracting the redex at position 0. -/
+@[reduction_sys "ℓ"]
+abbrev Leftmost (M N : Term Var) : Prop := BetaAt M N 0
 
 end LambdaCalculus.LocallyNameless.Untyped.Term
 

From 95315858c4474464bac4ba990565cf41071be32a Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 22:19:30 -0600
Subject: [PATCH 04/18] add redex counting and normal form lemmas

---
 .../Untyped/LeftmostReduction.lean            | 48 ++++++++++++++++++-
 1 file changed, 46 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index a70478575..e2ee9aba3 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -49,11 +49,11 @@ inductive BetaAt : Term Var → Term Var → Nat → Prop
 /-- The outermost redex sits at position `0`. -/
 | outer : LC (abs M) → LC N → BetaAt (app (abs M) N) (M ^ N) 0
 /-- Reducing a non-abstraction operator keeps the position. -/
-| appNoAbsL : BetaAt M M' i → ¬ IsAbs M → BetaAt (app M N) (app M' N) i
+| appNoAbsL : BetaAt M M' i → ¬IsAbs M → BetaAt (app M N) (app M' N) i
 /-- Reducing an abstraction operator advances the position by one. -/
 | appAbsL : BetaAt M M' i → IsAbs M → BetaAt (app M N) (app M' N) (i + 1)
 /-- Reducing the operand adds the redex count of a non-abstraction operator. -/
-| appNoAbsR : BetaAt M M' i → ¬ IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N)
+| appNoAbsR : BetaAt M M' i → ¬IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N)
 /-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
 | appAbsR : BetaAt M M' i → IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N + 1)
 /-- Reducing under a binder keeps the position. -/
@@ -64,6 +64,50 @@ inductive BetaAt : Term Var → Term Var → Nat → Prop
 @[reduction_sys "ℓ"]
 abbrev Leftmost (M N : Term Var) : Prop := BetaAt M N 0
 
+variable {L L' M M' N : Term Var} {i : Nat}
+
+/-- Opening with a free variable preserves the number of redexes. -/
+lemma countRedexes_openRec_fvar (M : Term Var) (k : Nat) (x : Var) :
+    countRedexes (M⟦k ↝ fvar x⟧) = countRedexes M := by
+  induction M generalizing k with
+  | bvar j => simp only [openRec_bvar]; split <;> rfl
+  | fvar => rfl
+  | abs M ih => grind [openRec_abs, countRedexes]
+  | app L R ihL ihR => cases L <;> grind [countRedexes, openRec_bvar, openRec_app, openRec_abs]
+
+/-- In a normal-form application, both sides are normal and the operator is not an
+    abstraction. -/
+lemma NormalForm.app_inv (h : NormalForm (app L M)) :
+    ¬IsAbs L ∧ NormalForm L ∧ NormalForm M := by
+  cases L <;> grind [NormalForm, countRedexes, IsAbs]
+
+/-- The body of a normal-form abstraction opens to a normal form. -/
+lemma NormalForm.abs_open {x : Var} (h : NormalForm (abs M)) : NormalForm (M ^ fvar x) := by
+  have e : countRedexes (M ^ fvar x) = countRedexes M := countRedexes_openRec_fvar M 0 x
+  rw [NormalForm, e]
+  exact h
+
+/-- The source of a Call-by-Name step is never an abstraction. -/
+lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
+  intro ha
+  cases ha
+  trivial
+
+variable [DecidableEq Var]
+
+/-- Renaming a free variable preserves the number of redexes. -/
+lemma countRedexes_subst_fvar (M : Term Var) (x y : Var) :
+    countRedexes (M[x := fvar y]) = countRedexes M := by
+  induction M with
+  | fvar z => simp only [subst_fvar]; split <;> rfl
+  | bvar => rfl
+  | abs M ih => grind [countRedexes]
+  | app L R ihL ihR => cases L <;> grind [countRedexes]
+
+/-- Renaming a free variable preserves being an abstraction. -/
+lemma isAbs_subst_fvar {x y : Var} : IsAbs (M[x := fvar y]) ↔ IsAbs M := by
+  cases M <;> grind [IsAbs]
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From 20fb8ed2204d39db9052c4be8c55857c4e9c6baf Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 22:20:43 -0600
Subject: [PATCH 05/18] add basic properties of BetaAt

---
 .../Untyped/LeftmostReduction.lean            | 68 +++++++++++++++++++
 1 file changed, 68 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index e2ee9aba3..14e5728e0 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -87,6 +87,18 @@ lemma NormalForm.abs_open {x : Var} (h : NormalForm (abs M)) : NormalForm (M ^ f
   rw [NormalForm, e]
   exact h
 
+/-- Contracting a redex of an abstraction yields an abstraction. -/
+lemma BetaAt.isAbs_r (h : BetaAt M N i) (ha : IsAbs M) : IsAbs N := by
+  cases ha
+  cases h
+  exact .abs _
+
+/-- Reducing the operand across a non-abstraction normal form keeps the position. -/
+lemma BetaAt.app_r_cong (h : BetaAt M M' i) (hL : NormalForm L) (hna : ¬IsAbs L) :
+    BetaAt (app L M) (app L M') i := by
+  have := h.appNoAbsR hna
+  rwa [hL] at this
+
 /-- The source of a Call-by-Name step is never an abstraction. -/
 lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
   intro ha
@@ -108,6 +120,62 @@ lemma countRedexes_subst_fvar (M : Term Var) (x y : Var) :
 lemma isAbs_subst_fvar {x y : Var} : IsAbs (M[x := fvar y]) ↔ IsAbs M := by
   cases M <;> grind [IsAbs]
 
+variable [HasFresh Var]
+
+/-- Renaming a free variable preserves the position of the contracted redex. -/
+lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
+    BetaAt (M[x := fvar y]) (M'[x := fvar y]) i := by
+  induction h
+  case outer lcm lcn =>
+    rw [subst_app, subst_abs, subst_open x (fvar y) _ _ (.fvar y)]
+    exact .outer (subst_lc lcm (.fvar y)) (subst_lc lcn (.fvar y))
+  case appNoAbsL _ hna ih =>
+    simp only [subst_app]
+    exact .appNoAbsL ih (mt isAbs_subst_fvar.mp hna)
+  case appAbsL _ ha ih =>
+    simp only [subst_app]
+    exact .appAbsL ih (isAbs_subst_fvar.mpr ha)
+  case appNoAbsR M M' i N _ hna ih =>
+    simp only [subst_app, ← countRedexes_subst_fvar N x y]
+    exact .appNoAbsR ih (mt isAbs_subst_fvar.mp hna)
+  case appAbsR M M' i N _ ha ih =>
+    simp only [subst_app, ← countRedexes_subst_fvar N x y]
+    exact .appAbsR ih (isAbs_subst_fvar.mpr ha)
+  case abs M M' i xs _ ih =>
+    simp only [subst_abs]
+    apply BetaAt.abs <| free_union [fv] Var
+    intro z hz
+    have hzx : x ≠ z := by aesop
+    rw [← subst_open_var z x (fvar y) M hzx (.fvar y),
+      ← subst_open_var z x (fvar y) M' hzx (.fvar y)]
+    exact ih z (by aesop)
+
+/-- Contracting a redex preserves local closure. -/
+lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
+  induction h with
+  | outer lcm lcn => exact beta_lc lcm lcn
+  | appNoAbsL _ _ ih | appAbsL _ _ ih =>
+    cases lc with
+    | app lcL lcR => exact .app (ih lcL) lcR
+  | appNoAbsR _ _ ih | appAbsR _ _ ih =>
+    cases lc with
+    | app lcL lcR => exact .app lcL (ih lcR)
+  | abs xs _ ih =>
+    cases lc with
+    | abs ys _ hbody =>
+      apply LC.abs (xs ∪ ys)
+      intro z hz
+      exact ih z (by aesop) (hbody z (by aesop))
+
+/-- Closing a variable and abstracting preserves the position of the contracted redex. -/
+lemma BetaAt.abs_close {x : Var} (h : BetaAt M M' i) (lc : LC M) :
+    BetaAt (M⟦0 ↜ x⟧.abs) (M'⟦0 ↜ x⟧.abs) i := by
+  apply BetaAt.abs ∅
+  intro z _
+  have lc' := h.lc_r lc
+  have hr : BetaAt (M[x := fvar z]) (M'[x := fvar z]) i := h.rename x z
+  grind
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From b722eff9204c9c1574a85a4324e02bbe78d79016 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 22:22:27 -0600
Subject: [PATCH 06/18] add lemmas for leftmost reduction

---
 .../Untyped/LeftmostReduction.lean            | 66 +++++++++++++++++++
 1 file changed, 66 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 14e5728e0..e5b8ae487 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -93,18 +93,61 @@ lemma BetaAt.isAbs_r (h : BetaAt M N i) (ha : IsAbs M) : IsAbs N := by
   cases h
   exact .abs _
 
+/-- Leftmost reduction preserves being an abstraction. -/
+lemma Leftmost.steps_isAbs_r (h : M ↠ℓ N) (ha : IsAbs M) : IsAbs N := by
+  induction h with
+  | refl => exact ha
+  | tail _ step ih => exact step.isAbs_r ih
+
+/-- Left congruence for leftmost reduction, provided the target is not an abstraction. -/
+lemma Leftmost.steps_app_l_cong (h : L ↠ℓ L') (hna : ¬IsAbs L') :
+    app L M ↠ℓ app L' M := by
+  induction h
+  case refl => rfl
+  case tail P _ _ step ih =>
+    have hnb : ¬IsAbs P := mt step.isAbs_r hna
+    exact (ih hnb).tail (step.appNoAbsL hnb)
+
 /-- Reducing the operand across a non-abstraction normal form keeps the position. -/
 lemma BetaAt.app_r_cong (h : BetaAt M M' i) (hL : NormalForm L) (hna : ¬IsAbs L) :
     BetaAt (app L M) (app L M') i := by
   have := h.appNoAbsR hna
   rwa [hL] at this
 
+/-- Right congruence for leftmost reduction, provided the operator is a non-abstraction
+    normal form. -/
+lemma Leftmost.steps_app_r_cong (h : M ↠ℓ M') (hL : NormalForm L) (hna : ¬IsAbs L) :
+    app L M ↠ℓ app L M' := by
+  induction h with
+  | refl => rfl
+  | tail _ step ih => exact ih.tail (step.app_r_cong hL hna)
+
+/-- Congruence for leftmost reduction on applications whose reduced operator is a
+    non-abstraction normal form. -/
+lemma Leftmost.steps_app_cong (hL : L ↠ℓ L') (hM : M ↠ℓ M')
+    (hnf : NormalForm L') (hna : ¬IsAbs L') : app L M ↠ℓ app L' M' :=
+  (steps_app_l_cong hL hna).trans (steps_app_r_cong hM hnf hna)
+
 /-- The source of a Call-by-Name step is never an abstraction. -/
 lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
   intro ha
   cases ha
   trivial
 
+/-- A single Call-by-Name step contracts the leftmost redex. -/
+lemma Leftmost.of_cbn_step (h : M ⭢ₙ N) : M ⭢ℓ N := by
+  induction h with
+  | base hb =>
+    cases hb with
+    | beta lcm lcn => exact .outer lcm lcn
+  | app _ hMN ih => exact .appNoAbsL ih (cbn_not_isAbs hMN)
+
+/-- Call-by-Name reduction is contained in leftmost reduction. -/
+lemma Leftmost.of_cbn (h : M ↠ₙ N) : M ↠ℓ N := by
+  induction h with
+  | refl => rfl
+  | tail _ step ih => exact ih.tail (of_cbn_step step)
+
 variable [DecidableEq Var]
 
 /-- Renaming a free variable preserves the number of redexes. -/
@@ -176,6 +219,29 @@ lemma BetaAt.abs_close {x : Var} (h : BetaAt M M' i) (lc : LC M) :
   have hr : BetaAt (M[x := fvar z]) (M'[x := fvar z]) i := h.rename x z
   grind
 
+/-- Leftmost reduction preserves local closure. -/
+lemma Leftmost.steps_lc_r (h : M ↠ℓ M') (lc : LC M) : LC M' := by
+  induction h with
+  | refl => exact lc
+  | tail _ step ih => exact step.lc_r ih
+
+/-- Leftmost reduction is preserved by closing a variable and abstracting. -/
+lemma Leftmost.steps_abs_close {x : Var} (h : M ↠ℓ M') (lc : LC M) :
+    (M⟦0 ↜ x⟧.abs) ↠ℓ (M'⟦0 ↜ x⟧.abs) := by
+  induction h with
+  | refl => rfl
+  | tail hs step ih => exact ih.tail (step.abs_close (Leftmost.steps_lc_r hs lc))
+
+/-- Cofinite congruence rule for leftmost reduction under an abstraction. -/
+lemma Leftmost.steps_abs_cong (xs : Finset Var)
+    (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ℓ (M' ^ fvar x)) (lc : LC (abs M)) :
+    abs M ↠ℓ abs M' := by
+  have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
+  rw [open_close w M 0 (by aesop), open_close w M' 0 (by aesop)]
+  have hstep := cofin w (by aesop)
+  have hlc := beta_lc lc (.fvar w)
+  exact Leftmost.steps_abs_close hstep hlc
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From 68118496cb7044d64e1e81a7cc520b86e4df1d91 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Tue, 7 Jul 2026 22:23:02 -0600
Subject: [PATCH 07/18] add leftmost reduction theorem

---
 .../Untyped/LeftmostReduction.lean            | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index e5b8ae487..4c4124c54 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -242,6 +242,30 @@ lemma Leftmost.steps_abs_cong (xs : Finset Var)
   have hlc := beta_lc lc (.fvar w)
   exact Leftmost.steps_abs_close hstep hlc
 
+/-- A standard reduction to a normal form is a leftmost reduction. -/
+theorem Leftmost.of_standard (h : M ⭢ₛ N) (hn : NormalForm N) : M ↠ℓ N := by
+  induction h
+  case fvar x => rfl
+  case app _ _ ihL ihM =>
+    obtain ⟨hna, hL', hM'⟩ := hn.app_inv
+    exact Leftmost.steps_app_cong (ihL hL') (ihM hM') hL' hna
+  case abs xs hbody ih =>
+    have lc := Standard.lc_l (Standard.abs xs hbody)
+    apply Leftmost.steps_abs_cong xs _ lc
+    intro x hx
+    exact ih x hx hn.abs_open
+  case rdx M N M' _ lcM lcN cbn stdP ih =>
+    have s1 : Term.app M N ↠ℓ Term.app (Term.abs M') N :=
+      of_cbn (CBN.steps_app_l_cong cbn lcN)
+    have s2 : Term.app (Term.abs M') N ⭢ℓ (M' ^ N) :=
+      BetaAt.outer (CBN.steps_lc_r lcM cbn) lcN
+    exact (s1.tail s2).trans (ih hn)
+
+/-- The leftmost reduction theorem: if a term β-reduces to a normal form, then leftmost
+    reduction reaches it. -/
+theorem Leftmost.normalization (lc : LC M) (h : M ↠βᶠ N) (hn : NormalForm N) : M ↠ℓ N :=
+  of_standard (.standardization lc h) hn
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From 45c8341409f57d21ae2362d29b20832daa398339 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 13:21:00 -0600
Subject: [PATCH 08/18] replace aesop with grind

---
 .../LocallyNameless/Untyped/LeftmostReduction.lean     | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 4c4124c54..31ee7f3de 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -188,10 +188,10 @@ lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
     simp only [subst_abs]
     apply BetaAt.abs <| free_union [fv] Var
     intro z hz
-    have hzx : x ≠ z := by aesop
+    have hzx : x ≠ z := by grind
     rw [← subst_open_var z x (fvar y) M hzx (.fvar y),
       ← subst_open_var z x (fvar y) M' hzx (.fvar y)]
-    exact ih z (by aesop)
+    exact ih z (by grind)
 
 /-- Contracting a redex preserves local closure. -/
 lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
@@ -208,7 +208,7 @@ lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
     | abs ys _ hbody =>
       apply LC.abs (xs ∪ ys)
       intro z hz
-      exact ih z (by aesop) (hbody z (by aesop))
+      exact ih z (by grind) (hbody z (by grind))
 
 /-- Closing a variable and abstracting preserves the position of the contracted redex. -/
 lemma BetaAt.abs_close {x : Var} (h : BetaAt M M' i) (lc : LC M) :
@@ -237,8 +237,8 @@ lemma Leftmost.steps_abs_cong (xs : Finset Var)
     (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ℓ (M' ^ fvar x)) (lc : LC (abs M)) :
     abs M ↠ℓ abs M' := by
   have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
-  rw [open_close w M 0 (by aesop), open_close w M' 0 (by aesop)]
-  have hstep := cofin w (by aesop)
+  rw [open_close w M 0 (by grind), open_close w M' 0 (by grind)]
+  have hstep := cofin w (by grind)
   have hlc := beta_lc lc (.fvar w)
   exact Leftmost.steps_abs_close hstep hlc
 

From ccddd9fb5ed3abdb47fd6d768fd4f87f3eb8fedd Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 13:22:48 -0600
Subject: [PATCH 09/18] use dot notation

---
 .../LocallyNameless/Untyped/LeftmostReduction.lean          | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 31ee7f3de..73340b39c 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -255,10 +255,8 @@ theorem Leftmost.of_standard (h : M ⭢ₛ N) (hn : NormalForm N) : M ↠ℓ N :
     intro x hx
     exact ih x hx hn.abs_open
   case rdx M N M' _ lcM lcN cbn stdP ih =>
-    have s1 : Term.app M N ↠ℓ Term.app (Term.abs M') N :=
-      of_cbn (CBN.steps_app_l_cong cbn lcN)
-    have s2 : Term.app (Term.abs M') N ⭢ℓ (M' ^ N) :=
-      BetaAt.outer (CBN.steps_lc_r lcM cbn) lcN
+    have s1 : M.app N ↠ℓ M'.abs.app N := of_cbn (CBN.steps_app_l_cong cbn lcN)
+    have s2 : M'.abs.app N ⭢ℓ M' ^ N := .outer (CBN.steps_lc_r lcM cbn) lcN
     exact (s1.tail s2).trans (ih hn)
 
 /-- The leftmost reduction theorem: if a term β-reduces to a normal form, then leftmost

From 6ed85b7c488a41f6141a1f6b1cbd69cb5c3b724a Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Wed, 8 Jul 2026 13:36:38 -0600
Subject: [PATCH 10/18] simplify BetaAt.rename proof

---
 .../LocallyNameless/Untyped/LeftmostReduction.lean        | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 73340b39c..33e3d5efb 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -170,19 +170,17 @@ lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
     BetaAt (M[x := fvar y]) (M'[x := fvar y]) i := by
   induction h
   case outer lcm lcn =>
-    rw [subst_app, subst_abs, subst_open x (fvar y) _ _ (.fvar y)]
+    rw [subst_open x (fvar y) _ _ (.fvar y)]
     exact .outer (subst_lc lcm (.fvar y)) (subst_lc lcn (.fvar y))
   case appNoAbsL _ hna ih =>
-    simp only [subst_app]
     exact .appNoAbsL ih (mt isAbs_subst_fvar.mp hna)
   case appAbsL _ ha ih =>
-    simp only [subst_app]
     exact .appAbsL ih (isAbs_subst_fvar.mpr ha)
   case appNoAbsR M M' i N _ hna ih =>
-    simp only [subst_app, ← countRedexes_subst_fvar N x y]
+    rw [← countRedexes_subst_fvar N x y]
     exact .appNoAbsR ih (mt isAbs_subst_fvar.mp hna)
   case appAbsR M M' i N _ ha ih =>
-    simp only [subst_app, ← countRedexes_subst_fvar N x y]
+    rw [← countRedexes_subst_fvar N x y]
     exact .appAbsR ih (isAbs_subst_fvar.mpr ha)
   case abs M M' i xs _ ih =>
     simp only [subst_abs]

From 59ce2ac8b5e117cd7280284b7e138e16ec4e3258 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Thu, 9 Jul 2026 09:48:44 -0600
Subject: [PATCH 11/18] rename NormalForm to BetaNormal

---
 .../Untyped/LeftmostReduction.lean            | 73 +++++++++----------
 1 file changed, 34 insertions(+), 39 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 33e3d5efb..62268ed23 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -37,7 +37,7 @@ def countRedexes : Term Var → Nat
 | app m n       => countRedexes m + countRedexes n
 
 /-- A term is in normal form when it contains no β-redexes. -/
-def NormalForm (m : Term Var) : Prop := countRedexes m = 0
+def BetaNormal (m : Term Var) : Prop := countRedexes m = 0
 
 /-- `IsAbs m` holds when `m` is an abstraction. -/
 inductive IsAbs : Term Var → Prop
@@ -77,14 +77,14 @@ lemma countRedexes_openRec_fvar (M : Term Var) (k : Nat) (x : Var) :
 
 /-- In a normal-form application, both sides are normal and the operator is not an
     abstraction. -/
-lemma NormalForm.app_inv (h : NormalForm (app L M)) :
-    ¬IsAbs L ∧ NormalForm L ∧ NormalForm M := by
-  cases L <;> grind [NormalForm, countRedexes, IsAbs]
+lemma BetaNormal.app_inv (h : BetaNormal (app L M)) :
+    ¬IsAbs L ∧ BetaNormal L ∧ BetaNormal M := by
+  cases L <;> grind [BetaNormal, countRedexes, IsAbs]
 
 /-- The body of a normal-form abstraction opens to a normal form. -/
-lemma NormalForm.abs_open {x : Var} (h : NormalForm (abs M)) : NormalForm (M ^ fvar x) := by
+lemma BetaNormal.abs_open {x : Var} (h : BetaNormal (abs M)) : BetaNormal (M ^ fvar x) := by
   have e : countRedexes (M ^ fvar x) = countRedexes M := countRedexes_openRec_fvar M 0 x
-  rw [NormalForm, e]
+  rw [BetaNormal, e]
   exact h
 
 /-- Contracting a redex of an abstraction yields an abstraction. -/
@@ -109,14 +109,14 @@ lemma Leftmost.steps_app_l_cong (h : L ↠ℓ L') (hna : ¬IsAbs L') :
     exact (ih hnb).tail (step.appNoAbsL hnb)
 
 /-- Reducing the operand across a non-abstraction normal form keeps the position. -/
-lemma BetaAt.app_r_cong (h : BetaAt M M' i) (hL : NormalForm L) (hna : ¬IsAbs L) :
+lemma BetaAt.app_r_cong (h : BetaAt M M' i) (hL : BetaNormal L) (hna : ¬IsAbs L) :
     BetaAt (app L M) (app L M') i := by
   have := h.appNoAbsR hna
   rwa [hL] at this
 
 /-- Right congruence for leftmost reduction, provided the operator is a non-abstraction
     normal form. -/
-lemma Leftmost.steps_app_r_cong (h : M ↠ℓ M') (hL : NormalForm L) (hna : ¬IsAbs L) :
+lemma Leftmost.steps_app_r_cong (h : M ↠ℓ M') (hL : BetaNormal L) (hna : ¬IsAbs L) :
     app L M ↠ℓ app L M' := by
   induction h with
   | refl => rfl
@@ -125,7 +125,7 @@ lemma Leftmost.steps_app_r_cong (h : M ↠ℓ M') (hL : NormalForm L) (hna : ¬I
 /-- Congruence for leftmost reduction on applications whose reduced operator is a
     non-abstraction normal form. -/
 lemma Leftmost.steps_app_cong (hL : L ↠ℓ L') (hM : M ↠ℓ M')
-    (hnf : NormalForm L') (hna : ¬IsAbs L') : app L M ↠ℓ app L' M' :=
+    (hnf : BetaNormal L') (hna : ¬IsAbs L') : app L M ↠ℓ app L' M' :=
   (steps_app_l_cong hL hna).trans (steps_app_r_cong hM hnf hna)
 
 /-- The source of a Call-by-Name step is never an abstraction. -/
@@ -137,10 +137,10 @@ lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
 /-- A single Call-by-Name step contracts the leftmost redex. -/
 lemma Leftmost.of_cbn_step (h : M ⭢ₙ N) : M ⭢ℓ N := by
   induction h with
-  | base hb =>
-    cases hb with
-    | beta lcm lcn => exact .outer lcm lcn
-  | app _ hMN ih => exact .appNoAbsL ih (cbn_not_isAbs hMN)
+  | base h_beta =>
+    cases h_beta with
+    | beta lc_M lc_N => exact .outer lc_M lc_N
+  | app _ step_M ih => exact .appNoAbsL ih (cbn_not_isAbs step_M)
 
 /-- Call-by-Name reduction is contained in leftmost reduction. -/
 lemma Leftmost.of_cbn (h : M ↠ₙ N) : M ↠ℓ N := by
@@ -169,9 +169,9 @@ variable [HasFresh Var]
 lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
     BetaAt (M[x := fvar y]) (M'[x := fvar y]) i := by
   induction h
-  case outer lcm lcn =>
+  case outer lc_M lc_N =>
     rw [subst_open x (fvar y) _ _ (.fvar y)]
-    exact .outer (subst_lc lcm (.fvar y)) (subst_lc lcn (.fvar y))
+    exact .outer (subst_lc lc_M (.fvar y)) (subst_lc lc_N (.fvar y))
   case appNoAbsL _ hna ih =>
     exact .appNoAbsL ih (mt isAbs_subst_fvar.mp hna)
   case appAbsL _ ha ih =>
@@ -182,31 +182,26 @@ lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
   case appAbsR M M' i N _ ha ih =>
     rw [← countRedexes_subst_fvar N x y]
     exact .appAbsR ih (isAbs_subst_fvar.mpr ha)
-  case abs M M' i xs _ ih =>
-    simp only [subst_abs]
+  case abs =>
     apply BetaAt.abs <| free_union [fv] Var
-    intro z hz
-    have hzx : x ≠ z := by grind
-    rw [← subst_open_var z x (fvar y) M hzx (.fvar y),
-      ← subst_open_var z x (fvar y) M' hzx (.fvar y)]
-    exact ih z (by grind)
+    grind
 
 /-- Contracting a redex preserves local closure. -/
 lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
   induction h with
-  | outer lcm lcn => exact beta_lc lcm lcn
+  | outer lc_M lc_N => exact beta_lc lc_M lc_N
   | appNoAbsL _ _ ih | appAbsL _ _ ih =>
     cases lc with
-    | app lcL lcR => exact .app (ih lcL) lcR
+    | app lc_L lc_R => exact .app (ih lc_L) lc_R
   | appNoAbsR _ _ ih | appAbsR _ _ ih =>
     cases lc with
-    | app lcL lcR => exact .app lcL (ih lcR)
+    | app lc_L lc_R => exact .app lc_L (ih lc_R)
   | abs xs _ ih =>
     cases lc with
-    | abs ys _ hbody =>
+    | abs ys _ h_body =>
       apply LC.abs (xs ∪ ys)
       intro z hz
-      exact ih z (by grind) (hbody z (by grind))
+      exact ih z (by grind) (h_body z (by grind))
 
 /-- Closing a variable and abstracting preserves the position of the contracted redex. -/
 lemma BetaAt.abs_close {x : Var} (h : BetaAt M M' i) (lc : LC M) :
@@ -228,7 +223,7 @@ lemma Leftmost.steps_abs_close {x : Var} (h : M ↠ℓ M') (lc : LC M) :
     (M⟦0 ↜ x⟧.abs) ↠ℓ (M'⟦0 ↜ x⟧.abs) := by
   induction h with
   | refl => rfl
-  | tail hs step ih => exact ih.tail (step.abs_close (Leftmost.steps_lc_r hs lc))
+  | tail hs step ih => exact ih.tail (step.abs_close (steps_lc_r hs lc))
 
 /-- Cofinite congruence rule for leftmost reduction under an abstraction. -/
 lemma Leftmost.steps_abs_cong (xs : Finset Var)
@@ -238,28 +233,28 @@ lemma Leftmost.steps_abs_cong (xs : Finset Var)
   rw [open_close w M 0 (by grind), open_close w M' 0 (by grind)]
   have hstep := cofin w (by grind)
   have hlc := beta_lc lc (.fvar w)
-  exact Leftmost.steps_abs_close hstep hlc
+  exact steps_abs_close hstep hlc
 
 /-- A standard reduction to a normal form is a leftmost reduction. -/
-theorem Leftmost.of_standard (h : M ⭢ₛ N) (hn : NormalForm N) : M ↠ℓ N := by
+theorem Leftmost.of_standard (h : M ⭢ₛ N) (hn : BetaNormal N) : M ↠ℓ N := by
   induction h
   case fvar x => rfl
   case app _ _ ihL ihM =>
-    obtain ⟨hna, hL', hM'⟩ := hn.app_inv
-    exact Leftmost.steps_app_cong (ihL hL') (ihM hM') hL' hna
-  case abs xs hbody ih =>
-    have lc := Standard.lc_l (Standard.abs xs hbody)
-    apply Leftmost.steps_abs_cong xs _ lc
+    have ⟨hna, hL', hM'⟩ := hn.app_inv
+    exact steps_app_cong (ihL hL') (ihM hM') hL' hna
+  case abs xs h_body ih =>
+    have lc := (Standard.abs xs h_body).lc_l
+    apply steps_abs_cong xs _ lc
     intro x hx
     exact ih x hx hn.abs_open
-  case rdx M N M' _ lcM lcN cbn stdP ih =>
-    have s1 : M.app N ↠ℓ M'.abs.app N := of_cbn (CBN.steps_app_l_cong cbn lcN)
-    have s2 : M'.abs.app N ⭢ℓ M' ^ N := .outer (CBN.steps_lc_r lcM cbn) lcN
+  case rdx M N M' _ lc_M lc_N cbn std_P ih =>
+    have s1 : M.app N ↠ℓ M'.abs.app N := of_cbn (CBN.steps_app_l_cong cbn lc_N)
+    have s2 : M'.abs.app N ⭢ℓ M' ^ N := .outer (CBN.steps_lc_r lc_M cbn) lc_N
     exact (s1.tail s2).trans (ih hn)
 
 /-- The leftmost reduction theorem: if a term β-reduces to a normal form, then leftmost
     reduction reaches it. -/
-theorem Leftmost.normalization (lc : LC M) (h : M ↠βᶠ N) (hn : NormalForm N) : M ↠ℓ N :=
+theorem Leftmost.normalization (lc : LC M) (h : M ↠βᶠ N) (hn : BetaNormal N) : M ↠ℓ N :=
   of_standard (.standardization lc h) hn
 
 end LambdaCalculus.LocallyNameless.Untyped.Term

From 396bb04e0297d72813381c32b71da4f1a312d472 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Sat, 11 Jul 2026 14:13:31 -0600
Subject: [PATCH 12/18] add standard sequences and equivalence with Standard

---
 .../Untyped/LeftmostReduction.lean            | 124 +------
 .../Untyped/StandardReduction.lean            | 311 +++++++++++++++++-
 2 files changed, 310 insertions(+), 125 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 62268ed23..4ac6e473e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -28,53 +28,15 @@ variable {Var : Type u}
 
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
-/-- The number of β-redexes occurring in a term. -/
-def countRedexes : Term Var → Nat
-| fvar _        => 0
-| bvar _        => 0
-| abs m         => countRedexes m
-| app (abs m) n => (countRedexes (abs m) + countRedexes n) + 1
-| app m n       => countRedexes m + countRedexes n
-
 /-- A term is in normal form when it contains no β-redexes. -/
 def BetaNormal (m : Term Var) : Prop := countRedexes m = 0
 
-/-- `IsAbs m` holds when `m` is an abstraction. -/
-inductive IsAbs : Term Var → Prop
-| abs (m : Term Var) : IsAbs (abs m)
-
-/-- `BetaAt M N i` reduces the redex at position `i` of `M` to obtain `N`;
-    positions are counted from left to right. -/
-inductive BetaAt : Term Var → Term Var → Nat → Prop
-/-- The outermost redex sits at position `0`. -/
-| outer : LC (abs M) → LC N → BetaAt (app (abs M) N) (M ^ N) 0
-/-- Reducing a non-abstraction operator keeps the position. -/
-| appNoAbsL : BetaAt M M' i → ¬IsAbs M → BetaAt (app M N) (app M' N) i
-/-- Reducing an abstraction operator advances the position by one. -/
-| appAbsL : BetaAt M M' i → IsAbs M → BetaAt (app M N) (app M' N) (i + 1)
-/-- Reducing the operand adds the redex count of a non-abstraction operator. -/
-| appNoAbsR : BetaAt M M' i → ¬IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N)
-/-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
-| appAbsR : BetaAt M M' i → IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N + 1)
-/-- Reducing under a binder keeps the position. -/
-| abs (xs : Finset Var) :
-    (∀ x ∉ xs, BetaAt (M ^ fvar x) (M' ^ fvar x) i) → BetaAt (abs M) (abs M') i
-
 /-- Leftmost reduction: a β-reduction contracting the redex at position 0. -/
 @[reduction_sys "ℓ"]
 abbrev Leftmost (M N : Term Var) : Prop := BetaAt M N 0
 
 variable {L L' M M' N : Term Var} {i : Nat}
 
-/-- Opening with a free variable preserves the number of redexes. -/
-lemma countRedexes_openRec_fvar (M : Term Var) (k : Nat) (x : Var) :
-    countRedexes (M⟦k ↝ fvar x⟧) = countRedexes M := by
-  induction M generalizing k with
-  | bvar j => simp only [openRec_bvar]; split <;> rfl
-  | fvar => rfl
-  | abs M ih => grind [openRec_abs, countRedexes]
-  | app L R ihL ihR => cases L <;> grind [countRedexes, openRec_bvar, openRec_app, openRec_abs]
-
 /-- In a normal-form application, both sides are normal and the operator is not an
     abstraction. -/
 lemma BetaNormal.app_inv (h : BetaNormal (app L M)) :
@@ -87,12 +49,6 @@ lemma BetaNormal.abs_open {x : Var} (h : BetaNormal (abs M)) : BetaNormal (M ^ f
   rw [BetaNormal, e]
   exact h
 
-/-- Contracting a redex of an abstraction yields an abstraction. -/
-lemma BetaAt.isAbs_r (h : BetaAt M N i) (ha : IsAbs M) : IsAbs N := by
-  cases ha
-  cases h
-  exact .abs _
-
 /-- Leftmost reduction preserves being an abstraction. -/
 lemma Leftmost.steps_isAbs_r (h : M ↠ℓ N) (ha : IsAbs M) : IsAbs N := by
   induction h with
@@ -128,89 +84,13 @@ lemma Leftmost.steps_app_cong (hL : L ↠ℓ L') (hM : M ↠ℓ M')
     (hnf : BetaNormal L') (hna : ¬IsAbs L') : app L M ↠ℓ app L' M' :=
   (steps_app_l_cong hL hna).trans (steps_app_r_cong hM hnf hna)
 
-/-- The source of a Call-by-Name step is never an abstraction. -/
-lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
-  intro ha
-  cases ha
-  trivial
-
-/-- A single Call-by-Name step contracts the leftmost redex. -/
-lemma Leftmost.of_cbn_step (h : M ⭢ₙ N) : M ⭢ℓ N := by
-  induction h with
-  | base h_beta =>
-    cases h_beta with
-    | beta lc_M lc_N => exact .outer lc_M lc_N
-  | app _ step_M ih => exact .appNoAbsL ih (cbn_not_isAbs step_M)
-
 /-- Call-by-Name reduction is contained in leftmost reduction. -/
 lemma Leftmost.of_cbn (h : M ↠ₙ N) : M ↠ℓ N := by
   induction h with
   | refl => rfl
-  | tail _ step ih => exact ih.tail (of_cbn_step step)
-
-variable [DecidableEq Var]
-
-/-- Renaming a free variable preserves the number of redexes. -/
-lemma countRedexes_subst_fvar (M : Term Var) (x y : Var) :
-    countRedexes (M[x := fvar y]) = countRedexes M := by
-  induction M with
-  | fvar z => simp only [subst_fvar]; split <;> rfl
-  | bvar => rfl
-  | abs M ih => grind [countRedexes]
-  | app L R ihL ihR => cases L <;> grind [countRedexes]
-
-/-- Renaming a free variable preserves being an abstraction. -/
-lemma isAbs_subst_fvar {x y : Var} : IsAbs (M[x := fvar y]) ↔ IsAbs M := by
-  cases M <;> grind [IsAbs]
-
-variable [HasFresh Var]
-
-/-- Renaming a free variable preserves the position of the contracted redex. -/
-lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
-    BetaAt (M[x := fvar y]) (M'[x := fvar y]) i := by
-  induction h
-  case outer lc_M lc_N =>
-    rw [subst_open x (fvar y) _ _ (.fvar y)]
-    exact .outer (subst_lc lc_M (.fvar y)) (subst_lc lc_N (.fvar y))
-  case appNoAbsL _ hna ih =>
-    exact .appNoAbsL ih (mt isAbs_subst_fvar.mp hna)
-  case appAbsL _ ha ih =>
-    exact .appAbsL ih (isAbs_subst_fvar.mpr ha)
-  case appNoAbsR M M' i N _ hna ih =>
-    rw [← countRedexes_subst_fvar N x y]
-    exact .appNoAbsR ih (mt isAbs_subst_fvar.mp hna)
-  case appAbsR M M' i N _ ha ih =>
-    rw [← countRedexes_subst_fvar N x y]
-    exact .appAbsR ih (isAbs_subst_fvar.mpr ha)
-  case abs =>
-    apply BetaAt.abs <| free_union [fv] Var
-    grind
-
-/-- Contracting a redex preserves local closure. -/
-lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
-  induction h with
-  | outer lc_M lc_N => exact beta_lc lc_M lc_N
-  | appNoAbsL _ _ ih | appAbsL _ _ ih =>
-    cases lc with
-    | app lc_L lc_R => exact .app (ih lc_L) lc_R
-  | appNoAbsR _ _ ih | appAbsR _ _ ih =>
-    cases lc with
-    | app lc_L lc_R => exact .app lc_L (ih lc_R)
-  | abs xs _ ih =>
-    cases lc with
-    | abs ys _ h_body =>
-      apply LC.abs (xs ∪ ys)
-      intro z hz
-      exact ih z (by grind) (h_body z (by grind))
+  | tail _ step ih => exact ih.tail (BetaAt.of_cbn_step step)
 
-/-- Closing a variable and abstracting preserves the position of the contracted redex. -/
-lemma BetaAt.abs_close {x : Var} (h : BetaAt M M' i) (lc : LC M) :
-    BetaAt (M⟦0 ↜ x⟧.abs) (M'⟦0 ↜ x⟧.abs) i := by
-  apply BetaAt.abs ∅
-  intro z _
-  have lc' := h.lc_r lc
-  have hr : BetaAt (M[x := fvar z]) (M'[x := fvar z]) i := h.rename x z
-  grind
+variable [DecidableEq Var] [HasFresh Var]
 
 /-- Leftmost reduction preserves local closure. -/
 lemma Leftmost.steps_lc_r (h : M ↠ℓ M') (lc : LC M) : LC M' := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index e9cfe09ec..d00cf8b24 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -10,9 +10,10 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 
 /-! # Standard Reduction and the Standardization Theorem
 
-## Reference
+## References
 
 * [B. Calisto, *Formalization in Coq of the Standardization Theorem for λ-calculus*][Calisto2022]
+* [M. Copes, *A machine-checked proof of the Standardization Theorem in λ-calculus*][Copes2018]
 
 -/
 
@@ -28,6 +29,43 @@ variable {Var : Type u}
 
 namespace LambdaCalculus.LocallyNameless.Untyped.Term
 
+/-- The number of β-redexes occurring in a term. -/
+def countRedexes : Term Var → Nat
+| fvar _        => 0
+| bvar _        => 0
+| abs m         => countRedexes m
+| app (abs m) n => (countRedexes (abs m) + countRedexes n) + 1
+| app m n       => countRedexes m + countRedexes n
+
+/-- `IsAbs m` holds when `m` is an abstraction. -/
+inductive IsAbs : Term Var → Prop
+| abs (m : Term Var) : IsAbs (abs m)
+
+/-- `BetaAt M N i` reduces the redex at position `i` of `M` to obtain `N`;
+    positions are counted from left to right. -/
+inductive BetaAt : Term Var → Term Var → Nat → Prop
+/-- The outermost redex sits at position `0`. -/
+| outer : LC (abs M) → LC N → BetaAt (app (abs M) N) (M ^ N) 0
+/-- Reducing a non-abstraction operator keeps the position. -/
+| appNoAbsL : BetaAt M M' i → ¬IsAbs M → BetaAt (app M N) (app M' N) i
+/-- Reducing an abstraction operator advances the position by one. -/
+| appAbsL : BetaAt M M' i → IsAbs M → BetaAt (app M N) (app M' N) (i + 1)
+/-- Reducing the operand adds the redex count of a non-abstraction operator. -/
+| appNoAbsR : BetaAt M M' i → ¬IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N)
+/-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
+| appAbsR : BetaAt M M' i → IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N + 1)
+/-- Reducing under a binder keeps the position. -/
+| abs (xs : Finset Var) :
+    (∀ x ∉ xs, BetaAt (M ^ fvar x) (M' ^ fvar x) i) → BetaAt (abs M) (abs M') i
+
+/-- A standard β-reduction sequence from `M` to `N`: the contracted redex positions are
+    non-decreasing and all at least `n`. -/
+inductive StandardSeq : Nat → Term Var → Term Var → Prop
+/-- The empty sequence is standard for any lower bound. -/
+| refl : StandardSeq n M M
+/-- A first step at position `i ≥ n`, followed by a standard sequence bounded below by `i`. -/
+| head : BetaAt M P i → n ≤ i → StandardSeq i P N → StandardSeq n M N
+
 /-- The Standard reduction relation. -/
 @[reduction_sys "ₛ"]
 inductive Standard : Term Var → Term Var → Prop
@@ -41,7 +79,7 @@ inductive Standard : Term Var → Term Var → Prop
 /-- Standard reduction of a head redex. -/
 | rdx : LC m → LC n → m ↠ₙ (abs m') → Standard (m' ^ n) p → Standard (app m n) p
 
-variable {M N P M' N' : Term Var}
+variable {L L' M M' N N' P : Term Var} {i m n : Nat}
 
 /-- The left side of a standard reduction is locally closed. -/
 lemma Standard.lc_l (step : M ⭢ₛ N) : LC M := by
@@ -91,7 +129,179 @@ lemma Standard.cbn_trans (h1 : M ↠ₙ P) (h2 : P ⭢ₛ N) : M ⭢ₛ N := by
 lemma Standard.of_cbn (step : M ↠ₙ N) (lc_N : LC N) : M ⭢ₛ N :=
   cbn_trans step (lc_refl N lc_N)
 
-variable [DecidableEq Var] [HasFresh Var]
+/-- Opening with a free variable preserves the number of redexes. -/
+lemma countRedexes_openRec_fvar (M : Term Var) (k : Nat) (x : Var) :
+    countRedexes (M⟦k ↝ fvar x⟧) = countRedexes M := by
+  induction M generalizing k with
+  | bvar j => simp only [openRec_bvar]; split <;> rfl
+  | fvar => rfl
+  | abs M ih => grind [openRec_abs, countRedexes]
+  | app L R ihL ihR => cases L <;> grind [countRedexes, openRec_bvar, openRec_app, openRec_abs]
+
+/-- Contracting a redex of an abstraction yields an abstraction. -/
+lemma BetaAt.isAbs_r (h : BetaAt M N i) (ha : IsAbs M) : IsAbs N := by
+  cases ha
+  cases h
+  exact .abs _
+
+/-- The source of a Call-by-Name step is never an abstraction. -/
+lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
+  intro ha
+  cases ha
+  trivial
+
+/-- A single Call-by-Name step contracts the redex at position `0`. -/
+lemma BetaAt.of_cbn_step (h : M ⭢ₙ N) : BetaAt M N 0 := by
+  induction h with
+  | base h_beta =>
+    cases h_beta with
+    | beta lc_M lc_N => exact .outer lc_M lc_N
+  | app _ step_M ih => exact .appNoAbsL ih (cbn_not_isAbs step_M)
+
+/-- A standard sequence remains standard under a smaller lower bound. -/
+lemma StandardSeq.mono (h : StandardSeq n M N) (hmn : m ≤ n) : StandardSeq m M N := by
+  cases h with
+  | refl => exact .refl
+  | head step hni tail => exact .head step (le_trans hmn hni) tail
+
+/-- Standard sequences preserve being an abstraction. -/
+lemma StandardSeq.isAbs_r (h : StandardSeq n M N) (ha : IsAbs M) : IsAbs N := by
+  induction h with
+  | refl => exact ha
+  | head step _ _ ih => exact ih (step.isAbs_r ha)
+
+/-- A standard sequence stays standard when preceded by a Call-by-Name reduction. -/
+lemma StandardSeq.cbn_head (h : M ↠ₙ P) (hseq : StandardSeq 0 P N) :
+    StandardSeq 0 M N := by
+  induction h with
+  | refl => exact hseq
+  | tail _ step ih => exact ih (.head (BetaAt.of_cbn_step step) (Nat.le_refl 0) hseq)
+
+/-- Right congruence for standard sequences when the operator is an abstraction. -/
+lemma StandardSeq.app_r_abs (h : StandardSeq n M M') (ha : IsAbs L) :
+    StandardSeq (n + countRedexes L + 1) (app L M) (app L M') := by
+  induction h with
+  | refl => exact .refl
+  | head step hni tail ih => exact .head (step.appAbsR ha) (by omega) ih
+
+/-- Right congruence for standard sequences when the operator is a non-abstraction. -/
+lemma StandardSeq.app_r_noAbs (h : StandardSeq n M M') (hna : ¬IsAbs L) :
+    StandardSeq (n + countRedexes L) (app L M) (app L M') := by
+  induction h with
+  | refl => exact .refl
+  | head step hni tail ih => exact .head (step.appNoAbsR hna) (by omega) ih
+
+/-- Renaming a free variable preserves the number of redexes. -/
+lemma countRedexes_subst_fvar [DecidableEq Var] (M : Term Var) (x y : Var) :
+    countRedexes (M[x := fvar y]) = countRedexes M := by
+  induction M with
+  | fvar z => simp only [subst_fvar]; split <;> rfl
+  | bvar => rfl
+  | abs M ih => grind [countRedexes]
+  | app L R ihL ihR => cases L <;> grind [countRedexes]
+
+/-- Renaming a free variable preserves being an abstraction. -/
+lemma isAbs_subst_fvar [DecidableEq Var] {x y : Var} : IsAbs (M[x := fvar y]) ↔ IsAbs M := by
+  cases M <;> grind [IsAbs]
+
+/-- A `BetaAt` step is a full β-step. -/
+lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt M N i) (lc : LC M) : M ⭢βᶠ N := by
+  induction h with
+  | outer lc_M lc_N => exact .base (.beta lc_M lc_N)
+  | appNoAbsL _ _ ih | appAbsL _ _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .appR lc_R (ih lc_L)
+  | appNoAbsR _ _ ih | appAbsR _ _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .appL lc_L (ih lc_R)
+  | abs xs _ ih =>
+    cases lc with
+    | abs ys _ h_body =>
+      apply Xi.abs (xs ∪ ys)
+      intro z hz
+      exact ih z (by grind) (h_body z (by grind))
+
+variable [HasFresh Var]
+
+/-- The position of a contracted redex is at most the redex count of the result. -/
+lemma BetaAt.le_countRedexes (h : BetaAt M N i) : i ≤ countRedexes N := by
+  induction h
+  case outer => exact Nat.zero_le _
+  case appNoAbsL K' _ _ _ _ _ => cases K' <;> grind [countRedexes]
+  case appAbsL step ha _ =>
+    cases step.isAbs_r ha
+    grind [countRedexes]
+  case appNoAbsR P _ _ _ => cases P <;> grind [countRedexes]
+  case appAbsR ha _ =>
+    cases ha
+    grind [countRedexes]
+  case abs xs _ _ =>
+    have := fresh_exists xs
+    grind [countRedexes_openRec_fvar, countRedexes]
+
+/-- In a nonempty standard sequence the lower bound is at most the target's redex count. -/
+lemma StandardSeq.bound_le (h : StandardSeq n M N) : n ≤ countRedexes N ∨ M = N := by
+  induction h with
+  | refl => exact .inr rfl
+  | head step hni _ ih =>
+    left
+    rcases ih with hle | rfl
+    · omega
+    · exact le_trans hni step.le_countRedexes
+
+/-- The leading position of a standard sequence is at most the redex count of its target. -/
+lemma StandardSeq.head_le (step : BetaAt M P i) (tail : StandardSeq i P N) :
+    i ≤ countRedexes N := by
+  rcases tail.bound_le with h | rfl
+  · exact h
+  · exact step.le_countRedexes
+
+/-- The reduction of an abstraction operator followed by an application sequence
+  is a standard sequence. -/
+lemma StandardSeq.app_l_trans_abs (hL : StandardSeq n L L') (ha : IsAbs L)
+    (hm : countRedexes L' + 1 ≤ m) (hnm : n + 1 ≤ m)
+    (hM : StandardSeq m (app L' M) (app L' M')) :
+    StandardSeq (n + 1) (app L M) (app L' M') := by
+  induction hL
+  case refl => exact hM.mono hnm
+  case head K P i _ N' step hni tail ih =>
+    have hseam : i ≤ countRedexes N' := StandardSeq.head_le step tail
+    exact .head (step.appAbsL ha) (by omega) (ih (step.isAbs_r ha) hm (by omega) hM)
+
+/-- The reduction of an operator ending in an abstraction followed by an application sequence
+  is a standard sequence. -/
+lemma StandardSeq.app_l_trans (hL : StandardSeq n L L') (ha : IsAbs L')
+    (hm : countRedexes L' + 1 ≤ m) (hnm : n ≤ m)
+    (hM : StandardSeq m (app L' M) (app L' M')) : StandardSeq n (app L M) (app L' M') := by
+  induction hL
+  case refl => exact hM.mono hnm
+  case head K P i _ N' step hni tail ih =>
+    have hseam : i ≤ countRedexes N' := StandardSeq.head_le step tail
+    by_cases haK : IsAbs K
+    · exact .head (step.appAbsL haK) (by omega)
+        (app_l_trans_abs tail (step.isAbs_r haK) hm (by omega) hM)
+    · exact .head (step.appNoAbsL haK) hni (ih ha hm (by omega) hM)
+
+/-- The reduction of a non-abstraction operator followed by an application sequence
+  is a standard sequence. -/
+lemma StandardSeq.app_l_trans_noAbs (hL : StandardSeq n L L') (hna : ¬IsAbs L')
+    (hm : countRedexes L' ≤ m) (hnm : n ≤ m)
+    (hM : StandardSeq m (app L' M) (app L' M')) : StandardSeq n (app L M) (app L' M') := by
+  induction hL
+  case refl => exact hM.mono hnm
+  case head K P i _ N' step hni tail ih =>
+    have hseam : i ≤ countRedexes N' := StandardSeq.head_le step tail
+    have hP : ¬IsAbs P := mt tail.isAbs_r hna
+    exact .head (step.appNoAbsL (mt step.isAbs_r hP)) hni (ih hna hm (by omega) hM)
+
+/-- If operator and operand each reduce by a standard sequence, so does the application. -/
+lemma StandardSeq.app_cong (hL : StandardSeq 0 L L') (hM : StandardSeq 0 M M') :
+    StandardSeq 0 (app L M) (app L' M') := by
+  by_cases ha : IsAbs L'
+  · exact hL.app_l_trans ha (by omega) (Nat.zero_le _) (hM.app_r_abs ha)
+  · exact hL.app_l_trans_noAbs ha (by omega) (Nat.zero_le _) (hM.app_r_noAbs ha)
+
+variable [DecidableEq Var]
 
 /-- Standard reduction is preserved by substitution. -/
 lemma Standard.subst (hM : M ⭢ₛ M') (hN : N ⭢ₛ N') (x : Var) (lc_N : LC N) (lc_N' : LC N') :
@@ -217,6 +427,101 @@ theorem Standard.standardization (lc_M : LC M) (step : M ↠βᶠ N) : M ⭢ₛ
 theorem Standard.iff_redex (lc_M : LC M) : M ⭢ₛ N ↔ M ↠βᶠ N :=
   ⟨to_redex, standardization lc_M⟩
 
+/-- Renaming a free variable preserves the position of the contracted redex. -/
+lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
+    BetaAt (M[x := fvar y]) (M'[x := fvar y]) i := by
+  induction h
+  case outer lc_M lc_N =>
+    rw [subst_open x (fvar y) _ _ (.fvar y)]
+    exact .outer (subst_lc lc_M (.fvar y)) (subst_lc lc_N (.fvar y))
+  case appNoAbsL _ hna ih =>
+    exact .appNoAbsL ih (mt isAbs_subst_fvar.mp hna)
+  case appAbsL _ ha ih =>
+    exact .appAbsL ih (isAbs_subst_fvar.mpr ha)
+  case appNoAbsR M M' i N _ hna ih =>
+    rw [← countRedexes_subst_fvar N x y]
+    exact .appNoAbsR ih (mt isAbs_subst_fvar.mp hna)
+  case appAbsR M M' i N _ ha ih =>
+    rw [← countRedexes_subst_fvar N x y]
+    exact .appAbsR ih (isAbs_subst_fvar.mpr ha)
+  case abs =>
+    apply BetaAt.abs <| free_union [fv] Var
+    grind
+
+/-- Contracting a redex preserves local closure. -/
+lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
+  induction h with
+  | outer lc_M lc_N => exact beta_lc lc_M lc_N
+  | appNoAbsL _ _ ih | appAbsL _ _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .app (ih lc_L) lc_R
+  | appNoAbsR _ _ ih | appAbsR _ _ ih =>
+    cases lc with
+    | app lc_L lc_R => exact .app lc_L (ih lc_R)
+  | abs xs _ ih =>
+    cases lc with
+    | abs ys _ h_body =>
+      apply LC.abs (xs ∪ ys)
+      intro z hz
+      exact ih z (by grind) (h_body z (by grind))
+
+/-- Closing a variable and abstracting preserves the position of the contracted redex. -/
+lemma BetaAt.abs_close {x : Var} (h : BetaAt M M' i) (lc : LC M) :
+    BetaAt (M⟦0 ↜ x⟧.abs) (M'⟦0 ↜ x⟧.abs) i := by
+  apply BetaAt.abs ∅
+  intro z _
+  have lc' := h.lc_r lc
+  have hr : BetaAt (M[x := fvar z]) (M'[x := fvar z]) i := h.rename x z
+  grind
+
+/-- Closing a variable and abstracting preserves a standard sequence. -/
+lemma StandardSeq.abs_close {x : Var} (h : StandardSeq i M M') (lc : LC M) :
+    StandardSeq i (M⟦0 ↜ x⟧.abs) (M'⟦0 ↜ x⟧.abs) := by
+  induction h with
+  | refl => exact .refl
+  | head step hni tail ih => exact .head (step.abs_close lc) hni (ih (step.lc_r lc))
+
+/-- Cofinite congruence rule for standard sequences under an abstraction. -/
+lemma StandardSeq.abs_cong (xs : Finset Var)
+    (cofin : ∀ x ∉ xs, StandardSeq i (M ^ fvar x) (M' ^ fvar x)) (lc : LC (abs M)) :
+    StandardSeq i (abs M) (abs M') := by
+  have ⟨w, _⟩ := fresh_exists <| free_union [fv] Var
+  rw [open_close w M 0 (by grind), open_close w M' 0 (by grind)]
+  have hseq := cofin w (by grind)
+  have hlc := beta_lc lc (.fvar w)
+  exact hseq.abs_close hlc
+
+/-- A standard sequence is a full β-reduction. -/
+lemma StandardSeq.to_redex (h : StandardSeq i M N) (lc_M : LC M) : M ↠βᶠ N := by
+  induction h with
+  | refl => rfl
+  | head step _ _ ih => exact (ih (step.lc_r lc_M)).head (step.to_step lc_M)
+
+/-- A standard reduction gives a standard β-reduction sequence. -/
+theorem Standard.to_seq (h : M ⭢ₛ N) : StandardSeq 0 M N := by
+  induction h
+  case fvar x => exact .refl
+  case app _ _ ihL ihM => exact ihL.app_cong ihM
+  case abs xs h_body ih => exact .abs_cong xs ih ((Standard.abs xs h_body).lc_l)
+  case rdx K P K' _ lc_K lc_P cbn _ ih =>
+    have cbn_full : K.app P ↠ₙ K' ^ P :=
+      (CBN.steps_app_l_cong cbn lc_P).tail (.base (.beta (CBN.steps_lc_r lc_K cbn) lc_P))
+    exact StandardSeq.cbn_head cbn_full ih
+
+/-- A standard β-reduction sequence gives a standard reduction. -/
+theorem StandardSeq.to_standard (h : StandardSeq i M N) (lc_M : LC M) : M ⭢ₛ N := by
+  induction h with
+  | refl => exact Standard.lc_refl _ lc_M
+  | head step _ _ ih =>
+    exact (Standard.of_beta_step (step.to_step lc_M) lc_M).trans (ih (step.lc_r lc_M))
+
+/-- Standard reduction coincides with the existence of a standard β-reduction sequence. -/
+theorem Standard.iff_seq (lc_M : LC M) : M ⭢ₛ N ↔ StandardSeq 0 M N := by
+  constructor
+  · exact Standard.to_seq
+  · intro h
+    exact h.to_standard lc_M
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib

From d5882de92523ea3f167f6e922b031a04ba0525f4 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Sun, 12 Jul 2026 23:47:46 -0600
Subject: [PATCH 13/18] add grind annotation to IsAbs

---
 .../LocallyNameless/Untyped/LeftmostReduction.lean             | 2 +-
 .../LocallyNameless/Untyped/StandardReduction.lean             | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 4ac6e473e..23febed8e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -41,7 +41,7 @@ variable {L L' M M' N : Term Var} {i : Nat}
     abstraction. -/
 lemma BetaNormal.app_inv (h : BetaNormal (app L M)) :
     ¬IsAbs L ∧ BetaNormal L ∧ BetaNormal M := by
-  cases L <;> grind [BetaNormal, countRedexes, IsAbs]
+  cases L <;> grind [BetaNormal, countRedexes]
 
 /-- The body of a normal-form abstraction opens to a normal form. -/
 lemma BetaNormal.abs_open {x : Var} (h : BetaNormal (abs M)) : BetaNormal (M ^ fvar x) := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index d00cf8b24..236e0b0d9 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -38,6 +38,7 @@ def countRedexes : Term Var → Nat
 | app m n       => countRedexes m + countRedexes n
 
 /-- `IsAbs m` holds when `m` is an abstraction. -/
+@[scoped grind]
 inductive IsAbs : Term Var → Prop
 | abs (m : Term Var) : IsAbs (abs m)
 
@@ -202,7 +203,7 @@ lemma countRedexes_subst_fvar [DecidableEq Var] (M : Term Var) (x y : Var) :
 
 /-- Renaming a free variable preserves being an abstraction. -/
 lemma isAbs_subst_fvar [DecidableEq Var] {x y : Var} : IsAbs (M[x := fvar y]) ↔ IsAbs M := by
-  cases M <;> grind [IsAbs]
+  cases M <;> grind
 
 /-- A `BetaAt` step is a full β-step. -/
 lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt M N i) (lc : LC M) : M ⭢βᶠ N := by

From 5bceac9f393335a7ffa6cc19508f763b8fbf0a7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maximiliano=20Onofre=20Mart=C3=ADnez?=
 <maxonomar@ciencias.unam.mx>
Date: Mon, 13 Jul 2026 09:08:31 -0600
Subject: [PATCH 14/18] Update
 Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean

Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
---
 .../LocallyNameless/Untyped/StandardReduction.lean              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 236e0b0d9..a7f2562f1 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -34,7 +34,7 @@ def countRedexes : Term Var → Nat
 | fvar _        => 0
 | bvar _        => 0
 | abs m         => countRedexes m
-| app (abs m) n => (countRedexes (abs m) + countRedexes n) + 1
+| app (abs m) n => countRedexes m + countRedexes n + 1
 | app m n       => countRedexes m + countRedexes n
 
 /-- `IsAbs m` holds when `m` is an abstraction. -/

From 8a345d568b3e9bd5ebda30dbe469fa098ada3c90 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Mon, 13 Jul 2026 09:32:24 -0600
Subject: [PATCH 15/18] specialize countRedexes_openRec_fvar

---
 .../LocallyNameless/Untyped/LeftmostReduction.lean         | 3 +--
 .../LocallyNameless/Untyped/StandardReduction.lean         | 7 ++++++-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index 23febed8e..cec9616df 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -45,8 +45,7 @@ lemma BetaNormal.app_inv (h : BetaNormal (app L M)) :
 
 /-- The body of a normal-form abstraction opens to a normal form. -/
 lemma BetaNormal.abs_open {x : Var} (h : BetaNormal (abs M)) : BetaNormal (M ^ fvar x) := by
-  have e : countRedexes (M ^ fvar x) = countRedexes M := countRedexes_openRec_fvar M 0 x
-  rw [BetaNormal, e]
+  rw [BetaNormal, countRedexes_open_fvar]
   exact h
 
 /-- Leftmost reduction preserves being an abstraction. -/
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index a7f2562f1..bfc7658cf 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -139,6 +139,11 @@ lemma countRedexes_openRec_fvar (M : Term Var) (k : Nat) (x : Var) :
   | abs M ih => grind [openRec_abs, countRedexes]
   | app L R ihL ihR => cases L <;> grind [countRedexes, openRec_bvar, openRec_app, openRec_abs]
 
+/-- Opening the outermost binder with a free variable preserves the number of redexes. -/
+lemma countRedexes_open_fvar (M : Term Var) (x : Var) :
+    countRedexes (M ^ fvar x) = countRedexes M :=
+  countRedexes_openRec_fvar M 0 x
+
 /-- Contracting a redex of an abstraction yields an abstraction. -/
 lemma BetaAt.isAbs_r (h : BetaAt M N i) (ha : IsAbs M) : IsAbs N := by
   cases ha
@@ -238,7 +243,7 @@ lemma BetaAt.le_countRedexes (h : BetaAt M N i) : i ≤ countRedexes N := by
     grind [countRedexes]
   case abs xs _ _ =>
     have := fresh_exists xs
-    grind [countRedexes_openRec_fvar, countRedexes]
+    grind [countRedexes_open_fvar, countRedexes]
 
 /-- In a nonempty standard sequence the lower bound is at most the target's redex count. -/
 lemma StandardSeq.bound_le (h : StandardSeq n M N) : n ≤ countRedexes N ∨ M = N := by

From cffccfa794546f7970f8154c103364e903479b3d Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Mon, 13 Jul 2026 10:26:49 -0600
Subject: [PATCH 16/18] reorder BetaAt

---
 .../Untyped/LeftmostReduction.lean            |  6 +-
 .../Untyped/StandardReduction.lean            | 92 ++++++++++---------
 2 files changed, 51 insertions(+), 47 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index cec9616df..1dd5a6139 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -33,7 +33,7 @@ def BetaNormal (m : Term Var) : Prop := countRedexes m = 0
 
 /-- Leftmost reduction: a β-reduction contracting the redex at position 0. -/
 @[reduction_sys "ℓ"]
-abbrev Leftmost (M N : Term Var) : Prop := BetaAt M N 0
+abbrev Leftmost : Term Var → Term Var → Prop := BetaAt 0
 
 variable {L L' M M' N : Term Var} {i : Nat}
 
@@ -64,8 +64,8 @@ lemma Leftmost.steps_app_l_cong (h : L ↠ℓ L') (hna : ¬IsAbs L') :
     exact (ih hnb).tail (step.appNoAbsL hnb)
 
 /-- Reducing the operand across a non-abstraction normal form keeps the position. -/
-lemma BetaAt.app_r_cong (h : BetaAt M M' i) (hL : BetaNormal L) (hna : ¬IsAbs L) :
-    BetaAt (app L M) (app L M') i := by
+lemma BetaAt.app_r_cong (h : BetaAt i M M') (hL : BetaNormal L) (hna : ¬IsAbs L) :
+    BetaAt i (app L M) (app L M') := by
   have := h.appNoAbsR hna
   rwa [hL] at this
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index bfc7658cf..5596ce391 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -42,22 +42,22 @@ def countRedexes : Term Var → Nat
 inductive IsAbs : Term Var → Prop
 | abs (m : Term Var) : IsAbs (abs m)
 
-/-- `BetaAt M N i` reduces the redex at position `i` of `M` to obtain `N`;
+/-- `BetaAt i M N` reduces the redex at position `i` of `M` to obtain `N`;
     positions are counted from left to right. -/
-inductive BetaAt : Term Var → Term Var → Nat → Prop
+inductive BetaAt : Nat → Term Var → Term Var → Prop
 /-- The outermost redex sits at position `0`. -/
-| outer : LC (abs M) → LC N → BetaAt (app (abs M) N) (M ^ N) 0
+| outer : LC (abs M) → LC N → BetaAt 0 (app (abs M) N) (M ^ N)
 /-- Reducing a non-abstraction operator keeps the position. -/
-| appNoAbsL : BetaAt M M' i → ¬IsAbs M → BetaAt (app M N) (app M' N) i
+| appNoAbsL : BetaAt i M M' → ¬IsAbs M → BetaAt i (app M N) (app M' N)
 /-- Reducing an abstraction operator advances the position by one. -/
-| appAbsL : BetaAt M M' i → IsAbs M → BetaAt (app M N) (app M' N) (i + 1)
+| appAbsL : BetaAt i M M' → IsAbs M → BetaAt (i + 1) (app M N) (app M' N)
 /-- Reducing the operand adds the redex count of a non-abstraction operator. -/
-| appNoAbsR : BetaAt M M' i → ¬IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N)
+| appNoAbsR : BetaAt i M M' → ¬IsAbs N → BetaAt (i + countRedexes N) (app N M) (app N M')
 /-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
-| appAbsR : BetaAt M M' i → IsAbs N → BetaAt (app N M) (app N M') (i + countRedexes N + 1)
+| appAbsR : BetaAt i M M' → IsAbs N → BetaAt (i + countRedexes N + 1) (app N M) (app N M')
 /-- Reducing under a binder keeps the position. -/
 | abs (xs : Finset Var) :
-    (∀ x ∉ xs, BetaAt (M ^ fvar x) (M' ^ fvar x) i) → BetaAt (abs M) (abs M') i
+    (∀ x ∉ xs, BetaAt i (M ^ fvar x) (M' ^ fvar x)) → BetaAt i (abs M) (abs M')
 
 /-- A standard β-reduction sequence from `M` to `N`: the contracted redex positions are
     non-decreasing and all at least `n`. -/
@@ -65,7 +65,7 @@ inductive StandardSeq : Nat → Term Var → Term Var → Prop
 /-- The empty sequence is standard for any lower bound. -/
 | refl : StandardSeq n M M
 /-- A first step at position `i ≥ n`, followed by a standard sequence bounded below by `i`. -/
-| head : BetaAt M P i → n ≤ i → StandardSeq i P N → StandardSeq n M N
+| head : BetaAt i M P → n ≤ i → StandardSeq i P N → StandardSeq n M N
 
 /-- The Standard reduction relation. -/
 @[reduction_sys "ₛ"]
@@ -144,8 +144,18 @@ lemma countRedexes_open_fvar (M : Term Var) (x : Var) :
     countRedexes (M ^ fvar x) = countRedexes M :=
   countRedexes_openRec_fvar M 0 x
 
+/-- An application has at least as many redexes as its operator and operand combined. -/
+lemma countRedexes_app_le (M N : Term Var) :
+    countRedexes M + countRedexes N ≤ countRedexes (app M N) := by
+  cases M <;> grind [countRedexes]
+
+/-- An application with an abstraction operator has one more redex than its parts. -/
+lemma countRedexes_app_abs {M : Term Var} (ha : IsAbs M) (N : Term Var) :
+    countRedexes (app M N) = countRedexes M + countRedexes N + 1 := by
+  cases ha; grind [countRedexes]
+
 /-- Contracting a redex of an abstraction yields an abstraction. -/
-lemma BetaAt.isAbs_r (h : BetaAt M N i) (ha : IsAbs M) : IsAbs N := by
+lemma BetaAt.isAbs_r (h : BetaAt i M N) (ha : IsAbs M) : IsAbs N := by
   cases ha
   cases h
   exact .abs _
@@ -157,7 +167,7 @@ lemma cbn_not_isAbs (h : M ⭢ₙ N) : ¬IsAbs M := by
   trivial
 
 /-- A single Call-by-Name step contracts the redex at position `0`. -/
-lemma BetaAt.of_cbn_step (h : M ⭢ₙ N) : BetaAt M N 0 := by
+lemma BetaAt.of_cbn_step (h : M ⭢ₙ N) : BetaAt 0 M N := by
   induction h with
   | base h_beta =>
     cases h_beta with
@@ -211,7 +221,7 @@ lemma isAbs_subst_fvar [DecidableEq Var] {x y : Var} : IsAbs (M[x := fvar y]) 
   cases M <;> grind
 
 /-- A `BetaAt` step is a full β-step. -/
-lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt M N i) (lc : LC M) : M ⭢βᶠ N := by
+lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt i M N) (lc : LC M) : M ⭢βᶠ N := by
   induction h with
   | outer lc_M lc_N => exact .base (.beta lc_M lc_N)
   | appNoAbsL _ _ ih | appAbsL _ _ ih =>
@@ -230,20 +240,14 @@ lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt M N i) (lc : LC M) : M ⭢β
 variable [HasFresh Var]
 
 /-- The position of a contracted redex is at most the redex count of the result. -/
-lemma BetaAt.le_countRedexes (h : BetaAt M N i) : i ≤ countRedexes N := by
-  induction h
-  case outer => exact Nat.zero_le _
-  case appNoAbsL K' _ _ _ _ _ => cases K' <;> grind [countRedexes]
-  case appAbsL step ha _ =>
-    cases step.isAbs_r ha
-    grind [countRedexes]
-  case appNoAbsR P _ _ _ => cases P <;> grind [countRedexes]
-  case appAbsR ha _ =>
-    cases ha
-    grind [countRedexes]
-  case abs xs _ _ =>
-    have := fresh_exists xs
-    grind [countRedexes_open_fvar, countRedexes]
+lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
+  induction h with
+  | outer => exact Nat.zero_le _
+  | appNoAbsL => exact le_trans (by omega) (countRedexes_app_le _ _)
+  | appAbsL step ha => rw [countRedexes_app_abs (step.isAbs_r ha)]; omega
+  | appNoAbsR => exact le_trans (by omega) (countRedexes_app_le _ _)
+  | appAbsR _ ha => rw [countRedexes_app_abs ha]; omega
+  | abs xs => have := fresh_exists xs; grind [countRedexes_open_fvar, countRedexes]
 
 /-- In a nonempty standard sequence the lower bound is at most the target's redex count. -/
 lemma StandardSeq.bound_le (h : StandardSeq n M N) : n ≤ countRedexes N ∨ M = N := by
@@ -256,7 +260,7 @@ lemma StandardSeq.bound_le (h : StandardSeq n M N) : n ≤ countRedexes N ∨ M
     · exact le_trans hni step.le_countRedexes
 
 /-- The leading position of a standard sequence is at most the redex count of its target. -/
-lemma StandardSeq.head_le (step : BetaAt M P i) (tail : StandardSeq i P N) :
+lemma StandardSeq.head_le (step : BetaAt i M P) (tail : StandardSeq i P N) :
     i ≤ countRedexes N := by
   rcases tail.bound_le with h | rfl
   · exact h
@@ -268,10 +272,10 @@ lemma StandardSeq.app_l_trans_abs (hL : StandardSeq n L L') (ha : IsAbs L)
     (hm : countRedexes L' + 1 ≤ m) (hnm : n + 1 ≤ m)
     (hM : StandardSeq m (app L' M) (app L' M')) :
     StandardSeq (n + 1) (app L M) (app L' M') := by
-  induction hL
-  case refl => exact hM.mono hnm
-  case head K P i _ N' step hni tail ih =>
-    have hseam : i ≤ countRedexes N' := StandardSeq.head_le step tail
+  induction hL with
+  | refl => exact hM.mono hnm
+  | head step hni tail ih =>
+    have hseam := StandardSeq.head_le step tail
     exact .head (step.appAbsL ha) (by omega) (ih (step.isAbs_r ha) hm (by omega) hM)
 
 /-- The reduction of an operator ending in an abstraction followed by an application sequence
@@ -281,8 +285,8 @@ lemma StandardSeq.app_l_trans (hL : StandardSeq n L L') (ha : IsAbs L')
     (hM : StandardSeq m (app L' M) (app L' M')) : StandardSeq n (app L M) (app L' M') := by
   induction hL
   case refl => exact hM.mono hnm
-  case head K P i _ N' step hni tail ih =>
-    have hseam : i ≤ countRedexes N' := StandardSeq.head_le step tail
+  case head _ K _ _ _ step hni tail ih =>
+    have hseam := StandardSeq.head_le step tail
     by_cases haK : IsAbs K
     · exact .head (step.appAbsL haK) (by omega)
         (app_l_trans_abs tail (step.isAbs_r haK) hm (by omega) hM)
@@ -293,11 +297,11 @@ lemma StandardSeq.app_l_trans (hL : StandardSeq n L L') (ha : IsAbs L')
 lemma StandardSeq.app_l_trans_noAbs (hL : StandardSeq n L L') (hna : ¬IsAbs L')
     (hm : countRedexes L' ≤ m) (hnm : n ≤ m)
     (hM : StandardSeq m (app L' M) (app L' M')) : StandardSeq n (app L M) (app L' M') := by
-  induction hL
-  case refl => exact hM.mono hnm
-  case head K P i _ N' step hni tail ih =>
-    have hseam : i ≤ countRedexes N' := StandardSeq.head_le step tail
-    have hP : ¬IsAbs P := mt tail.isAbs_r hna
+  induction hL with
+  | refl => exact hM.mono hnm
+  | head step hni tail ih =>
+    have hseam := StandardSeq.head_le step tail
+    have hP := mt tail.isAbs_r hna
     exact .head (step.appNoAbsL (mt step.isAbs_r hP)) hni (ih hna hm (by omega) hM)
 
 /-- If operator and operand each reduce by a standard sequence, so does the application. -/
@@ -434,8 +438,8 @@ theorem Standard.iff_redex (lc_M : LC M) : M ⭢ₛ N ↔ M ↠βᶠ N :=
   ⟨to_redex, standardization lc_M⟩
 
 /-- Renaming a free variable preserves the position of the contracted redex. -/
-lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
-    BetaAt (M[x := fvar y]) (M'[x := fvar y]) i := by
+lemma BetaAt.rename (h : BetaAt i M M') (x y : Var) :
+    BetaAt i (M[x := fvar y]) (M'[x := fvar y]) := by
   induction h
   case outer lc_M lc_N =>
     rw [subst_open x (fvar y) _ _ (.fvar y)]
@@ -455,7 +459,7 @@ lemma BetaAt.rename (h : BetaAt M M' i) (x y : Var) :
     grind
 
 /-- Contracting a redex preserves local closure. -/
-lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
+lemma BetaAt.lc_r (h : BetaAt i M M') (lc : LC M) : LC M' := by
   induction h with
   | outer lc_M lc_N => exact beta_lc lc_M lc_N
   | appNoAbsL _ _ ih | appAbsL _ _ ih =>
@@ -472,12 +476,12 @@ lemma BetaAt.lc_r (h : BetaAt M M' i) (lc : LC M) : LC M' := by
       exact ih z (by grind) (h_body z (by grind))
 
 /-- Closing a variable and abstracting preserves the position of the contracted redex. -/
-lemma BetaAt.abs_close {x : Var} (h : BetaAt M M' i) (lc : LC M) :
-    BetaAt (M⟦0 ↜ x⟧.abs) (M'⟦0 ↜ x⟧.abs) i := by
+lemma BetaAt.abs_close {x : Var} (h : BetaAt i M M') (lc : LC M) :
+    BetaAt i (M⟦0 ↜ x⟧.abs) (M'⟦0 ↜ x⟧.abs) := by
   apply BetaAt.abs ∅
   intro z _
   have lc' := h.lc_r lc
-  have hr : BetaAt (M[x := fvar z]) (M'[x := fvar z]) i := h.rename x z
+  have hr : BetaAt i (M[x := fvar z]) (M'[x := fvar z]) := h.rename x z
   grind
 
 /-- Closing a variable and abstracting preserves a standard sequence. -/

From 59ff789283fcbe94b8c2b7dac7b47abd222bfc91 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Mon, 13 Jul 2026 10:45:00 -0600
Subject: [PATCH 17/18] move IsAbs next to Value

---
 .../LambdaCalculus/LocallyNameless/Untyped/LcAt.lean         | 5 +++++
 .../LocallyNameless/Untyped/StandardReduction.lean           | 5 -----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index 539e92ff8..bd6ad1d7c 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -86,6 +86,11 @@ attribute [scoped grind .] LC.fvar LC.app
 inductive Value : Term Var → Prop
 | abs (e : Term Var) : e.abs.LC → e.abs.Value
 
+/-- `IsAbs m` holds when `m` is an abstraction. -/
+@[scoped grind]
+inductive IsAbs : Term Var → Prop
+| abs (m : Term Var) : IsAbs (abs m)
+
 set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- `M` is `LcAt 0` if and only if `M` is locally closed. -/
 theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 5596ce391..3718568ba 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -37,11 +37,6 @@ def countRedexes : Term Var → Nat
 | app (abs m) n => countRedexes m + countRedexes n + 1
 | app m n       => countRedexes m + countRedexes n
 
-/-- `IsAbs m` holds when `m` is an abstraction. -/
-@[scoped grind]
-inductive IsAbs : Term Var → Prop
-| abs (m : Term Var) : IsAbs (abs m)
-
 /-- `BetaAt i M N` reduces the redex at position `i` of `M` to obtain `N`;
     positions are counted from left to right. -/
 inductive BetaAt : Nat → Term Var → Term Var → Prop

From a7ebcbe9d8a7dc120b5f8da4e63cb209046bb749 Mon Sep 17 00:00:00 2001
From: Maximiliano <maxonomar@ciencias.unam.mx>
Date: Mon, 13 Jul 2026 14:57:28 -0600
Subject: [PATCH 18/18] replace appNoAbs/appAbs pairs with appL/appR

---
 .../LocallyNameless/Untyped/LcAt.lean         |  5 ++
 .../Untyped/StandardReduction.lean            | 84 ++++++++++++-------
 2 files changed, 59 insertions(+), 30 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
index bd6ad1d7c..4a74cf41d 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean
@@ -91,6 +91,11 @@ inductive Value : Term Var → Prop
 inductive IsAbs : Term Var → Prop
 | abs (m : Term Var) : IsAbs (abs m)
 
+instance (m : Term Var) : Decidable (IsAbs m) := by
+  cases m
+  case abs => exact isTrue (.abs _)
+  all_goals exact isFalse (by intro _; contradiction)
+
 set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- `M` is `LcAt 0` if and only if `M` is locally closed. -/
 theorem lcAt_iff_LC (M : Term Var) [HasFresh Var] : LcAt 0 M ↔ M.LC := by
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 3718568ba..74919b2cf 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -42,14 +42,11 @@ def countRedexes : Term Var → Nat
 inductive BetaAt : Nat → Term Var → Term Var → Prop
 /-- The outermost redex sits at position `0`. -/
 | outer : LC (abs M) → LC N → BetaAt 0 (app (abs M) N) (M ^ N)
-/-- Reducing a non-abstraction operator keeps the position. -/
-| appNoAbsL : BetaAt i M M' → ¬IsAbs M → BetaAt i (app M N) (app M' N)
-/-- Reducing an abstraction operator advances the position by one. -/
-| appAbsL : BetaAt i M M' → IsAbs M → BetaAt (i + 1) (app M N) (app M' N)
-/-- Reducing the operand adds the redex count of a non-abstraction operator. -/
-| appNoAbsR : BetaAt i M M' → ¬IsAbs N → BetaAt (i + countRedexes N) (app N M) (app N M')
-/-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
-| appAbsR : BetaAt i M M' → IsAbs N → BetaAt (i + countRedexes N + 1) (app N M) (app N M')
+/-- Reducing the operator advances the position by one when the operator is an abstraction. -/
+| appL : BetaAt i M M' → BetaAt (i + if IsAbs M then 1 else 0) (app M N) (app M' N)
+/-- Reducing the operand adds the operator's redex count, plus one when it is an abstraction. -/
+| appR : BetaAt i M M' →
+    BetaAt (i + countRedexes N + if IsAbs N then 1 else 0) (app N M) (app N M')
 /-- Reducing under a binder keeps the position. -/
 | abs (xs : Finset Var) :
     (∀ x ∉ xs, BetaAt i (M ^ fvar x) (M' ^ fvar x)) → BetaAt i (abs M) (abs M')
@@ -77,6 +74,26 @@ inductive Standard : Term Var → Term Var → Prop
 
 variable {L L' M M' N N' P : Term Var} {i m n : Nat}
 
+/-- Reducing a non-abstraction operator keeps the position. -/
+lemma BetaAt.appNoAbsL (h : BetaAt i M M') (hna : ¬IsAbs M) :
+    BetaAt i (app M N) (app M' N) := by
+  simpa [if_neg hna] using h.appL
+
+/-- Reducing an abstraction operator advances the position by one. -/
+lemma BetaAt.appAbsL (h : BetaAt i M M') (ha : IsAbs M) :
+    BetaAt (i + 1) (app M N) (app M' N) := by
+  simpa [if_pos ha] using h.appL
+
+/-- Reducing the operand adds the redex count of a non-abstraction operator. -/
+lemma BetaAt.appNoAbsR (h : BetaAt i M M') (hna : ¬IsAbs N) :
+    BetaAt (i + countRedexes N) (app N M) (app N M') := by
+  simpa [if_neg hna] using h.appR (N := N)
+
+/-- Reducing the operand adds the redex count of an abstraction operator, plus one. -/
+lemma BetaAt.appAbsR (h : BetaAt i M M') (ha : IsAbs N) :
+    BetaAt (i + countRedexes N + 1) (app N M) (app N M') := by
+  simpa [if_pos ha] using h.appR (N := N)
+
 /-- The left side of a standard reduction is locally closed. -/
 lemma Standard.lc_l (step : M ⭢ₛ N) : LC M := by
   induction step
@@ -219,10 +236,10 @@ lemma isAbs_subst_fvar [DecidableEq Var] {x y : Var} : IsAbs (M[x := fvar y]) 
 lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt i M N) (lc : LC M) : M ⭢βᶠ N := by
   induction h with
   | outer lc_M lc_N => exact .base (.beta lc_M lc_N)
-  | appNoAbsL _ _ ih | appAbsL _ _ ih =>
+  | appL _ ih =>
     cases lc with
     | app lc_L lc_R => exact .appR lc_R (ih lc_L)
-  | appNoAbsR _ _ ih | appAbsR _ _ ih =>
+  | appR _ ih =>
     cases lc with
     | app lc_L lc_R => exact .appL lc_L (ih lc_R)
   | abs xs _ ih =>
@@ -238,11 +255,19 @@ variable [HasFresh Var]
 lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
   induction h with
   | outer => exact Nat.zero_le _
-  | appNoAbsL => exact le_trans (by omega) (countRedexes_app_le _ _)
-  | appAbsL step ha => rw [countRedexes_app_abs (step.isAbs_r ha)]; omega
-  | appNoAbsR => exact le_trans (by omega) (countRedexes_app_le _ _)
-  | appAbsR _ ha => rw [countRedexes_app_abs ha]; omega
-  | abs xs => have := fresh_exists xs; grind [countRedexes_open_fvar, countRedexes]
+  | appL step =>
+    split
+    · rw [countRedexes_app_abs (step.isAbs_r (by assumption))]
+      omega
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | appR =>
+    split
+    · rw [countRedexes_app_abs (by assumption)]
+      omega
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | abs xs =>
+    have := fresh_exists xs
+    grind [countRedexes_open_fvar, countRedexes]
 
 /-- In a nonempty standard sequence the lower bound is at most the target's redex count. -/
 lemma StandardSeq.bound_le (h : StandardSeq n M N) : n ≤ countRedexes N ∨ M = N := by
@@ -435,21 +460,20 @@ theorem Standard.iff_redex (lc_M : LC M) : M ⭢ₛ N ↔ M ↠βᶠ N :=
 /-- Renaming a free variable preserves the position of the contracted redex. -/
 lemma BetaAt.rename (h : BetaAt i M M') (x y : Var) :
     BetaAt i (M[x := fvar y]) (M'[x := fvar y]) := by
-  induction h
-  case outer lc_M lc_N =>
+  induction h with
+  | outer lc_M lc_N =>
     rw [subst_open x (fvar y) _ _ (.fvar y)]
     exact .outer (subst_lc lc_M (.fvar y)) (subst_lc lc_N (.fvar y))
-  case appNoAbsL _ hna ih =>
-    exact .appNoAbsL ih (mt isAbs_subst_fvar.mp hna)
-  case appAbsL _ ha ih =>
-    exact .appAbsL ih (isAbs_subst_fvar.mpr ha)
-  case appNoAbsR M M' i N _ hna ih =>
-    rw [← countRedexes_subst_fvar N x y]
-    exact .appNoAbsR ih (mt isAbs_subst_fvar.mp hna)
-  case appAbsR M M' i N _ ha ih =>
-    rw [← countRedexes_subst_fvar N x y]
-    exact .appAbsR ih (isAbs_subst_fvar.mpr ha)
-  case abs =>
+  | appL _ ih =>
+    split
+    · exact ih.appAbsL (isAbs_subst_fvar.mpr (by assumption))
+    · exact ih.appNoAbsL (mt isAbs_subst_fvar.mp (by assumption))
+  | appR _ ih =>
+    rw [← countRedexes_subst_fvar _ x y]
+    split
+    · exact ih.appAbsR (isAbs_subst_fvar.mpr (by assumption))
+    · exact ih.appNoAbsR (mt isAbs_subst_fvar.mp (by assumption))
+  | abs =>
     apply BetaAt.abs <| free_union [fv] Var
     grind
 
@@ -457,10 +481,10 @@ lemma BetaAt.rename (h : BetaAt i M M') (x y : Var) :
 lemma BetaAt.lc_r (h : BetaAt i M M') (lc : LC M) : LC M' := by
   induction h with
   | outer lc_M lc_N => exact beta_lc lc_M lc_N
-  | appNoAbsL _ _ ih | appAbsL _ _ ih =>
+  | appL _ ih =>
     cases lc with
     | app lc_L lc_R => exact .app (ih lc_L) lc_R
-  | appNoAbsR _ _ ih | appAbsR _ _ ih =>
+  | appR _ ih =>
     cases lc with
     | app lc_L lc_R => exact .app lc_L (ih lc_R)
   | abs xs _ ih =>