From 6102cf915d9ccb012de31c93d292cc5a961fc5e8 Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Tue, 7 Apr 2026 07:03:11 -0400
Subject: [PATCH 01/12] =?UTF-8?q?feat:=20Church=E2=80=93Rosser=20theorem?=
 =?UTF-8?q?=20(Q1308502)=20for=20ULC=20(de=20Bruijn)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../LambdaCalculus/BetaReduction.lean         |  89 +++++
 .../LambdaCalculus/ChurchRosser.lean          |  58 +++
 .../LambdaCalculus/ConfluentReduction.lean    |  81 +++++
 .../LambdaCalculus/DeBruijnSyntax.lean        | 330 ++++++++++++++++++
 .../LambdaCalculus/ParallelReduction.lean     | 177 ++++++++++
 5 files changed, 735 insertions(+)
 create mode 100644 Cslib/Computability/LambdaCalculus/BetaReduction.lean
 create mode 100644 Cslib/Computability/LambdaCalculus/ChurchRosser.lean
 create mode 100644 Cslib/Computability/LambdaCalculus/ConfluentReduction.lean
 create mode 100644 Cslib/Computability/LambdaCalculus/DeBruijnSyntax.lean
 create mode 100644 Cslib/Computability/LambdaCalculus/ParallelReduction.lean

diff --git a/Cslib/Computability/LambdaCalculus/BetaReduction.lean b/Cslib/Computability/LambdaCalculus/BetaReduction.lean
new file mode 100644
index 000000000..72d6adca9
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/BetaReduction.lean
@@ -0,0 +1,89 @@
+/-
+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.Computability.LambdaCalculus.DeBruijnSyntax
+public import Mathlib.Logic.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). -/
+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/Computability/LambdaCalculus/ChurchRosser.lean b/Cslib/Computability/LambdaCalculus/ChurchRosser.lean
new file mode 100644
index 000000000..2ed766c5b
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/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.Computability.LambdaCalculus.ConfluentReduction
+public import Cslib.Computability.LambdaCalculus.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 Term
+
+/-- 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 :=
+    confluent_of_diamond (r := Par) diamond_par
+  -- Identify BetaStar and ParStar via sandwich
+  have hEq {a b : Term} : BetaStar a b ↔ ParStar a b :=
+      rtc_eq_of_sandwich (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/Computability/LambdaCalculus/ConfluentReduction.lean b/Cslib/Computability/LambdaCalculus/ConfluentReduction.lean
new file mode 100644
index 000000000..3abcc1438
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/ConfluentReduction.lean
@@ -0,0 +1,81 @@
+/-
+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 Mathlib.Logic.Relation
+
+/-!
+# Confluent Reduction
+
+This file contain the definition of the Diamond property and
+Confluent property. Then investigate the relationship between
+these two property.
+
+## Main definition
+
+* `Diamond r`: $r$ is diamond iff we have $a$ to $b$ and $a$ to $c$ through $r$,
+    then we could find a $d$ where $b$ and $c$ arrives through $r$.
+* `Confluent r`: $r$ is confluent iff we have $a$ to $b$ and $a$ to $c$ through $r^*$,
+    then we could find a $d$ where $b$ and $c$ arrives through $r^*$.
+
+## Main Theorem
+
+* `confluent_of_diamond`: Diamond is the confluence of the refl-closure.
+* `rtc_eq_of_sandwich`: if we can find a relation $p$ where `r ⊆ p ⊆ r*`,
+    then the refl-trans closure $p^* = r^*$.
+
+-/
+
+open Relation
+
+namespace Lambda
+
+@[simp, expose] public def Diamond {α} (r : α → α → Prop) : Prop :=
+  ∀ ⦃a b c⦄, r a b → r a c → ∃ d, r b d ∧ r c d
+
+@[simp, expose] public def Confluent {α} (r : α → α → Prop) : Prop :=
+  ∀ ⦃a b c⦄,
+    ReflTransGen r a b →
+    ReflTransGen r a c →
+    ∃ d, ReflTransGen r b d ∧ ReflTransGen r c d
+
+/-- Diamond = confluence of the refl–trans closure. -/
+public theorem confluent_of_diamond {α} {r : α → α → Prop}
+    (hd : Diamond r) : Confluent r := by
+  have strip : ∀ ⦃a b c⦄, r a b → ReflTransGen r a c →
+      ∃ d, ReflTransGen r b d ∧ r c d := by
+    intro a b c hab hac
+    induction hac with
+    | refl => exact ⟨b, ReflTransGen.refl, hab⟩
+    | tail had hce ih =>
+        rcases ih with ⟨d, hbd, hcd⟩
+        rcases hd hcd hce with ⟨f, hdf, hef⟩
+        exact ⟨f, ReflTransGen.tail hbd hdf, hef⟩
+  intro a b c hab hac
+  induction hab with
+  | refl => exact ⟨c, hac, ReflTransGen.refl⟩
+  | tail hab hbc ih =>
+      rcases ih with ⟨d, hbd, hcd⟩
+      rcases strip hbc hbd with ⟨f, hcf, hdf⟩
+      exact ⟨f, hcf, ReflTransGen.tail hcd hdf⟩
+
+/-- Sandwich: if `r ⊆ p ⊆ r*` then `r* = p*`. -/
+public theorem rtc_eq_of_sandwich {α} {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)
+
+end Lambda
diff --git a/Cslib/Computability/LambdaCalculus/DeBruijnSyntax.lean b/Cslib/Computability/LambdaCalculus/DeBruijnSyntax.lean
new file mode 100644
index 000000000..00ee91fe8
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/DeBruijnSyntax.lean
@@ -0,0 +1,330 @@
+/-
+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
+
+/-!
+# 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`. -/
+@[simp, 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`. -/
+@[simp, 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 c t` decrements free vars `> c` by 1. -/
+@[simp, expose] public def decre (l : Nat) : Term → Term
+  | var k   => if l < k then var (k - 1) else var k
+  | abs t   => abs (decre (l + 1) t)
+  | app t u => app (decre l t) (decre l u)
+
+/-- Substitute into the body of a lambda: `(λ.t) s` -/
+@[simp, expose] public def sub (t : Term) (n : Nat) (s : Term) := decre n (subst n (incre 1 n s) t)
+
+/-- 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
+  | abs t ih => simp_all
+  | app t u iht ihu => simp_all
+
+/-- Decrement of increment with same bound is the same.
+Lemma for `var_sub` -/
+@[simp] public theorem decre_incre_elim {l t} : decre 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 [Nat.lt_succ_of_le h]
+      | inr h =>
+          have : ¬(l < k) := by omega
+          simp only [if_neg h, if_neg this]
+  | abs t ih => simp_all
+  | app t u iht ihu => simp_all
+
+/-- 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
+  simp_all only [sub, subst, Nat.ne_of_lt hk, ↓reduceIte, decre, Nat.not_lt_of_gt hk]
+
+/-- 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
+  simp_all [Nat.ne_of_gt hk]
+
+/-- 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 [le_trans h (Nat.le_add_right k j)]
+          simp_all [Nat.add_comm, Nat.add_left_comm]
+      | inr h => simp_all [if_neg h]
+  | abs t' ih => simp_all
+  | app t₁ t₂ ih₁ ih₂ => simp_all
+
+/-- 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 [le_trans this (Nat.le_add_right _ _)]
+          simp [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 [Nat.add_assoc, Nat.add_comm]
+  | app t₁ t₂ ih₁ ih₂ => simp_all
+
+public theorem incre_comm_zero {n s} :
+    incre 1 (n + 1) (incre 1 0 s) =
+      incre 1 0 (incre 1 n s) := by
+  simpa 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 [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 [if_neg this]
+  | inr h =>
+      cases em (l + n + 1 ≤ k) with
+      | inl h' =>
+          have : k + i ≠ n := by omega
+          have : n < k := by omega
+          have : l + n ≤ k - 1 := by omega
+          have : n < k + i := by omega
+          have : k + i - 1 = k - 1 + i := by omega
+          simp_all only [ne_eq, 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'' =>
+              simp_all only [↓reduceIte, incre,
+                right_eq_ite_iff, var.injEq, Nat.left_eq_add]
+              intro; omega
+          | inr h'' =>
+              simp_all only [not_lt, if_neg h'', incre,
+                right_eq_ite_iff, var.injEq, Nat.left_eq_add]
+              intro; omega
+
+/-- 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 [← incre_comm_zero, ← incre_comm] using ih
+  | app t₁ t₂ ih₁ ih₂ => simp_all
+
+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
+  | app t v iht ihv => simp_all
+
+private lemma sub_incre_same {u r m} :
+    ((incre 1 m u).sub m r) = u := by
+  simp_all [subst_zero_incre]
+
+@[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
+      | inr hk =>
+        cases em (k < n + i) with
+          | inl hlt =>
+              have hlt' : k + 1 < n + i + 1 := by omega
+              have hnlt : ¬(n + i < k) := by omega
+              simp only [sub, incre, subst]
+              cases em (i ≤ k) with
+              | inl hlt' => simp_all [if_neg hnlt]
+              | inr hlt' =>
+                  have h' : ¬(k = n + i + 1) := by omega
+                  have : ¬(n + i + 1 < k) := by omega
+                  simp_all [if_neg hlt', if_neg this, if_neg hnlt]
+          | inr hlt =>
+              have hle : i ≤ k := by omega
+              have hgt : n + i < k := by omega
+              have hlt : i ≤ k - 1 := by omega
+              simp_all
+              omega
+  | abs t ih =>
+      simpa [← incre_comm_zero] using
+        (ih (i := i + 1) (n := n) (u := incre 1 0 u))
+  | app t₁ t₂ ih₁ ih₂ => simp_all
+
+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 < n + m + 1 := by omega
+      simp_all [subst_zero_incre]
+  | inr hk =>
+      cases em (k = m) with
+      | inl hkm =>
+          have : ¬(n + m + 1 < m) := by omega
+          simp_all [if_neg this]
+      | inr hkm =>
+          have : ¬(k - 1 = n + m) := by omega
+          cases em (n + m + 1 < k) with
+          | inl hlt =>
+              have : ¬(k - 1 = m) := by omega
+              have : m < k := by omega
+              have : m < k - 1 := by omega
+              simp_all only [sub, subst, ↓reduceIte, decre,
+                left_eq_ite_iff, not_lt, Nat.sub_le_iff_le_add, var.injEq]
+              intro h
+              exact (Nat.not_lt_of_ge h hlt).elim
+          | inr hlt =>
+              simp_all only [not_lt, sub, subst,
+                ↓reduceIte, decre, if_neg hlt]
+              cases em (m < k) with
+              | inl hlt =>
+                  simp_all only [↓reduceIte, subst, decre,
+                    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 [not_false_eq_true, not_lt, if_neg hnlt, 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 k (subst k (incre 1 k u) s))) =
+          (decre (k + 1) (subst (k + 1) (incre 1 (k + 1)
+          (incre 1 0 u)) (incre 1 0 s))) := by
+        intro k
+        simpa using
+        (sub_lift_zero (t := s) (n := k) (u := u) (i := 0)).symm
+      simpa [← incre_comm_zero, this] using
+        (ih (n := n) (m := m + 1) (u := incre 1 0 u) (s := incre 1 0 s))
+  | app t₁ t₂ ih₁ ih₂ => simp_all
+
+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 using (sub_comm (t := t) (u := incre k 0 u) (s := s) (n := n) (m := 0))
+  simpa using h'
+
+
+end Term
+end Lambda
diff --git a/Cslib/Computability/LambdaCalculus/ParallelReduction.lean b/Cslib/Computability/LambdaCalculus/ParallelReduction.lean
new file mode 100644
index 000000000..471fbd8fa
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/ParallelReduction.lean
@@ -0,0 +1,177 @@
+/-
+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.Computability.LambdaCalculus.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). -/
+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 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
+          | inr h => cases em (t < n) with
+              | inl h' => simp_all
+              | inr h' =>
+                  simp_all [ (Nat.lt_of_le_of_ne
+                      (Nat.le_of_not_gt h') (Ne.symm h))]
+  | abs t, abs t' => match ht with
+      | Par.abs ht' =>
+          have hp := Par.abs
+            (par_subst ht' hu (1 + k) (n + 1))
+          simp_all [← incre_comm_zero]
+  | 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 [← incre_comm_zero]
+      | 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

From 1c74c358e126c5920557e78b003d76bdc7570727 Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 06:38:27 -0400
Subject: [PATCH 02/12] upd: change dir

---
 .../LambdaCalculus/Unscoped/Untyped}/BetaReduction.lean       | 2 +-
 .../LambdaCalculus/Unscoped/Untyped}/ChurchRosser.lean        | 4 ++--
 .../LambdaCalculus/Unscoped/Untyped}/ConfluentReduction.lean  | 0
 .../LambdaCalculus/Unscoped/Untyped}/DeBruijnSyntax.lean      | 0
 .../LambdaCalculus/Unscoped/Untyped}/ParallelReduction.lean   | 2 +-
 5 files changed, 4 insertions(+), 4 deletions(-)
 rename Cslib/{Computability/LambdaCalculus => Languages/LambdaCalculus/Unscoped/Untyped}/BetaReduction.lean (97%)
 rename Cslib/{Computability/LambdaCalculus => Languages/LambdaCalculus/Unscoped/Untyped}/ChurchRosser.lean (91%)
 rename Cslib/{Computability/LambdaCalculus => Languages/LambdaCalculus/Unscoped/Untyped}/ConfluentReduction.lean (100%)
 rename Cslib/{Computability/LambdaCalculus => Languages/LambdaCalculus/Unscoped/Untyped}/DeBruijnSyntax.lean (100%)
 rename Cslib/{Computability/LambdaCalculus => Languages/LambdaCalculus/Unscoped/Untyped}/ParallelReduction.lean (98%)

diff --git a/Cslib/Computability/LambdaCalculus/BetaReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
similarity index 97%
rename from Cslib/Computability/LambdaCalculus/BetaReduction.lean
rename to Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
index 72d6adca9..782d04915 100644
--- a/Cslib/Computability/LambdaCalculus/BetaReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
@@ -5,7 +5,7 @@ Authors: Zayn Wang
 -/
 module
 
-public import Cslib.Computability.LambdaCalculus.DeBruijnSyntax
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.DeBruijnSyntax
 public import Mathlib.Logic.Relation
 
 /-!
diff --git a/Cslib/Computability/LambdaCalculus/ChurchRosser.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
similarity index 91%
rename from Cslib/Computability/LambdaCalculus/ChurchRosser.lean
rename to Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
index 2ed766c5b..0fb473026 100644
--- a/Cslib/Computability/LambdaCalculus/ChurchRosser.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
@@ -5,8 +5,8 @@ Authors: Zayn Wang
 -/
 module
 
-public import Cslib.Computability.LambdaCalculus.ConfluentReduction
-public import Cslib.Computability.LambdaCalculus.ParallelReduction
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ConfluentReduction
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ParallelReduction
 
 /-!
 # The Church–Rosser theorem for β-reduction
diff --git a/Cslib/Computability/LambdaCalculus/ConfluentReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
similarity index 100%
rename from Cslib/Computability/LambdaCalculus/ConfluentReduction.lean
rename to Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
diff --git a/Cslib/Computability/LambdaCalculus/DeBruijnSyntax.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
similarity index 100%
rename from Cslib/Computability/LambdaCalculus/DeBruijnSyntax.lean
rename to Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
diff --git a/Cslib/Computability/LambdaCalculus/ParallelReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
similarity index 98%
rename from Cslib/Computability/LambdaCalculus/ParallelReduction.lean
rename to Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
index 471fbd8fa..99b33f7cf 100644
--- a/Cslib/Computability/LambdaCalculus/ParallelReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
@@ -5,7 +5,7 @@ Authors: Zayn Wang
 -/
 module
 
-public import Cslib.Computability.LambdaCalculus.BetaReduction
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.BetaReduction
 
 /-!
 # Parallel β-reduction and complete developments

From d381f04bfa4f2873bbf3f1a84e070f5c0976ce6f Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 06:45:13 -0400
Subject: [PATCH 03/12] upd: localize from  to

---
 .../LambdaCalculus/Unscoped/Untyped/BetaReduction.lean          | 2 +-
 .../LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
index 782d04915..bb465f982 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
@@ -6,7 +6,7 @@ Authors: Zayn Wang
 module
 
 public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.DeBruijnSyntax
-public import Mathlib.Logic.Relation
+public import Cslib.Foundations.Data.Relation
 
 /-!
 # One-step β-reduction and its reflexive-transitive closure
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
index 3abcc1438..3bebacec7 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
@@ -5,7 +5,7 @@ Authors: Zayn Wang
 -/
 module
 
-public import Mathlib.Logic.Relation
+public import Cslib.Foundations.Data.Relation 
 
 /-!
 # Confluent Reduction

From 67a3cb1e241791b891b4c67fb95ee8ac3525a7de Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 07:10:54 -0400
Subject: [PATCH 04/12] upd: eliminate  for de bruijn syntax and explicit all 
 and

---
 .../Unscoped/Untyped/DeBruijnSyntax.lean      | 120 +++++++++++-------
 .../Unscoped/Untyped/ParallelReduction.lean   |  25 ++--
 2 files changed, 92 insertions(+), 53 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
index 00ee91fe8..60ce84e0b 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
@@ -57,32 +57,32 @@ notation:max "λ." t => Term.abs t
 infixl:77 "·" => Term.app
 
 /-- `incre i l t` increments `i` for all free vars `≥ l`. -/
-@[simp, expose] public def incre (i : Nat) (l : Nat) : Term → Term
+@[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`. -/
-@[simp, expose] public def subst (j : Nat) (s : Term) : Term → Term
+@[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 c t` decrements free vars `> c` by 1. -/
-@[simp, expose] public def decre (l : Nat) : Term → Term
+@[expose] public def decre (l : Nat) : Term → Term
   | var k   => if l < k then var (k - 1) else var k
   | abs t   => abs (decre (l + 1) t)
   | app t u => app (decre l t) (decre l u)
 
 /-- Substitute into the body of a lambda: `(λ.t) s` -/
-@[simp, expose] public def sub (t : Term) (n : Nat) (s : Term) := decre n (subst n (incre 1 n s) t)
+@[expose] public def sub (t : Term) (n : Nat) (s : Term) := decre n (subst n (incre 1 n s) t)
 
 /-- 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
-  | abs t ih => simp_all
-  | app t u iht ihu => simp_all
+  | 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` -/
@@ -91,12 +91,13 @@ Lemma for `var_sub` -/
   | var k =>
       unfold decre incre
       cases em (l ≤ k) with
-      | inl h => simp_all [Nat.lt_succ_of_le h]
+      | inl h => simp_all only [↓reduceIte, 
+          Nat.lt_succ_of_le h, Nat.add_one_sub_one]
       | inr h =>
           have : ¬(l < k) := by omega
           simp only [if_neg h, if_neg this]
-  | abs t ih => simp_all
-  | app t u iht ihu => simp_all
+  | 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
@@ -110,7 +111,8 @@ Lemma for `var_sub` -/
 /-- 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
-  simp_all [Nat.ne_of_gt hk]
+  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
@@ -121,11 +123,12 @@ his idea of generalizing proper variable. -/
   | var k =>
       cases em (n ≤ k) with
       | inl h =>
-          simp_all [le_trans h (Nat.le_add_right k j)]
-          simp_all [Nat.add_comm, Nat.add_left_comm]
-      | inr h => simp_all [if_neg h]
-  | abs t' ih => simp_all
-  | app t₁ t₂ ih₁ ih₂ => simp_all
+          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} :
@@ -136,8 +139,10 @@ public theorem incre_comm {i j k l t} :
       cases em (k + l ≤ n) with
       | inl h =>
           have : l ≤ n := le_trans (Nat.le_add_left _ _) h
-          simp_all [le_trans this (Nat.le_add_right _ _)]
-          simp [Nat.add_comm, Nat.add_left_comm]
+          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
@@ -154,18 +159,19 @@ public theorem incre_comm {i j k l t} :
               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 [Nat.add_assoc, Nat.add_comm]
-  | app t₁ t₂ ih₁ ih₂ => simp_all
+  | 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 using
-      (incre_comm (i := 1) (l := 0) (j := 1) (k := n) (t := s))
+  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 [incre_comm_zero]
+  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) =
@@ -173,7 +179,8 @@ private lemma incre_sub_var {i l n k s} :
   cases em (k = n) with
   | inl h =>
       have : ¬ (l + n + 1 ≤ n) := by omega
-      simp_all [if_neg this]
+      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' =>
@@ -204,8 +211,10 @@ private lemma incre_sub_var {i l n k s} :
   induction t generalizing l n s with
   | var k => exact incre_sub_var
   | abs t' ih =>
-      simpa [← incre_comm_zero, ← incre_comm] using ih
-  | app t₁ t₂ ih₁ ih₂ => simp_all
+      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
@@ -219,12 +228,12 @@ private lemma subst_zero_incre {n t u} :
           simp_all only [not_le, incre, if_neg h,
             subst, ite_eq_right_iff]
           intro; omega
-  | abs t ih => simp_all
-  | app t v iht ihv => simp_all
+  | 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 [subst_zero_incre]
+  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)) =
@@ -232,7 +241,9 @@ private lemma sub_incre_same {u r m} :
   induction t generalizing n u i with
   | var k =>
       cases em (k = n + i) with
-      | inl hk => simp_all
+      | 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 =>
@@ -240,21 +251,32 @@ private lemma sub_incre_same {u r m} :
               have hnlt : ¬(n + i < k) := by omega
               simp only [sub, incre, subst]
               cases em (i ≤ k) with
-              | inl hlt' => simp_all [if_neg hnlt]
+              | inl hlt' => 
+                  simp_all only [Nat.add_lt_add_iff_right, 
+                    not_lt, ↓reduceIte, subst, 
+                    Nat.add_right_cancel_iff, decre,
+                    Nat.add_one_sub_one, if_neg hnlt, incre]
               | inr hlt' =>
                   have h' : ¬(k = n + i + 1) := by omega
                   have : ¬(n + i + 1 < k) := by omega
-                  simp_all [if_neg hlt', if_neg this, if_neg hnlt]
+                  simp_all only [Nat.add_lt_add_iff_right, 
+                    not_lt, not_le, if_neg hlt', subst, 
+                    ↓reduceIte, decre, if_neg this,
+                    if_neg hnlt, incre]
           | inr hlt =>
               have hle : i ≤ k := by omega
               have hgt : n + i < k := by omega
               have hlt : i ≤ k - 1 := by omega
-              simp_all
+              simp_all only [not_lt, sub, incre, ↓reduceIte, 
+                subst, Nat.add_right_cancel_iff, decre, 
+                Nat.add_lt_add_iff_right, 
+                Nat.add_one_sub_one, var.injEq]
               omega
   | abs t ih =>
-      simpa [← incre_comm_zero] using
-        (ih (i := i + 1) (n := n) (u := incre 1 0 u))
-  | app t₁ t₂ ih₁ ih₂ => simp_all
+      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))
@@ -263,12 +285,15 @@ private lemma sub_comm_var {k n m u s} :
   | inl hk =>
       have : ¬(n + m + 1 = m) := by omega
       have : m < n + m + 1 := by omega
-      simp_all [subst_zero_incre]
+      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 < m) := by omega
-          simp_all [if_neg this]
+          simp_all only [not_lt, sub, subst, ↓reduceIte, 
+            decre, if_neg this, decre_incre_elim]
       | inr hkm =>
           have : ¬(k - 1 = n + m) := by omega
           cases em (n + m + 1 < k) with
@@ -309,11 +334,14 @@ public theorem sub_comm {t : Term} {n m s u} :
           (decre (k + 1) (subst (k + 1) (incre 1 (k + 1)
           (incre 1 0 u)) (incre 1 0 s))) := by
         intro k
-        simpa using
-        (sub_lift_zero (t := s) (n := k) (u := u) (i := 0)).symm
-      simpa [← incre_comm_zero, this] using
-        (ih (n := n) (m := m + 1) (u := incre 1 0 u) (s := incre 1 0 s))
-  | app t₁ t₂ ih₁ ih₂ => simp_all
+        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)))
@@ -322,8 +350,10 @@ public theorem sub_sub_incre {t : Term} {n k u s} :
       ((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 using (sub_comm (t := t) (u := incre k 0 u) (s := s) (n := n) (m := 0))
-  simpa using h'
+    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
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
index 99b33f7cf..d3031b03a 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
@@ -87,8 +87,9 @@ public theorem par_subset_betaStar {a b} (h : Par a b) :
       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 using
-          (incre_sub (i := i) (l := l) (n := 0) (t := t) (s := s))
+        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
 
@@ -99,17 +100,24 @@ private lemma par_subst {t t' u u'} (ht : Par t t') (hu : Par u u')
   match t, t' with
   | var t, var t' => match ht with
       | Par.var t => cases em (t = n) with
-          | inl h => simp_all
+          | inl h => 
+              simp_all only [sub, subst, ↓reduceIte, 
+                decre_incre_elim, incre_par]
           | inr h => cases em (t < n) with
-              | inl h' => simp_all
+              | inl h' => 
+                  simp_all only [sub, subst, ↓reduceIte, 
+                    decre.eq_1, par_refl]
               | inr h' =>
-                  simp_all [ (Nat.lt_of_le_of_ne
-                      (Nat.le_of_not_gt h') (Ne.symm h))]
+                  simp_all only [not_lt, sub, subst, 
+                  ↓reduceIte, decre.eq_1, 
+                  (Nat.lt_of_le_of_ne (Nat.le_of_not_gt h') 
+                  (Ne.symm h)), 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 [← incre_comm_zero]
+          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₂ =>
@@ -120,7 +128,8 @@ private lemma par_subst {t t' u u'} (ht : Par t t') (hu : Par u u')
                 (par_subst ht₁ hu (1 + k) (n + 1))
                 (par_subst ht₂ hu k n)
               rw [sub_sub_incre] at hp
-              simp_all [← incre_comm_zero]
+              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

From 653d4dcf094eb0cedaf683709911c13ce0f71ded Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 07:13:29 -0400
Subject: [PATCH 05/12] upd: eliminate  for diamond and Confluent definition

---
 .../LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean   | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
index 3bebacec7..113601003 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
@@ -33,10 +33,10 @@ open Relation
 
 namespace Lambda
 
-@[simp, expose] public def Diamond {α} (r : α → α → Prop) : Prop :=
+@[expose] public def Diamond {α} (r : α → α → Prop) : Prop :=
   ∀ ⦃a b c⦄, r a b → r a c → ∃ d, r b d ∧ r c d
 
-@[simp, expose] public def Confluent {α} (r : α → α → Prop) : Prop :=
+@[expose] public def Confluent {α} (r : α → α → Prop) : Prop :=
   ∀ ⦃a b c⦄,
     ReflTransGen r a b →
     ReflTransGen r a c →

From fd07da03b23b970234ae0e946b65922adf216934 Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 07:57:38 -0400
Subject: [PATCH 06/12] upd: generalize decrement for consistency

---
 .../Unscoped/Untyped/DeBruijnSyntax.lean      | 105 ++++++++++--------
 .../Unscoped/Untyped/ParallelReduction.lean   |   4 +-
 2 files changed, 59 insertions(+), 50 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
index 60ce84e0b..520d263ab 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
@@ -68,14 +68,14 @@ infixl:77 "·" => Term.app
   | abs t   => abs (subst (j + 1) (incre 1 0 s) t)
   | app t u => app (subst j s t) (subst j s u)
 
-/-- `decre c t` decrements free vars `> c` by 1. -/
-@[expose] public def decre (l : Nat) : Term → Term
-  | var k   => if l < k then var (k - 1) else var k
-  | abs t   => abs (decre (l + 1) t)
-  | app t u => app (decre l t) (decre l u)
+/-- `decre c t` decrements free vars `> c` by `i`. -/
+@[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 n (subst n (incre 1 n s) t)
+@[expose] public def sub (t : Term) (n : Nat) (s : Term) := decre 1 n (subst n (incre 1 n s) t)
 
 /-- Increment of 0 is identity -/
 @[simp] public theorem incre_rfl {l t} : incre 0 l t = t := by
@@ -86,15 +86,15 @@ infixl:77 "·" => Term.app
 
 /-- Decrement of increment with same bound is the same.
 Lemma for `var_sub` -/
-@[simp] public theorem decre_incre_elim {l t} : decre l (incre 1 l t) = t := by
+@[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.lt_succ_of_le h, Nat.add_one_sub_one]
+          Nat.add_le_add_iff_right, Nat.add_one_sub_one]
       | inr h =>
-          have : ¬(l < k) := by omega
+          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]
@@ -106,11 +106,14 @@ Lemma for `var_sub` -/
 /-- 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
-  simp_all only [sub, subst, Nat.ne_of_lt hk, ↓reduceIte, decre, Nat.not_lt_of_gt hk]
+  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]
 
@@ -184,25 +187,31 @@ private lemma incre_sub_var {i l n k s} :
   | inr h =>
       cases em (l + n + 1 ≤ k) with
       | inl h' =>
-          have : k + i ≠ n := by omega
-          have : n < k := by omega
+          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 : n < k + i := by omega
           have : k + i - 1 = k - 1 + i := by omega
-          simp_all only [ne_eq, sub, incre,
-            ↓reduceIte, subst, decre]
+          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'' =>
-              simp_all only [↓reduceIte, incre,
+              have : (n + 1 ≤ k) := by omega
+              simp_all only [↓reduceIte, incre, 
                 right_eq_ite_iff, var.injEq, Nat.left_eq_add]
-              intro; omega
+              intro h
+              have : ¬(l + n ≤ k - 1) := by omega
+              exact (this h).elim
           | inr h'' =>
-              simp_all only [not_lt, if_neg h'', incre,
+              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; omega
+              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} :
@@ -248,30 +257,33 @@ private lemma sub_incre_same {u r m} :
         cases em (k < n + i) with
           | inl hlt =>
               have hlt' : k + 1 < n + i + 1 := by omega
-              have hnlt : ¬(n + i < k) := 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_lt, ↓reduceIte, subst, 
+                    not_le, ↓reduceIte, subst, 
                     Nat.add_right_cancel_iff, decre,
-                    Nat.add_one_sub_one, if_neg hnlt, incre]
+                    Nat.add_le_add_iff_right, 
+                    Nat.add_one_sub_one, if_neg, incre]
               | inr hlt' =>
                   have h' : ¬(k = n + i + 1) := by omega
-                  have : ¬(n + i + 1 < k) := by omega
                   simp_all only [Nat.add_lt_add_iff_right, 
-                    not_lt, not_le, if_neg hlt', subst, 
-                    ↓reduceIte, decre, if_neg this,
-                    if_neg hnlt, incre]
+                    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 < 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_lt_add_iff_right, 
+                Nat.add_le_add_iff_right, 
                 Nat.add_one_sub_one, var.injEq]
-              omega
+              exact by omega
   | abs t ih =>
       simpa only [sub, incre, subst, 
         ← incre_comm_zero, decre, abs.injEq] 
@@ -284,33 +296,31 @@ private lemma sub_comm_var {k n m u s} :
   cases em (k = n + m + 1) with
   | inl hk =>
       have : ¬(n + m + 1 = m) := by omega
-      have : m < n + m + 1 := 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 < m) := by omega
-          simp_all only [not_lt, sub, subst, ↓reduceIte, 
-            decre, if_neg this, decre_incre_elim]
+          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 < k) with
+          cases em (n + m + 1 + 1 ≤ k) with
           | inl hlt =>
               have : ¬(k - 1 = m) := by omega
-              have : m < k := by omega
-              have : m < k - 1 := 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, not_lt, Nat.sub_le_iff_le_add, var.injEq]
-              intro h
-              exact (Nat.not_lt_of_ge h hlt).elim
+                left_eq_ite_iff, var.injEq]
+              exact by omega
           | inr hlt =>
-              simp_all only [not_lt, sub, subst,
-                ↓reduceIte, decre, if_neg hlt]
-              cases em (m < k) with
+              cases em (m + 1 ≤ k) with
               | inl hlt =>
-                  simp_all only [↓reduceIte, subst, decre,
+                  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
@@ -318,8 +328,9 @@ private lemma sub_comm_var {k n m u s} :
               | inr hlt =>
                   have hneq : ¬(k = n + m) := by omega
                   have hnlt : ¬(m < k) := by omega
-                  simp_all only [not_false_eq_true, not_lt, if_neg hnlt, subst,
-                    ↓reduceIte, decre, right_eq_ite_iff, var.injEq]
+                  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
@@ -330,8 +341,8 @@ public theorem sub_comm {t : Term} {n m s u} :
   induction t generalizing n m s u with
   | var k => exact sub_comm_var
   | abs t' ih =>
-      have : ∀ k, (incre 1 0 (decre k (subst k (incre 1 k u) s))) =
-          (decre (k + 1) (subst (k + 1) (incre 1 (k + 1)
+      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] 
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
index d3031b03a..2953cb14c 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
@@ -109,9 +109,7 @@ private lemma par_subst {t t' u u'} (ht : Par t t') (hu : Par u u')
                     decre.eq_1, par_refl]
               | inr h' =>
                   simp_all only [not_lt, sub, subst, 
-                  ↓reduceIte, decre.eq_1, 
-                  (Nat.lt_of_le_of_ne (Nat.le_of_not_gt h') 
-                  (Ne.symm h)), par_refl]
+                  ↓reduceIte, decre.eq_1, par_refl]
   | abs t, abs t' => match ht with
       | Par.abs ht' =>
           have hp := Par.abs

From 089b99ad499d7ea7448bc72b982b4d71ee11a1fd Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 08:18:11 -0400
Subject: [PATCH 07/12] upd: instantiate with

---
 .../LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean      | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
index 520d263ab..848b07087 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
@@ -6,6 +6,7 @@ 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
@@ -77,6 +78,10 @@ infixl:77 "·" => Term.app
 /-- 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

From 901cf2834a9d3c9d2221eae3c6f703e4ab8445cc Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 08:25:37 -0400
Subject: [PATCH 08/12] upd: newline between theorems

---
 .../LambdaCalculus/Unscoped/Untyped/BetaReduction.lean       | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
index bb465f982..e0d57e533 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
@@ -50,12 +50,15 @@ 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 :=
@@ -66,11 +69,13 @@ public theorem appL {t t' u : Term} (h : BetaStar t t') :
   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') :

From 28e7a79deee335a4afc846052de594f970672010 Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 16:06:11 -0400
Subject: [PATCH 09/12] upd: clean up `ConfluentReduction.lean` to
 `Cslib.Foundations.Data.Relation`, and add `rtc_eq_of_sandwich`

---
 Cslib/Foundations/Data/Relation.lean             | 16 ++++++++++++++++
 .../Unscoped/Untyped/ChurchRosser.lean           |  8 ++++----
 2 files changed, 20 insertions(+), 4 deletions(-)

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/ChurchRosser.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
index 0fb473026..fc6c54f2c 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean
@@ -5,7 +5,7 @@ Authors: Zayn Wang
 -/
 module
 
-public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ConfluentReduction
+public import Cslib.Foundations.Data.Relation
 public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ParallelReduction
 
 /-!
@@ -31,7 +31,7 @@ the complete-development machinery from `ParallelReduction`.
 -/
 
 namespace Lambda
-open Term
+open Relation
 
 /-- Parallel Reduction is Diamond. -/
 private lemma diamond_par : Diamond Par := by
@@ -42,10 +42,10 @@ private lemma diamond_par : Diamond Par := by
 public theorem churchRosser_beta : Confluent Beta := by
   -- Confluence of Par from diamond
   have hPar : Confluent Par :=
-    confluent_of_diamond (r := Par) diamond_par
+    Diamond.toConfluent (r := Par) diamond_par
   -- Identify BetaStar and ParStar via sandwich
   have hEq {a b : Term} : BetaStar a b ↔ ParStar a b :=
-      rtc_eq_of_sandwich (r := Beta) (p := Par)
+      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

From d38b50169dcbee2c72574911b79a68c1d6402b3a Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 16:07:14 -0400
Subject: [PATCH 10/12] upd: clean up `ConfluentReduction.lean` to
 `Cslib.Foundations.Data.Relation`, and add `rtc_eq_of_sandwich`

---
 .../Unscoped/Untyped/ConfluentReduction.lean  | 81 -------------------
 1 file changed, 81 deletions(-)
 delete mode 100644 Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
deleted file mode 100644
index 113601003..000000000
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ConfluentReduction.lean
+++ /dev/null
@@ -1,81 +0,0 @@
-/-
-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 
-
-/-!
-# Confluent Reduction
-
-This file contain the definition of the Diamond property and
-Confluent property. Then investigate the relationship between
-these two property.
-
-## Main definition
-
-* `Diamond r`: $r$ is diamond iff we have $a$ to $b$ and $a$ to $c$ through $r$,
-    then we could find a $d$ where $b$ and $c$ arrives through $r$.
-* `Confluent r`: $r$ is confluent iff we have $a$ to $b$ and $a$ to $c$ through $r^*$,
-    then we could find a $d$ where $b$ and $c$ arrives through $r^*$.
-
-## Main Theorem
-
-* `confluent_of_diamond`: Diamond is the confluence of the refl-closure.
-* `rtc_eq_of_sandwich`: if we can find a relation $p$ where `r ⊆ p ⊆ r*`,
-    then the refl-trans closure $p^* = r^*$.
-
--/
-
-open Relation
-
-namespace Lambda
-
-@[expose] public def Diamond {α} (r : α → α → Prop) : Prop :=
-  ∀ ⦃a b c⦄, r a b → r a c → ∃ d, r b d ∧ r c d
-
-@[expose] public def Confluent {α} (r : α → α → Prop) : Prop :=
-  ∀ ⦃a b c⦄,
-    ReflTransGen r a b →
-    ReflTransGen r a c →
-    ∃ d, ReflTransGen r b d ∧ ReflTransGen r c d
-
-/-- Diamond = confluence of the refl–trans closure. -/
-public theorem confluent_of_diamond {α} {r : α → α → Prop}
-    (hd : Diamond r) : Confluent r := by
-  have strip : ∀ ⦃a b c⦄, r a b → ReflTransGen r a c →
-      ∃ d, ReflTransGen r b d ∧ r c d := by
-    intro a b c hab hac
-    induction hac with
-    | refl => exact ⟨b, ReflTransGen.refl, hab⟩
-    | tail had hce ih =>
-        rcases ih with ⟨d, hbd, hcd⟩
-        rcases hd hcd hce with ⟨f, hdf, hef⟩
-        exact ⟨f, ReflTransGen.tail hbd hdf, hef⟩
-  intro a b c hab hac
-  induction hab with
-  | refl => exact ⟨c, hac, ReflTransGen.refl⟩
-  | tail hab hbc ih =>
-      rcases ih with ⟨d, hbd, hcd⟩
-      rcases strip hbc hbd with ⟨f, hcf, hdf⟩
-      exact ⟨f, hcf, ReflTransGen.tail hcd hdf⟩
-
-/-- Sandwich: if `r ⊆ p ⊆ r*` then `r* = p*`. -/
-public theorem rtc_eq_of_sandwich {α} {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)
-
-end Lambda

From 45d3c754d896fb5196e7a4821674cee880ec1e89 Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 16:16:39 -0400
Subject: [PATCH 11/12] upd: clarification for consistency of decre

---
 .../LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean     | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
index 848b07087..07f5d8b17 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean
@@ -69,7 +69,11 @@ infixl:77 "·" => Term.app
   | abs t   => abs (subst (j + 1) (incre 1 0 s) t)
   | app t u => app (subst j s t) (subst j s u)
 
-/-- `decre c t` decrements free vars `> c` by `i`. -/
+/-- `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)

From 2c3aac6ca1538a49b2fb26ad8f8196ecdc11b77b Mon Sep 17 00:00:00 2001
From: zayn7lie <zayn7lie.ber7+git@gmail.com>
Date: Fri, 10 Apr 2026 16:44:56 -0400
Subject: [PATCH 12/12] upd: `reduction_sys` for generating notations for
 reductions and the multi-step closure

---
 .../Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean | 1 +
 .../LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean       | 1 +
 2 files changed, 2 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
index e0d57e533..e6be26f74 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean
@@ -39,6 +39,7 @@ 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)
diff --git a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
index 2953cb14c..ed03ae8d0 100644
--- a/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ParallelReduction.lean
@@ -41,6 +41,7 @@ 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')