diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index b969bf9c2..1962a3ace 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -51,6 +51,22 @@ theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := by
 theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := by
   induction h <;> grind
 
+/-- Sandwich: if `r ⊆ p ⊆ r*` then `r* = p*`. -/
+theorem ReflTransGen.sandwich_to_eq {α} {r p : α → α → Prop}
+    (h₁ : ∀ {a b}, r a b → p a b)
+    (h₂ : ∀ {a b}, p a b → ReflTransGen r a b) :
+    ∀ {a b}, ReflTransGen r a b ↔ ReflTransGen p a b := by
+  intro a b
+  constructor
+  · intro hr
+    induction hr with
+    | refl => exact ReflTransGen.refl
+    | tail hab hbc ih => exact ReflTransGen.tail ih (h₁ hbc)
+  · intro hp
+    induction hp with
+    | refl => exact ReflTransGen.refl
+    | tail hab hbc ih => exact ReflTransGen.trans ih (h₂ hbc)
+
 attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.to_eqvGen
   SymmGen.to_eqvGen
 
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
new file mode 100644
index 000000000..e6be26f74
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 zayn7lie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zayn Wang
+-/
+module
+
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.DeBruijnSyntax
+public import Cslib.Foundations.Data.Relation
+
+/-!
+# One-step β-reduction and its reflexive-transitive closure
+
+This file defines the usual compatible one-step β-reduction on de Bruijn lambda terms.
+It also introduces its reflexive-transitive closure and proves basic closure lemmas for
+application and abstraction.
+
+## Main definitions
+
+* `Lambda.Beta`: one-step β-reduction.
+* `Lambda.BetaStar`: the reflexive-transitive closure of `Beta`.
+
+## Main lemmas
+
+Inside `namespace BetaStar` we provide the standard constructors and congruence lemmas:
+
+* `BetaStar.refl`
+* `BetaStar.head`
+* `BetaStar.tail`
+* `BetaStar.trans`
+* `BetaStar.appL`, `BetaStar.appR`, `BetaStar.app`
+* `BetaStar.abs`
+
+These lemmas are used later to compare β-reduction with parallel reduction.
+-/
+
+
+namespace Lambda
+open Term
+
+/-- One-step β-reduction (compatible closure). -/
+@[reduction_sys "β"]
+public inductive Beta : Term → Term → Prop
+  | abs  {t t'}        : Beta t t' → Beta (λ.t) (λ.t')
+  | appL {t t' u}      : Beta t t' → Beta (t·u) (t'·u)
+  | appR {t u u'}      : Beta u u' → Beta (t·u) (t·u')
+  | red  (t' s : Term) : Beta ((λ.t')·s) (t'.sub 0 s)
+public abbrev BetaStar := Relation.ReflTransGen Beta
+
+namespace BetaStar
+
+public theorem refl (t : Term) : BetaStar t t :=
+  Relation.ReflTransGen.refl
+
+public theorem head {a b c} (hab : Beta a b) (hbc : BetaStar b c) :
+    BetaStar a c :=
+  Relation.ReflTransGen.head hab hbc
+
+public theorem tail {a b c} (hab : BetaStar a b) (hbc : Beta b c) :
+    BetaStar a c :=
+  Relation.ReflTransGen.tail hab hbc
+
+public theorem trans {a b c}
+    (hab : BetaStar a b) (hbc : BetaStar b c) :
+    BetaStar a c :=
+  Relation.ReflTransGen.trans hab hbc
+
+public theorem appL {t t' u : Term} (h : BetaStar t t') :
+    BetaStar (t·u) (t'·u) := by
+  induction h with
+  | refl => exact BetaStar.refl (t·u)
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.appL hbc)
+
+public theorem appR {t u u' : Term} (h : BetaStar u u') :
+    BetaStar (t·u) (t·u') := by
+  induction h with
+  | refl => exact BetaStar.refl (t·u)
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.appR hbc)
+
+public theorem app {t t' u u'}
+    (ht : BetaStar t t')
+    (hu : BetaStar u u') :
+    BetaStar (t·u) (t'·u') := by
+  induction ht with
+  | refl => exact BetaStar.appR hu
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.appL hbc)
+
+public theorem abs {t t' : Term} (h : BetaStar t t') :
+    BetaStar (λ.t) (λ.t') := by
+  induction h with
+  | refl => exact BetaStar.refl (λ.t)
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.abs hbc)
+
+end BetaStar
+end Lambda
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
new file mode 100644
index 000000000..fc6c54f2c
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 zayn7lie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zayn Wang
+-/
+module
+
+public import Cslib.Foundations.Data.Relation
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ParallelReduction
+
+/-!
+# The Church–Rosser theorem for β-reduction
+
+This file proves confluence of β-reduction on de Bruijn lambda terms.  The proof follows
+the classical route:
+
+1. define parallel β-reduction,
+2. show that parallel reduction has the diamond property using complete developments,
+3. compare parallel reduction with ordinary β-reduction via reflexive-transitive closure,
+4. transport confluence back to β-reduction.
+
+## Main results
+
+* `diamond_par`: parallel reduction is diamond.
+* `churchRosser_beta`: β-reduction is confluent.
+
+## Implementation note
+
+The proof relies on the generic rewriting lemmas from `ConfluentReduction` together with
+the complete-development machinery from `ParallelReduction`.
+-/
+
+namespace Lambda
+open Relation
+
+/-- Parallel Reduction is Diamond. -/
+private lemma diamond_par : Diamond Par := by
+  intro a b c hab hac
+  exact ⟨a.dev, par_to_dev hab, par_to_dev hac⟩
+
+/-- Church–Rosser: β is confluent (on RTC). -/
+public theorem churchRosser_beta : Confluent Beta := by
+  -- Confluence of Par from diamond
+  have hPar : Confluent Par :=
+    Diamond.toConfluent (r := Par) diamond_par
+  -- Identify BetaStar and ParStar via sandwich
+  have hEq {a b : Term} : BetaStar a b ↔ ParStar a b :=
+      ReflTransGen.sandwich_to_eq (r := Beta) (p := Par)
+    (by intro a b h; exact beta_subset_par h)
+    (by intro a b h; exact par_subset_betaStar h)
+  -- Transport confluence
+  intro a b c hab hac
+  have hab' : ParStar a b := (hEq).1 hab
+  have hac' : ParStar a c := (hEq).1 hac
+  rcases hPar hab' hac' with ⟨d, hbd, hcd⟩
+  exact ⟨d, (hEq).2 hbd, (hEq).2 hcd⟩
+
+end Lambda
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
new file mode 100644
index 000000000..07f5d8b17
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
@@ -0,0 +1,380 @@
+/-
+Copyright (c) 2026 zayn7lie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zayn Wang, Maksym Radziwill
+-/
+module
+
+public import Mathlib.Data.Nat.Basic
+public import Cslib.Foundations.Syntax.HasSubstitution
+
+/-!
+# Untyped lambda calculus with de Bruijn indices
+
+This file defines the syntax of untyped lambda terms using de Bruijn indices, together
+with the basic operations on terms needed for β-reduction.  Using de Bruijn indices avoids
+explicit reasoning about α-conversion and variable names.
+
+## Main definitions
+
+* `Lambda.Term`: the type of lambda terms.
+* `Term.incre`: lifting (shifting) of free variables above a cutoff.
+* `Term.subst`: raw substitution at a de Bruijn index.
+* `Term.decre`: lowering of free variables above a cutoff.
+* `Term.sub`: the substitution operation implementing β-contraction.
+
+## Main lemmas
+
+* `Term.incre_rfl`: shifting by `0` is the identity.
+* `Term.decre_incre_elim`: lowering cancels a corresponding shift.
+* `Term.var_sub_elim`, `Term.var_lt_sub`, `Term.var_gt_sub`: basic computations for
+  substitution on variables.
+
+## Notes
+
+The definitions in this file are tailored to the later development of one-step β-reduction,
+parallel reduction, and the Church–Rosser theorem.
+
+## References
+
+* <https://en.wikipedia.org/wiki/De_Bruijn_index>
+-/
+
+
+namespace Lambda
+
+/-- using de Bruijn syntax avoiding α-conversion -/
+public inductive Term : Type where
+  | var : Nat → Term
+  | abs : Term → Term
+  | app : Term → Term → Term
+deriving DecidableEq, Repr
+
+open Term
+namespace Term
+
+notation:max "𝕧" str => Term.var str
+notation:max "λ." t => Term.abs t
+infixl:77 "·" => Term.app
+
+/-- `incre i l t` increments `i` for all free vars `≥ l`. -/
+@[expose] public def incre (i : Nat) (l : Nat) : Term → Term
+  | var k   => if l ≤ k then var (k + i) else var k
+  | abs t   => abs (incre i (l + 1) t)
+  | app t u => app (incre i l t) (incre i l u)
+
+/-- `subst j s t` substitutes `j` with term `s` in `t`. -/
+@[expose] public def subst (j : Nat) (s : Term) : Term → Term
+  | var k   => if k = j then s else var k
+  | abs t   => abs (subst (j + 1) (incre 1 0 s) t)
+  | app t u => app (subst j s t) (subst j s u)
+
+/-- `decre i l t` decrements `i` for all free vars `≥ l + i`.
+    the reason using `l + i` is that it is more explicit for
+    free variable elimination. For example, after eliminating
+    `var k` for Term `t` from the most outside, `decre 1 k t`
+    will close the gap caused by `k` elimination. -/
+@[expose] public def decre (i : Nat) (l : Nat) : Term → Term
+  | var k   => if l + i ≤ k then var (k - i) else var k
+  | abs t   => abs (decre i (l + 1) t)
+  | app t u => app (decre i l t) (decre i l u)
+
+/-- Substitute into the body of a lambda: `(λ.t) s` -/
+@[expose] public def sub (t : Term) (n : Nat) (s : Term) := decre 1 n (subst n (incre 1 n s) t)
+
+@[expose] public instance : 
+    Cslib.HasSubstitution Term Nat Term where
+  subst t n s := t.sub n s
+
+/-- Increment of 0 is identity -/
+@[simp] public theorem incre_rfl {l t} : incre 0 l t = t := by
+  induction t generalizing l with
+  | var k => simp_all only [incre, Nat.add_zero, ite_self]
+  | abs t ih => simp_all only [incre]
+  | app t u iht ihu => simp_all only [incre]
+
+/-- Decrement of increment with same bound is the same.
+Lemma for `var_sub` -/
+@[simp] public theorem decre_incre_elim {l t} : decre 1 l (incre 1 l t) = t := by
+  induction t generalizing l with
+  | var k =>
+      unfold decre incre
+      cases em (l ≤ k) with
+      | inl h => simp_all only [↓reduceIte, 
+          Nat.add_le_add_iff_right, Nat.add_one_sub_one]
+      | inr h =>
+          have : ¬(l + 1 ≤ k) := by omega
+          simp only [if_neg h, if_neg this]
+  | abs t ih => simp_all only [incre, decre]
+  | app t u iht ihu => simp_all only [incre, decre]
+
+/-- Substitution of var n. -/
+@[simp] public theorem var_sub_elim {n s} : ((𝕧 n).sub) n s = s := by
+  simp_all only [sub, subst, ↓reduceIte, decre_incre_elim]
+
+/-- Vacuously Substitution of var k to var k. -/
+@[simp] public theorem var_lt_sub {k n s} (hk : k < n) :
+    ((𝕧 k).sub) n s = 𝕧 k := by
+  have : ¬(n + 1 ≤ k) := by omega
+  simp_all only [sub, subst, Nat.ne_of_lt hk, 
+    ↓reduceIte, decre]
+
+/-- Vacuously Substitution of var k to var k - 1. -/
+@[simp] public theorem var_gt_sub {k n s} (hk : k > n) :
+    ((𝕧 k).sub) n s = 𝕧 (k - 1) := by
+  have : n + 1 ≤ k := by omega
+  simp_all only [gt_iff_lt, sub, subst, 
+    Nat.ne_of_gt hk, ↓reduceIte, decre]
+
+/-- Increments elimination for same lower bound.
+Special thanks to professor Radziwill @maksym-radziwill about
+his idea of generalizing proper variable. -/
+@[simp] public theorem incre_same_bound_elim {i j n t} :
+    (incre i n (incre j n t)) = (incre (i + j) n t) := by
+  induction t generalizing i n with
+  | var k =>
+      cases em (n ≤ k) with
+      | inl h =>
+          simp_all only [incre, ↓reduceIte, 
+            le_trans h (Nat.le_add_right k j), var.injEq]
+          simp_all only [Nat.add_comm, Nat.add_left_comm]
+      | inr h => simp_all only [not_le, incre, if_neg h]
+  | abs t' ih => simp_all only [incre]
+  | app t₁ t₂ ih₁ ih₂ => simp_all only [incre]
+
+/-- Communitivity of incre. -/
+public theorem incre_comm {i j k l t} :
+    (incre j (k + l + i) (incre i l t))=
+      (incre i l (incre j (k + l) t)) := by
+  induction t generalizing l with
+  | var n =>
+      cases em (k + l ≤ n) with
+      | inl h =>
+          have : l ≤ n := le_trans (Nat.le_add_left _ _) h
+          simp_all only [incre, ↓reduceIte, 
+            Nat.add_le_add_iff_right, 
+            le_trans this (Nat.le_add_right _ _), var.injEq]
+          simp only [Nat.add_comm, Nat.add_left_comm]
+      | inr h =>
+          simp only [incre, if_neg h]
+          cases em (l ≤ n) with
+          | inl h' =>
+              simp_all only [not_le, ↓reduceIte, incre,
+                Nat.add_le_add_iff_right, ite_eq_right_iff]
+              intro hk
+              have : n < n := Nat.lt_of_lt_of_le h hk
+              exact (Nat.lt_irrefl n this).elim
+          | inr h' =>
+              simp_all only [not_le, if_neg h', incre,
+                ite_eq_right_iff, var.injEq, Nat.add_eq_left]
+              intro hk
+              have hl : l ≤ n := by omega
+              exact (Nat.lt_irrefl n
+                (Nat.lt_of_lt_of_le h' hl)).elim
+  | abs t' ih => 
+      simp_all only [Nat.add_comm, incre, Nat.add_assoc]
+  | app t₁ t₂ ih₁ ih₂ => simp_all only [incre]
+
+public theorem incre_comm_zero {n s} :
+    incre 1 (n + 1) (incre 1 0 s) =
+      incre 1 0 (incre 1 n s) := by
+  simpa only [Nat.add_zero] 
+    using (incre_comm (i := 1) (l := 0) (j := 1) (k := n) (t := s))
+
+@[simp] public theorem abs_sub_zero {t n s} :
+    ((λ.t).sub n s) = λ.(t.sub (n + 1) (incre 1 0 s)) := by
+  simp_all only [sub, subst, decre, incre_comm_zero]
+
+private lemma incre_sub_var {i l n k s} :
+    (incre i (l + n + 1) 𝕧 k).sub n (incre i (l + n) s) =
+    incre i (l + n) ((𝕧 k).sub n s) := by
+  cases em (k = n) with
+  | inl h =>
+      have : ¬ (l + n + 1 ≤ n) := by omega
+      simp_all only [not_le, sub, incre, if_neg this, subst, 
+        ↓reduceIte, decre_incre_elim]
+  | inr h =>
+      cases em (l + n + 1 ≤ k) with
+      | inl h' =>
+          have : ¬(k + i = n) := by omega
+          have : n + 1 ≤ k + i := by omega
+          have : n + 1 ≤ k := by omega
+          have : l + n ≤ k - 1 := by omega
+          have : k + i - 1 = k - 1 + i := by omega
+          simp_all only [sub, incre, ↓reduceIte, 
+            subst, decre]
+      | inr h' =>
+          simp_all only [not_le, sub, incre, if_neg h',
+            subst, ↓reduceIte, decre]
+          cases em (n < k) with
+          | inl h'' =>
+              have : (n + 1 ≤ k) := by omega
+              simp_all only [↓reduceIte, incre, 
+                right_eq_ite_iff, var.injEq, Nat.left_eq_add]
+              intro h
+              have : ¬(l + n ≤ k - 1) := by omega
+              exact (this h).elim
+          | inr h'' =>
+              have : ¬(n + 1 ≤ k) := by omega
+              simp_all only [not_lt, not_le, if_neg, incre, 
+                right_eq_ite_iff, var.injEq, Nat.left_eq_add]
+              intro h
+              have : ¬(l + n ≤ k) := by omega
+              exact (this h).elim
+
+/-- The communitivity between sub and incre for free var. -/
+@[simp] public theorem incre_sub {i l n t s} :
+    ((incre i (l + n + 1) t).sub n (incre i (l + n) s)) =
+    (incre i (l + n) (t.sub n s)) := by
+  induction t generalizing l n s with
+  | var k => exact incre_sub_var
+  | abs t' ih =>
+      simpa only [sub, ← incre_comm, incre, subst, 
+        Nat.add_zero, ← incre_comm_zero, decre, abs.injEq] 
+        using ih
+  | app t₁ t₂ ih₁ ih₂ => simp_all only [sub, incre, subst, decre]
+
+private lemma subst_zero_incre {n t u} :
+    subst n t (incre 1 n u) = incre 1 n u := by
+  induction u generalizing n t with
+  | var k =>
+      cases em (n ≤ k) with
+      | inl h =>
+          simp_all only [incre, ↓reduceIte, subst, ite_eq_right_iff]
+          intro; omega
+      | inr h =>
+          simp_all only [not_le, incre, if_neg h,
+            subst, ite_eq_right_iff]
+          intro; omega
+  | abs t ih => simp_all only [incre, subst]
+  | app t v iht ihv => simp_all only [incre, subst]
+
+private lemma sub_incre_same {u r m} :
+    ((incre 1 m u).sub m r) = u := by
+  simp_all only [sub, subst_zero_incre, decre_incre_elim]
+
+@[simp] public theorem sub_lift_zero {i t n u} :
+    ((incre 1 i t).sub (n + i + 1) (incre 1 i u)) =
+      incre 1 i (t.sub (n + i) u) := by
+  induction t generalizing n u i with
+  | var k =>
+      cases em (k = n + i) with
+      | inl hk => 
+          simp_all only [sub, incre, Nat.le_add_left, 
+            ↓reduceIte, subst, decre_incre_elim]
+      | inr hk =>
+        cases em (k < n + i) with
+          | inl hlt =>
+              have hlt' : k + 1 < n + i + 1 := by omega
+              have hnlt : ¬(n + i + 1 ≤ k) := by omega
+              simp only [sub, incre, subst]
+              cases em (i ≤ k) with
+              | inl hlt' => 
+                  simp_all only [Nat.add_lt_add_iff_right, 
+                    not_le, ↓reduceIte, subst, 
+                    Nat.add_right_cancel_iff, decre,
+                    Nat.add_le_add_iff_right, 
+                    Nat.add_one_sub_one, if_neg, incre]
+              | inr hlt' =>
+                  have h' : ¬(k = n + i + 1) := by omega
+                  simp_all only [Nat.add_lt_add_iff_right, 
+                    not_le, if_neg, subst, ↓reduceIte, 
+                    decre, incre, ite_eq_right_iff, 
+                    var.injEq]
+                  intro h
+                  have : ¬(n + i + 1 + 1 ≤ k) := by omega
+                  exact (this h).elim
+          | inr hlt =>
+              have hle : i ≤ k := by omega
+              have hgt : n + i + 1 ≤ k := by omega
+              have hlt : i ≤ k - 1 := by omega
+              simp_all only [not_lt, sub, incre, ↓reduceIte, 
+                subst, Nat.add_right_cancel_iff, decre, 
+                Nat.add_le_add_iff_right, 
+                Nat.add_one_sub_one, var.injEq]
+              exact by omega
+  | abs t ih =>
+      simpa only [sub, incre, subst, 
+        ← incre_comm_zero, decre, abs.injEq] 
+        using (ih (i := i + 1) (n := n) (u := incre 1 0 u))
+  | app t₁ t₂ ih₁ ih₂ => simp_all only [sub, incre, subst, decre]
+
+private lemma sub_comm_var {k n m u s} :
+    (((𝕧 k).sub ((n + m) + 1) (incre 1 m u)).sub m (s.sub (n + m) u))
+    = (((𝕧 k).sub m s).sub (n + m) u) := by
+  cases em (k = n + m + 1) with
+  | inl hk =>
+      have : ¬(n + m + 1 = m) := by omega
+      have : m + 1 ≤ n + m + 1 := by omega
+      simp_all only [sub, subst, ↓reduceIte, 
+        decre_incre_elim, subst_zero_incre, decre,
+        Nat.add_one_sub_one]
+  | inr hk =>
+      cases em (k = m) with
+      | inl hkm =>
+          have : ¬(n + m + 1 + 1 ≤ m) := by omega
+          simp_all only [sub, subst, ↓reduceIte, 
+            decre, decre_incre_elim]
+      | inr hkm =>
+          have : ¬(k - 1 = n + m) := by omega
+          cases em (n + m + 1 + 1 ≤ k) with
+          | inl hlt =>
+              have : ¬(k - 1 = m) := by omega
+              have : m + 1 ≤ k := by omega
+              have : m + 1 ≤ k - 1 := by omega
+              simp_all only [sub, subst, ↓reduceIte, decre,
+                left_eq_ite_iff, var.injEq]
+              exact by omega
+          | inr hlt =>
+              cases em (m + 1 ≤ k) with
+              | inl hlt =>
+                  simp_all only [not_le, sub, subst, 
+                    ↓reduceIte, decre, if_neg, 
+                    right_eq_ite_iff, var.injEq]
+                  intro h
+                  have nh : ¬(n + m < k - 1) := by omega
+                  exact (nh h).elim
+              | inr hlt =>
+                  have hneq : ¬(k = n + m) := by omega
+                  have hnlt : ¬(m < k) := by omega
+                  simp_all only [sub, subst, not_lt, subst,
+                    ↓reduceIte, decre, right_eq_ite_iff, 
+                    var.injEq]
+                  intro h
+                  have nh : ¬(n + m < k) := by omega
+                  exact (nh h).elim
+
+public theorem sub_comm {t : Term} {n m s u} :
+    ((t.sub ((n + m) + 1) (incre 1 m u)).sub m (s.sub (n + m) u))
+    = ((t.sub m s).sub (n + m) u) := by
+  induction t generalizing n m s u with
+  | var k => exact sub_comm_var
+  | abs t' ih =>
+      have : ∀ k, (incre 1 0 (decre 1 k (subst k (incre 1 k u) s))) =
+          (decre 1 (k + 1) (subst (k + 1) (incre 1 (k + 1)
+          (incre 1 0 u)) (incre 1 0 s))) := by
+        intro k
+        simpa only [sub, Nat.add_zero] 
+          using (sub_lift_zero (t := s) (n := k) (u := u) 
+                  (i := 0)).symm
+      simpa only [sub, subst, ← incre_comm_zero, 
+        decre, this, abs.injEq] 
+        using (ih (n := n) 
+          (m := m + 1) (u := incre 1 0 u) (s := incre 1 0 s))
+  | app t₁ t₂ ih₁ ih₂ => simp_all only [sub, subst, decre]
+
+public theorem sub_sub_incre {t : Term} {n k u s} :
+    ((t.sub (n + 1) (incre (1 + k) 0 u)).sub 0 (s.sub n (incre k 0 u)))
+    = ((t.sub 0 s).sub n (incre k 0 u)) := by
+  have h' :
+      ((t.sub (n + 1) (incre 1 0 (incre k 0 u))).sub 0
+          ((s.sub n (incre k 0 u)))) =
+        ((t.sub 0 s).sub n (incre k 0 u)) := by
+    simpa only [sub, incre_same_bound_elim, Nat.add_zero] 
+      using (sub_comm (t := t) (u := incre k 0 u) (s := s) 
+        (n := n) (m := 0))
+  simpa only [sub, incre_same_bound_elim] using h'
+
+
+end Term
+end Lambda
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
new file mode 100644
index 000000000..ed03ae8d0
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
@@ -0,0 +1,185 @@
+/-
+Copyright (c) 2026 zayn7lie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zayn Wang
+-/
+module
+
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.BetaReduction
+
+/-!
+# Parallel β-reduction and complete developments
+
+This file defines parallel β-reduction on de Bruijn lambda terms.  Parallel reduction
+contracts β-redexes across a term in a syntax-directed way, and it is the key technical
+device used later to prove the Church–Rosser theorem.
+
+The file also defines the complete development `Term.dev` of a term and proves that every
+parallel reduct further reduces in parallel to this complete development.
+
+## Main definitions
+
+* `Lambda.Par`: parallel β-reduction.
+* `Lambda.ParStar`: the reflexive-transitive closure of `Par`.
+* `Term.dev`: the complete development of a term.
+
+## Main lemmas
+
+* `par_refl`: reflexivity of parallel reduction.
+* `beta_subset_par`: every β-step is a parallel step.
+* `par_subset_betaStar`: every parallel step induces a β-reduction sequence.
+* `incre_par`: parallel reduction is preserved by shifting.
+* `par_subst`: parallel reduction is preserved by substitution.
+* `par_dev`: every term parallel-reduces to its complete development.
+* `par_to_dev`: every parallel reduct of a term further parallel-reduces to the complete
+  development of the original term.
+
+These results provide the diamond argument used in the final Church–Rosser proof.
+-/
+
+namespace Lambda
+open Term
+
+/-- Parallel β-reduction (syntax-directed). -/
+@[reduction_sys "∥"]
+public inductive Par : Term → Term → Prop
+  | var (n) : Par (𝕧 n) (𝕧 n)
+  | abs {t t'} : Par t t' → Par (λ.t) (λ.t')
+  | app {t t' u u'} : Par t t' → Par u u' → Par (t·u) (t'·u')
+  | red {t t' s s'} : Par t t' → Par s s' →
+      Par ((λ.t)·s) (t'.sub 0 s')
+public abbrev ParStar := Relation.ReflTransGen Par
+
+/-- reflexivity of Par. -/
+@[simp] public theorem par_refl {t} : Par t t := by
+  induction t with
+  | var n => exact Par.var n
+  | app t u iht ihu => exact Par.app iht ihu
+  | abs t iht => exact Par.abs iht
+
+/-- `Beta ⊆ Par`. -/
+public theorem beta_subset_par {a b} (h : Beta a b) : Par a b := by
+  induction h with
+  | appL h ih => exact Par.app ih par_refl
+  | appR h ih => exact Par.app par_refl ih
+  | abs h ih  => exact Par.abs ih
+  | red t s  => exact Par.red par_refl par_refl
+
+/-- Simulation lemma: `Par ⊆ BetaStar`. -/
+public theorem par_subset_betaStar {a b} (h : Par a b) :
+    BetaStar a b := by
+  induction h with
+  | var n => exact BetaStar.refl (𝕧 n)
+  | app hpt hpu hbt hbu =>
+      exact BetaStar.trans
+              (BetaStar.appL hbt) (BetaStar.appR hbu)
+  | abs h ht => exact BetaStar.abs ht
+  | red ht hs iht ihs =>
+      exact BetaStar.trans (BetaStar.appL (BetaStar.abs iht))
+        (BetaStar.tail (BetaStar.appR ihs) (Beta.red _ _))
+
+@[simp] public theorem incre_par {a b i l} (h : Par a b) :
+    Par (incre i l a) (incre i l b) := by
+  induction h generalizing l with
+  | var n => exact par_refl
+  | abs ht ih => exact Par.abs ih
+  | app ht hu iht ihu => exact Par.app iht ihu
+  | red ht hs iht ihs =>
+      have hsub {t s : Term} :
+          (incre i (l + 1) t).sub 0 (incre i l s) =
+          incre i l (t.sub 0 s) := by
+        simpa only [sub, Nat.add_zero] 
+          using (incre_sub (i := i) (l := l) (n := 0) 
+            (t := t) (s := s))
+      rw [← hsub]
+      exact Par.red iht ihs
+
+/-- Substitution lemma for `par_to_dev`. -/
+private lemma par_subst {t t' u u'} (ht : Par t t') (hu : Par u u')
+  (k : Nat) (n : Nat) :
+    Par (t.sub n (incre k 0 u)) (t'.sub n (incre k 0 u')) := by
+  match t, t' with
+  | var t, var t' => match ht with
+      | Par.var t => cases em (t = n) with
+          | inl h => 
+              simp_all only [sub, subst, ↓reduceIte, 
+                decre_incre_elim, incre_par]
+          | inr h => cases em (t < n) with
+              | inl h' => 
+                  simp_all only [sub, subst, ↓reduceIte, 
+                    decre.eq_1, par_refl]
+              | inr h' =>
+                  simp_all only [not_lt, sub, subst, 
+                  ↓reduceIte, decre.eq_1, par_refl]
+  | abs t, abs t' => match ht with
+      | Par.abs ht' =>
+          have hp := Par.abs
+            (par_subst ht' hu (1 + k) (n + 1))
+          simp_all only [sub, subst, ← incre_comm_zero, 
+            incre_same_bound_elim, decre.eq_2]
+  | app t₁ t₂, t' => match t₁ with
+      | abs t₁ => match ht with
+          | Par.app ht₁ ht₂ =>
+              exact Par.app
+                (par_subst ht₁ hu k n) (par_subst ht₂ hu k n)
+          | Par.red ht₁ ht₂ =>
+              have hp := Par.red
+                (par_subst ht₁ hu (1 + k) (n + 1))
+                (par_subst ht₂ hu k n)
+              rw [sub_sub_incre] at hp
+              simp_all only [sub, subst, ← incre_comm_zero, 
+                incre_same_bound_elim, decre.eq_3, decre]
+      | var t₁ => match ht with
+          | Par.app ht₁ ht₂ =>
+              exact Par.app
+                (par_subst ht₁ hu k n) (par_subst ht₂ hu k n)
+      | app t₁ t₁' => match ht with
+          | Par.app ht₁ ht₂ =>
+              exact Par.app
+                (par_subst ht₁ hu k n) (par_subst ht₂ hu k n)
+
+/-- Complete development (maximal Par) for a term. -/
+public def Term.dev : Term → Term
+  | 𝕧 n     => 𝕧 n
+  | λ.t     => λ.(t.dev)
+  | (λ.t)·s => t.dev.sub 0 s.dev
+  | t·u     => t.dev·u.dev
+
+/-- t.dev is a par reduction for t. -/
+public theorem par_dev (t : Term) : Par t t.dev :=
+  match t with
+  | 𝕧 n     => Par.var n
+  | λ.t     => Par.abs (par_dev t)
+  | (λ.t)·u => Par.red (par_dev t) (par_dev u)
+  | t·u => match t with
+      | var n     => Par.app (Par.var n) (par_dev u)
+      | abs t'    => Par.red (par_dev t') (par_dev u)
+      | app t₁ t₂ => Par.app (par_dev (t₁·t₂)) (par_dev u)
+
+/-- t.dev is max par reduction for t. -/
+public theorem par_to_dev {t u} (h : Par t u) : Par u (t.dev) := by
+  match t, u with
+  | var t', var u' =>
+      match h with | Par.var t' => exact Par.var t'
+  | abs t', abs u' =>
+      match h with
+      | Par.abs h' => exact Par.abs (par_to_dev h')
+  | app t t', _ => match h with
+      | Par.app ht hu =>
+          rename_i u u'
+          match t, u with
+          | abs t, abs u => match ht with
+              | Par.abs ht' =>
+                exact Par.red
+                  (par_to_dev ht') (par_to_dev hu)
+          | var _, _ =>
+              exact Par.app (par_to_dev ht) (par_to_dev hu)
+          | app _ _, _ =>
+              exact Par.app (par_to_dev ht) (par_to_dev hu)
+      | Par.red hu ht =>
+          have hp := par_subst
+            (par_to_dev hu) (par_to_dev ht) 0 0
+          repeat rw [incre_rfl] at hp
+          exact hp
+
+end Lambda