WF-1: restore main's Order.agda and re-target WellFounded.agda

Repairs two issues from the PR-16 merge resolution:

  1. Smoke.agda stale: the merged Order.agda used PR-16's renamed
     constructors (<ᵇ-0Ω, <ᵇ-Ω+, <ᵇ-Ωψ, <ᵇ-ψν without the side
     condition, etc.) while Smoke.agda still pinned main's original
     seven names. Compile broke at Smoke.agda's import clause.

  2. WellFounded.agda orphan: the new module was never imported from
     All.agda, so its headline `wf-<ᵇ` and `<ᵇ-irreflexive` lived as
     dead code.

Plus a design concern: PR-16's rewritten order relaxed `<ᵇ-Ω+` /
`<ᵇ-Ωψ` to unconditional, dropped `<ᵇ-ΩΩ` entirely, and restricted
`<ᵇ-ψν` to same-α. The rank function in the PR's WellFounded.agda
was carefully shaped around those weakenings. The resulting
relation is well-founded but not a plausible Buchholz comparison:
`bOmega Omegaω <ᵇ bplus bzero bzero` becomes provable despite ω
being vastly bigger than 0 ordinally.

Resolution:

  * proofs/agda/Ordinal/Buchholz/Order.agda
      Restored from origin/main (7 constructors with the Ω-index
      side conditions; `<ᵇ-irrefl`, `<ᵇ-trans`, named strict
      witnesses).

  * proofs/agda/Ordinal/Buchholz/WellFounded.agda
      Rewritten against the restored order. Proof structure:
        1. `<Ω-wf`: well-foundedness of _<Ω_ via ℕ's <-wellFounded,
           lifted through the fin embedding, plus a separate ω step.
        2. `wf-<ᵇ`: structural induction on BT. bOmega and bpsi use
           well-founded recursion on their Ω-index (via <Ω-wf). bplus
           uses mutual recursion with wf-<ᵇ on the first summand.
        3. `<ᵇ-irreflexive`: derived from wf-<ᵇ via `wf⇒asym`. Sits
           alongside the direct-pattern `<ᵇ-irrefl` in Order.agda.

  * proofs/agda/All.agda
      Wires in Ordinal.Buchholz.WellFounded (was missing).

  * proofs/agda/Smoke.agda
      Pins `<Ω-wf`, `wf-<ᵇ`, `<ᵇ-irreflexive` from the new module.
      Order.agda pins stay as-is (Order.agda is restored verbatim).

Verified: `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda`
both exit 0 under --safe --without-K. No postulates introduced. The
rank-embedding machinery from PR-16 is dropped in favour of direct
structural accessibility, which fits the restored order's conditional
constructors naturally.

https://claude.ai/code/session_01JRLz84fAaWvRBKyXuc4tyK

Author: claude

proofs/agda/All.agda

@@ -35,6 +35,7 @@ open import Ordinal.OmegaMarkers
 open import Ordinal.Buchholz.Syntax
 open import Ordinal.Buchholz.Closure
 open import Ordinal.Buchholz.Order
+open import Ordinal.Buchholz.WellFounded
 open import Ordinal.Buchholz.Psi
 open import Ordinal.Buchholz.Examples
 open import Ordinal.Buchholz.WellFormed

proofs/agda/Ordinal/Buchholz/Order.agda

@@ -1,29 +1,146 @@
 {-# OPTIONS --safe --without-K #-}
 
--- WF-1 core order for Buchholz terms.
+-- Stage WF-0 of the Buchholz well-foundedness workstream
+-- (docs/buchholz-plan.adoc, follow-up to E5–E7).
 --
--- This keeps the seven constructors that do not use the blocked
--- shared-binder cases `<ᵇ-ψα` and `<ᵇ-+2`.
+-- Defines the binary strict order `_<ᵇ_` on Buchholz terms (BT) and
+-- establishes irreflexivity and transitivity across the cases that
+-- the term heads naturally determine. Totality is *not* proved here
+-- and neither is well-foundedness; those are WF-1 and WF-2.
+--
+-- Scope of this module. The 7 constructors below cover the head
+-- pairs marked ✓ in the matrix, with the lex-on-left-summand case
+-- for bplus and the lex-on-Ω-index case for bpsi:
+--
+--   head of x \ head of y │ bzero │ bOmega │ bplus │ bpsi
+--   ──────────────────────┼───────┼────────┼───────┼──────
+--   bzero                 │   –   │   ✓    │   ✓   │  ✓
+--   bOmega                │       │   ✓    │       │  ✓ (when μ <Ω ν)
+--   bplus                 │       │        │   ✓   │
+--   bpsi                  │       │        │       │  ✓ (when μ <Ω ν)
+--
+-- Open cases (no constructor yet; must be discharged in follow-ups
+-- before `<ᵇ`-totality and well-foundedness can land):
+--
+--   * bOmega vs bplus (either direction) — requires a comparison
+--     between atomic heads and additive normal forms.
+--   * bpsi vs bplus (either direction) — same reason, mediated by
+--     the leading bpsi summand of a bplus in CNF.
+--   * bpsi vs bOmega with ν ≤Ω μ — the admissibility condition makes
+--     bpsi ν α ≤ᵇ bOmega μ when μ exceeds ν; the exact form is part
+--     of the Buchholz 1986 comparison and is deferred.
+--   * Two same-binder sub-cases whose natural shapes run into Agda
+--     2.6.3's `--without-K` restriction on reflexive-equation
+--     elimination and are deferred pending a K-free reformulation:
+--       - bpsi ν α <ᵇ bpsi ν β with α <ᵇ β (same Ω-index ν).
+--       - bplus x y₂ <ᵇ bplus x z₂ with y₂ <ᵇ z₂ (same left summand).
+--     In both cases the constructor shares a binder between the two
+--     sides of `<ᵇ`, which `<ᵇ-irrefl`'s pattern unification cannot
+--     reduce. A rank-embedding or heterogeneous-equality formulation
+--     is the next follow-up on top of WF-0.
 
 module Ordinal.Buchholz.Order where
 
-open import Data.Nat.Base using (ℕ; _<_)
+open import Data.Empty using (⊥)
 
-open import Ordinal.OmegaMarkers using (OmegaIndex; fin)
+open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_; <Ω-irrefl; <Ω-trans)
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
 
-data _<Ω_ : OmegaIndex → OmegaIndex → Set where
-  <Ω-fin : ∀ {m n : ℕ} → m < n → fin m <Ω fin n
+data _<ᵇ_ : BT → BT → Set where
+  -- bzero is minimum against every non-bzero head.
+  <ᵇ-0-Ω : ∀ {μ}   → bzero <ᵇ bOmega μ
+  <ᵇ-0-+ : ∀ {x y} → bzero <ᵇ bplus x y
+  <ᵇ-0-ψ : ∀ {ν α} → bzero <ᵇ bpsi ν α
 
-infix 4 _<Ω_
+  -- bOmega ordering by Ω-index.
+  <ᵇ-ΩΩ  : ∀ {μ ν} → μ <Ω ν → bOmega μ <ᵇ bOmega ν
 
-data _<ᵇ_ : BT → BT → Set where
-  <ᵇ-0Ω : ∀ {μ} → bzero <ᵇ bOmega μ
-  <ᵇ-0+ : ∀ {α β} → bzero <ᵇ bplus α β
-  <ᵇ-0ψ : ∀ {μ α} → bzero <ᵇ bpsi μ α
-  <ᵇ-Ω+ : ∀ {κ α β} → bOmega κ <ᵇ bplus α β
-  <ᵇ-Ωψ : ∀ {κ μ α} → bOmega κ <ᵇ bpsi μ α
-  <ᵇ-+1 : ∀ {α β γ} → α <ᵇ β → bplus α γ <ᵇ bplus β γ
-  <ᵇ-ψν : ∀ {μ ν α} → μ <Ω ν → bpsi μ α <ᵇ bpsi ν α
+  -- Ω_μ < ψ_ν(α) whenever μ <Ω ν. This is the admissibility side:
+  -- ψ-terms at higher index dominate Ω-markers at lower index. The
+  -- reverse direction (bpsi ν α <ᵇ bOmega μ with ν ≤Ω μ) is deferred.
+  <ᵇ-Ωψ  : ∀ {μ ν α} → μ <Ω ν → bOmega μ <ᵇ bpsi ν α
+
+  -- bpsi comparison by Ω-index only. The same-index sub-case (lex on
+  -- the ψ-argument) is deferred pending a K-free formulation.
+  <ᵇ-ψΩ  : ∀ {μ ν α β} → μ <Ω ν → bpsi μ α <ᵇ bpsi ν β
+
+  -- bplus comparison by the left summand. The same-left sub-case
+  -- (compare right summands when lefts agree) is deferred for the
+  -- same `--without-K` reason as `<ᵇ-ψα` above: its natural shape
+  -- `bplus x y₂ <ᵇ bplus x z₂` shares the binder `x` on both sides.
+  <ᵇ-+1  : ∀ {x₁ x₂ y₁ y₂} → x₁ <ᵇ y₁ → bplus x₁ x₂ <ᵇ bplus y₁ y₂
 
 infix 4 _<ᵇ_
+
+----------------------------------------------------------------------------
+-- Irreflexivity
+----------------------------------------------------------------------------
+
+-- Every constructor of `_<ᵇ_` with equal LHS and RHS reduces to a
+-- witness of irreflexivity at a strictly smaller structure (either
+-- `_<Ω_` or `_<ᵇ_` on a subterm). Explicit binds on the `{x}` ensure
+-- the K-free unifier does not get stuck on reflexive equations at the
+-- shared Ω-index of `<ᵇ-ψα`.
+
+<ᵇ-irrefl : ∀ {x} → x <ᵇ x → ⊥
+<ᵇ-irrefl (<ᵇ-ΩΩ μ<μ)  = <Ω-irrefl μ<μ
+<ᵇ-irrefl (<ᵇ-ψΩ μ<μ)  = <Ω-irrefl μ<μ
+<ᵇ-irrefl (<ᵇ-+1 x<x)  = <ᵇ-irrefl x<x
+
+----------------------------------------------------------------------------
+-- Transitivity
+----------------------------------------------------------------------------
+
+-- Case analysis on the two ordering derivations, recursing on
+-- `_<Ω_` or `_<ᵇ_` subterms as needed. Covers every pair of
+-- constructors whose middle term has a compatible head; pairs with
+-- incompatible middle heads are absurd by construction (no
+-- constructor witnesses them).
+
+<ᵇ-trans : ∀ {x y z} → x <ᵇ y → y <ᵇ z → x <ᵇ z
+-- Left leg: <ᵇ-0-Ω (x = bzero, y = bOmega _)
+<ᵇ-trans <ᵇ-0-Ω       (<ᵇ-ΩΩ _)            = <ᵇ-0-Ω
+<ᵇ-trans <ᵇ-0-Ω       (<ᵇ-Ωψ _)            = <ᵇ-0-ψ
+-- Left leg: <ᵇ-0-+ (x = bzero, y = bplus _ _)
+<ᵇ-trans <ᵇ-0-+       (<ᵇ-+1 _)            = <ᵇ-0-+
+-- Left leg: <ᵇ-0-ψ (x = bzero, y = bpsi _ _)
+<ᵇ-trans <ᵇ-0-ψ       (<ᵇ-ψΩ _)            = <ᵇ-0-ψ
+-- Left leg: <ᵇ-ΩΩ (x = bOmega _, y = bOmega _)
+<ᵇ-trans (<ᵇ-ΩΩ p)    (<ᵇ-ΩΩ q)            = <ᵇ-ΩΩ (<Ω-trans p q)
+<ᵇ-trans (<ᵇ-ΩΩ p)    (<ᵇ-Ωψ q)            = <ᵇ-Ωψ (<Ω-trans p q)
+-- Left leg: <ᵇ-Ωψ (x = bOmega _, y = bpsi _ _)
+<ᵇ-trans (<ᵇ-Ωψ p)    (<ᵇ-ψΩ q)            = <ᵇ-Ωψ (<Ω-trans p q)
+-- Left leg: <ᵇ-ψΩ (x = bpsi _ _, y = bpsi _ _)
+<ᵇ-trans (<ᵇ-ψΩ p)    (<ᵇ-ψΩ q)            = <ᵇ-ψΩ (<Ω-trans p q)
+-- Left leg: <ᵇ-+1 (x = bplus _ _, y = bplus _ _)
+<ᵇ-trans (<ᵇ-+1 p)    (<ᵇ-+1 q)            = <ᵇ-+1 (<ᵇ-trans p q)
+
+----------------------------------------------------------------------------
+-- Strict-below-ψ examples, for downstream ordering checks
+----------------------------------------------------------------------------
+
+-- These use the pinned `Omega*` constants from OmegaMarkers to keep
+-- the Buchholz example terms in a strict chain: bzero <ᵇ Ω₀ <ᵇ Ω₁
+-- <ᵇ Ω_ω <ᵇ ψ_ω(bzero). The last strict inequality uses the cross-
+-- constructor <ᵇ-Ωψ since ω <Ω ω is absent (ω is top).
+
+open import Ordinal.OmegaMarkers using
+  ( Omega0
+  ; Omega1
+  ; Omegaω
+  ; Omega0<Omega1
+  ; Omega0<Omegaω
+  ; Omega1<Omegaω
+  )
+
+bzero<Ω0 : bzero <ᵇ bOmega Omega0
+bzero<Ω0 = <ᵇ-0-Ω
+
+Ω0<Ω1 : bOmega Omega0 <ᵇ bOmega Omega1
+Ω0<Ω1 = <ᵇ-ΩΩ Omega0<Omega1
+
+Ω1<Ωω : bOmega Omega1 <ᵇ bOmega Omegaω
+Ω1<Ωω = <ᵇ-ΩΩ Omega1<Omegaω
+
+Ω0<ψ1-zero : bOmega Omega0 <ᵇ bpsi Omega1 bzero
+Ω0<ψ1-zero = <ᵇ-Ωψ Omega0<Omega1

proofs/agda/Ordinal/Buchholz/WellFounded.agda

@@ -1,108 +1,142 @@
 {-# OPTIONS --safe --without-K #-}
 
--- WF-1 skeleton: prove accessibility by term constructor, with
--- predecessor inversion lemmas separated out. Recursive predecessor
--- bridges are discharged through a small rank-to-ℕ subrelation proof.
+-- WF-1: well-foundedness of the binary strict order `_<ᵇ_` on
+-- Buchholz terms (from Ordinal.Buchholz.Order).
+--
+-- Proof by structural induction on the BT term, using:
+--  * `<Ω-wf` for the bOmega and bpsi cases (their predecessors
+--    decrease only along the Ω-index);
+--  * recursion on the inductive BT structure for the bplus case
+--    (whose only internal predecessor `<ᵇ-+1` decreases along the
+--    first summand).
+--
+-- Irreflexivity follows from well-foundedness via `wf⇒asym`. This
+-- cross-checks `<ᵇ-irrefl` (pattern-matched directly in Order.agda)
+-- and derives a matching `<ᵇ-irreflexive` via the wf channel.
 
 module Ordinal.Buchholz.WellFounded where
 
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; _<_; z≤n; s≤s; zero; suc)
 open import Data.Nat.Induction as NatInd using (<-wellFounded)
-open import Function.Base using (_on_)
+open import Induction.WellFounded using
+  ( Acc
+  ; acc
+  ; WellFounded
+  ; wf⇒asym
+  )
 open import Relation.Nullary using (¬_)
-open import Induction.WellFounded as WF using (Acc; acc; WellFounded; wf⇒asym)
 
-open import Ordinal.OmegaMarkers using (OmegaIndex; fin; ω)
+open import Ordinal.OmegaMarkers using
+  ( OmegaIndex
+  ; fin
+  ; ω
+  ; _<Ω_
+  ; fin<fin
+  ; fin<ω
+  )
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
 open import Ordinal.Buchholz.Order using
-  ( _<Ω_
-  ; _<ᵇ_
-  ; <Ω-fin
-  ; <ᵇ-0Ω
-  ; <ᵇ-0+
-  ; <ᵇ-0ψ
-  ; <ᵇ-Ω+
+  ( _<ᵇ_
+  ; <ᵇ-0-Ω
+  ; <ᵇ-0-+
+  ; <ᵇ-0-ψ
+  ; <ᵇ-ΩΩ
   ; <ᵇ-Ωψ
+  ; <ᵇ-ψΩ
   ; <ᵇ-+1
-  ; <ᵇ-ψν
   )
 
-<ᵇ-inv-bzero : ∀ {x} → x <ᵇ bzero → ⊥
-<ᵇ-inv-bzero ()
-
-<ᵇ-pred-bzero : ∀ {x} → x <ᵇ bzero → Acc _<ᵇ_ x
-<ᵇ-pred-bzero x<0 = ⊥-elim (<ᵇ-inv-bzero x<0)
-
-rankΩ : OmegaIndex → ℕ
-rankΩ (fin n) = n
-rankΩ ω       = zero
-
-rankBT : BT → ℕ
-rankBT bzero       = zero
-rankBT (bOmega μ)  = suc zero
-rankBT (bplus α β) = suc (suc (rankBT α))
-rankBT (bpsi μ α)  = suc (suc (suc (rankΩ μ)))
+----------------------------------------------------------------------------
+-- Step 1: well-foundedness of `_<Ω_`
+----------------------------------------------------------------------------
 
-<Ω⇒<rankΩ : ∀ {μ ν} → μ <Ω ν → rankΩ μ < rankΩ ν
-<Ω⇒<rankΩ (<Ω-fin m<n) = m<n
+-- Every finite marker `fin n` is accessible by lifting accessibility
+-- of `n` in ℕ's `_<_`. The limit marker `ω` is accessible because its
+-- only strict predecessors are finite markers, each covered by the
+-- finite case.
 
-<ᵇ⇒<rankBT : ∀ {x y} → x <ᵇ y → rankBT x < rankBT y
-<ᵇ⇒<rankBT <ᵇ-0Ω = s≤s z≤n
-<ᵇ⇒<rankBT <ᵇ-0+ = s≤s z≤n
-<ᵇ⇒<rankBT <ᵇ-0ψ = s≤s z≤n
-<ᵇ⇒<rankBT <ᵇ-Ω+ = s≤s (s≤s z≤n)
-<ᵇ⇒<rankBT <ᵇ-Ωψ = s≤s (s≤s z≤n)
-<ᵇ⇒<rankBT (<ᵇ-+1 α<β) = s≤s (s≤s (<ᵇ⇒<rankBT α<β))
-<ᵇ⇒<rankBT (<ᵇ-ψν μ<ν) = s≤s (s≤s (s≤s (<Ω⇒<rankΩ μ<ν)))
-
-wf-rankBT : WellFounded (_<_ on rankBT)
-wf-rankBT x = rank-accessible (NatInd.<-wellFounded (rankBT x))
+<Ω-wf-fin : ∀ n → Acc _<Ω_ (fin n)
+<Ω-wf-fin n = aux (<-wellFounded n)
   where
-  rank-accessible : ∀ {t} → Acc _<_ (rankBT t) → Acc (_<_ on rankBT) t
-  rank-accessible (acc rs) = acc λ t<x → rank-accessible (rs t<x)
-
-wf-<ᵇ-rank : WellFounded _<ᵇ_
-wf-<ᵇ-rank = WF.Subrelation.wellFounded <ᵇ⇒<rankBT wf-rankBT
+    aux : ∀ {k} → Acc _<_ k → Acc _<Ω_ (fin k)
+    aux {k} (acc rs) = acc step
+      where
+        step : ∀ {y} → y <Ω fin k → Acc _<Ω_ y
+        step (fin<fin m<k) = aux (rs m<k)
+
+<Ω-wf-ω : Acc _<Ω_ ω
+<Ω-wf-ω = acc step
+  where
+    step : ∀ {y} → y <Ω ω → Acc _<Ω_ y
+    step (fin<ω {m = m}) = <Ω-wf-fin m
 
-<ᵇ-rec-+1 : ∀ {α β γ} → α <ᵇ β → Acc _<ᵇ_ (bplus α γ)
+<Ω-wf : WellFounded _<Ω_
+<Ω-wf (fin n) = <Ω-wf-fin n
+<Ω-wf ω       = <Ω-wf-ω
 
-<ᵇ-rec-ψν : ∀ {μ ν α} → μ <Ω ν → Acc _<ᵇ_ (bpsi μ α)
+----------------------------------------------------------------------------
+-- Step 2: well-foundedness of `_<ᵇ_` by structural induction on BT
+----------------------------------------------------------------------------
 
+-- bzero is accessible: it has no predecessors (no `_<ᵇ_` constructor
+-- has bzero on the right-hand side).
 <ᵇ-acc-bzero : Acc _<ᵇ_ bzero
-<ᵇ-acc-bzero = acc <ᵇ-pred-bzero
-
-<ᵇ-pred-bOmega : ∀ {μ x} → x <ᵇ bOmega μ → Acc _<ᵇ_ x
-<ᵇ-pred-bOmega <ᵇ-0Ω = <ᵇ-acc-bzero
-
-<ᵇ-acc-bOmega : (μ : OmegaIndex) → Acc _<ᵇ_ (bOmega μ)
-<ᵇ-acc-bOmega μ = acc <ᵇ-pred-bOmega
-
-<ᵇ-pred-bplus : ∀ {α β x} → x <ᵇ bplus α β → Acc _<ᵇ_ x
-<ᵇ-pred-bplus <ᵇ-0+ = <ᵇ-acc-bzero
-<ᵇ-pred-bplus (<ᵇ-Ω+ {κ = κ}) = <ᵇ-acc-bOmega κ
-<ᵇ-pred-bplus (<ᵇ-+1 α<β) = <ᵇ-rec-+1 α<β
-
-<ᵇ-pred-bpsi : ∀ {μ α x} → x <ᵇ bpsi μ α → Acc _<ᵇ_ x
-<ᵇ-pred-bpsi <ᵇ-0ψ = <ᵇ-acc-bzero
-<ᵇ-pred-bpsi (<ᵇ-Ωψ {κ = κ}) = <ᵇ-acc-bOmega κ
-<ᵇ-pred-bpsi (<ᵇ-ψν μ<ν) = <ᵇ-rec-ψν μ<ν
-
-<ᵇ-acc-bplus : (α β : BT) → Acc _<ᵇ_ (bplus α β)
-<ᵇ-acc-bplus α β = acc <ᵇ-pred-bplus
-
-<ᵇ-acc-bpsi : (μ : OmegaIndex) (α : BT) → Acc _<ᵇ_ (bpsi μ α)
-<ᵇ-acc-bpsi μ α = acc <ᵇ-pred-bpsi
+<ᵇ-acc-bzero = acc step
+  where
+    step : ∀ {y} → y <ᵇ bzero → Acc _<ᵇ_ y
+    step ()
 
-<ᵇ-rec-+1 {α = α} {γ = γ} _ = wf-<ᵇ-rank (bplus α γ)
+-- bOmega μ is accessible by well-founded recursion on μ in `_<Ω_`.
+<ᵇ-acc-bOmega : ∀ μ → Acc _<ᵇ_ (bOmega μ)
+<ᵇ-acc-bOmega μ = go (<Ω-wf μ)
+  where
+    go : ∀ {ν} → Acc _<Ω_ ν → Acc _<ᵇ_ (bOmega ν)
+    go (acc rs) = acc step
+      where
+        step : ∀ {y} → y <ᵇ bOmega _ → Acc _<ᵇ_ y
+        step <ᵇ-0-Ω        = <ᵇ-acc-bzero
+        step (<ᵇ-ΩΩ μ'<ν)  = go (rs μ'<ν)
+
+-- bpsi ν α is accessible by well-founded recursion on ν in `_<Ω_`.
+-- Predecessors: bzero, bOmega μ' with μ' <Ω ν, and bpsi μ' β with
+-- μ' <Ω ν for any β.
+<ᵇ-acc-bpsi : ∀ ν α → Acc _<ᵇ_ (bpsi ν α)
+<ᵇ-acc-bpsi ν α = go (<Ω-wf ν) α
+  where
+    go : ∀ {ν'} → Acc _<Ω_ ν' → ∀ α → Acc _<ᵇ_ (bpsi ν' α)
+    go (acc rs) α = acc step
+      where
+        step : ∀ {y} → y <ᵇ bpsi _ α → Acc _<ᵇ_ y
+        step <ᵇ-0-ψ              = <ᵇ-acc-bzero
+        step (<ᵇ-Ωψ {μ = μ'} _)  = <ᵇ-acc-bOmega μ'
+        step (<ᵇ-ψΩ μ'<ν)        = go (rs μ'<ν) _
 
-<ᵇ-rec-ψν {μ = μ} {α = α} _ = wf-<ᵇ-rank (bpsi μ α)
+-- bplus α β is accessible by outer well-founded recursion on α.
+<ᵇ-acc-bplus : ∀ α β → Acc _<ᵇ_ (bplus α β)
 
 wf-<ᵇ : WellFounded _<ᵇ_
 wf-<ᵇ bzero       = <ᵇ-acc-bzero
 wf-<ᵇ (bOmega μ)  = <ᵇ-acc-bOmega μ
 wf-<ᵇ (bplus α β) = <ᵇ-acc-bplus α β
-wf-<ᵇ (bpsi μ α)  = <ᵇ-acc-bpsi μ α
+wf-<ᵇ (bpsi ν α)  = <ᵇ-acc-bpsi ν α
 
+<ᵇ-acc-bplus α β = go (wf-<ᵇ α) β
+  where
+    go : ∀ {α'} → Acc _<ᵇ_ α' → ∀ β' → Acc _<ᵇ_ (bplus α' β')
+    go (acc rs) β' = acc step
+      where
+        step : ∀ {y} → y <ᵇ bplus _ β' → Acc _<ᵇ_ y
+        step <ᵇ-0-+            = <ᵇ-acc-bzero
+        step (<ᵇ-+1 α₁<α')     = go (rs α₁<α') _
+
+----------------------------------------------------------------------------
+-- Step 3: irreflexivity as a corollary of well-foundedness
+----------------------------------------------------------------------------
+
+-- Derived via `wf⇒asym`: a well-founded relation is asymmetric, hence
+-- cannot hold between an element and itself. This duplicates the
+-- direct pattern-matched `<ᵇ-irrefl` in Order.agda; keeping both
+-- makes `wf-<ᵇ` load-bearing and exercises the standard WF API.
 <ᵇ-irreflexive : ∀ {x} → ¬ (x <ᵇ x)
 <ᵇ-irreflexive {x} x<x = wf⇒asym wf-<ᵇ x<x x<x