diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -238,16 +238,16 @@
 $ phino explain --morph
 \begin{tabular}{rl}
 \phinoMorphingRule{prim}
-  { \mathbb{M}( [[ B ]] ) }
+  { \mathbb{M}( [[ B ]], e ) }
   { [[ B ]] }
   { }
   { }
 ...
 \phinoMorphingRule{root}
-  { \mathbb{M}( Q ) }
-  { \mathbb{M}( \phinoNormalize{ e } ) }
+  { \mathbb{M}( Q, e ) }
+  { \mathbb{M}( \phinoNormalize{ e }, e ) }
   { $ e \not= Q $ }
-  { $ e \coloneqq \phinoGlobal{  } $ }
+  { }
 \end{tabular}
 ```
 
@@ -262,7 +262,7 @@
 ...
 \phinoDataizationRule{norm}
   { \phinoDataize{ n } }
-  { \phinoDataize{ \mathbb{M}( n ) } }
+  { \phinoDataize{ \mathbb{M}( n, e ) } }
   { }
   { }
 \end{tabular}
@@ -310,6 +310,10 @@
   | part-of:             # returns True if given expression is attached to any
       - Expression'      # attribute in ginve bindings
       - BiMeta'
+  | formation:           # returns True if given expression is a formation
+      Expression'        # (an abstraction ⟦…⟧); used by morphing 'dispatch'
+                         # as 'not (formation 𝑛)', so a non-formation head is
+                         # morphed and a formation head is left to 'lambda'
 
 Comparable:              # comparable object that may be used in 'eq' condition
   = Attribute'
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.85
+version: 0.0.86
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/resources/dataization.yaml b/resources/dataization.yaml
--- a/resources/dataization.yaml
+++ b/resources/dataization.yaml
@@ -1,57 +1,78 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. The input
-# is always a normal form: a non-NF expression matches no clause.
+# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. It is
+# binary, 𝔻(n, e): the second argument e is the global universe, the same
+# expression that 𝕄 takes as its second argument; 𝔻 forwards it to 𝕄. The first
+# argument is always a normal form: a non-NF expression matches no clause.
+#
+# Each rule is an inference rule: when 'match' matches the term and 'e-match'
+# matches the universe (binding the meta e), the rule yields the conclusion
+# 'd-result' (a premise bytes meta or a literal), provided 'when' holds and the
+# ordered 'premises' reduce as stated. A premise binds its 'n-result'/'d-result'
+# to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('lambda')
+# or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of
+# 𝔻(n, e); it is always the e meta. The single bytes result is named δ; derived
+# terms are 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match'
+# already binds it.
 
 - name: delta
   label: \Delta
-  description: '𝔻(⟦𝐵1, Δ ⤍ δ, 𝐵2⟧) ⟿ δ'
   match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧
-  then: δ
+  e-match: 𝑒
+  d-result: δ
 
 - name: box
-  description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒩(𝒞(e))) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅'
-  match: ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧
-  where:
-    - meta: 𝑒1
-      function: contextualize
-      args:
-        - 𝑒
-        - ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧
+  label: box
+  match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧
+  e-match: 𝑒
+  d-result: δ
   when:
     disjoint:
       - [Δ, λ]
       - [𝐵1, 𝐵2]
-  then:
-    dataize:
-      normalize: 𝑒1
+  premises:
+    - n-result: 𝑛
+      contextualize:
+        - 𝑒1
+        - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧
+    - n-result: 𝑛1
+      normalize: 𝑛
+    - d-result: δ
+      dataize: 𝑛1
 
 - name: fire
-  description: '𝔻(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧) ⟿ 𝔻(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧)))'
+  label: fire
   match: ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧
-  where:
-    - meta: 𝑒
-      function: lambda
-      args:
-        - ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧
-  then:
-    dataize:
-      normalize: 𝑒
+  e-match: 𝑒
+  d-result: δ
+  premises:
+    - n-result: 𝑛
+      lambda: ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧
+    - n-result: 𝑛1
+      normalize: 𝑛
+    - d-result: δ
+      dataize: 𝑛1
 
 - name: none
-  description: '𝔻(⟦𝐵⟧) ⟿ nothing'
+  label: none
   match: ⟦𝐵⟧
-  then: nothing
+  e-match: 𝑒
+  d-result: '--'
 
 - name: bott
-  description: '𝔻(⊥) ⟿ nothing'
+  label: bott
   match: ⊥
-  then: nothing
+  e-match: 𝑒
+  d-result: '--'
 
 - name: norm
-  description: '𝔻(n) ⟿ 𝔻(𝕄(n)) otherwise'
+  label: norm
   match: 𝑛
-  then:
-    dataize:
+  e-match: 𝑒
+  d-result: δ
+  premises:
+    - n-result: 𝑛1
       morph: 𝑛
+    - d-result: δ
+      dataize: 𝑛1
diff --git a/resources/morphing.yaml b/resources/morphing.yaml
--- a/resources/morphing.yaml
+++ b/resources/morphing.yaml
@@ -1,93 +1,121 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. The input is
+# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. It is binary,
+# 𝕄(n, e): n is the term being morphed and e is the fixed global universe,
+# threaded unchanged through every recursive call and substituted for Φ by the
+# 'root' rule (Φ, rendered Q, is just the locator of e). The first argument is
 # always a normal form: a non-NF expression matches no clause. 𝕄 navigates a
-# normal form down to a formation one operation at a time,
-# resolving the universe Φ and peeling dispatches and applications through
-# normalization 𝒩. It never fires a bare atom: a saturated λ-formation is
-# returned untouched and fired later by 𝔼 (the 'fire' rule of 𝔻).
+# normal form to a formation one operation at a time, resolving Φ against e and
+# peeling dispatches and applications through normalization 𝒩. It never fires a
+# bare atom: a saturated λ-formation is returned untouched and fired later by 𝔼
+# (the 'fire' rule of 𝔻).
+#
+# Each rule is an inference rule: when 'match' matches the term and 'e-match'
+# matches the universe (binding the meta e), the rule yields the conclusion
+# 'n-result' (a premise meta or a literal), provided 'when' holds and the
+# ordered 'premises' reduce as stated. A premise binds 'n-result' to the result
+# of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('lambda'). 'e-match' is
+# the universe-argument matcher of 𝕄(n, e); it is always the e meta. Derived
+# terms are named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is skipped only when
+# 'match' already binds it.
+#
+# 'lambda' and 'dispatch' are kept mutually exclusive: 'dispatch' fires only
+# when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation
+# head — λ-bearing or not — is left to 'lambda' (and 'prim'). The two clauses
+# are disjoint and their relative order does not change behavior.
 
 - name: prim
-  description: '𝕄(⟦𝐵⟧) ⟿ ⟦𝐵⟧'
+  label: prim
   match: ⟦𝐵⟧
-  then: ⟦𝐵⟧
+  e-match: 𝑒
+  n-result: ⟦𝐵⟧
 
 - name: lambda
   label: \lambda
-  description: '𝕄(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.τ) ⟿ 𝕄(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧).τ))'
   match: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.𝜏'
-  where:
-    - meta: 𝑒
-      function: lambda
-      args:
-        - '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧'
-  then:
-    morph:
-      normalize: '𝑒.𝜏'
+  e-match: 𝑒
+  n-result: 𝑛2
+  premises:
+    - n-result: 𝑛
+      lambda: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧'
+    - n-result: 𝑛1
+      normalize: '𝑛.𝜏'
+    - n-result: 𝑛2
+      morph: 𝑛1
 
 - name: dispatch
-  description: '𝕄(n.τ) ⟿ 𝕄(𝒩(𝕄(n).τ))'
+  label: disp
   match: '𝑛.𝜏'
-  where:
-    - meta: 𝑒
-      function: morph
-      args:
-        - 𝑛
-  then:
-    morph:
-      normalize: '𝑒.𝜏'
+  e-match: 𝑒
+  n-result: 𝑛3
+  when:
+    not:
+      formation: 𝑛
+  premises:
+    - n-result: 𝑛1
+      morph: 𝑛
+    - n-result: 𝑛2
+      normalize: '𝑛1.𝜏'
+    - n-result: 𝑛3
+      morph: 𝑛2
 
 - name: application
-  description: '𝕄(n(τ ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(τ ↦ e)))'
-  match: '𝑛(𝜏 ↦ 𝑒)'
-  where:
-    - meta: 𝑒1
-      function: morph
-      args:
-        - 𝑛
-  then:
-    morph:
-      normalize: '𝑒1(𝜏 ↦ 𝑒)'
+  label: app
+  match: '𝑛(𝜏 ↦ 𝑒1)'
+  e-match: 𝑒
+  n-result: 𝑛3
+  premises:
+    - n-result: 𝑛1
+      morph: 𝑛
+    - n-result: 𝑛2
+      normalize: '𝑛1(𝜏 ↦ 𝑒1)'
+    - n-result: 𝑛3
+      morph: 𝑛2
 
 - name: applicationa
-  description: '𝕄(n(α_i ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(α_i ↦ e)))'
-  match: '𝑛(α𝑖 ↦ 𝑒)'
-  where:
-    - meta: 𝑒1
-      function: morph
-      args:
-        - 𝑛
-  then:
-    morph:
-      normalize: '𝑒1(α𝑖 ↦ 𝑒)'
+  label: appa
+  match: '𝑛(α𝑖 ↦ 𝑒1)'
+  e-match: 𝑒
+  n-result: 𝑛3
+  premises:
+    - n-result: 𝑛1
+      morph: 𝑛
+    - n-result: 𝑛2
+      normalize: '𝑛1(α𝑖 ↦ 𝑒1)'
+    - n-result: 𝑛3
+      morph: 𝑛2
 
 - name: root
-  description: '𝕄(Φ) ⟿ 𝕄(𝒩(e)) where e := global(), unless e is Φ'
+  label: root
   match: Φ
-  where:
-    - meta: 𝑒
-      function: global
+  e-match: 𝑒
+  n-result: 𝑛1
   when:
     not:
       eq:
         - 𝑒
         - Φ
-  then:
-    morph:
+  premises:
+    - n-result: 𝑛
       normalize: 𝑒
+    - n-result: 𝑛1
+      morph: 𝑛
 
 - name: dead
-  description: '𝕄(⊥) ⟿ ⊥'
+  label: dead
   match: ⊥
-  then: ⊥
+  e-match: 𝑒
+  n-result: ⊥
 
 - name: xi
-  description: '𝕄(ξ) ⟿ ⊥'
+  label: xi
   match: ξ
-  then: ⊥
+  e-match: 𝑒
+  n-result: ⊥
 
 - name: globe
-  description: '𝕄(Φ) ⟿ ⊥ when the universe is Φ itself'
+  label: globe
   match: Φ
-  then: ⊥
+  e-match: 𝑒
+  n-result: ⊥
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
--- a/src/CLI/Runners.hs
+++ b/src/CLI/Runners.hs
@@ -147,9 +147,9 @@
       canonize = if _canonize then C.canonize else id
       exclude = (`F.exclude` excluded)
       include = (`F.include` included)
-  (maybeBytes, chain) <- dataize (context loc prog printCtx)
+  (bytes, chain) <- dataize prog (context loc printCtx)
   when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain, False) >>= putStrLn)
-  unless _quiet (putStrLn (maybe (P.printExpression ExTermination) P.printBytes maybeBytes))
+  unless _quiet (putStrLn (P.printBytes bytes))
   where
     validateOpts :: IO ()
     validateOpts = do
@@ -160,8 +160,8 @@
         [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]
       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
-    context :: Expression -> Program -> PrintProgramContext -> DataizeContext
-    context loc prog ctx = DataizeContext loc prog _maxDepth _maxCycles _depthSensitive buildTerm (saveStepFunc _stepsDir ctx)
+    context :: Expression -> PrintProgramContext -> DataizeContext
+    context loc ctx = DataizeContext loc _maxDepth _maxCycles _depthSensitive buildTerm (saveStepFunc _stepsDir ctx)
     printProgCtx :: Expression -> PrintProgramContext
     printProgCtx focus =
       PrintProgCtx
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -234,6 +234,7 @@
   | CO_MATCHES {regex :: String, expr :: EXPRESSION}
   | CO_PART_OF {expr :: EXPRESSION, binding :: BINDING}
   | CO_DISJOINT {attrs :: [ATTRIBUTE], groups :: [BINDING]}
+  | CO_FORMATION {expr :: EXPRESSION}
   deriving (Eq, Show)
 
 data EXTRA_ARG
@@ -540,6 +541,7 @@
   toCST (Y.Gt left right) _ = CO_COMPARE (comparableToCST left) GREATER (comparableToCST right)
   toCST (Y.Matches regex expr) _ = CO_MATCHES regex (expressionToCST expr)
   toCST (Y.PartOf expr binding) _ = CO_PART_OF (expressionToCST expr) (bindingsToCST [binding])
+  toCST (Y.IsFormation expr) _ = CO_FORMATION (expressionToCST expr)
 
 instance ToCST Y.Comparable COMPARABLE where
   toCST (Y.CmpAttr attr) _ = CMP_ATTR (attributeToCST attr)
diff --git a/src/Condition.hs b/src/Condition.hs
--- a/src/Condition.hs
+++ b/src/Condition.hs
@@ -142,6 +142,11 @@
         bd <- _binding phiParser
         _ <- rparen
         return (Y.PartOf expr bd)
+    , do
+        _ <- symbol "formation" >> lparen
+        expr <- _expression phiParser
+        _ <- rparen
+        return (Y.IsFormation expr)
     ]
 
 parseCondition :: String -> Either String Y.Condition
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -14,13 +14,14 @@
 import AST
 import Builder (buildBytesThrows, buildExpressionThrows)
 import Control.Exception (throwIO)
-import Data.List (partition)
+import Control.Monad (foldM)
+import Data.List (find, partition)
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Text as T
-import Deps (BuildTermFunc, BuildTermMethod, SaveStepFunc, Term (TeAttribute, TeExpression))
+import Deps (BuildTermFunc, BuildTermMethod, SaveStepFunc, Term (..))
 import Locator (locatedExpression, withLocatedExpression)
-import Matcher (Subst (..), substEmpty)
+import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle)
 import Misc
 import Must (Must (..))
 import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)
@@ -29,15 +30,19 @@
 import Yaml (ExtraArgument (..), normalizationRules)
 import qualified Yaml as Y
 
-type Dataized = (Maybe Bytes, [Rewritten])
+type Dataized = (Bytes, [Rewritten])
 
 type Dataizable = (Expression, NonEmpty Rewritten)
 
 type Morphed = Dataizable
 
+-- The evaluation context carries only configuration. Nothing global is fixed
+-- here: the universe (the second argument 'e' of 𝕄(n, e) and 𝔻(n, e)) is a plain
+-- expression threaded as an argument to 'dataize'', 'morph' and on to the atoms.
+-- The working program needed for normalization is taken from the head of the
+-- step chain, so no 'Program' is threaded around.
 data DataizeContext = DataizeContext
   { _locator :: Expression
-  , _program :: Program
   , _maxDepth :: Int
   , _maxCycles :: Int
   , _depthSensitive :: Bool
@@ -46,13 +51,13 @@
   }
 
 -- Resolve formation for LAMBDA Morphing rule.
--- If formation contains λ binding, the called atom
--- result is returned.
-formation :: [Binding] -> DataizeContext -> IO (Maybe Expression)
-formation bds ctx = do
+-- If formation contains λ binding, the called atom result is returned. The
+-- universe 'univ' is forwarded to the atom.
+formation :: [Binding] -> Expression -> DataizeContext -> IO (Maybe Expression)
+formation bds univ ctx = do
   let (lambda, bds') = maybeLambda bds
   case lambda of
-    Just (BiLambda (Function func)) -> Just <$> atom func (ExFormation bds') ctx
+    Just (BiLambda (Function func)) -> Just <$> atom func (ExFormation bds') univ ctx
     _ -> pure Nothing
   where
     maybeLambda :: [Binding] -> (Maybe Binding, [Binding])
@@ -65,119 +70,202 @@
             [bd] -> (Just bd, rest)
             _ -> (Nothing, bds)
 
--- The Morphing function 𝕄 maps normal forms to formations. It is driven by the
--- ordered rules from 'morphing.yaml': the first matching rule's 'then' outcome
--- either stops at a formation ('MoStop') or keeps morphing ('MoMorph'). When
--- the morphed argument is a normalization ('MaNormalize', as in the 'lambda' and
--- 'root' rules), the rewriter runs over the rule's product and its individual
--- steps are spliced into the chain before morphing continues.
-morph :: Morphed -> DataizeContext -> IO Morphed
-morph (expr, seq) ctx@DataizeContext{..} = do
+-- The Morphing function 𝕄 maps normal forms to formations. It is binary,
+-- 𝕄(n, e): besides the term 'n' it takes the universe 'e' ('univ') — a plain
+-- expression — and matches it against the rule's 'e-match' pattern (always the
+-- '𝑒' meta), which binds 'e' so the 'root' rule substitutes it. It is driven by
+-- the ordered rules from 'morphing.yaml': the first matching rule's premises are
+-- evaluated and its conclusion 'nresult' is built, always forwarding the same
+-- universe. The 'morph' premise that produces the conclusion is the spine: when
+-- its argument comes from a 'normalize' premise, the rewriter runs over that
+-- argument and its individual steps (alpha, copy, dot, …) are spliced into the
+-- chain before morphing continues. Every other premise is a side-computation
+-- evaluated in isolation by 'sidePremise', its own steps discarded.
+morph :: Morphed -> Expression -> DataizeContext -> IO Morphed
+morph (expr, seq) univ ctx = do
   matched <- firstMatch Y.morphingRules
   case matched of
-    Just (rule, subst) -> apply rule.then_ rule.name subst
+    Just (rule, subst) -> reduce rule subst
     Nothing -> throwIO (userError "no morphing rule matched")
   where
     firstMatch :: [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))
     firstMatch [] = pure Nothing
     firstMatch (rule : rest) = do
-      substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx))
+      substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))
       case substs of
         (subst : _) -> pure (Just (rule, subst))
         [] -> firstMatch rest
-    -- The M/D rules evaluate as 'match → where → when', so the rule's guard
-    -- maps onto the 'having' slot (which runs after 'where'), not 'when' (which
-    -- 'matchExpressionWithRule'' runs before 'where').
+    -- Match the conclusion term and check the guard; premises are no longer the
+    -- matcher's business, so 'where'/'having' stay empty and the guard lives in
+    -- 'when'. Every morphing guard reads only meta-variables bound by 'match'
+    -- and 'e-match', so it holds before any premise runs.
     asRule :: Y.MorphRule -> Y.Rule
-    asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when
-    apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed
-    apply (Y.MoStop result) name subst = do
-      built <- buildExpressionThrows result subst
-      seq' <- leadsTo seq name built ctx
-      pure (built, seq')
-    apply (Y.MoMorph (Y.MaExpr result)) name subst = do
-      built <- buildExpressionThrows result subst
-      seq' <- leadsTo seq name built ctx
-      morph (built, seq') ctx
-    -- 𝕄(𝒩(e)) records the producing step, then delegates to the normalization
-    -- rewriter and splices its individual steps (alpha, copy, dot, …) into the
-    -- chain before morphing on the resulting normal form. Termination is the
-    -- rules' job: the 'root' rule's 'when' refuses to expand a universe that is
-    -- Φ itself, so the 'globe' rule catches it and yields ⊥ instead of looping.
-    apply (Y.MoMorph (Y.MaNormalize arg)) name subst = do
-      built <- buildExpressionThrows arg subst
-      labelled <- leadsTo seq name built ctx
-      (expr', seq') <- normalized built labelled ctx
-      morph (expr', seq') ctx
+    asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing
+    -- Evaluate the rule's premises and build its conclusion. A literal
+    -- conclusion is terminal. Otherwise the conclusion meta is produced by a
+    -- trailing 'morph' premise (the spine); if that premise's argument is itself
+    -- bound by a 'normalize' premise, the normalization joins the spine and its
+    -- steps splice in before morphing continues.
+    reduce :: Y.MorphRule -> Subst -> IO Morphed
+    reduce rule subst = case producer rule.nresult rule.premises of
+      Nothing -> do
+        final <- sides rule.premises subst
+        built <- buildExpressionThrows rule.nresult final
+        seq' <- leadsTo seq rule.name built ctx
+        pure (built, seq')
+      Just concl@(Y.Premise _ (Y.OpMorph arg)) -> case producer arg rule.premises of
+        Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do
+          final <- sides (rule.premises `excluding` [concl, normal]) subst
+          built <- buildExpressionThrows inner final
+          labelled <- leadsTo seq rule.name built ctx
+          (normal', seq') <- normalized built labelled ctx
+          morph (normal', seq') univ ctx
+        _ -> do
+          final <- sides (rule.premises `excluding` [concl]) subst
+          built <- buildExpressionThrows arg final
+          seq' <- leadsTo seq rule.name built ctx
+          morph (built, seq') univ ctx
+      Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name))
+    sides :: [Y.Premise] -> Subst -> IO Subst
+    sides premises subst = foldM (sidePremise univ ctx) subst premises
 
-dataize :: DataizeContext -> IO Dataized
-dataize ctx@DataizeContext{..} = do
-  expr <- locatedExpression _locator _program
-  (maybeBytes, seq) <- dataize' (expr, (_program, Nothing) :| []) ctx
-  pure (maybeBytes, reverse seq)
+-- Dataize the program located at '_locator'. The program's root is the universe
+-- (the 'e' argument) passed to 𝔻 and 𝕄.
+dataize :: Program -> DataizeContext -> IO Dataized
+dataize program@(Program univ) ctx@DataizeContext{..} = do
+  expr <- locatedExpression _locator program
+  (bytes, seq) <- dataize' (expr, (program, Nothing) :| []) univ ctx
+  pure (bytes, reverse seq)
 
--- The Dataization function 𝔻 retrieves bytes from an expression. It is driven
--- by the ordered rules from 'dataization.yaml': 'delta' yields the asset bytes,
--- 'none' (a formation) and 'bott' (⊥) yield nothing, 'box' contextualizes the
--- φ-body and keeps dataizing (its step is labelled by the operation,
--- 'contextualize'), and 'norm' reduces through morphing, splicing the morphing
--- steps into the chain.
-dataize' :: Dataizable -> DataizeContext -> IO Dataized
-dataize' (expr, seq) ctx = do
+-- The Dataization function 𝔻 retrieves bytes from an expression. It is total and
+-- binary, 𝔻(n, e): besides the term 'n' it takes the universe 'e' ('univ'),
+-- which it forwards to 𝕄. It is driven by the ordered rules from
+-- 'dataization.yaml': 'delta' yields the asset bytes, 'none' (a formation) and
+-- 'bott' (⊥) yield empty bytes (--), 'box' contextualizes the φ-body and keeps
+-- dataizing (its step is labelled by its 'contextualize' side-computation), and
+-- 'norm' reduces through morphing, splicing the morphing steps into the chain.
+-- The conclusion bytes 'dresult' are produced by a trailing 'dataize' premise;
+-- when its argument is bound by a 'morph' or 'normalize' premise, that step
+-- joins the spine, otherwise the premise is an isolated side-computation.
+dataize' :: Dataizable -> Expression -> DataizeContext -> IO Dataized
+dataize' (expr, seq) univ ctx = do
   matched <- firstMatch Y.dataizationRules
   case matched of
-    Just (rule, subst) -> apply rule subst
+    Just (rule, subst) -> reduce rule subst
     Nothing -> throwIO (userError "no dataization rule matched")
   where
     firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))
     firstMatch [] = pure Nothing
     firstMatch (rule : rest) = do
-      substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx))
+      substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))
       case substs of
         (subst : _) -> pure (Just (rule, subst))
         [] -> firstMatch rest
     asRule :: Y.DataizeRule -> Y.Rule
-    asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when
-    apply :: Y.DataizeRule -> Subst -> IO Dataized
-    apply rule subst = case rule.then_ of
-      Y.DoData bytes -> do
-        bts <- buildBytesThrows bytes subst
-        pure (Just bts, NE.toList seq)
-      Y.DoNothing -> pure (Nothing, NE.toList seq)
-      Y.DoDataize (Y.DaExpr result) -> do
-        built <- buildExpressionThrows result subst
-        seq' <- leadsTo seq (operation rule) built ctx
-        dataize' (built, seq') ctx
-      -- 𝔻(𝕄(e)) delegates to the morphing relation, splicing its steps into
-      -- the chain before dataizing on.
-      Y.DoDataize (Y.DaMorph arg) -> do
-        built <- buildExpressionThrows arg subst
-        (morphed, seq') <- morph (built, seq) ctx
-        dataize' (morphed, seq') ctx
-      -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization), then
-      -- normalizes its result back to a normal form before dataizing on, so 𝔻
-      -- only ever sees normal forms.
-      Y.DoDataize (Y.DaNormalize arg) -> do
-        built <- buildExpressionThrows arg subst
-        labelled <- leadsTo seq (operation rule) built ctx
-        (normal, seq') <- normalized built labelled ctx
-        dataize' (normal, seq') ctx
-    operation :: Y.DataizeRule -> String
-    operation rule = case rule.where_ of
-      Just (extra : _) -> Y.function extra
-      _ -> ""
+    asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing
+    reduce :: Y.DataizeRule -> Subst -> IO Dataized
+    reduce rule subst = case bytesProducer rule.dresult rule.premises of
+      Nothing -> do
+        final <- sides rule.premises subst
+        bts <- buildBytesThrows rule.dresult final
+        pure (bts, NE.toList seq)
+      Just concl@(Y.Premise _ (Y.OpDataize arg)) -> case producer arg rule.premises of
+        -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization or the
+        -- 'fire' λ-application), then normalizes its result back to a normal form
+        -- before dataizing on, so 𝔻 only ever sees normal forms.
+        Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do
+          let side = rule.premises `excluding` [concl, normal]
+          final <- sides side subst
+          built <- buildExpressionThrows inner final
+          labelled <- leadsTo seq (labelOf side) built ctx
+          (normal', seq') <- normalized built labelled ctx
+          dataize' (normal', seq') univ ctx
+        -- 𝔻(𝕄(e)) delegates to the morphing relation, splicing its steps into the
+        -- chain before dataizing on.
+        Just morphed@(Y.Premise _ (Y.OpMorph inner)) -> do
+          final <- sides (rule.premises `excluding` [concl, morphed]) subst
+          built <- buildExpressionThrows inner final
+          (morphed', seq') <- morph (built, seq) univ ctx
+          dataize' (morphed', seq') univ ctx
+        _ -> do
+          let side = rule.premises `excluding` [concl]
+          final <- sides side subst
+          built <- buildExpressionThrows arg final
+          seq' <- leadsTo seq (labelOf side) built ctx
+          dataize' (built, seq') univ ctx
+      Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name))
+    sides :: [Y.Premise] -> Subst -> IO Subst
+    sides premises subst = foldM (sidePremise univ ctx) subst premises
+    -- A spliced dataization step is labelled by its first side-computation —
+    -- 'box' by its 'contextualize', 'fire' by its 'lambda'; with none it is blank.
+    labelOf :: [Y.Premise] -> String
+    labelOf (premise : _) = verb premise.operation
+    labelOf [] = ""
 
+-- The premise binding the given expression meta, if any. The conclusion of a
+-- morphing rule and the argument of a continuation premise are looked up here to
+-- find the premise that produces them.
+producer :: Expression -> [Y.Premise] -> Maybe Y.Premise
+producer (ExMeta name) = find (\premise -> premise.result == name)
+producer _ = const Nothing
+
+-- The premise binding the given bytes meta, if any — the dataization analogue of
+-- 'producer' for a rule's bytes conclusion.
+bytesProducer :: Bytes -> [Y.Premise] -> Maybe Y.Premise
+bytesProducer (BtMeta name) = find (\premise -> premise.result == name)
+bytesProducer _ = const Nothing
+
+-- The premises whose result meta is not bound by any of the given ones — the
+-- side-computations left once the spine premises are removed.
+excluding :: [Y.Premise] -> [Y.Premise] -> [Y.Premise]
+excluding premises removed = filter (\premise -> premise.result `notElem` map (.result) removed) premises
+
+-- Evaluate one side-computation premise — a 'morph', 'lambda' or 'contextualize'
+-- of an earlier term — in isolation, binding its result meta. These never splice
+-- steps into the trace: 'morph' and 'lambda' reduce on a fresh chain and discard
+-- it, 'contextualize' is pure.
+sidePremise :: Expression -> DataizeContext -> Subst -> Y.Premise -> IO Subst
+sidePremise univ ctx subst premise = do
+  term <- execBuildTerm univ ctx (verb premise.operation) (verbArgs premise.operation) subst
+  case combine (substSingle premise.result (metaValue term)) subst of
+    Just subst' -> pure subst'
+    Nothing -> throwIO (userError (printf "premise meta '%s' clashes with an existing binding" (T.unpack premise.result)))
+  where
+    metaValue :: Term -> MetaValue
+    metaValue (TeExpression value) = MvExpression value
+    metaValue (TeAttribute value) = MvAttribute value
+    metaValue (TeBytes value) = MvBytes value
+    metaValue (TeBindings value) = MvBindings value
+
+-- The build-term function name backing a premise operation.
+verb :: Y.Operation -> String
+verb (Y.OpMorph _) = "morph"
+verb (Y.OpNormalize _) = "normalize"
+verb (Y.OpLambda _) = "lambda"
+verb (Y.OpContextualize _ _) = "contextualize"
+verb (Y.OpDataize _) = "dataize"
+
+-- The build-term arguments backing a premise operation.
+verbArgs :: Y.Operation -> [ExtraArgument]
+verbArgs (Y.OpMorph expr) = [ArgExpression expr]
+verbArgs (Y.OpNormalize expr) = [ArgExpression expr]
+verbArgs (Y.OpLambda expr) = [ArgExpression expr]
+verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context]
+verbArgs (Y.OpDataize expr) = [ArgExpression expr]
+
 leadsTo :: NonEmpty Rewritten -> String -> Expression -> DataizeContext -> IO (NonEmpty Rewritten)
 leadsTo ((prog, _) :| rest) rule expr DataizeContext{..} = do
   prog' <- withLocatedExpression _locator expr prog
   pure ((prog', Nothing) :| (prog, Just rule) : rest)
 
--- Reduce 'expr' to its normal form through the normalization rewriter,
--- splicing the individual steps (alpha, copy, dot, …) into the chain and
--- returning the normalized expression together with the extended sequence.
+-- Reduce 'expr' to its normal form through the normalization rewriter, embedding
+-- it at '_locator' into the working program taken from the head of the step
+-- chain so the rewriter sees the surrounding context. Splices the individual
+-- steps (alpha, copy, dot, …) into the chain and returns the normalized
+-- expression together with the extended sequence.
 normalized :: Expression -> NonEmpty Rewritten -> DataizeContext -> IO (Expression, NonEmpty Rewritten)
 normalized expr seq ctx@DataizeContext{..} = do
-  prog' <- withLocatedExpression _locator expr _program
+  prog' <- withLocatedExpression _locator expr (fst (NE.head seq))
   (rewrittens, _) <- rewrite prog' normalizationRules (rewriteContext ctx)
   let (rw :| rws) = NE.reverse rewrittens
       seq' = rw :| rws <> NE.tail seq
@@ -190,87 +278,82 @@
     rewriteContext DataizeContext{..} =
       RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep
 
--- Synthetic dataize function for internal usage inside atoms
--- Here we modify original program from context by adding new binding
--- which refers to expression we want to dataize. As a caller of 𝔻, it first
--- reduces the expression to a normal form, since 𝔻 only accepts normal forms.
-_dataize :: Expression -> DataizeContext -> IO (Maybe Bytes)
-_dataize expr ctx@DataizeContext{_buildTerm = buildTerm, _program = Program (ExFormation bds)} = do
-  (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty
-  let prog = Program (ExFormation (BiTau attr expr : bds))
-      ctx' = ctx{_program = prog}
-  (normal, seq) <- normalized expr ((prog, Nothing) :| []) ctx'
-  (bts, _) <- dataize' (normal, seq) ctx'
-  pure bts
-_dataize _ _ = throwIO (userError "Can't call _dataize from atoms with non-formation program")
+-- Synthetic dataize function for internal usage inside atoms. Here we modify the
+-- universe by adding a new binding which refers to the expression we want to
+-- dataize, building a local working program to reduce within. As a caller of 𝔻,
+-- it first reduces the expression to a normal form, since 𝔻 only accepts normal
+-- forms. The universe 'univ' itself is forwarded unchanged, so morphing Φ under
+-- this context still resolves to the true universe rather than to this
+-- synthetic, binding-prepended formation.
+_dataize :: Expression -> Expression -> DataizeContext -> IO Bytes
+_dataize expr univ ctx@DataizeContext{_buildTerm = buildTerm} = case univ of
+  ExFormation bds -> do
+    (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty
+    let prog = Program (ExFormation (BiTau attr expr : bds))
+    (normal, seq) <- normalized expr ((prog, Nothing) :| []) ctx
+    (bts, _) <- dataize' (normal, seq) univ ctx
+    pure bts
+  _ -> throwIO (userError "Can't call _dataize from atoms with non-formation universe")
 
-atom :: T.Text -> Expression -> DataizeContext -> IO Expression
-atom "L_number_plus" self ctx = do
-  left <- _dataize (ExDispatch self (AtLabel "x")) ctx
-  right <- _dataize (ExDispatch self AtRho) ctx
-  case (left, right) of
-    (Just left', Just right') -> do
-      let first = either toDouble id (btsToNum left')
-          second = either toDouble id (btsToNum right')
-          sum = first + second
-      pure (DataNumber (numToBts sum))
+-- A number atom only operates on numeric data. Empty bytes (the result of
+-- dataizing a bare formation ⟦𝐵⟧ or ⊥ now that 𝔻 is total) carry no number,
+-- so the operand is rejected and the atom yields ⊥.
+asNumber :: Bytes -> Maybe Double
+asNumber BtEmpty = Nothing
+asNumber bts = Just (either toDouble id (btsToNum bts))
+
+atom :: T.Text -> Expression -> Expression -> DataizeContext -> IO Expression
+atom "L_number_plus" self univ ctx = do
+  left <- _dataize (ExDispatch self (AtLabel "x")) univ ctx
+  right <- _dataize (ExDispatch self AtRho) univ ctx
+  case (asNumber left, asNumber right) of
+    (Just first, Just second) -> pure (DataNumber (numToBts (first + second)))
     _ -> pure ExTermination
-atom "L_number_times" self ctx = do
-  left <- _dataize (ExDispatch self (AtLabel "x")) ctx
-  right <- _dataize (ExDispatch self AtRho) ctx
-  case (left, right) of
-    (Just left', Just right') -> do
-      let first = either toDouble id (btsToNum left')
-          second = either toDouble id (btsToNum right')
-          sum = first * second
-      pure (DataNumber (numToBts sum))
+atom "L_number_times" self univ ctx = do
+  left <- _dataize (ExDispatch self (AtLabel "x")) univ ctx
+  right <- _dataize (ExDispatch self AtRho) univ ctx
+  case (asNumber left, asNumber right) of
+    (Just first, Just second) -> pure (DataNumber (numToBts (first * second)))
     _ -> pure ExTermination
-atom "L_number_eq" self ctx = do
-  x <- _dataize (ExDispatch self (AtLabel "x")) ctx
-  rho <- _dataize (ExDispatch self AtRho) ctx
-  case (x, rho) of
-    (Just x', Just rho') -> do
-      let self' = either toDouble id (btsToNum rho')
-          first = either toDouble id (btsToNum x')
+atom "L_number_eq" self univ ctx = do
+  x <- _dataize (ExDispatch self (AtLabel "x")) univ ctx
+  rho <- _dataize (ExDispatch self AtRho) univ ctx
+  case (asNumber x, asNumber rho) of
+    (Just first, Just self') ->
       if self' == first
         then pure (DataNumber (numToBts first))
         else pure (ExDispatch self (AtLabel "y"))
     _ -> pure ExTermination
-atom func _ _ = throwIO (userError (printf "Atom '%s' does not exist" (T.unpack func)))
+atom func _ _ _ = throwIO (userError (printf "Atom '%s' does not exist" (T.unpack func)))
 
 -- Augment the injected, context-free term builder with the dataization and
--- morphing operations that need the full evaluation context: 'lambda' applies
--- an atom and 'global' dispatches from the universe Q. Every other function is
--- delegated unchanged.
-execBuildTerm :: DataizeContext -> BuildTermFunc
-execBuildTerm ctx "lambda" = _lambda ctx
-execBuildTerm ctx "global" = _global ctx
-execBuildTerm ctx "morph" = _morph ctx
-execBuildTerm ctx func = _buildTerm ctx func
+-- morphing operations that need the universe: 'lambda' applies an atom and
+-- 'morph' morphs a sub-expression. Both receive the universe 'univ'. Every other
+-- function is delegated unchanged.
+execBuildTerm :: Expression -> DataizeContext -> BuildTermFunc
+execBuildTerm univ ctx "lambda" = _lambda univ ctx
+execBuildTerm univ ctx "morph" = _morph univ ctx
+execBuildTerm _ ctx func = _buildTerm ctx func
 
-_lambda :: DataizeContext -> BuildTermMethod
-_lambda ctx [ArgExpression expr] subst = do
+_lambda :: Expression -> DataizeContext -> BuildTermMethod
+_lambda univ ctx [ArgExpression expr] subst = do
   form <- buildExpressionThrows expr subst
   case form of
     ExFormation bds -> do
-      resolved <- formation bds ctx
+      resolved <- formation bds univ ctx
       case resolved of
         Just obj -> pure (TeExpression obj)
         Nothing -> throwIO (userError "Function lambda() expects a formation with a λ binding")
     _ -> throwIO (userError "Function lambda() expects a formation")
-_lambda _ _ _ = throwIO (userError "Function lambda() requires exactly 1 expression argument")
-
-_global :: DataizeContext -> BuildTermMethod
-_global DataizeContext{_program = Program prog} [] _ = pure (TeExpression prog)
-_global _ _ _ = throwIO (userError "Function global() requires no arguments")
+_lambda _ _ _ _ = throwIO (userError "Function lambda() requires exactly 1 expression argument")
 
 -- The Morphing function 𝕄 exposed as a build-term function so a rule can morph
 -- a sub-expression in its 'where' (the 'dispatch' and 'application' rules morph
 -- the head before re-attaching it). The step chain is discarded: the producing
 -- rule splices the surrounding normalization steps itself.
-_morph :: DataizeContext -> BuildTermMethod
-_morph ctx@DataizeContext{_program = prog} [ArgExpression expr] subst = do
+_morph :: Expression -> DataizeContext -> BuildTermMethod
+_morph univ ctx [ArgExpression expr] subst = do
   built <- buildExpressionThrows expr subst
-  (morphed, _) <- morph (built, (prog, Nothing) :| []) ctx
+  (morphed, _) <- morph (built, (Program univ, Nothing) :| []) univ ctx
   pure (TeExpression morphed)
-_morph _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")
+_morph _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")
diff --git a/src/Encoding.hs b/src/Encoding.hs
--- a/src/Encoding.hs
+++ b/src/Encoding.hs
@@ -104,6 +104,7 @@
   toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr)
   toASCII CO_PART_OF{..} = CO_PART_OF (toASCII expr) (toASCII binding)
   toASCII CO_DISJOINT{..} = CO_DISJOINT (map toASCII attrs) (map toASCII groups)
+  toASCII CO_FORMATION{..} = CO_FORMATION (toASCII expr)
   toASCII CO_EMPTY = CO_EMPTY
 
 instance ToASCII EXTRA_ARG where
diff --git a/src/Functions.hs b/src/Functions.hs
--- a/src/Functions.hs
+++ b/src/Functions.hs
@@ -29,7 +29,7 @@
 -- 'Dataize.execBuildTerm', not by 'buildTerm'. They are available while
 -- executing dataization and morphing rules, but not rewriting rules.
 execFunctions :: [String]
-execFunctions = ["lambda", "global", "morph"]
+execFunctions = ["lambda", "morph"]
 
 buildTerm :: BuildTermFunc
 buildTerm func args subst = do
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -21,6 +21,7 @@
   , LatexContext (..)
   , meetInPrograms
   , meetInProgram
+  , conditionToLatex
   ) where
 
 import AST
@@ -339,6 +340,7 @@
   toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr)
   toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding)
   toLaTeX CO_DISJOINT{..} = CO_DISJOINT (map toLaTeX attrs) (map toLaTeX groups)
+  toLaTeX CO_FORMATION{..} = CO_FORMATION (toLaTeX expr)
   toLaTeX CO_EMPTY = CO_EMPTY
 
 instance ToLaTeX EXTRA_ARG where
@@ -368,46 +370,63 @@
     joinedConditions Nothing second@(Just _) = second
     joinedConditions (Just first) (Just second) = Just (Y.And [first, second])
 
+-- Render a morphing rule as a LaTeX inference rule: each premise becomes a
+-- judgment above the line and the conclusion is 𝕄(match, e) ⟿ n-result below.
 explainMorphRule :: Y.MorphRule -> String
 explainMorphRule rule =
-  trrule
-    "\\phinoMorphingRule"
-    rule.label
+  inference
     rule.name
-    (morph (renderToLatex (expressionToCST rule.match) defaultLatexContext))
-    (morphOutcome rule.then_)
+    rule.label
     rule.when
-    rule.where_
-  where
-    morphOutcome :: Y.MorphOutcome -> String
-    morphOutcome (Y.MoMorph (Y.MaExpr expr)) = morph (renderToLatex (expressionToCST expr) defaultLatexContext)
-    morphOutcome (Y.MoMorph (Y.MaNormalize expr)) = morph (normalize (renderToLatex (expressionToCST expr) defaultLatexContext))
-    morphOutcome (Y.MoStop expr) = renderToLatex (expressionToCST expr) defaultLatexContext
+    (map premiseToLatex rule.premises)
+    (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (renderExpr rule.nresult))
 
+-- Render a dataization rule as a LaTeX inference rule, with 𝔻(match, e) ⟿
+-- d-result as the conclusion below the line.
 explainDataizeRule :: Y.DataizeRule -> String
 explainDataizeRule rule =
-  trrule
-    "\\phinoDataizationRule"
-    rule.label
+  inference
     rule.name
-    (dataize (renderToLatex (expressionToCST rule.match) defaultLatexContext))
-    (dataizeOutcome rule.then_)
+    rule.label
     rule.when
-    rule.where_
-  where
-    dataizeOutcome :: Y.DataizeOutcome -> String
-    dataizeOutcome (Y.DoDataize (Y.DaExpr expr)) = dataize (renderToLatex (expressionToCST expr) defaultLatexContext)
-    dataizeOutcome (Y.DoDataize (Y.DaMorph expr)) = dataize (morph (renderToLatex (expressionToCST expr) defaultLatexContext))
-    dataizeOutcome (Y.DoDataize (Y.DaNormalize expr)) = dataize (normalize (renderToLatex (expressionToCST expr) defaultLatexContext))
-    dataizeOutcome (Y.DoData bytes) = T.unpack (render (toLaTeX (toCST' bytes :: BYTES)))
-    dataizeOutcome Y.DoNothing = "\\varnothing"
+    (map premiseToLatex rule.premises)
+    (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (renderBytes rule.dresult))
 
--- Render a single rule row through the given macro (one of
--- \phinoMorphingRule, \phinoNormalizationRule, \phinoDataizationRule): an
--- optional typeset label, name, left-hand side, right-hand side, the optional
--- 'if' condition and 'where' extras. When the label is present it becomes the
--- macro's first optional argument ('\macro[label]{name}'); when absent the
--- optional argument is omitted entirely ('\macro{name}').
+-- One premise judgment, rendered per its operation. 𝕄 ('morph') and 𝔻
+-- ('dataize') are binary and carry the universe 'e' they were given; the rest
+-- are unary.
+premiseToLatex :: Y.Premise -> String
+premiseToLatex premise = case premise.operation of
+  Y.OpMorph arg -> phinoMorph (renderExpr arg) "e" (renderExpr (ExMeta premise.result))
+  Y.OpDataize arg -> phinoDataize (renderExpr arg) "e" (renderBytes (BtMeta premise.result))
+  Y.OpNormalize arg -> phinoNormalize (renderExpr arg) (renderExpr (ExMeta premise.result))
+  Y.OpLambda arg -> phinoEvaluate (renderExpr arg) (renderExpr (ExMeta premise.result))
+  Y.OpContextualize arg context -> phinoContextualize (renderExpr arg) (renderExpr context) (renderExpr (ExMeta premise.result))
+
+-- Assemble an inference block from a name, optional label, optional side
+-- condition, the premise judgments and the conclusion judgment.
+inference :: String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String
+inference name label cond premises conclusion =
+  intercalate "\n" $
+    ["\\begin{phinoInference}", "  \\phinoName{" ++ name ++ "}"]
+      ++ maybe [] (\symbol -> ["  \\phinoLabel{" ++ symbol ++ "}"]) label
+      ++ maybe [] (\rendered -> ["  \\phinoCondition{ " ++ rendered ++ " }"]) (conditionInLatex cond)
+      ++ map (\premise -> "  \\phinoPremise{ " ++ premise ++ " }") premises
+      ++ ["  \\phinoConclusion{ " ++ conclusion ++ " }", "\\end{phinoInference}"]
+
+renderExpr :: Expression -> String
+renderExpr expr = renderToLatex (expressionToCST expr) defaultLatexContext
+
+renderBytes :: Bytes -> String
+renderBytes bytes = T.unpack (render (toLaTeX (toCST' bytes :: BYTES)))
+
+-- Render a single normalization rule row through the \phinoNormalizationRule
+-- macro: an optional typeset label, name, left-hand side, right-hand side, the
+-- optional 'if' condition and 'where' extras. When the label is present it
+-- becomes the macro's first optional argument ('\macro[label]{name}'); when
+-- absent the optional argument is omitted entirely ('\macro{name}').
+-- Morphing and dataization rules render as inference rules instead (see
+-- 'explainMorphRule' and 'explainDataizeRule').
 trrule :: String -> Maybe String -> String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String
 trrule macro label name lhs rhs cond extras =
   intercalate
@@ -421,14 +440,29 @@
   where
     labelArg = maybe "" (\symbol -> "[" ++ symbol ++ "]") label
 
-morph :: String -> String
-morph inner = "\\phinoMorph{ " ++ inner ++ " }"
+-- 𝕄 and 𝔻 are binary, 𝕄(input, e) ⟿ output, so they render with the universe
+-- as the middle argument: \phinoMorph{ input }{ e }{ output }. 𝒩, 𝔼 and 𝒞 carry
+-- no universe.
+phinoMorph :: String -> String -> String -> String
+phinoMorph input univ output = printf "\\phinoMorph{ %s }{ %s }{ %s }" input univ output
 
-dataize :: String -> String
-dataize inner = "\\phinoDataize{ " ++ inner ++ " }"
+phinoDataize :: String -> String -> String -> String
+phinoDataize input univ output = printf "\\phinoDataize{ %s }{ %s }{ %s }" input univ output
 
-normalize :: String -> String
-normalize inner = "\\phinoNormalize{ " ++ inner ++ " }"
+phinoNormalize :: String -> String -> String
+phinoNormalize input = printf "\\phinoNormalize{ %s }{ %s }" input
+
+phinoEvaluate :: String -> String -> String
+phinoEvaluate input = printf "\\phinoEvaluate{ %s }{ %s }" input
+
+phinoContextualize :: String -> String -> String -> String
+phinoContextualize input context = printf "\\phinoContextualize{ %s }{ %s }{ %s }" input context
+
+conditionInLatex :: Maybe Y.Condition -> Maybe String
+conditionInLatex Nothing = Nothing
+conditionInLatex (Just cond) = case conditionToCST cond of
+  CO_EMPTY -> Nothing
+  cond' -> Just (renderToLatex cond' defaultLatexContext)
 
 braced :: String -> String
 braced = printf "{ %s }"
diff --git a/src/Lining.hs b/src/Lining.hs
--- a/src/Lining.hs
+++ b/src/Lining.hs
@@ -83,6 +83,7 @@
   toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr)
   toSingleLine CO_PART_OF{..} = CO_PART_OF (toSingleLine expr) (toSingleLine binding)
   toSingleLine CO_DISJOINT{..} = CO_DISJOINT attrs (map toSingleLine groups)
+  toSingleLine CO_FORMATION{..} = CO_FORMATION (toSingleLine expr)
   toSingleLine CO_EMPTY = CO_EMPTY
 
 instance ToSingleLine EXTRA_ARG where
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -247,7 +247,7 @@
   render EQUAL = "="
   render NOT_EQUAL = "\\not="
   render GREATER = ">"
-  render NOT_GREATER = "\\not>"
+  render NOT_GREATER = "\\leq"
 
 instance Render CONDITION where
   render CO_BELONGS{..} = render attr <> " " <> render belongs <> " " <> render set
@@ -260,10 +260,12 @@
       renderWrapped cond = render cond
   render CO_NF{..} = "\\isnormal{ " <> render expr <> " }"
   render CO_ABSOLUTE{..} = render expr <> " " <> render belongs <> " \\mathcal{K}"
+  render CO_NOT{condition = CO_FORMATION{..}} = "\\phinoNotFormation{ " <> render expr <> " }"
   render CO_NOT{..} = renderFunc "not" condition
   render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right
   render CO_MATCHES{..} = "matches( " <> T.pack regex <> ", " <> render expr <> " )"
   render CO_PART_OF{..} = "part-of( " <> render expr <> ", " <> render binding <> " )"
+  render CO_FORMATION{..} = "\\phinoIsFormation{ " <> render expr <> " }"
   render CO_DISJOINT{..} =
     "[ "
       <> T.intercalate ", " (map render attrs)
@@ -283,10 +285,12 @@
 
 instance Render EXTRA where
   render EXTRA{func = "contextualize", args = arg : rest, ..} = render meta <> " \\coloneqq \\ctx{ " <> render arg <> " }{ " <> T.intercalate ", " (map render rest) <> " }"
+  -- 𝕄 is binary, 𝕄(n, e), so a 'morph' extra renders with the universe
+  -- metavariable 'e' as its second argument, matching how the morphing rules
+  -- forward the universe unchanged.
+  render EXTRA{func = "morph", ..} = render meta <> " \\coloneqq \\phinoMorph{ " <> T.intercalate ", " (map render args) <> " }{ e }"
   render EXTRA{..} = render meta <> " \\coloneqq " <> macro func <> "{ " <> T.intercalate ", " (map render args) <> " }"
     where
       macro :: String -> Text
       macro "lambda" = "\\phinoEvaluate"
-      macro "morph" = "\\phinoMorph"
-      macro "global" = "\\phinoGlobal"
       macro name = "\\" <> T.pack name
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -195,6 +195,18 @@
     xiFree (ExDispatch e _) = xiFree e
     xiFree _ = False
 
+-- Hold when the given expression is a formation (an abstraction ⟦…⟧). A meta
+-- is resolved first, so 'binding 𝑛' inspects whatever 𝑛 is bound to.
+_isFormation :: Expression -> Subst -> RuleContext -> IO [Subst]
+_isFormation (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of
+  Just (MvExpression expr) -> _isFormation expr (Subst mp) ctx
+  _ -> pure []
+_isFormation expr subst _ = pure [subst | isFormation expr]
+  where
+    isFormation :: Expression -> Bool
+    isFormation (ExFormation _) = True
+    isFormation _ = False
+
 _matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst]
 _matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of
   Just (MvExpression expr) -> _matches pat expr (Subst mp) ctx
@@ -247,6 +259,7 @@
 meetCondition' (Y.Matches pat expr) = _matches pat expr
 meetCondition' (Y.PartOf expr bd) = _partOf expr bd
 meetCondition' (Y.Disjoint attrs bds) = _disjoint attrs bds
+meetCondition' (Y.IsFormation expr) = _isFormation expr
 
 -- For each substitution check if it meetCondition to given condition
 -- If substitution does not meet the condition - it's thrown out
@@ -343,19 +356,25 @@
 kMetaNames = metaNamesWithPrefix "k"
 
 matchExpressionWithRule :: Expression -> Y.Rule -> RuleContext -> IO [Subst]
-matchExpressionWithRule = matchExpressionBy matchExpression
+matchExpressionWithRule = matchExpressionBy matchExpression [substEmpty]
 
 -- Like 'matchExpressionWithRule' but matches the pattern against the whole
 -- expression only (no deep, sub-expression matching). Used by the dataization
 -- and morphing driver, where a rule applies to the entire configuration rather
--- than to nested redexes.
-matchExpressionWithRule' :: Expression -> Y.Rule -> RuleContext -> IO [Subst]
+-- than to nested redexes. The leading '[Subst]' seeds matching with pre-bound
+-- meta-variables: the morphing driver passes the global universe bound to 'e',
+-- the second argument of 𝕄(n, e), so the 'root' rule reads it directly instead
+-- of through a 'global()' build-term function. Pass '[substEmpty]' for no seed.
+matchExpressionWithRule' :: [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst]
 matchExpressionWithRule' = matchExpressionBy matchExpression'
 
-matchExpressionBy :: MatchExpressionFunc -> Expression -> Y.Rule -> RuleContext -> IO [Subst]
-matchExpressionBy matcher expr rule ctx =
+-- The seed substitutions are combined into every match, so a pre-bound meta in
+-- the seed is dropped only when the pattern binds the same name to a different
+-- value; rules that do not mention the name simply carry it along unused.
+matchExpressionBy :: MatchExpressionFunc -> [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst]
+matchExpressionBy matcher seed expr rule ctx =
   let ptn = rule.pattern
-      matched = matcher ptn expr
+      matched = combineMany seed (matcher ptn expr)
       name = rule.name
    in if null matched
         then do
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -197,6 +197,7 @@
   toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr)
   toSalty CO_PART_OF{..} = CO_PART_OF (toSalty expr) (toSalty binding)
   toSalty CO_DISJOINT{..} = CO_DISJOINT attrs (map toSalty groups)
+  toSalty CO_FORMATION{..} = CO_FORMATION (toSalty expr)
   toSalty CO_EMPTY = CO_EMPTY
 
 instance ToSalty EXTRA_ARG where
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -83,13 +83,14 @@
     withObject
       "Condition"
       ( \v -> do
-          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "gt", "in", "matches", "part-of", "disjoint"]
+          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "gt", "in", "matches", "part-of", "disjoint", "formation"]
           asum
             [ And <$> v .: "and"
             , Or <$> v .: "or"
             , Not <$> v .: "not"
             , NF <$> v .: "nf"
             , Absolute <$> v .: "absolute"
+            , IsFormation <$> v .: "formation"
             , do
                 vals <- v .: "disjoint"
                 case vals of
@@ -180,6 +181,7 @@
   | Matches String Expression
   | PartOf Expression Binding
   | Disjoint [Attribute] [Binding]
+  | IsFormation Expression
   deriving (Eq, Generic, Show)
 
 data ExtraArgument
@@ -221,92 +223,90 @@
 yamlRule :: FilePath -> IO Rule
 yamlRule = Yaml.decodeFileThrow
 
--- The right-hand side of a morphing reduction 𝕄(match) ⟿ then.
--- A mapping ('{ morph: arg }') keeps reducing under 𝕄; a bare expression
--- (including ⊥) is the terminal result.
-data MorphOutcome
-  = MoMorph MorphArg
-  | MoStop Expression
-  deriving (Eq, Generic, Show)
-
--- The argument of a morphing continuation: either a plain expression ('𝕄(e)')
--- or the normalization of one ('𝕄(𝒩(e))', written '{ normalize: e }').
-data MorphArg
-  = MaExpr Expression
-  | MaNormalize Expression
-  deriving (Eq, Generic, Show)
-
--- The right-hand side of a dataization reduction 𝔻(match) ⟿ then.
--- A mapping ('{ dataize: arg }') keeps reducing under 𝔻; a bare bytes scalar
--- yields data; the 'nothing' keyword marks the function as undefined.
-data DataizeOutcome
-  = DoDataize DataizeArg
-  | DoData Bytes
-  | DoNothing
+-- One premise above the inference line of a morphing or dataization rule: bind
+-- the meta named 'result' to the value of applying 'operation' to its argument.
+-- The universe e is the fixed second argument of 𝕄 and 𝔻, not a per-premise
+-- value, so it is not recorded here.
+data Premise = Premise
+  { result :: Text
+  , operation :: Operation
+  }
   deriving (Eq, Generic, Show)
 
--- The argument of a dataization continuation: a plain expression ('𝔻(e)'),
--- the morphing of one ('𝔻(𝕄(e))', written '{ morph: e }'), or the
--- normalization of one ('𝔻(𝒩(e))', written '{ normalize: e }').
-data DataizeArg
-  = DaExpr Expression
-  | DaMorph Expression
-  | DaNormalize Expression
+-- The reduction a premise performs, mirroring the build-term functions and the
+-- 𝒩 and 𝔻 reducers the engine already provides.
+data Operation
+  = OpMorph Expression
+  | OpNormalize Expression
+  | OpLambda Expression
+  | OpContextualize Expression Expression
+  | OpDataize Expression
   deriving (Eq, Generic, Show)
 
--- One ordered morphing rule: match the expression, build extra metas in
--- 'where', filter by 'when', then reduce per 'then'.
+-- One morphing rule in inference-rule form: when 'match' matches the term and
+-- 'ematch' matches the universe (binding 'e'), the rule yields 'nresult' (a
+-- premise meta or a literal) provided 'when' holds and the ordered 'premises'
+-- reduce as stated. 'ematch' is the universe-argument matcher of 𝕄(n, e), in
+-- practice always the '𝑒' meta.
 data MorphRule = MorphRule
   { name :: String
   , label :: Maybe String
-  , description :: Maybe String
   , match :: Expression
-  , where_ :: Maybe [Extra]
+  , ematch :: Expression
+  , nresult :: Expression
   , when :: Maybe Condition
-  , then_ :: MorphOutcome
+  , premises :: [Premise]
   }
   deriving (Generic, Show)
 
--- One ordered dataization rule, structured like 'MorphRule' but reducing
--- under 𝔻 and able to terminate with bytes or 'nothing'.
+-- One dataization rule in inference-rule form, structured like 'MorphRule' but
+-- terminating with bytes ('dresult').
 data DataizeRule = DataizeRule
   { name :: String
   , label :: Maybe String
-  , description :: Maybe String
   , match :: Expression
-  , where_ :: Maybe [Extra]
+  , ematch :: Expression
+  , dresult :: Bytes
   , when :: Maybe Condition
-  , then_ :: DataizeOutcome
+  , premises :: [Premise]
   }
   deriving (Generic, Show)
 
-instance FromJSON MorphOutcome where
-  parseJSON (Object o) = do
-    validateYamlObject o ["morph"]
-    MoMorph <$> o .: "morph"
-  parseJSON v = MoStop <$> parseJSON v
-
-instance FromJSON MorphArg where
-  parseJSON (Object o) = do
-    validateYamlObject o ["normalize"]
-    MaNormalize <$> o .: "normalize"
-  parseJSON v = MaExpr <$> parseJSON v
+instance FromJSON Premise where
+  parseJSON =
+    withObject
+      "Premise"
+      (\o -> Premise <$> premiseResult o <*> premiseOperation o)
 
-instance FromJSON DataizeOutcome where
-  parseJSON (Object o) = do
-    validateYamlObject o ["dataize"]
-    DoDataize <$> o .: "dataize"
-  parseJSON (String "nothing") = pure DoNothing
-  parseJSON v = DoData <$> parseJSON v
+-- The meta a premise binds, taken from its 'n-result' (an expression meta) or
+-- 'd-result' (a bytes meta).
+premiseResult :: Object -> Parser Text
+premiseResult o = do
+  expr <- o .:? "n-result"
+  case expr of
+    Just (ExMeta metaName) -> pure metaName
+    Just _ -> fail "'n-result' must be an expression meta"
+    Nothing -> do
+      bytes <- o .:? "d-result"
+      case bytes of
+        Just (BtMeta metaName) -> pure metaName
+        Just _ -> fail "'d-result' must be a bytes meta"
+        Nothing -> fail "a premise needs an 'n-result' or 'd-result' meta"
 
-instance FromJSON DataizeArg where
-  parseJSON (Object o) = do
-    validateYamlObject o ["morph", "normalize"]
-    morphed <- o .:? "morph"
-    case morphed of
-      Just expr -> pure (DaMorph expr)
-      Nothing -> DaNormalize <$> o .: "normalize"
-  parseJSON v = DaExpr <$> parseJSON v
+-- The single verb of a premise.
+premiseOperation :: Object -> Parser Operation
+premiseOperation o =
+  asum
+    [ OpMorph <$> o .: "morph"
+    , OpNormalize <$> o .: "normalize"
+    , OpLambda <$> o .: "lambda"
+    , do
+        vals <- o .: "contextualize"
+        case vals of
+          [expr, context] -> OpContextualize <$> parseJSON expr <*> parseJSON context
+          _ -> fail "'contextualize' expects exactly two arguments"
+    , OpDataize <$> o .: "dataize"
+    ]
 
 instance FromJSON MorphRule where
   parseJSON =
@@ -316,11 +316,11 @@
           MorphRule
             <$> o .: "name"
             <*> o .:? "label"
-            <*> o .:? "description"
             <*> o .: "match"
-            <*> o .:? "where"
+            <*> o .: "e-match"
+            <*> o .: "n-result"
             <*> o .:? "when"
-            <*> o .: "then"
+            <*> o .:? "premises" .!= []
       )
 
 instance FromJSON DataizeRule where
@@ -331,11 +331,11 @@
           DataizeRule
             <$> o .: "name"
             <*> o .:? "label"
-            <*> o .:? "description"
             <*> o .: "match"
-            <*> o .:? "where"
+            <*> o .: "e-match"
+            <*> o .: "d-result"
             <*> o .:? "when"
-            <*> o .: "then"
+            <*> o .:? "premises" .!= []
       )
 
 decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a]
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -867,9 +867,9 @@
       withStdin "Q -> [[ D> 01- ]]" $
         testCLISucceeded ["dataize"] ["01-"]
 
-    it "dataizes to dead" $
+    it "dataizes empty object to empty bytes" $
       withStdin "Q -> [[ ]]" $
-        testCLISucceeded ["dataize"] ["⊥"]
+        testCLISucceeded ["dataize"] ["--"]
 
     it "dataizes with --sequence" $
       withStdin "{[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]}" $
@@ -981,7 +981,7 @@
             , "\\phinoNormalizationRule{amiss}"
             , "  { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"
             , "  { T }"
-            , "  { \\vert \\overline{ B } \\vert \\not> i }"
+            , "  { \\vert \\overline{ B } \\vert \\leq i }"
             , "  { }"
             , "\\phinoNormalizationRule{copy}"
             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
@@ -1045,51 +1045,67 @@
       testCLISucceeded
         ["explain", "--morph"]
         [ unlines
-            [ "\\phinoMorphingRule{prim}"
-            , "  { \\phinoMorph{ [[ B ]] } }"
-            , "  { [[ B ]] }"
-            , "  { }"
-            , "  { }"
-            , "\\phinoMorphingRule[\\lambda]{lambda}"
-            , "  { \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau } }"
-            , "  { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }"
-            , "  { }"
-            , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"
-            , "\\phinoMorphingRule{dispatch}"
-            , "  { \\phinoMorph{ n . \\tau } }"
-            , "  { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }"
-            , "  { }"
-            , "  { e \\coloneqq \\phinoMorph{ n } }"
-            , "\\phinoMorphingRule{application}"
-            , "  { \\phinoMorph{ n ( \\tau -> e ) } }"
-            , "  { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\tau -> e ) } } }"
-            , "  { }"
-            , "  { e_1 \\coloneqq \\phinoMorph{ n } }"
-            , "\\phinoMorphingRule{applicationa}"
-            , "  { \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e ) } }"
-            , "  { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\phiTerminal{\\alpha_{i}} -> e ) } } }"
-            , "  { }"
-            , "  { e_1 \\coloneqq \\phinoMorph{ n } }"
-            , "\\phinoMorphingRule{root}"
-            , "  { \\phinoMorph{ Q } }"
-            , "  { \\phinoMorph{ \\phinoNormalize{ e } } }"
-            , "  { e \\not= Q }"
-            , "  { e \\coloneqq \\phinoGlobal{  } }"
-            , "\\phinoMorphingRule{dead}"
-            , "  { \\phinoMorph{ T } }"
-            , "  { T }"
-            , "  { }"
-            , "  { }"
-            , "\\phinoMorphingRule{xi}"
-            , "  { \\phinoMorph{ \\phiTerminal{\\xi} } }"
-            , "  { T }"
-            , "  { }"
-            , "  { }"
-            , "\\phinoMorphingRule{globe}"
-            , "  { \\phinoMorph{ Q } }"
-            , "  { T }"
-            , "  { }"
-            , "  { }"
+            [ "\\begin{phinoInference}"
+            , "  \\phinoName{prim}"
+            , "  \\phinoLabel{prim}"
+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ [[ B ]] } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{lambda}"
+            , "  \\phinoLabel{\\lambda}"
+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n . \\tau }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ n_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ n_2 } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{dispatch}"
+            , "  \\phinoLabel{disp}"
+            , "  \\phinoCondition{ \\phinoNotFormation{ n } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ n_3 } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{application}"
+            , "  \\phinoLabel{app}"
+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> e_1 ) }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> e_1 ) }{ e }{ n_3 } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{applicationa}"
+            , "  \\phinoLabel{appa}"
+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ n_3 } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{root}"
+            , "  \\phinoLabel{root}"
+            , "  \\phinoCondition{ e \\not= Q }"
+            , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ n_1 } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{dead}"
+            , "  \\phinoLabel{dead}"
+            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e }{ T } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{xi}"
+            , "  \\phinoLabel{xi}"
+            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ T } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{globe}"
+            , "  \\phinoLabel{globe}"
+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ T } }"
+            , "\\end{phinoInference}"
             ]
         ]
 
@@ -1097,36 +1113,45 @@
       testCLISucceeded
         ["explain", "--dataize"]
         [ unlines
-            [ "\\phinoDataizationRule[\\Delta]{delta}"
-            , "  { \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] } }"
-            , "  { \\delta }"
-            , "  { }"
-            , "  { }"
-            , "\\phinoDataizationRule{box}"
-            , "  { \\phinoDataize{ [[ B_1, @ -> e, B_2 ]] } }"
-            , "  { \\phinoDataize{ \\phinoNormalize{ e_1 } } }"
-            , "  { [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset }"
-            , "  { e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } }"
-            , "\\phinoDataizationRule{fire}"
-            , "  { \\phinoDataize{ [[ B_1, L> F, B_2 ]] } }"
-            , "  { \\phinoDataize{ \\phinoNormalize{ e } } }"
-            , "  { }"
-            , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"
-            , "\\phinoDataizationRule{none}"
-            , "  { \\phinoDataize{ [[ B ]] } }"
-            , "  { \\varnothing }"
-            , "  { }"
-            , "  { }"
-            , "\\phinoDataizationRule{bott}"
-            , "  { \\phinoDataize{ T } }"
-            , "  { \\varnothing }"
-            , "  { }"
-            , "  { }"
-            , "\\phinoDataizationRule{norm}"
-            , "  { \\phinoDataize{ n } }"
-            , "  { \\phinoDataize{ \\phinoMorph{ n } } }"
-            , "  { }"
-            , "  { }"
+            [ "\\begin{phinoInference}"
+            , "  \\phinoName{delta}"
+            , "  \\phinoLabel{\\Delta}"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ \\delta } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{box}"
+            , "  \\phinoLabel{box}"
+            , "  \\phinoCondition{ [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset }"
+            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ n } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ \\delta } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{fire}"
+            , "  \\phinoLabel{fire}"
+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ \\delta } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{none}"
+            , "  \\phinoLabel{none}"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ -- } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{bott}"
+            , "  \\phinoLabel{bott}"
+            , "  \\phinoConclusion{ \\phinoDataize{ T }{ e }{ -- } }"
+            , "\\end{phinoInference}"
+            , "\\begin{phinoInference}"
+            , "  \\phinoName{norm}"
+            , "  \\phinoLabel{norm}"
+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ n }{ e }{ \\delta } }"
+            , "\\end{phinoInference}"
             ]
         ]
 
diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs
--- a/test/ConditionSpec.hs
+++ b/test/ConditionSpec.hs
@@ -25,6 +25,7 @@
       , "absolute(!e1)"
       , "matches(\"hello(\\\"\\u0000)\", !e)"
       , "part-of ( [[ x -> 1 ]] , !B ) "
+      , "not(formation(!n))"
       ]
       (\expr -> it expr (parseCondition expr `shouldSatisfy` isRight))
 
@@ -39,6 +40,7 @@
       , ("eq(!t1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "t1")) (Y.CmpExpr (ExMeta "e2")))
       , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))])
       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])
+      , ("not(formation(!n))", Y.Not (Y.IsFormation (ExMeta "n")))
       ]
       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res))
 
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -7,35 +7,38 @@
 module DataizeSpec (spec) where
 
 import AST
+import Control.Exception (SomeException)
 import Control.Monad
-import Data.List (nub)
+import Data.List (find, isInfixOf, nub)
 import Data.List.NonEmpty (NonEmpty (..))
+import Data.Maybe (fromMaybe)
 import Dataize (DataizeContext (DataizeContext), dataize, dataize', execBuildTerm, morph)
-import Deps (Term (TeExpression), dontSaveStep)
+import Deps (dontSaveStep)
 import Functions (buildTerm)
 import Matcher (substEmpty)
 import Parser (parseExpressionThrows, parseProgramThrows)
 import Rewriter (Rewritten)
+import Rule (RuleContext (RuleContext), matchExpressionWithRule')
 import Test.Hspec
 import Yaml qualified
 
-defaultDataizeContext :: Expression -> Program -> DataizeContext
-defaultDataizeContext loc prog = DataizeContext loc prog 25 25 False buildTerm dontSaveStep
+defaultDataizeContext :: Expression -> DataizeContext
+defaultDataizeContext loc = DataizeContext loc 25 25 False buildTerm dontSaveStep
 
-test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> DataizeContext -> IO (Maybe a, [Rewritten])) -> [(String, Expression, Expression, Maybe a)] -> Spec
+test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> DataizeContext -> IO (a, [Rewritten])) -> [(String, Expression, Expression, a)] -> Spec
 test func useCases =
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
       let prog = Program expr
-      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog)
+      (res, _) <- func (input, (prog, Nothing) :| []) expr (defaultDataizeContext ExRoot)
       res `shouldBe` output
 
-test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> DataizeContext -> IO (a, NonEmpty Rewritten)) -> [(String, Expression, Expression, a)] -> Spec
+test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> DataizeContext -> IO (a, NonEmpty Rewritten)) -> [(String, Expression, Expression, a)] -> Spec
 test' func useCases =
   forM_ useCases $ \(desc, input, expr, output) ->
     it desc $ do
       let prog = Program expr
-      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog)
+      (res, _) <- func (input, (prog, Nothing) :| []) expr (defaultDataizeContext ExRoot)
       res `shouldBe` output
 
 testDataize :: [(String, String, String, Bytes)] -> Spec
@@ -44,8 +47,8 @@
     it name $ do
       prog' <- parseProgramThrows prog
       loc' <- parseExpressionThrows loc
-      (value, _) <- dataize (defaultDataizeContext loc' prog')
-      value `shouldBe` Just res
+      (value, _) <- dataize prog' (defaultDataizeContext loc')
+      value `shouldBe` res
 
 spec :: Spec
 spec = do
@@ -64,16 +67,45 @@
         )
       ]
 
+  -- 'dispatch' fires only when its head is not a formation ('not (formation 𝑛)'),
+  -- so a formation head — λ-bearing or not — is left to 'lambda'/'prim'. The
+  -- two clauses are mutually exclusive and their order in 'morphing.yaml'
+  -- cannot change behavior.
+  describe "morphing 'dispatch' is disjoint from 'lambda'" $ do
+    let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot))
+        morphRule :: String -> Yaml.MorphRule
+        morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules)
+        asRule :: Yaml.MorphRule -> Yaml.Rule
+        asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing
+        lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho]
+    it "does not fire on a λ-bearing formation dispatch" $ do
+      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "dispatch")) rctx
+      substs `shouldBe` []
+    it "still fires on a non-λ-formation dispatch" $ do
+      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "dispatch")) rctx
+      null substs `shouldBe` False
+    -- ⟦λ ⤍ F⟧.a.b.c : 'dispatch' peels .c then .b (their heads are dispatches,
+    -- not λ-formations, so 'λ ∉ 𝐵' holds), then 'lambda' handles the base
+    -- ⟦λ ⤍ F⟧.a and fires the atom. The chain therefore routes
+    -- dispatch → dispatch → lambda; firing the undefined atom 'F' is what
+    -- raises the error, proving the base λ-formation reached 'lambda'.
+    it "drills a chained λ-formation dispatch down to the base 'lambda'" $ do
+      let base = ExFormation [BiLambda (Function "F")]
+          chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")
+      morph (chain, (Program ExRoot, Nothing) :| []) ExRoot (defaultDataizeContext ExRoot)
+        `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException))
+
   describe "dataize" $
     test
       dataize'
-      [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, Just (BtOne "00"))
-      , ("T => X", ExTermination, ExRoot, Nothing)
+      [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, BtOne "00")
+      , ("T => --", ExTermination, ExRoot, BtEmpty)
+      , ("[[ ]] => --", ExFormation [], ExRoot, BtEmpty)
       ,
         ( "[[ @ -> [[ D> 00-]] ]] => 00-"
         , ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "00"), BiVoid AtRho]), BiVoid AtRho]
         , ExRoot
-        , Just (BtOne "00")
+        , BtOne "00"
         )
       ,
         ( "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]] => 01-"
@@ -99,27 +131,23 @@
                 )
             ]
         , ExRoot
-        , Just (BtOne "01")
+        , BtOne "01"
         )
       ]
 
-  describe "execBuildTerm" $
-    it "returns the universe Q body for global()" $ do
-      prog <- parseProgramThrows "Q -> [[ x -> [[ D> 42- ]] ]]"
-      expected <- parseExpressionThrows "[[ x -> [[ D> 42- ]] ]]"
-      term <- execBuildTerm (defaultDataizeContext ExRoot prog) "global" [] substEmpty
-      case term of
-        TeExpression actual -> actual `shouldBe` expected
-        _ -> expectationFailure "global() did not return an expression"
-
   describe "labels every step with a defined rule or operation" $ do
-    let funcs = maybe [] (map Yaml.function)
+    let verb op = case op of
+          Yaml.OpMorph _ -> "morph"
+          Yaml.OpNormalize _ -> "normalize"
+          Yaml.OpLambda _ -> "lambda"
+          Yaml.OpContextualize _ _ -> "contextualize"
+          Yaml.OpDataize _ -> "dataize"
         allowed =
           map (.name) Yaml.morphingRules
             ++ map (.name) Yaml.dataizationRules
             ++ map (.name) Yaml.normalizationRules
-            ++ concatMap (funcs . (.where_)) Yaml.morphingRules
-            ++ concatMap (funcs . (.where_)) Yaml.dataizationRules
+            ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.morphingRules
+            ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.dataizationRules
     it "uses no step label without a defining rule or operation" $ do
       prog <-
         parseProgramThrows
@@ -132,7 +160,7 @@
               ]
           )
       loc <- parseExpressionThrows "Q"
-      (_, chain) <- dataize (defaultDataizeContext loc prog)
+      (_, chain) <- dataize prog (defaultDataizeContext loc)
       let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]
       unless
         (null orphans)
@@ -151,7 +179,7 @@
     let labelsOf loc src = do
           prog <- parseProgramThrows src
           loc' <- parseExpressionThrows loc
-          (_, chain) <- dataize (defaultDataizeContext loc' prog)
+          (_, chain) <- dataize prog (defaultDataizeContext loc')
           pure [label | (_, Just label) <- chain]
     it "dataizes 5.plus(6) through the expected rules" $ do
       labels <-
diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs
--- a/test/LaTeXSpec.hs
+++ b/test/LaTeXSpec.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
@@ -6,13 +8,15 @@
 -}
 module LaTeXSpec where
 
+import AST (Expression (ExMeta))
 import Control.Monad (forM_)
-import LaTeX (meetInProgram)
+import LaTeX (conditionToLatex, meetInProgram)
 import Parser (parseExpressionThrows, parseProgramThrows)
 import Test.Hspec (Spec, describe, it, shouldBe)
+import Yaml qualified as Y
 
 spec :: Spec
-spec =
+spec = do
   describe "meet program in program" $
     forM_
       [ ("Q.x.y", "{Q.x.y}", "{[[ x -> Q.x.y ]]}", ["Q.x.y"])
@@ -28,3 +32,10 @@
           res <- traverse parseExpressionThrows exprs
           meetInProgram ptn 4 tgt `shouldBe` res
       )
+
+  describe "renders the 'formation' condition" $
+    forM_
+      [ ("formation", Y.IsFormation (ExMeta "n"), "{ \\phinoIsFormation{ n } }")
+      , ("not formation", Y.Not (Y.IsFormation (ExMeta "n")), "{ \\phinoNotFormation{ n } }")
+      ]
+      (\(desc, cond, expected) -> it desc (conditionToLatex (Just cond) `shouldBe` expected))