diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -126,10 +126,12 @@
 ```
 
 Dataizing a symbol always gives the same bytes, the number 42, as above.
+Like `morph`, `dataize` fails on a term that is not a normal form.
 
 Inside an entry, `$` is the formation being fired and `Φ` is the universe.
 A meta is a named placeholder: `𝛿1`, `𝛿2` and so on hold bytes, while `𝑛1`,
-`𝑛2` and so on hold terms.
+`𝑛2` and so on hold normal forms, and a line that would bind one to any other
+term fails the run.
 An entry may hold only the keys below, and any other key refuses the whole
 file:
 
@@ -236,7 +238,7 @@
 * `--max-memory` bounds the live heap of the run, such as `8G`.
 
 `--partial` leaves a site in place when it runs out of steps, firings,
-nodes or memory, but a run out of time always fails.
+seconds, nodes or memory.
 
 ## Morph
 
@@ -377,7 +379,8 @@
 
 The `--abridged` option folds every formation longer than sixty-four
 characters, or than `--abridged=WIDTH`, into its `φ`, `Δ` and `λ` and a count
-of the rest.
+of the rest, and every application that long into its head and a count of its
+arguments.
 The `--abridged-data` option also cuts every byte string longer than eight
 bytes down to its first two bytes and its last two.
 
@@ -628,7 +631,9 @@
   replaces all the spaces with empty string. To escape braces and slashes
   in pattern and replacement parts - use them with `\\`,
   e.g. `s/\\(.+\\)//g`. In the replacement, `\\1` to `\\9`, as well as
-  `$1`, put what a group of the pattern matched, e.g. `s/([0-9]+)/\\1!/g`.
+  `$1`, put what a group of the pattern matched, e.g. `s/([0-9]+)/\\1!/g`,
+  and `&` puts the whole match, e.g. `s/[0-9]+/<&>/g`, while `\\&` puts a
+  literal `&`.
 * `random-string` - accepts dataizable expression or bytes as pattern.
   Replaces `%x` and `%d` formatters with random hex numbers and
   decimals accordingly. Uniqueness is guaranteed during one
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.163
+version: 0.0.164
 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/src/Abridge.hs b/src/Abridge.hs
--- a/src/Abridge.hs
+++ b/src/Abridge.hs
@@ -21,7 +21,9 @@
       | short expr || salient pair = EX_SINGLE (goPair pair) space (goExpr formation)
       | otherwise = goExpr formation
     goExpr EX_DISPATCH{..} = EX_DISPATCH (goExpr expr) space attr
-    goExpr EX_APPLICATION{..} = EX_APPLICATION (goExpr expr) space eol tab (goArgument argument) eol' tab' indent
+    goExpr app@EX_APPLICATION{..}
+      | short app = EX_APPLICATION (goExpr expr) space eol tab (goArgument argument) eol' tab' indent
+      | otherwise = EX_APPLICATION (goExpr expr) space eol tab (AA_TAU (APP_BINDING (PA_FOLDED (counted argument)))) eol' tab' indent
     goExpr EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (goExpr expr)
     goExpr EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (goExpr expr)
     goExpr EX_BYTES{..} = EX_BYTES (goBytes bytes)
@@ -55,6 +57,23 @@
     goArgument (AA_TAU APP_BINDING{..}) = AA_TAU (APP_BINDING (goPair pair))
     goArgument (AA_TAUS binding) = AA_TAUS (goIntact binding)
     goArgument (AA_EXPRS APP_ARG{..}) = AA_EXPRS (APP_ARG (goExpr expr) (goAppArgs args))
+    counted :: APP_ARGUMENT -> Int
+    counted (AA_TAU _) = 1
+    counted (AA_TAUS binding) = goCount binding
+      where
+        goCount :: BINDING -> Int
+        goCount BI_EMPTY{} = 0
+        goCount BI_PAIR{..} = 1 + goCounts bindings
+        goCount BI_META{..} = 1 + goCounts bindings
+        goCounts :: BINDINGS -> Int
+        goCounts BDS_EMPTY{} = 0
+        goCounts BDS_PAIR{..} = 1 + goCounts bindings
+        goCounts BDS_META{..} = 1 + goCounts bindings
+    counted (AA_EXPRS APP_ARG{args = rest}) = 1 + goCount rest
+      where
+        goCount :: APP_ARGS -> Int
+        goCount AAS_EMPTY = 0
+        goCount AAS_EXPR{..} = 1 + goCount args
     goIntact :: BINDING -> BINDING
     goIntact BI_PAIR{..} = BI_PAIR (goPair pair) (goIntacts bindings) tab
     goIntact BI_META{..} = BI_META meta (goIntacts bindings) tab
diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs
--- a/src/CLI/Parsers.hs
+++ b/src/CLI/Parsers.hs
@@ -344,7 +344,8 @@
         ( long "abridged"
             <> help
               "Shorten every 𝜑-expression written to the --protocol and --minutes files: a formation longer \
-              \than the width keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', while \
+              \than the width keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', an \
+              \application longer than the width keeps its head and folds its arguments the same way, while \
               \every byte string it writes stays whole; the width is 64 characters unless given as --abridged=WIDTH"
         )
         <|> option
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -20,7 +20,7 @@
 import Engine (Engine (..))
 import qualified Inference as In
 import Locator (locatedExpression)
-import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, carried, deeper, inferred, insideUniverse, leadsTo, onward, opening, parking, severing, universed)
+import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, carried, deeper, inferred, insideUniverse, leadsTo, onward, opening, parking, severing, universed, vetted)
 import Rewriter (Rewritten)
 
 type Dataized = (Bytes, [Rewritten])
@@ -35,11 +35,13 @@
 dataize :: Expression -> State -> ReduceContext -> IO (Outcome, [Rewritten], State)
 dataize universe state ctx@ReduceContext{..} = do
   expr <- locatedExpression _locator universe
+  vetted Dataization expr ctx
   result <- try (dataize' (expr, (universe, Nothing) :| []) universe state ctx)
   case result of
     Right ((bytes, seq), state') -> pure (Dataized bytes, reverse seq, state')
     Left (StuckAt func seq parked) | _partial -> residual seq parked{_stuck = Just func}
     Left (OutOfStepsAt _ seq parked) | _partial -> residual seq parked
+    Left (OutOfSteps _) | _partial -> pure (Residual expr, [(universe, Nothing)], state)
     Left (LoopingAt _ seq parked) | _partial -> residual seq parked
     Left (Undataizable term seq parked) | _partial -> do
       unless (dead `elem` _parked) (_saveEval (EvStuck _nesting dead Dataization term))
diff --git a/src/Evaluate.hs b/src/Evaluate.hs
--- a/src/Evaluate.hs
+++ b/src/Evaluate.hs
@@ -24,8 +24,8 @@
 import Forks (Refusal (Unnamed, Unripe), forked, joined)
 import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), cast, emptyLambdas, matched, minted, rewritten, stayed, symbolized, thrown)
 import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)
-import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, noted, opening, recalled, remember, remembered, remembering, retained, settled, starved, unparked, voided)
-import Printer (printFunction)
+import Morph (Answer (..), Budget (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, noted, opening, recalled, remember, remembered, remembering, retained, settled, starved, unparked, voided)
+import Printer (printExpression, printFunction)
 import Rule (RuleContext (RuleContext))
 import Text.Printf (printf)
 
@@ -335,7 +335,8 @@
               outcome <- try (settled placed univ state' reading)
               case outcome of
                 Right (sole@(ExFormation [BiLambda (FnSymbol _)]), _) -> pure (BiTau attr sole)
-                Left (OutOfTime cap) -> expired ctx cap
+                Left (OutOfSteps (Seconds cap)) -> expired ctx cap
+                Left (OutOfStepsAt (Seconds cap) _ _) -> expired ctx cap
                 _ -> pure bd
         resolved bd = pure bd
         reducible :: Expression -> Bool
@@ -422,6 +423,9 @@
     operand :: Expression -> IO Expression
     operand term = caller._engine._contextualize term self
     bind :: Meta -> MetaValue -> Subst -> IO Subst
+    bind meta (MvExpression term) _
+      | not (caller._engine._normal term) =
+          throwIO (userError (printf "The meta '%s' of λ function '%s' may hold only a normal form, but got: %s" (T.unpack meta._spelling) (T.unpack func) (printExpression term)))
     bind meta value bound = case combine (substSingle meta._name value) bound of
       Just bound' -> pure bound'
       Nothing ->
diff --git a/src/Functions.hs b/src/Functions.hs
--- a/src/Functions.hs
+++ b/src/Functions.hs
@@ -175,7 +175,7 @@
         | h == '/' -> (acc, rest, True)
         | otherwise -> nextUntilSlash rest (B.snoc acc h) escape
     referring :: Char -> Bool
-    referring char = isDigit char || char == '\\'
+    referring char = isDigit char || char == '\\' || char == '&'
 
 _randomString :: BuildTermMethod
 _randomString [arg] subst = do
diff --git a/src/Morph.hs b/src/Morph.hs
--- a/src/Morph.hs
+++ b/src/Morph.hs
@@ -11,7 +11,7 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Morph (Answer (..), Deadline (..), Firing (..), Facts, Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, declared, deeper, emptyState, ended, enter, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, factual, memoized, morph, noted, remembering, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked, voided) where
+module Morph (Answer (..), Budget (..), Deadline (..), Firing (..), Facts, Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, declared, deeper, emptyState, ended, enter, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, factual, memoized, morph, noted, remembering, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked, vetted, voided) where
 
 import AST
 import Builder (buildExpressionThrows, nameIn)
@@ -21,10 +21,12 @@
 import Data.Bifunctor (first, second)
 import Data.IORef (IORef, atomicModifyIORef', modifyIORef', newIORef, readIORef, writeIORef)
 import Data.List (find, partition, sortOn)
+import qualified Data.List as List
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Map.Strict as Map
-import Data.Maybe (fromMaybe, isJust, listToMaybe)
+import Data.Maybe (fromMaybe, isJust, listToMaybe, maybeToList)
+import qualified Data.Set as Set
 import qualified Data.Text as T
 import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dispatched, dontSaveStep, sized)
 import Engine (Engine (..))
@@ -89,8 +91,12 @@
 
 type Store answer = Map.Map Int [(Expression, answer)]
 
-type Facts = IORef (Store Expression)
+data Facts = Facts (IORef (Store Expression)) (IORef Lodgings)
 
+data Lodging = Lodging [(Expression, Attribute)] [(Attribute, Expression)]
+
+data Lodgings = Lodgings !(Store Lodging) !(Map.Map Int [Expression])
+
 data ReduceContext = ReduceContext
   { _locator :: Expression
   , _site :: Expression
@@ -132,10 +138,10 @@
   | Cycles Int
   | Nodes Int
   | Memory Int
+  | Seconds Int
 
 data ReduceException
   = OutOfSteps Budget
-  | OutOfTime Int
   | Stuck T.Text
   | StuckAt T.Text (NonEmpty Rewritten) State
   | OutOfStepsAt Budget (NonEmpty Rewritten) State
@@ -144,6 +150,7 @@
   | LoopingAt Expression (NonEmpty Rewritten) State
   | Undataizable Expression (NonEmpty Rewritten) State
   | Unmorphable Expression
+  | Abnormal Judgment Expression
   deriving anyclass (Exception)
 
 instance Show ReduceException where
@@ -157,9 +164,9 @@
     printf "Evaluation did not finish before reaching the limit of nodes: --max-nodes=%d" limit
   show (OutOfSteps (Memory limit)) =
     printf "Evaluation did not finish before reaching the limit of memory: --max-memory=%s" (sized limit)
-  show (OutOfStepsAt budget _ _) = show (OutOfSteps budget)
-  show (OutOfTime limit) =
+  show (OutOfSteps (Seconds limit)) =
     printf "Evaluation did not finish before reaching the limit of seconds: --max-seconds=%d" limit
+  show (OutOfStepsAt budget _ _) = show (OutOfSteps budget)
   show (Stuck func) = printf "No entry of --symbolic answers the λ function '%s'" (T.unpack func)
   show (StuckAt func _ _) = show (Stuck func)
   show (Diverged func) = printf "The λ function '%s' could not join its two sides" (T.unpack func)
@@ -168,6 +175,8 @@
   show (Undataizable ExTermination _ _) = "dataization reached the terminator ⊥, which signals an error and cannot be dataized"
   show (Undataizable term _ _) = printf "no dataization rule matched, while dataization expects a normal form: %s" (printExpression term)
   show (Unmorphable term) = printf "Morphing expects a normal form, but no morphing rule matches: %s" (printExpression term)
+  show (Abnormal Morphing term) = printf "Morphing expects a normal form, but the term at the locator is not one: %s" (printExpression term)
+  show (Abnormal _ term) = printf "Dataization expects a normal form, but the term at the locator is not one: %s" (printExpression term)
 
 deeper :: ReduceContext -> IO ReduceContext
 deeper ctx@ReduceContext{_steps = Steps limit spent} = do
@@ -227,7 +236,7 @@
 expired :: ReduceContext -> Int -> IO a
 expired ctx cap = do
   ctx._saveEval (EvTimeout ctx._nesting cap ctx._judgment ctx._site)
-  throwIO (OutOfTime cap)
+  throwIO (OutOfSteps (Seconds cap))
 
 awaited :: ReduceContext -> IO a -> IO a
 awaited ctx action = case ctx._deadline of
@@ -326,7 +335,7 @@
 
 severed :: Maybe Attribute -> Expression -> ReduceContext -> State -> Expression -> [Binding] -> (Acyclic, Expression) -> IO Expression
 severed taken univ ctx state form bds (mode, before) = do
-  call <- (<|>) <$> traced ctx._facts form <*> traced ctx._facts before
+  call <- awaited ctx (evaluate =<< ((<|>) <$> traced ctx._facts form <*> traced ctx._facts before))
   forM_ call (recited ctx . snd)
   reckoned <- traverse (spelled taken . fst) call
   fresh <- coined ctx
@@ -343,34 +352,55 @@
 recited ctx = mapM_ (\(term, source) -> ctx._saveEval (EvRecalled ctx._nesting term source))
 
 factual :: IO Facts
-factual = newIORef Map.empty
+factual = Facts <$> newIORef Map.empty <*> newIORef (Lodgings Map.empty Map.empty)
 
 noted :: ReduceContext -> Expression -> Expression -> IO ()
-noted ctx object source = forM_ ctx._facts $ \facts -> do
+noted ctx object source = forM_ ctx._facts $ \(Facts facts lodgings) -> do
   known <- (Just source ==) . lookup object . Map.findWithDefault [] (hashExpression object) <$> readIORef facts
   unless known $ do
     modifyIORef' facts (Map.insertWith (++) (hashExpression object) [(object, source)])
+    modifyIORef' lodgings (\index -> fst (lodged Nothing index object))
     ctx._saveEval (EvRemembered ctx._nesting object source)
+  where
+    lodged :: Maybe (Expression, Attribute) -> Lodgings -> Expression -> (Lodgings, Expression)
+    lodged edge index@(Lodgings nodes shapes) term@(ExFormation bds) = case [node | (node, _) <- Map.findWithDefault [] (hashExpression term) nodes, node == term] of
+      node : _ -> (maybe index (\parent -> Lodgings (Map.adjust (map (adopted node parent)) (hashExpression node) nodes) shapes) edge, node)
+      [] -> case List.foldl' (lodging term) (index, []) [(attr, body) | BiTau attr body@(ExFormation _) <- bds, attr /= AtRho] of
+        (Lodgings inner shapes', kids) -> (Lodgings (Map.insertWith (++) (hashExpression term) [(term, Lodging (maybeToList edge) (reverse kids))] inner) (Map.insertWith (++) (shaped bds) [term] shapes'), term)
+    lodged _ index term = (index, term)
+    lodging :: Expression -> (Lodgings, [(Attribute, Expression)]) -> (Attribute, Expression) -> (Lodgings, [(Attribute, Expression)])
+    lodging parent (index, kids) (attr, body) = case lodged (Just (parent, attr)) index body of
+      (index', kid) -> index' `seq` (index', (attr, kid) : kids)
+    adopted :: Expression -> (Expression, Attribute) -> (Expression, Lodging) -> (Expression, Lodging)
+    adopted node parent (term, Lodging parents kids)
+      | term == node = (term, Lodging (parent : parents) kids)
+      | otherwise = (term, Lodging parents kids)
 
+shaped :: [Binding] -> Int
+shaped bds = hashExpression (ExFormation (rholess bds))
+
+rholess :: [Binding] -> [Binding]
+rholess = filter ((/= Just AtRho) . attributeFromBinding)
+
 remembering :: Maybe Facts -> Expression -> IO Bool
 remembering Nothing _ = pure False
-remembering (Just facts) term = isJust . lookup term . Map.findWithDefault [] (hashExpression term) <$> readIORef facts
+remembering (Just (Facts facts _)) term = isJust . lookup term . Map.findWithDefault [] (hashExpression term) <$> readIORef facts
 
 traced :: Maybe Facts -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))
 traced Nothing _ = pure Nothing
-traced (Just facts) form = do
+traced (Just (Facts facts lodgings)) form = do
   known <- readIORef facts
-  pure (go known (Map.size known) form)
+  index <- readIORef lodgings
+  pure (go index known [] form)
   where
-    go :: Store Expression -> Int -> Expression -> Maybe (Expression, [(Expression, Expression)])
-    go _ 0 _ = Nothing
-    go known budget term = listToMaybe [(named, (object, source) : hops) | (path, object, source) <- sortOn (\(path, _, _) -> length path) [(path, object, source) | (object, source) <- concat (Map.elems known), path <- take 1 (lodged term object)], let (base, hops) = resolved known budget source, Just named <- [rooted (foldl ExDispatch base path)]]
-    resolved :: Store Expression -> Int -> Expression -> (Expression, [(Expression, Expression)])
-    resolved known budget source = case lookup source (Map.findWithDefault [] (hashExpression source) known) of
-      Just _ -> fromMaybe (source, []) (go known (budget - 1) source)
+    go :: Lodgings -> Store Expression -> [Expression] -> Expression -> Maybe (Expression, [(Expression, Expression)])
+    go index known passed term = listToMaybe [(named, (object, source) : hops) | (path, object, source) <- lodged index known term, object `notElem` passed, let (base, hops) = resolved index known (object : passed) source, Just named <- [rooted (foldl ExDispatch base path)]]
+    resolved :: Lodgings -> Store Expression -> [Expression] -> Expression -> (Expression, [(Expression, Expression)])
+    resolved index known passed source = case lookup source (Map.findWithDefault [] (hashExpression source) known) of
+      Just _ -> fromMaybe (source, []) (go index known passed source)
       Nothing -> case source of
-        ExApplication target arg -> first (`ExApplication` arg) (resolved known budget target)
-        ExDispatch target attr -> first (`ExDispatch` attr) (resolved known budget target)
+        ExApplication target arg -> first (`ExApplication` arg) (resolved index known passed target)
+        ExDispatch target attr -> first (`ExDispatch` attr) (resolved index known passed target)
         _ -> (source, [])
     rooted :: Expression -> Maybe Expression
     rooted term = term <$ guard (grounded term)
@@ -379,18 +409,29 @@
     grounded (ExDispatch target _) = grounded target
     grounded (ExApplication target _) = grounded target
     grounded _ = False
-    lodged :: Expression -> Expression -> [[Attribute]]
-    lodged (ExFormation bds) whole = searched (filter (not . rho) bds) [([], whole)] Map.empty
-    lodged _ _ = []
-    searched :: [Binding] -> [([Attribute], Expression)] -> Store () -> [[Attribute]]
-    searched _ [] _ = []
-    searched own ((path, term@(ExFormation inner)) : rest) seen
-      | isJust (lookup term (Map.findWithDefault [] (hashExpression term) seen)) = searched own rest seen
-      | filter (not . rho) inner == own = reverse path : searched own rest seen
-      | otherwise = searched own (rest ++ [(attr : path, body) | BiTau attr body <- inner, attr /= AtRho]) (Map.insertWith (++) (hashExpression term) [(term, ())] seen)
-    searched own (_ : rest) seen = searched own rest seen
-    rho :: Binding -> Bool
-    rho bd = attributeFromBinding bd == Just AtRho
+    lodged :: Lodgings -> Store Expression -> Expression -> [([Attribute], Expression, Expression)]
+    lodged (Lodgings nodes shapes) known (ExFormation bds) = sortOn (\(path, _, _) -> length path) [(descended distances object, object, source) | digest <- Set.toAscList (Set.fromList (map hashExpression (concatMap (map fst) (Map.elems distances)))), (object, source) <- Map.findWithDefault [] digest known, isJust (lookup object (Map.findWithDefault [] digest distances))]
+      where
+        distances :: Store Int
+        distances = spread 0 matched (Map.fromListWith (++) [(hashExpression node, [(node, 0)]) | node <- matched])
+        matched :: [Expression]
+        matched = [node | node@(ExFormation inner) <- Map.findWithDefault [] (shaped bds) shapes, rholess inner == rholess bds]
+        spread :: Int -> [Expression] -> Store Int -> Store Int
+        spread _ [] reached = reached
+        spread depth frontier reached = uncurry (spread (succ depth)) (List.foldl' (climbed (succ depth)) ([], reached) [parent | node <- frontier, (parent, _) <- lodging node])
+        climbed :: Int -> ([Expression], Store Int) -> Expression -> ([Expression], Store Int)
+        climbed depth (next, reached) parent
+          | isJust (lookup parent (Map.findWithDefault [] (hashExpression parent) reached)) = (next, reached)
+          | otherwise = (parent : next, Map.insertWith (++) (hashExpression parent) [(parent, depth)] reached)
+        descended :: Store Int -> Expression -> [Attribute]
+        descended reached node = case lookup node (Map.findWithDefault [] (hashExpression node) reached) of
+          Just depth | depth > 0 -> concat (take 1 [attr : descended reached kid | (attr, kid) <- children node, lookup kid (Map.findWithDefault [] (hashExpression kid) reached) == Just (pred depth)])
+          _ -> []
+        lodging :: Expression -> [(Expression, Attribute)]
+        lodging node = maybe [] (\(Lodging parents _) -> parents) (lookup node (Map.findWithDefault [] (hashExpression node) nodes))
+        children :: Expression -> [(Attribute, Expression)]
+        children node = maybe [] (\(Lodging _ kids) -> kids) (lookup node (Map.findWithDefault [] (hashExpression node) nodes))
+    lodged _ _ _ = []
 
 coined :: ReduceContext -> IO Int
 coined ctx = atomicModifyIORef' ctx._minted (\count -> (succ count, succ count))
@@ -405,7 +446,7 @@
 
 voided :: ReduceContext -> Expression -> IO (Maybe [Attribute])
 voided ReduceContext{_facts = Nothing} _ = pure Nothing
-voided ctx@ReduceContext{_facts = Just facts} form@(ExFormation bds) = do
+voided ctx@ReduceContext{_facts = Just (Facts facts _)} form@(ExFormation bds) = do
   known <- readIORef facts
   case lookup form (Map.findWithDefault [] (hashExpression form) known) of
     Just source -> do
@@ -501,7 +542,12 @@
     hits = take (succ ctx._maxLoops) (filter (repeated mode) (Map.findWithDefault [] (digest mode form) ctx._entered))
     repeated :: Acyclic -> Expression -> Bool
     repeated Proven before = alike form before
-    repeated Plausible before = within before form
+    repeated Plausible before
+      | atomic form = alike form before
+      | otherwise = within before form
+    atomic :: Expression -> Bool
+    atomic (ExFormation bds) = any isLambda bds
+    atomic _ = False
 
 digest :: Acyclic -> Expression -> Int
 digest Proven = hashShape
@@ -565,6 +611,7 @@
 morph :: Expression -> State -> ReduceContext -> IO (Expression, [Rewritten], State)
 morph universe state caller@ReduceContext{..} = do
   expr <- locatedExpression _locator universe
+  vetted Morphing expr caller
   prepared <- try (universed universe caller)
   case prepared of
     Left (OutOfSteps _) | _partial -> pure (expr, [(universe, Nothing)], state)
@@ -578,6 +625,7 @@
         Right ((morphed, seq), state') -> pure (morphed, reverse (NE.toList seq), state')
         Left (StuckAt func seq parked) | _partial -> residue seq parked{_stuck = Just func}
         Left (OutOfStepsAt _ seq parked) | _partial -> residue seq parked
+        Left (OutOfSteps _) | _partial -> pure (expr, [(universe, Nothing)], state)
         Left (LoopingAt _ seq parked) -> residue seq parked
         Left failure -> throwIO (failure :: ReduceException)
     residue :: NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)
@@ -585,6 +633,9 @@
       expr <- locatedExpression _locator (fst (NE.head seq))
       pure (expr, reverse (NE.toList seq), parked)
 
+vetted :: Judgment -> Expression -> ReduceContext -> IO ()
+vetted judgment expr ctx = unless (ctx._engine._normal expr) (throwIO (Abnormal judgment expr))
+
 inferred :: Expression -> Expression -> State -> ReduceContext -> [In.Inference value] -> IO (Maybe (In.Conclusion value, State))
 inferred expr univ state ctx rules = do
   ordered <- if ctx._shuffle then shuffle rules else pure rules
@@ -628,7 +679,8 @@
   whole <- withLocatedExpression _locator expr (fst (NE.head seq))
   taken <- newIORef Map.empty
   peeled <- newIORef Map.empty
-  (rewrittens, exceeded) <- rewrite whole _engine._normalization (rewriteContext taken peeled ctx)
+  copies <- newIORef Map.empty
+  (rewrittens, exceeded) <- rewrite whole _engine._normalization (rewriteContext taken peeled copies ctx)
   when exceeded $ do
     _saveEval (EvExceeded _nesting _maxCycles _judgment _site)
     throwIO (OutOfSteps (Cycles _maxCycles))
@@ -637,24 +689,29 @@
   expr' <- locatedExpression _locator (fst rw)
   pure (expr', seq')
   where
-    rewriteContext :: IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> RewriteContext
-    rewriteContext taken peeled whole@ReduceContext{..} =
-      RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing (\term -> (measured whole =<< locatedExpression _locator term) >> _saveStep term) (made taken peeled whole)
-    made :: IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> Expression -> Expression -> IO ()
-    made _ _ whole redex@(ExApplication head' (ArTau attr _)) object@(ExFormation bds)
+    rewriteContext :: IORef (Store Expression) -> IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> RewriteContext
+    rewriteContext taken peeled copies whole@ReduceContext{..} =
+      RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing (\term -> (measured whole =<< locatedExpression _locator term) >> _saveStep term) (made taken peeled copies whole)
+    made :: IORef (Store Expression) -> IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> Expression -> Expression -> IO ()
+    made _ _ copies whole redex@(ExApplication head' (ArTau attr _)) object@(ExFormation bds)
       | attr /= AtRho && object /= head' = do
-          whole._saveEval (EvApplied whole._nesting whole._judgment (called whole._universe redex) object whole._site)
-          known <- remembering whole._facts head'
-          when (known && copied bds) (noted whole object redex)
-    made taken _ whole redex@(ExApplication _ (ArTau AtRho _)) object@(ExFormation bds)
+          made' <- readIORef copies
+          if lookup redex (Map.findWithDefault [] (hashExpression redex) made') == Just object
+            then whole._saveEval (EvRecalled whole._nesting (called whole._universe redex) object)
+            else do
+              modifyIORef' copies (Map.insertWith (++) (hashExpression redex) [(redex, object)])
+              whole._saveEval (EvApplied whole._nesting whole._judgment (called whole._universe redex) object whole._site)
+              known <- remembering whole._facts head'
+              when (known && copied bds) (noted whole object redex)
+    made taken _ _ whole redex@(ExApplication _ (ArTau AtRho _)) object@(ExFormation bds)
       | copied bds = do
           pending <- readIORef taken
           forM_ (lookup redex (Map.findWithDefault [] (hashExpression redex) pending)) (noted whole object)
-    made taken peeled whole redex@(ExDispatch target attr) object
+    made taken peeled _ whole redex@(ExDispatch target attr) object
       | attr /= AtRho = do
           stripped peeled whole target attr
           dispatched taken peeled whole redex object
-    made _ _ _ _ _ = pure ()
+    made _ _ _ _ _ _ = pure ()
     stripped :: IORef (Store Expression) -> ReduceContext -> Expression -> Attribute -> IO ()
     stripped peeled whole target@(ExFormation bds) attr = do
       known <- remembering whole._facts target
diff --git a/src/Regexp.hs b/src/Regexp.hs
--- a/src/Regexp.hs
+++ b/src/Regexp.hs
@@ -68,8 +68,10 @@
                     Just idx -> fromMaybe (B.pack ('$' : digits)) (safeIndex idx groups)
                in val : go afterDigits
     go ('\\' : '\\' : rest) = B.singleton '\\' : go rest
+    go ('\\' : '&' : rest) = B.singleton '&' : go rest
     go ('\\' : digit : rest)
       | isDigit digit = fromMaybe (B.pack ['\\', digit]) (safeIndex (toInteger (digitToInt digit)) groups) : go rest
+    go ('&' : rest) = fromMaybe (B.singleton '&') (safeIndex 0 groups) : go rest
     go (c : rest) = B.singleton c : go rest
     safeIndex :: Integer -> [B.ByteString] -> Maybe B.ByteString
     safeIndex i xs
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -322,6 +322,10 @@
     where
       macro :: String -> Text
       macro "evaluate" = "\\phinoEvaluate"
+      macro "number" = "\\phinoNumber"
+      macro "string" = "\\phinoString"
+      macro "sum" = "\\phinoSum"
+      macro "tau" = "\\phinoTau"
       macro name = "\\" <> T.concat (zipWith camel [0 :: Int ..] (T.splitOn "-" (T.pack name)))
       camel :: Int -> Text -> Text
       camel 0 part = part
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -183,8 +183,14 @@
   pure (object [("name", name), ("base", base)] children)
 
 nestedBindings :: [Binding] -> XmirContext -> IO [Node]
-nestedBindings bds ctx@XmirContext{..} = catMaybes <$> mapM (`formationBinding` ctx) bds'
+nestedBindings bds ctx@XmirContext{..} = catMaybes <$> mapM (\bd -> fmap (typed bd) <$> formationBinding bd ctx) bds'
   where
+    typed :: Binding -> Node -> Node
+    typed (BiVoid (AtLabel label)) (NodeElement (Element name attrs kids)) =
+      NodeElement (Element name (M.union attrs (M.fromList [(toName key, T.pack value) | fn <- lambda, key <- ["type", "args"], Just value <- [M.lookup (voidKey fn label key) _atoms]])) kids)
+    typed _ node = node
+    lambda :: [T.Text]
+    lambda = [fn | BiLambda (Function fn) <- bds]
     bds' :: [Binding]
     bds' = if _hideRho then filter (not . isRho) bds else bds
     isRho :: Binding -> Bool
@@ -309,8 +315,14 @@
 
 renameAtoms :: [(T.Text, T.Text)] -> XmirContext -> XmirContext
 renameAtoms renames ctx@XmirContext{..} =
-  ctx{_atoms = M.fromList [(new, atom) | (old, new) <- renames, Just atom <- [M.lookup old _atoms]]}
+  ctx{_atoms = M.fromList [(new <> rest, atom) | (old, new) <- renames, (key, atom) <- M.toList _atoms, Just rest <- [owned old key]]}
+  where
+    owned :: T.Text -> T.Text -> Maybe T.Text
+    owned old key = T.stripPrefix old key >>= \rest -> if T.null rest || T.isPrefixOf "." rest then Just rest else Nothing
 
+voidKey :: T.Text -> T.Text -> String -> T.Text
+voidKey fn label key = fn <> "." <> label <> "@" <> T.pack key
+
 escapeXML :: String -> String
 escapeXML = concatMap escapeChar
   where
@@ -539,21 +551,28 @@
   ]
 
 xmirAtoms :: Document -> IO Atoms
-xmirAtoms xmir = M.fromList <$> mapM entry markers
+xmirAtoms xmir = M.fromList . concat <$> mapM entries markers
   where
     markers :: [C.Cursor]
     markers =
       C.fromDocument xmir
         C.$// C.element (toName "o")
         C.>=> C.attributeIs (toName "name") "λ"
-        C.>=> C.check (hasAttr "atom")
     derived :: Derived
     derived = derivedNames xmir
-    entry :: C.Cursor -> IO (T.Text, String)
-    entry cur = do
+    entries :: C.Cursor -> IO [(T.Text, String)]
+    entries cur = do
       name <- lambdaName derived cur (lambdaPath cur)
-      atom <- getAttr "atom" cur
-      pure (name, atom)
+      atom <- if hasAttr "atom" cur then (\value -> [(name, value)]) <$> getAttr "atom" cur else pure []
+      pure
+        ( atom
+            ++ [ (voidKey name label key, T.unpack value)
+               | void <- (C.parent C.>=> C.child C.>=> C.element (toName "o") C.>=> C.attributeIs (toName "base") "∅") cur
+               , label <- C.attribute (toName "name") void
+               , key <- ["type", "args"]
+               , value <- C.attribute (toName key) void
+               ]
+        )
 
 xmirToFormation :: Derived -> C.Cursor -> [String] -> IO Expression
 xmirToFormation derived cur fqn = do
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -19,6 +19,7 @@
 import qualified Data.Aeson.KeyMap as KeyMap
 import Data.Aeson.Types (formatRelativePath)
 import qualified Data.ByteString as BS
+import qualified Data.ByteString.Char8 as BC
 import Data.Conduit ((.|))
 import qualified Data.Conduit.List as CL
 import Data.FileEmbed (embedDir)
@@ -543,6 +544,8 @@
     worded :: Libyaml.Event -> Libyaml.Event
     worded (Libyaml.EventScalar value Libyaml.NoTag style anchor)
       | value `elem` spelled = Libyaml.EventScalar value Libyaml.StrTag style anchor
+    worded (Libyaml.EventScalar value (Libyaml.UriTag tag@('!' : _)) style anchor)
+      | BS.null value = Libyaml.EventScalar (BC.pack tag) Libyaml.StrTag style anchor
     worded event = event
     spelled :: [BS.ByteString]
     spelled = ["y", "Y", "yes", "Yes", "YES", "n", "N", "no", "No", "NO", "on", "On", "ON", "off", "Off", "OFF"]
diff --git a/test-resources/evaluate-packs/copies-a-call-written-twice-once.yaml b/test-resources/evaluate-packs/copies-a-call-written-twice-once.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/copies-a-call-written-twice-once.yaml
@@ -0,0 +1,17 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# The call '⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ )' stands twice in 'c', once in 'a'
+# and once in 'b'. Normalization of the world copies it once and recalls that
+# copy for the second place, instead of copying the same call again (#2343).
+symbolic: '[]'
+location: 'Q.y'
+input: '⟦ c ↦ ⟦ a ↦ ⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ ), b ↦ ⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ ) ⟧, y ↦ Φ.c.b ⟧'
+result: '⟦ x ↦ 𝜎1:λ, φ ↦ x ⟧'
+protocol: |
+  𝕄(Φ.y):
+    𝑛·0·1 := ⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ )
+    𝑛·0·2 := ⟦ x ↦ 𝜎1:λ, φ ↦ x ⟧
+    recalled 𝑛·0·1 ⇒ 𝑛·0·2
+    morphed 𝑛·0·3 := 𝑛·0·2
diff --git a/test-resources/evaluate-packs/joins-two-sides-a-stay-brought-to-one-shape.yaml b/test-resources/evaluate-packs/joins-two-sides-a-stay-brought-to-one-shape.yaml
--- a/test-resources/evaluate-packs/joins-two-sides-a-stay-brought-to-one-shape.yaml
+++ b/test-resources/evaluate-packs/joins-two-sides-a-stay-brought-to-one-shape.yaml
@@ -29,10 +29,11 @@
       right: 𝑛4
 location: 'Q.y'
 hide-rho: false
-input: '⟦ number ↦ ⟦ φ ↦ ∅ ⟧, bytes ↦ ⟦ φ ↦ ∅ ⟧, y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎3 ⟧, a ↦ ⟦ φ ↦ Φ.number( φ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), x ↦ ∅ ⟧.ρ ) ⟧, b ↦ ⟦ φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) ) ⟧, λ ⤍ L_fork ⟧.φ ⟧'
+input: '⟦ number ↦ ⟦ φ ↦ ∅ ⟧, bytes ↦ ⟦ φ ↦ ∅ ⟧, f ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎3 ⟧, a ↦ ⟦ φ ↦ Φ.number( φ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), x ↦ ∅ ⟧.ρ ) ⟧, b ↦ ⟦ φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) ) ⟧, λ ⤍ L_fork ⟧, y ↦ Φ.f.φ ⟧'
 result: 'Φ.bytes( φ ↦ 𝜎4:λ ):φ'
 protocol: |
   𝕄(Φ.y):
+    remembered 𝑛·0·1 ≡ Φ.f  # ⟦ c ↦ 𝜎3:λ, a ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ, ρ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ 𝜎1:λ ), x ↦ ∅ ⟧ ) ):φ, b ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ):φ, λ ⤍ L_fork ⟧
     𝔼(L_fork):
       𝔻(ξ.c):
         𝛿·1·1 := 𝔻(𝜎3:λ)
@@ -46,6 +47,7 @@
       𝑛3·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ):φ  # stay(𝑛1)
       joined 𝜎4 := 𝛿1·1 ? 𝜎1 : 𝜎2
       𝑛·1·3 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) ):φ
-    𝑛·0·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) )
-    𝑛·0·2 := Φ.bytes( φ ↦ 𝜎4:λ ):φ
-    morphed 𝑛·0·3 := 𝑛·0·2
+      remembered 𝑛·1·3 ≡ 𝑛·0·1
+    𝑛·0·2 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) )
+    𝑛·0·3 := Φ.bytes( φ ↦ 𝜎4:λ ):φ
+    morphed 𝑛·0·4 := 𝑛·0·3
diff --git a/test-resources/evaluate-packs/refuses-a-meta-bound-to-a-term-that-is-not-a-normal-form.yaml b/test-resources/evaluate-packs/refuses-a-meta-bound-to-a-term-that-is-not-a-normal-form.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/refuses-a-meta-bound-to-a-term-that-is-not-a-normal-form.yaml
@@ -0,0 +1,30 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# A meta 𝑛 of an entry may hold only a normal form (#2343). The 'rewrite'
+# line normalizes nothing, and its rule wraps the term into a dispatch off a
+# formation, which 'dot' of normalization would still take, so the firing
+# refuses to bind '𝑛2' to it.
+symbolic: |
+  - λ: L_wrap
+    morph:
+      𝑛1: $.x
+    rewrite:
+      𝑛2:
+        of: 𝑛1
+        rules:
+          - name: wrap
+            pattern: ⟦ 𝐵1 ⟧
+            result: ⟦ k ↦ ⟦ 𝐵1 ⟧ ⟧.k
+    𝑛: 𝑛2
+location: 'Q.y'
+input: '⟦ y ↦ ⟦ x ↦ ⟦ Δ ⤍ 01- ⟧, λ ⤍ L_wrap ⟧.φ ⟧'
+fails: "The meta '𝑛2' of λ function 'L_wrap' may hold only a normal form"
+protocol: |
+  𝕄(Φ.y):
+    𝔼(L_wrap):
+      𝕄(ξ.x):
+        morphed 𝑛·1·1 := 01-:Δ
+      𝑛1·1 := 01-:Δ  # 𝕄(ξ.x)
+      𝑛2·1 := 01-:Δ:k.k  # rewrite(𝑛1)
diff --git a/test-resources/morph-packs/answers-bottom-on-rho-of-a-formation-without-rho.yaml b/test-resources/morph-packs/answers-bottom-on-rho-of-a-formation-without-rho.yaml
--- a/test-resources/morph-packs/answers-bottom-on-rho-of-a-formation-without-rho.yaml
+++ b/test-resources/morph-packs/answers-bottom-on-rho-of-a-formation-without-rho.yaml
@@ -2,7 +2,9 @@
 # SPDX-License-Identifier: MIT
 ---
 # A formation that declares no ρ has no receiver, so asking it for one is
-# dead and does not go through its φ (#1859).
+# dead and does not go through its φ (#1859). The dispatch stands in the
+# world, since 'morph' refuses a term at the locator that is not a normal
+# form (#2343).
 location: 'Q.x'
-input: '[[ x -> [[ @ -> $.y, y -> [[ ]] ]].^ ]]'
+input: '[[ k -> [[ @ -> $.y, y -> [[ ]] ]].^, x -> Q.k ]]'
 result: '⊥'
diff --git a/test-resources/morph-packs/fails-on-an-input-that-is-not-a-normal-form.yaml b/test-resources/morph-packs/fails-on-an-input-that-is-not-a-normal-form.yaml
--- a/test-resources/morph-packs/fails-on-an-input-that-is-not-a-normal-form.yaml
+++ b/test-resources/morph-packs/fails-on-an-input-that-is-not-a-normal-form.yaml
@@ -3,10 +3,10 @@
 ---
 # 𝕄 maps normal forms to formations, and 'morph' does not normalize what it is
 # handed. A dispatch off a formation with neither φ nor λ is not a normal form,
-# since 'dot' of normalization eats it, and no morphing rule takes it, so the
-# run tells the user so instead of failing with a bare "user error" (#1442).
+# since 'dot' of normalization eats it, so the run refuses it as broken input
+# instead of failing with a bare "user error" (#1442, #2343).
 location: 'Q.t'
 input: '⟦ t ↦ ⟦ x ↦ ⟦⟧ ⟧.x ⟧'
 fails: >-
-  Morphing expects a normal form, but no morphing rule matches:
+  Morphing expects a normal form, but the term at the locator is not one:
   ⟦⟧:x.x
diff --git a/test/AbridgeSpec.hs b/test/AbridgeSpec.hs
--- a/test/AbridgeSpec.hs
+++ b/test/AbridgeSpec.hs
@@ -70,6 +70,34 @@
         )
         (SWEET, UNICODE, SINGLELINE, defaultMargin)
         `shouldBe` "⟦ λ ⤍ L_weit, φ ↦ ∅, +5 ⟧"
+    it "leaves an application no longer than the width as it is" $
+      printExpressionWith
+        (const (abridged True 64))
+        (ExApplication (ExApplication (ExDispatch ExRoot (AtLabel "brücke")) (ArTau (AtLabel "links") ExXi)) (ArTau (AtLabel "rechts") ExRoot))
+        (SWEET, UNICODE, SINGLELINE, defaultMargin)
+        `shouldBe` "Φ.brücke( links ↦ ξ, rechts ↦ Φ )"
+    it "folds the arguments of an application wider than the width into a count" $
+      printExpressionWith
+        (const (abridged True 64))
+        (foldl (\expr idx -> ExApplication expr (ArTau (AtLabel (T.pack ("strasse-" <> show idx))) ExRoot)) (ExDispatch ExRoot (AtLabel "stadt")) [1 .. 7 :: Int])
+        (SWEET, UNICODE, SINGLELINE, defaultMargin)
+        `shouldBe` "Φ.stadt( +7 )"
+    it "folds a long application in the φ of a long formation" $
+      printExpressionWith
+        (const (abridged True 64))
+        ( ExFormation
+            [ BiTau (AtLabel "wolke") ExRoot
+            , BiTau AtPhi (foldl (\expr idx -> ExApplication expr (ArTau (AtLabel (T.pack ("regen-" <> show idx))) ExXi)) (ExDispatch ExXi (AtLabel "himmel")) [1 .. 8 :: Int])
+            ]
+        )
+        (SWEET, UNICODE, SINGLELINE, defaultMargin)
+        `shouldBe` "⟦ φ ↦ himmel( +8 ), +1 ⟧"
+    it "folds a long application its dispatch is made of" $
+      printExpressionWith
+        (const (abridged True 64))
+        (ExDispatch (foldl (\expr idx -> ExApplication expr (ArAlpha (Alpha idx) (ExDispatch ExRoot (AtLabel "langer-name")))) (ExDispatch ExRoot (AtLabel "fluss")) [0 .. 5 :: Int]) (AtLabel "ufer"))
+        (SWEET, UNICODE, SINGLELINE, defaultMargin)
+        `shouldBe` "Φ.fluss( +6 ).ufer"
     it "cuts a long byte string to its first bytes, its last bytes and the count of the bytes between them" $
       printExpressionWith
         (const (abridged True 64))
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -1433,7 +1433,7 @@
 
   it "names the term dataization cannot take, and says a normal form is expected" $
     withStdin "⟦ x ↦ ⟦ b ↦ ⟦ Δ ⤍ 01- ⟧ ⟧.b ⟧" $
-      testCLIFailed ["dataize", "--locator=Q.x"] ["expects a normal form: 01-:Δ:b.b"]
+      testCLIFailed ["dataize", "--locator=Q.x"] ["Dataization expects a normal form, but the term at the locator is not one: 01-:Δ:b.b"]
 
   describe "--partial parks a universe that --max-cycles stops" $ do
     let heavy = "⟦ simple ↦ ⟦ Δ ⤍ 01- ⟧, heavy ↦ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 02- ⟧ ⟧ ⟧ ⟧.a.b.c ⟧"
@@ -1673,7 +1673,7 @@
         recorded "2" "protocolXXXXXX.txt" >>= (`shouldContain` ["          looped 𝜎3 := Φ.down( i ↦ 𝑛·6·6 )  # plausible, repeats 𝑛·0·4"])
 
     describe "--acyclic at a copy holding a λ" $ do
-      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, down(i) ↦ ⟦ φ ↦ Φ.dataized( Φ.fork( Φ.dataized( Φ.down( ⟦ λ ⤍ 𝜎2 ⟧ ) ), ⟦ λ ⤍ 𝜎3 ⟧ ) ) ⟧, x ↦ Φ.down( ⟦ λ ⤍ 𝜎1 ⟧ ) ⟧"
+      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, x ↦ Φ.dataized( Φ.fork( Φ.dataized( Φ.x ), ⟦ λ ⤍ 𝜎3 ⟧ ) ) ⟧"
           forking = T.pack "- λ: L_fork\n  dataize:\n    𝛿1: $.on🌵\n  morph:\n    𝑛1: $.left🌵\n    𝑛2: $.right🌵\n  evaluate:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  join:\n    on: 𝛿1\n    left: 𝑛3\n    right: 𝑛4\n    otherwise: L_fork\n- λ: L_dataized\n  dataize:\n    𝛿1: $.target\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"
           recorded :: String -> IO [String]
           recorded name =
@@ -1691,7 +1691,7 @@
             testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]
 
       it "writes the copy holding a λ it cuts to the protocol as a call of the object" $
-        recorded "protocolXXXXXX.txt" >>= (`shouldContain` ["                      looped 𝜎8 := Φ.dataized( target ↦ 𝜎7:λ )  # 𝔻(𝑛·6·4), plausible, repeats 𝑛·7·2"])
+        recorded "protocolXXXXXX.txt" >>= (`shouldContain` ["                                looped 𝜎6 := Φ.dataized( target ↦ 𝜎5:λ )  # plausible, repeats 𝑛·9·2"])
 
     describe "--acyclic at a copy holding a λ that evaluate fires" $ do
       let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ ⟦ φ ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x ) ) ) ⟧ ⟧"
@@ -1702,7 +1702,7 @@
             testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]
 
     describe "--acyclic at a copy whose call ends with an attribute" $ do
-      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ), Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x ) ) ) ) ⟧"
+      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ), Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x.φ ) ) ) ) ⟧"
           forking = T.pack "- λ: L_fork\n  dataize:\n    𝛿1: $.on🌵\n  morph:\n    𝑛1: $.left🌵\n    𝑛2: $.right🌵\n  evaluate:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  join:\n    on: 𝛿1\n    left: 𝑛3\n    right: 𝑛4\n    otherwise: L_fork\n- λ: L_dataized\n  dataize:\n    𝛿1: $.target\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"
           recorded :: String -> IO [String]
           recorded name =
@@ -1715,10 +1715,10 @@
                     []
               lines <$> readProtocol path
       it "writes the copy it cuts to the protocol as a call of the object with the attribute it ends with" $
-        recorded "protocolXXXXXX.txt" >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎6 := Φ.fork( left ↦ 𝑛·9·9, right ↦ 𝑛·11·1 ).φ  # 𝔻(𝑛·9·6)"))
+        recorded "protocolXXXXXX.txt" >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎6 := Φ.fork( left ↦ 𝑛·13·8, right ↦ 𝑛·15·1 ).right🌵.φ  # plausible"))
 
       it "writes the copy it cuts to the XML protocol with the object, the metas of its arguments and the attribute it ends with" $
-        recorded "protocolXXXXXX.xml" >>= (`shouldSatisfy` any (isInfixOf "object=\"Φ.fork\" dispatch=\"φ\"><with><meta attr=\"left\">𝑛·9·9</meta><meta attr=\"right\">𝑛·11·1</meta></with></looped>"))
+        recorded "protocolXXXXXX.xml" >>= (`shouldSatisfy` any (isInfixOf "object=\"Φ.fork\" dispatch=\"right🌵.φ\"><with><meta attr=\"left\">𝑛·13·8</meta><meta attr=\"right\">𝑛·15·1</meta></with></looped>"))
 
     describe "--acyclic at a copy whose argument repeats the same loop" $ do
       let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, times(b) ↦ ⟦ λ ⤍ L_times ⟧, x ↦ Φ.times( Φ.dataized( Φ.x ) ) ⟧"
@@ -1814,29 +1814,41 @@
                     ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"]
                     []
               lines <$> readProtocol path
-      it "writes the loop it cuts inside the nested fork by its symbol alone, since no fact names it" $
-        recorded >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎7  # 𝔻(𝑛·9·10), plausible"))
+      it "writes the loop it cuts inside the nested fork as a call of the object" $
+        recorded >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎7 := Φ.p  # plausible"))
 
       it "dont get stuck above the nested fork it cuts" $
         recorded >>= (`shouldNotSatisfy` any (isInfixOf "stuck L_dataized"))
 
+    describe "--acyclic at copies of one atom called from different places" $
+      it "dont cut a copy of an atom that only resembles the copies open above it" $
+        withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
+          hClose stream
+          withLambdasOf (T.pack "- λ: L_d\n  dataize:\n    𝛿1: $.t\n  𝑛: Φ.w( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )\n") $ \file ->
+            withStdin "⟦ w ↦ ⟦ φ ↦ ∅, me ↦ ξ, you ↦ ξ, x ↦ Φ.d( t ↦ ξ ).me.you ⟧, d(t) ↦ ⟦ λ ⤍ L_d ⟧, e ↦ Φ.d( t ↦ Φ.d( t ↦ Φ.d( t ↦ ⟦ φ ↦ Φ.d( t ↦ ⟦ Δ ⤍ 01- ⟧ ).x ⟧ ) ) ) ⟧" $
+              testCLISucceeded
+                ["dataize", "--symbolic=" ++ file, "--locator=Q.e", "--acyclic=plausible", "--max-loops=2", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"]
+                []
+          records <- readProtocol path
+          lines records `shouldNotSatisfy` any (isInfixOf "looped")
+
     it "dataizes with --sequence" $
-      withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $
+      withStdin "[[ @ -> $.f(y -> [[ ]]), f -> [[ D> 00-, y -> ? ]] ]]" $
         testCLISucceeded
           ["dataize", "--sequence", "--output=latex", "--flat", "--sweet"]
           [ intercalate
               "\n"
               [ "\\begin{phiquation}"
-              , "[[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ \\phiDataize[\\nameref{r:box}]"
-              , "  \\phiDataize [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ . @ \\phiNormalize[\\nameref{r:copy}]"
-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] : |x| . |x| : @ . @ \\phiNormalize[\\nameref{r:dot}]"
-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ D> |01-|, |y| -> [[]] ]] : |x| ) : @ . @ \\phiNormalize[\\nameref{r:skip}]"
-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] : @ . @ \\phiNormalize[\\nameref{r:dot}]"
-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:skip}]"
-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] \\phiDataize[\\nameref{r:delta}]"
-              , "  \\phiDataize |01-|{.}"
+              , "[[ @ -> |f| ( |y| -> [[]] ), |f|(|y|) -> |00-| : D ]] \\phiDataize[\\nameref{r:box}]"
+              , "  \\phiDataize [[ @ -> |f| ( |y| -> [[]] ), |f|(|y|) -> |00-| : D ]] . @ \\phiNormalize[\\nameref{r:dot}]"
+              , "  \\phiNormalize [[ |f|(|y|) -> |00-| : D ]] . |f| ( |y| -> [[]], \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:dot}]"
+              , "  \\phiNormalize [[ D> |00-|, |y| -> ? ]] ( \\phiTerminal{\\rho} -> [[ |f|(|y|) -> |00-| : D ]], |y| -> [[]], \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:skip}]"
+              , "  \\phiNormalize [[ D> |00-|, |y| -> ? ]] ( |y| -> [[]], \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:copy}]"
+              , "  \\phiNormalize [[ D> |00-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:skip}]"
+              , "  \\phiNormalize [[ D> |00-|, |y| -> [[]] ]] \\phiDataize[\\nameref{r:delta}]"
+              , "  \\phiDataize |00-|{.}"
               , "\\end{phiquation}"
-              , "01-"
+              , "00-"
               ]
           ]
 
@@ -3545,7 +3557,7 @@
         testCLISucceeded ["dataize", "--max-cycles=1"] ["01-"]
 
     it "reports --max-cycles exceeded when a rule still applies at the limit" $
-      withStdin "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]" $
+      withStdin "[[ @ -> $.f(y -> [[ ]]), f -> [[ D> 00-, y -> ? ]] ]]" $
         testCLIFailed
           ["dataize", "--max-cycles=1"]
           ["[ERROR]: Normalization did not finish before reaching the limit of cycles: --max-cycles=1"]
@@ -3769,7 +3781,7 @@
             ["Φ.m( 𝜎1:λ )"]
 
       it "passes a small run in a large program under --max-nodes" $
-        withStdin ("⟦ x ↦ ⟦ φ ↦ ⟦ y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧.y ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $
+        withStdin ("⟦ x ↦ ⟦ φ ↦ ξ.y, y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $
           testCLISucceeded ["dataize", "--max-nodes=50", "--locator=Q.x"] ["05-"]
 
     describe "--max-memory" $ do
@@ -3795,7 +3807,7 @@
             ["Φ.m( 𝜎1:λ )"]
 
       it "passes a small run in a large program under --max-memory" $
-        withStdin ("⟦ x ↦ ⟦ φ ↦ ⟦ y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧.y ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $
+        withStdin ("⟦ x ↦ ⟦ φ ↦ ξ.y, y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $
           testCLISucceeded ["dataize", "--max-memory=1G", "--locator=Q.x"] ["05-"]
 
     describe "--max-seconds" $ do
@@ -3829,24 +3841,32 @@
                 ["dataize", "--symbolic=" ++ table, "--locator=Q.x", "--max-seconds=1"]
                 ["[ERROR]: Evaluation did not finish before reaching the limit of seconds: --max-seconds=1"]
 
-      it "fails once the --max-seconds budget is spent with --partial" $
+      it "prints the residue once the --max-seconds budget is spent with --partial" $
         ladder $ \table ->
           bounded $
             withStdin rungs $
-              testCLIFailed
-                ["morph", "--symbolic=" ++ table, "--max-seconds=1", "--locator=Q.x", "--partial"]
-                ["[ERROR]: Evaluation did not finish before reaching the limit of seconds: --max-seconds=1"]
+              testCLISucceeded
+                ["morph", "--symbolic=" ++ table, "--max-seconds=1", "--locator=Q.x", "--partial", "--flat", "--hide-rho", "--sweet"]
+                ["⟦ λ ⤍ L_split, n ↦ Φ.l1 ⟧.foo"]
 
-      forM_ [["--locator=Q.x"], ["--locator=Q.x", "--partial"]] $ \opts ->
+      it "prints the residue of a dataization once the --max-seconds budget is spent with --partial" $
+        ladder $ \table ->
+          bounded $
+            withStdin rungs $
+              testCLISucceeded
+                ["dataize", "--symbolic=" ++ table, "--max-seconds=1", "--locator=Q.x", "--partial", "--flat", "--hide-rho", "--sweet"]
+                ["⟦ λ ⤍ L_split, n ↦ Φ.l1 ⟧.foo"]
+
+      forM_ [(testCLIFailed, ["--max-seconds=1"], ["--locator=Q.x"]), (testCLISucceeded, [], ["--locator=Q.x", "--partial"])] $ \(run, outputs, opts) ->
         it ("writes the timeout as the last line of the protocol with " ++ unwords opts) $
           ladder $ \table ->
             withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
               hClose stream
               bounded $
                 withStdin rungs $
-                  testCLIFailed
+                  run
                     (["morph", "--symbolic=" ++ table, "--max-seconds=1", "--minutes=" ++ path, "--quiet"] ++ opts)
-                    ["--max-seconds=1"]
+                    outputs
               records <- readProtocol path
               dropWhile (== ' ') (last (lines records)) `shouldBe` "timeout 1"
 
@@ -3856,9 +3876,9 @@
             hClose stream
             bounded $
               withStdin rungs $
-                testCLIFailed
+                testCLISucceeded
                   ["morph", "--symbolic=" ++ table, "--locator=Q.x", "--partial", "--max-seconds=1", "--protocol=" ++ path, "--quiet"]
-                  ["--max-seconds=1"]
+                  []
             records <- readProtocol path
             length (filter (isInfixOf "<timeout limit=\"1\" by=\"morph\" at=\"") (lines records)) `shouldBe` 1
 
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -188,12 +188,12 @@
           Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts)
 
   describe "stops a dataization by the clock of --max-seconds" $
-    it "fails a partial dataization once the deadline has passed" $ do
+    it "leaves a partial dataization as a residual once the deadline has passed" $ do
       expr <- parseExpressionThrows "[[ @ -> [[ D> 7E- ]] ]]"
       deadline <- overdue 29
       ctx <- defaultReduceContext ExRoot
-      dataize expr emptyState ctx{_deadline = Just deadline, _partial = True}
-        `shouldThrow` (\e -> "--max-seconds=29" `isInfixOf` show (e :: SomeException))
+      (outcome, _, _) <- dataize expr emptyState ctx{_deadline = Just deadline, _partial = True}
+      outcome `shouldBe` Residual expr
 
   describe "partially evaluates around a λ function that cannot fire (--partial)" $ do
     let placeholder = ExFormation [BiLambda (Function "Sym_arg_0")]
@@ -313,7 +313,7 @@
       ]
       ( \(flag, reducing, message) ->
           it ("throws once " ++ flag ++ " is exhausted with --depth-sensitive") $ do
-            expr <- parseExpressionThrows "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]"
+            expr <- parseExpressionThrows "[[ @ -> $.f(y -> [[ ]]), f -> [[ D> 00-, y -> ? ]] ]]"
             ctx <- reducing <$> newIORef 0
             dataize expr emptyState ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))
       )
diff --git a/test/EvaluateSpec.hs b/test/EvaluateSpec.hs
--- a/test/EvaluateSpec.hs
+++ b/test/EvaluateSpec.hs
@@ -113,7 +113,13 @@
       (_, Just recall)
         | paired " ⇒ " recall `elem` facts -> orphans rest facts
         | otherwise -> line : orphans rest facts
-      _ -> orphans rest facts
+      _ -> orphans rest (applied line rest ++ facts)
+    applied :: String -> [String] -> [(String, String)]
+    applied line (next : _)
+      | " := " `T.isInfixOf` T.pack line && " := " `T.isInfixOf` T.pack next = [(named line, named next)]
+    applied _ _ = []
+    named :: String -> String
+    named = T.unpack . fst . T.breakOn " := " . T.pack
     paired :: T.Text -> T.Text -> (String, String)
     paired arrow text = let (left, right) = T.breakOn arrow text in (T.unpack left, T.unpack (T.drop (T.length arrow) right))
 
diff --git a/test/FunctionsSpec.hs b/test/FunctionsSpec.hs
--- a/test/FunctionsSpec.hs
+++ b/test/FunctionsSpec.hs
@@ -158,6 +158,18 @@
         , \term -> expectExpression term (DataString (strToBts "\\1"))
         )
       ,
+        ( "sed puts the whole match where the replacement holds an ampersand"
+        , "sed"
+        , [ArgExpression (DataString (strToBts "order 42")), ArgExpression (DataString (strToBts "s/([0-9]+)/<&>/g"))]
+        , \term -> expectExpression term (DataString (strToBts "order <42>"))
+        )
+      ,
+        ( "sed keeps an escaped ampersand in the replacement literal"
+        , "sed"
+        , [ArgExpression (DataString (strToBts "order 42")), ArgExpression (DataString (strToBts "s/([0-9]+)/<\\&>/g"))]
+        , \term -> expectExpression term (DataString (strToBts "order <&>"))
+        )
+      ,
         ( "random-string returns a literal pattern with no specials unchanged"
         , "random-string"
         , [ArgExpression (DataString (strToBts "static-name"))]
diff --git a/test/MorphSpec.hs b/test/MorphSpec.hs
--- a/test/MorphSpec.hs
+++ b/test/MorphSpec.hs
@@ -17,11 +17,11 @@
 import Data.IORef (modifyIORef', newIORef, readIORef)
 import Data.List (find, isInfixOf, nub)
 import Data.List.NonEmpty (NonEmpty (..))
-import Data.Map.Strict qualified as Map
 import Data.Maybe (fromMaybe)
+import Data.Text qualified as T
 import Data.Yaml qualified as Decode
 import Dataize (Outcome (..), dataize)
-import Deps (Acyclic (..), Evaluation (EvMorphed, EvRecalled, EvWorld), Judgment (..), State, Term (TeExpression))
+import Deps (Acyclic (..), Evaluation (EvLooped, EvMorphed, EvRecalled, EvWorld), Judgment (..), State, Term (TeExpression))
 import Engine (Engine (_normal))
 import Files (allPathsIn)
 import Fixtures (defaultReduceContext, fixtureLambdas, linked, overdue, primitives)
@@ -30,7 +30,7 @@
 import Inference (Conclusion (Answered), Premises (Concludes, Morphs), direct)
 import Lambdas (Lambdas, emptyLambdas)
 import Matcher (substEmpty)
-import Morph (Deadline (..), ReduceContext (..), declared, emptyState, enter, execBuildTerm, inferred, insideUniverse, morph, morph', voided)
+import Morph (Deadline (..), ReduceContext (..), declared, emptyState, enter, execBuildTerm, factual, fired, inferred, insideUniverse, morph, morph', noted, voided)
 import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows')
 import Rewriter (Rewritten)
 import Rule (RuleContext (RuleContext), matchExpressionWithRule')
@@ -270,68 +270,112 @@
       ctx <- defaultReduceContext ExRoot
       morph expr emptyState ctx{_deadline = Just deadline}
         `shouldThrow` (\e -> "--max-seconds=17" `isInfixOf` show (e :: SomeException))
-    it "fails a partial morphing once the deadline has passed" $ do
+    it "leaves a partial morphing in place once the deadline has passed" $ do
       expr <- parseExpressionThrows "[[ q -> [[ D> 5A- ]] ]]"
       deadline <- overdue 23
       ctx <- defaultReduceContext ExRoot
-      morph expr emptyState ctx{_deadline = Just deadline, _partial = True}
-        `shouldThrow` (\e -> "--max-seconds=23" `isInfixOf` show (e :: SomeException))
+      (residue, _, _) <- morph expr emptyState ctx{_deadline = Just deadline, _partial = True}
+      residue `shouldBe` expr
 
   describe "stops an entrance by the clock of --max-seconds" $
     it "fails a comparison that outlasts the deadline" $ do
       due <- (+ 0.2) <$> getMonotonicTime
       let formation :: Expression -> Int -> Expression
-          formation base depth = ExFormation [BiTau (AtLabel "x") (iterate (`ExDispatch` AtLabel "w") base !! depth), BiLambda (Function "L_q")]
+          formation base depth = ExFormation [BiTau (AtLabel "x") (iterate (`ExDispatch` AtLabel "w") base !! depth), BiTau AtPhi ExRoot]
       base <- defaultReduceContext ExRoot
       ctx <- enter (formation ExRoot 1300) base{_acyclic = Just Plausible, _deadline = Just (Deadline 31 due)}
       timeout 10000000 (enter (formation ExXi 1700) ctx)
         `shouldThrow` (\e -> "--max-seconds=31" `isInfixOf` show (e :: SomeException))
 
+  describe "names a cut by the facts however wide they are" $
+    it "names a cut held at the end of a wide fact long before the deadline" $ do
+      let looping :: Expression
+          looping = ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "pz"))]
+          wide :: Expression
+          wide = ExFormation ([BiTau (AtLabel (T.pack ("w" ++ show index))) (ExFormation [BiTau (AtLabel (T.pack ("v" ++ show index))) (ExFormation [BiDelta (BtOne "5C")])]) | index <- [1 :: Int .. 30000]] ++ [BiTau (AtLabel "kq") looping])
+      facts <- factual
+      told <- newIORef []
+      base <- defaultReduceContext ExRoot
+      noted base{_facts = Just facts} wide (ExDispatch ExRoot (AtLabel "cq"))
+      due <- (+ 2) <$> getMonotonicTime
+      ctx <- enter looping base{_acyclic = Just Plausible, _maxLoops = 0, _facts = Just facts, _reckoning = True, _deadline = Just (Deadline 43 due), _saveEval = \record -> modifyIORef' told (record :)}
+      _ <- timeout 10000000 (fired ExRoot ctx ExRoot emptyState looping)
+      records <- readIORef told
+      [answered | EvLooped _ _ _ _ _ (Just (_, answered)) <- records] `shouldBe` [Just (ExDispatch (ExDispatch ExRoot (AtLabel "cq")) (AtLabel "kq"))]
+
   describe "enters a formation again as many times as --max-loops allows" $ do
     it "enters a formation holding the one entered above it under --max-loops=1" $ do
       let formation :: Int -> Expression
-          formation depth = ExFormation [BiTau (AtLabel "kv") (iterate (`ExDispatch` AtLabel "zu") ExRoot !! depth), BiLambda (Function "L_hop")]
+          formation depth = ExFormation [BiTau (AtLabel "kv") (iterate (`ExDispatch` AtLabel "zu") ExRoot !! depth), BiTau AtPhi ExRoot]
       base <- defaultReduceContext ExRoot
       ctx <- enter (formation 4) =<< enter (formation 3) base{_acyclic = Just Plausible, _maxLoops = 1}
       length (concat ctx._entered) `shouldBe` 2
     it "cuts a formation holding the two entered above it under --max-loops=1" $ do
       let formation :: Int -> Expression
-          formation depth = ExFormation [BiTau (AtLabel "qe") (iterate (`ExDispatch` AtLabel "yo") ExRoot !! depth), BiLambda (Function "L_kit")]
+          formation depth = ExFormation [BiTau (AtLabel "qe") (iterate (`ExDispatch` AtLabel "yo") ExRoot !! depth), BiTau AtPhi ExRoot]
       base <- defaultReduceContext ExRoot
       (enter (formation 7) =<< enter (formation 6) =<< enter (formation 5) base{_acyclic = Just Plausible, _maxLoops = 1})
         `shouldThrow` (\e -> "already inside" `isInfixOf` show (e :: SomeException))
+    it "enters a copy of an atom that only resembles the copy entered above it" $ do
+      base <- defaultReduceContext ExRoot
+      ctx <- enter (ExFormation [BiTau (AtLabel "t") (ExFormation [BiLambda (FnSymbol 4)]), BiLambda (Function "L_vo")]) =<< enter (ExFormation [BiTau (AtLabel "t") (ExDispatch ExRoot (AtLabel "pu")), BiLambda (Function "L_vo")]) base{_acyclic = Just Plausible, _maxLoops = 0}
+      length (concat ctx._entered) `shouldBe` 2
+    it "cuts a copy of an atom that repeats the copy entered above it exactly" $ do
+      let formation :: Expression
+          formation = ExFormation [BiTau (AtLabel "ka") (ExDispatch ExRoot (AtLabel "mi")), BiLambda (Function "L_ru")]
+      base <- defaultReduceContext ExRoot
+      (enter formation =<< enter formation base{_acyclic = Just Plausible, _maxLoops = 0})
+        `shouldThrow` (\e -> "already inside" `isInfixOf` show (e :: SomeException))
 
   describe "places a formation among the objects of the world" $ do
     it "places a formation by the object the fact table maps it to" $ do
       let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))
-      facts <- newIORef (Map.fromList [(hashExpression (ExFormation [BiTau AtPhi body]), [(ExFormation [BiTau AtPhi body], ExDispatch ExRoot (AtLabel "nq"))])])
+      facts <- factual
       base <- defaultReduceContext ExRoot
+      noted base{_facts = Just facts} (ExFormation [BiTau AtPhi body]) (ExDispatch ExRoot (AtLabel "nq"))
       fmap fst <$> declared (ExFormation [BiTau (AtLabel "nq") (ExFormation [BiVoid AtPhi]), BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])
         `shouldReturn` Just (ExDispatch ExRoot (AtLabel "nq"))
     it "recalls every fact it follows on its way to the world, one by one" $ do
       let head' = ExFormation [BiVoid (AtLabel "ru"), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]
           copy = ExFormation [BiTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]
           applied = ExApplication head' (ArTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]))
-      facts <- newIORef (Map.fromListWith (++) [(hashExpression term, [(term, source)]) | (term, source) <- [(head', ExDispatch ExRoot (AtLabel "vex")), (copy, applied)]])
+      facts <- factual
       told <- newIORef []
       base <- defaultReduceContext ExRoot
+      mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "vex")), (copy, applied)]
       _ <- declared (ExFormation [BiTau (AtLabel "vex") head']) base{_facts = Just facts, _saveEval = \record -> modifyIORef' told (record :)} copy
       records <- readIORef told
       reverse [(term, reply) | EvRecalled _ term reply <- records] `shouldBe` [(copy, applied), (head', ExDispatch ExRoot (AtLabel "vex"))]
+    it "recalls every fact of a circle of facts once, whatever symbol the copy holds" $ do
+      let recalls :: Int -> IO Int
+          recalls symbol = do
+            let head' = ExFormation [BiVoid (AtLabel "ko"), BiLambda (Function "L_jew")]
+                copy = ExFormation [BiTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]), BiLambda (Function "L_jew")]
+                twin = ExFormation [BiTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]), BiLambda (Function "L_jew"), BiTau AtRho (ExDispatch ExRoot (AtLabel "jew"))]
+                answer = ExFormation [BiTau AtPhi twin]
+            facts <- factual
+            told <- newIORef []
+            base <- defaultReduceContext ExRoot
+            mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "jew")), (copy, ExApplication head' (ArTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]))), (answer, copy), (twin, ExDispatch answer AtPhi)]
+            mapM_ (\index -> noted base{_facts = Just facts} (ExFormation [BiLambda (FnSymbol (symbol + index))]) (ExDispatch ExRoot (AtLabel "pad"))) [1 .. 12]
+            _ <- declared (ExFormation [BiTau (AtLabel "jew") head']) base{_facts = Just facts, _saveEval = \record -> modifyIORef' told (record :)} answer
+            (\records -> length [term | EvRecalled _ term _ <- records]) <$> readIORef told
+      mapM recalls [3, 17 .. 700] `shouldReturn` replicate 50 3
     it "answers the voids of the first head a chain of remembered copies was applied to" $ do
       let head' = ExFormation [BiVoid (AtLabel "ka"), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]
           half = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]
           full = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)]), BiLambda (Function "L_ozu")]
-      facts <- newIORef (Map.fromListWith (++) [(hashExpression term, [(term, source)]) | (term, source) <- [(head', ExDispatch ExRoot (AtLabel "ozu")), (half, ExApplication head' (ArTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]))), (full, ExApplication half (ArTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)])))]])
+      facts <- factual
       base <- defaultReduceContext ExRoot
+      mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "ozu")), (half, ExApplication head' (ArTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]))), (full, ExApplication half (ArTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)])))]
       voided base{_facts = Just facts} full `shouldReturn` Just [AtLabel "ka", AtLabel "mu"]
     it "answers no voids for a formation the fact table does not hold" $ do
-      facts <- newIORef Map.empty
+      facts <- factual
       base <- defaultReduceContext ExRoot
       voided base{_facts = Just facts} (ExFormation [BiTau (AtLabel "pe") (ExFormation []), BiLambda (Function "L_uv")]) `shouldReturn` Nothing
     it "places nothing the fact table does not map" $ do
       let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))
-      facts <- newIORef Map.empty
+      facts <- factual
       base <- defaultReduceContext ExRoot
       fmap fst <$> declared (ExFormation [BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])
         `shouldReturn` Nothing
diff --git a/test/RegexpSpec.hs b/test/RegexpSpec.hs
--- a/test/RegexpSpec.hs
+++ b/test/RegexpSpec.hs
@@ -113,6 +113,9 @@
       , ("reads a back reference as a single digit", "\\10", ["full", "a"], "a0")
       , ("keeps an out of bounds back reference literal", "\\9", ["only"], "\\9")
       , ("keeps a digit after an escaped backslash literal", "\\\\1", ["full", "a"], "\\1")
+      , ("substitutes the whole match for an ampersand", "<&>", ["full", "a"], "<full>")
+      , ("keeps an escaped ampersand literal", "\\&", ["full"], "&")
+      , ("substitutes the whole match after an escaped backslash", "\\\\&", ["full"], "\\full")
       ]
       ( \(desc, template, groups, expected) ->
           it desc $ R.substituteGroups (utf8 template) (map utf8 groups) `shouldBe` utf8 expected
diff --git a/test/RenderSpec.hs b/test/RenderSpec.hs
--- a/test/RenderSpec.hs
+++ b/test/RenderSpec.hs
@@ -386,6 +386,18 @@
       ( render (EXTRA (ARG_EXPR xiExpr) "evaluate" [ARG_ATTR (AT_LABEL "n")])
           `shouldBe` "ξ \\coloneqq \\phinoEvaluate{ n }"
       )
+    forM_
+      [ ("number", "\\phinoNumber{ n }")
+      , ("string", "\\phinoString{ n }")
+      , ("sum", "\\phinoSum{ n }")
+      , ("tau", "\\phinoTau{ n }")
+      , ("random-tau", "\\randomTau{ n }")
+      ]
+      ( \(fn, expected) ->
+          it
+            (fn ++ " does not collide with a TeX primitive or symbol")
+            (render (EXTRA (ARG_EXPR xiExpr) fn [ARG_ATTR (AT_LABEL "n")]) `shouldBe` "ξ \\coloneqq " <> expected)
+      )
     it
       "any other function becomes its own backslash macro"
       ( render (EXTRA (ARG_EXPR xiExpr) "dataize" [ARG_ATTR (AT_LABEL "n")])
diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs
--- a/test/XMIRSpec.hs
+++ b/test/XMIRSpec.hs
@@ -26,7 +26,7 @@
 import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldNotContain, shouldReturn, shouldThrow)
 import Text.XML (Document (..), Element (..), Node (NodeElement), Prologue (..))
 import Text.XML.Cursor qualified as C
-import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirAtoms, xmirTime, xmirToPhi)
+import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, renameAtoms, toName, xmirAtoms, xmirTime, xmirToPhi)
 
 data ParsePack = ParsePack
   { failure :: Maybe Bool
@@ -225,6 +225,28 @@
     it "stays unique when two paths spell alike, and keeps the type of each atom" $ do
       doc <- parseXMIRThrows "<object><o name=\"top\"><o name=\"as-int\"><o atom=\"Φ.number\" name=\"λ\"/></o><o name=\"as_int\"><o atom=\"Φ.string\" name=\"λ\"/></o></o></object>"
       xmirAtoms doc `shouldReturn` M.fromList [("L_top_as_int", "Φ.number"), ("L_top_as_int_2", "Φ.string")]
+
+  describe "types of the voids of an atom in XMIR" $ do
+    let alloc :: String
+        alloc = "<object><o name=\"alloc\"><o base=\"∅\" name=\"size\" type=\"Φ.number\"/><o args=\"Φ.chunk\" base=\"∅\" name=\"scope\"/><o base=\"∅\" name=\"free\"/><o atom=\"Φ.bytes\" name=\"λ\"/></o></object>"
+        printed :: IO String
+        printed = do
+          doc <- parseXMIRThrows alloc
+          expr <- xmirToPhi doc
+          atoms <- xmirAtoms doc
+          printXMIR <$> expressionToXMIR expr (XmirContext True True False (const "") atoms)
+    it "keeps @type of a void through a round trip" $
+      printed >>= (`shouldContain` "<o base=\"∅\" name=\"size\" type=\"Φ.number\"/>")
+    it "keeps @args of a void through a round trip" $
+      printed >>= (`shouldContain` "<o args=\"Φ.chunk\" base=\"∅\" name=\"scope\"/>")
+    it "adds nothing to a void without a type" $
+      printed >>= (`shouldContain` "<o base=\"∅\" name=\"free\"/>")
+    it "keeps the type when the λ function is renamed" $ do
+      doc <- parseXMIRThrows alloc
+      atoms <- xmirAtoms doc
+      expr <- parseExpressionThrows "⟦ alloc ↦ ⟦ size ↦ ∅, scope ↦ ∅, free ↦ ∅, λ ⤍ Fn1 ⟧ ⟧"
+      result <- expressionToXMIR expr (renameAtoms [("L_alloc", "Fn1")] (XmirContext True True False (const "") atoms))
+      printXMIR result `shouldContain` "<o base=\"∅\" name=\"size\" type=\"Φ.number\"/>"
 
   describe "atom result types in XMIR" $ do
     let atom :: String
diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs
--- a/test/YamlSpec.hs
+++ b/test/YamlSpec.hs
@@ -34,6 +34,21 @@
 failsAsRedundant :: Either Yaml.ParseException a -> Bool
 failsAsRedundant = failsWith "redundant"
 
+loadedFrom :: String -> String -> IO Rule
+loadedFrom file content = do
+  tmp <- getTemporaryDirectory
+  bracket
+    (openTempFile tmp file)
+    (\(path, handle) -> hClose handle >> removeFile path)
+    ( \(path, handle) -> do
+        BS.hPut handle (encodeUtf8 (T.pack content))
+        hClose handle
+        yamlRule path
+    )
+
+quoted :: String -> String
+quoted word = "'" ++ word ++ "'"
+
 spec :: Spec
 spec = do
   describe "validates rewriting rule keys" $ do
@@ -62,21 +77,22 @@
   it "reads a bare y, n, yes, no, on and off in a rule file as the attributes they spell" $ do
     let written :: (String -> String) -> String
         written spelled = "name: bare-words\npattern: ⟦ 𝜏1 ↦ 𝑒1, 𝐵1 ⟧\nresult: ⟦ 𝐵1 ⟧\nwhen:\n  and:\n    - eq: [𝜏1, " ++ spelled "n" ++ "]\n    - in: [" ++ spelled "y" ++ ", 𝐵1]\n    - disjoint: [[" ++ intercalate ", " (map spelled ["yes", "no", "on", "off"]) ++ "], [𝐵1]]"
-    tmp <- getTemporaryDirectory
-    bare <-
-      bracket
-        (openTempFile tmp "bare-words.yaml")
-        (\(path, handle) -> hClose handle >> removeFile path)
-        ( \(path, handle) -> do
-            BS.hPut handle (encodeUtf8 (T.pack (written id)))
-            hClose handle
-            yamlRule path
-        )
+    bare <- loadedFrom "bare-words.yaml" (written id)
     show bare
       `shouldBe` either
         Yaml.prettyPrintParseException
         (show :: Rule -> String)
-        (decodeYaml' (written (\word -> "'" ++ word ++ "'")))
+        (decodeYaml' (written quoted))
+
+  it "reads a bare ASCII meta in a rule file as the meta it spells" $ do
+    let written :: (String -> String) -> String
+        written spelled = "name: bare-metas\npattern: ⟦ φ ↦ !e1, !t1 ↦ !e2, !B1 ⟧.!t2\nresult: " ++ spelled "!e1" ++ "\nwhen:\n  and:\n    - nf: " ++ spelled "!e2" ++ "\n    - not:\n        eq:\n          - " ++ spelled "!t1" ++ "\n          - " ++ spelled "!t2" ++ "\n    - not:\n        in:\n          - " ++ spelled "!t2" ++ "\n          - " ++ spelled "!B1"
+    bare <- loadedFrom "bare-metas.yaml" (written id)
+    show bare
+      `shouldBe` either
+        Yaml.prettyPrintParseException
+        (show :: Rule -> String)
+        (decodeYaml' (written quoted))
 
   describe "fails on yaml typos" $ do
     let resources = "test-resources/yaml-typos"