diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -157,6 +157,10 @@
 * `rewrite` binds a term meta to the term the meta under `of` holds, with the
   rules under `rules` applied and nothing normalized afterwards.
   The rules are written as in a [rule file](#rule-structure).
+* `cast` holds exactly two lines and binds their two metas as one pair.
+  When one term is a bare symbol, `⟦ λ ⤍ 𝜎1 ⟧`, and the φ chain of the other
+  ends in the only symbol it holds, the bare symbol becomes a copy of the other
+  term with `𝜎1` at the end of that chain.
 * `𝑛` is the term the entry answers with.
   A bare `𝜎` in it stands for a fresh symbol, and no `𝛿` may appear in it.
 * `join` answers with one term made of two sides, in place of `𝑛`.
@@ -338,6 +342,8 @@
   two sides, or why it could not join them.
 * `deferred …` and `symbolized …` are the symbols a `defer` or a `symbolize`
   line minted.
+* `cast …` binds a meta to the copy a `cast` block made of a bare symbol, and
+  the comment names the meta it read and the meta whose shape it took.
 * `unanswered …` is a λ name no entry answers.
 * `stuck …` closes a firing that got stuck, and `stall …` stands under one
   that `--acyclic=plausible` answered with an earlier stall.
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.159
+version: 0.0.160
 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/CLI/Parsers.hs b/src/CLI/Parsers.hs
--- a/src/CLI/Parsers.hs
+++ b/src/CLI/Parsers.hs
@@ -263,7 +263,8 @@
               \the copies one of whose arguments reads to a bare symbol it answers with a fresh symbol under \
               \\"defer\", the terms it keeps with every ρ applied to a dispatch dropped under \"stay\", the terms \
               \it rewrites with rules spelled as in a rule file under \"rewrite\", the terms it keeps with \
-              \every datum they hold turned into a fresh symbol under \"symbolize\", and \
+              \every datum they hold turned into a fresh symbol under \"symbolize\", the pair of terms whose \
+              \bare symbol it casts into the shape of the other under \"cast\", and \
               \answering with the term under \"𝑛\", or joining under \"join\" the two sides of a datum of \
               \\"dataize\" into one term, with a fresh symbol where they differ"
         )
diff --git a/src/Deps.hs b/src/Deps.hs
--- a/src/Deps.hs
+++ b/src/Deps.hs
@@ -132,19 +132,20 @@
   | EvSpent Int Int Judgment Expression
   | EvData Int T.Text Expression (Either Int Bytes)
   | EvTerm Int T.Text Judgment Expression Expression
-  | EvBound Int T.Text Expression Expression
+  | EvBound Int Expression Expression
   | EvReshaped Int T.Text T.Text Expression Expression
   | EvSymbolized Int Int Bytes
+  | EvCast Int T.Text Expression Expression Expression
   | EvMinted Int Int [Either Int Bytes]
   | EvDeferred Int Int Judgment Expression (Maybe Expression) Expression
   | EvApplied Int Judgment Expression Expression Expression
   | EvBuilt Int Expression
   | EvAnswer Int Expression
   | EvMorphed Int Expression
-  | EvJoined Int (Either T.Text Expression) Int (Int, Int)
+  | EvJoined Int (Either T.Text Expression) Int (Int, Int) (Maybe Int)
   | EvDiverged Int (Expression, Expression) (Expression, Expression) [Attribute] Refusal
   | EvFabricated Int (Expression, Expression) (Expression, Expression) Expression
-  | EvTaken Int [Expression] Expression
+  | EvTaken Int Expression
   | EvWorld Expression
   | EvHeader Header Expression Expression
 
@@ -194,19 +195,20 @@
 tier (EvSpent depth _ _ _) = depth
 tier (EvData depth _ _ _) = depth
 tier (EvTerm depth _ _ _ _) = depth
-tier (EvBound depth _ _ _) = depth
+tier (EvBound depth _ _) = depth
 tier (EvReshaped depth _ _ _ _) = depth
 tier (EvSymbolized depth _ _) = depth
+tier (EvCast depth _ _ _ _) = depth
 tier (EvMinted depth _ _) = depth
 tier (EvDeferred depth _ _ _ _ _) = depth
 tier (EvApplied depth _ _ _ _) = depth
 tier (EvBuilt depth _) = depth
 tier (EvAnswer depth _) = depth
 tier (EvMorphed depth _) = depth
-tier (EvJoined depth _ _ _) = depth
+tier (EvJoined depth _ _ _ _) = depth
 tier (EvDiverged depth _ _ _ _) = depth
 tier (EvFabricated depth _ _ _) = depth
-tier (EvTaken depth _ _) = depth
+tier (EvTaken depth _) = depth
 tier EvWorld{} = maxBound
 tier EvHeader{} = 0
 
@@ -254,10 +256,11 @@
   , _found :: Maybe (Either Int Bytes, String)
   , _blocks :: [(Int, Maybe (Judgment, String), String, Bool)]
   , _answered :: [(Int, Expression, String)]
+  , _unwritten :: Map.Map Int (Named Expression)
   }
 
 emptyProtocol :: Protocol
-emptyProtocol = Protocol 0 Map.empty [] False Map.empty Map.empty Map.empty Map.empty Nothing [] []
+emptyProtocol = Protocol 0 Map.empty [] False Map.empty Map.empty Map.empty Map.empty Nothing [] [] Map.empty
 
 data Nesting = Nesting
   { _fires :: Int
@@ -274,12 +277,13 @@
   , _world :: Map.Map Attribute Expression
   , _shapes :: Map.Map [Maybe Attribute] [(Expression, [Binding])]
   , _opaque :: Int
+  , _unmarked :: Map.Map Int (Named Expression)
   }
 
 type Naming = StateT (Nesting, [String]) IO
 
 emptyNesting :: Nesting
-emptyNesting = Nesting 0 [] [] Map.empty Map.empty Map.empty Map.empty Nothing [] [] [] Map.empty Map.empty 0
+emptyNesting = Nesting 0 [] [] Map.empty Map.empty Map.empty Map.empty Nothing [] [] [] Map.empty Map.empty 0 Map.empty
 
 saveEval :: Handle -> IORef Protocol -> (Expression -> IO String) -> (Expression -> IO String) -> SaveEvalFunc
 saveEval handle cursor printed printed' report = do
@@ -287,6 +291,7 @@
   mapM_ saved made
   where
     forgotten :: Evaluation -> Protocol -> Protocol
+    forgotten EvBound{} protocol = protocol
     forgotten EvDelta{} protocol = protocol
     forgotten EvManufactured{} protocol = protocol
     forgotten EvWorld{} protocol = protocol
@@ -294,6 +299,7 @@
     beside :: Int -> Evaluation -> Protocol -> Protocol
     beside _ EvStarted{} protocol = protocol
     beside _ EvMinted{} protocol = protocol
+    beside _ EvBound{} protocol = protocol
     beside at _ protocol = protocol{_blocks = dropWhile (\(level, _, _, _) -> level >= at) protocol._blocks}
     headed :: (Protocol, Maybe String) -> (Protocol, [String])
     headed (protocol, Nothing) = (protocol, [])
@@ -308,7 +314,7 @@
     located :: Protocol -> Expression -> IO String
     located protocol site = case [naming | (_, built, naming) <- protocol._answered, built == site] of
       naming : _ -> pure naming
-      [] -> salted site
+      [] -> salted (unwritten protocol site)
     context :: Protocol -> Judgment -> Expression -> IO [String]
     context protocol judgment site = do
       locator <- located protocol site
@@ -387,26 +393,29 @@
       pure (protocol, Just (indented at (remarked (printf "spent %d" limit) remarks)))
     written at (EvData _ spelling operand value) protocol = do
       datum <- maybe (spelt value) pure (found value protocol._found)
-      line <- commented (printf "%s := %s" (labelled protocol spelling) datum) Dataization operand
+      line <- commented protocol (printf "%s := %s" (labelled protocol spelling) datum) Dataization operand
       pure (protocol, Just (indented at line))
     written at (EvTerm _ spelling judgment operand term) protocol = do
       let naming = labelled protocol spelling
       (protocol', value) <- valued protocol naming term
-      line <- commented (printf "%s := %s" naming value) judgment operand
-      pure (protocol', Just (indented at line))
-    written at (EvBound _ spelling source term) protocol = do
-      let naming = labelled protocol spelling
-      (protocol', value) <- valued protocol naming term
-      line <- commented' (printf "%s := %s" naming value) source
+      line <- commented protocol (printf "%s := %s" naming value) judgment operand
       pure (protocol', Just (indented at line))
+    written _ (EvBound _ meta term) protocol =
+      pure (protocol{_unwritten = Map.alter (Just . namedInsert meta term . fromMaybe Map.empty) (opener protocol) protocol._unwritten}, Nothing)
     written at (EvReshaped _ spelling block source term) protocol = do
       let naming = labelled protocol spelling
       (protocol', value) <- valued protocol naming term
-      line <- printf "%s := %s  # %s(%s)" naming value (T.unpack block) <$> salted source
+      line <- printf "%s := %s  # %s(%s)" naming value (T.unpack block) <$> salted (unwritten protocol source)
       pure (protocol', Just (indented at line))
     written at (EvSymbolized _ symbol bytes) protocol = do
       datum <- render (ExBytes bytes)
       pure (protocol, Just (indented at (remarked (printf "symbolized %s := %s" (printFunction (FnSymbol symbol)) datum) (maybe [] pure (ieee bytes)))))
+    written at (EvCast _ spelling source model term) protocol = do
+      let naming = labelled protocol spelling
+      (protocol', value) <- valued protocol naming term
+      one <- spoken protocol source
+      two <- spoken protocol model
+      pure (protocol', Just (indented at (printf "cast %s := %s  # %s up to %s" naming value one two)))
     written _ EvMinted{} protocol = pure (protocol, Nothing)
     written at (EvDeferred _ symbol judgment copy call site) protocol = do
       form <- maybe (render copy) (printed . abbreviatedInside protocol._made) call
@@ -445,9 +454,10 @@
         (Nothing, Nothing) -> valued counted naming term
         _ -> (,) counted <$> borrowed protocol term
       pure (protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, Just (indented at (printf "morphed %s := %s" naming value)))
-    written at (EvJoined _ condition symbol (left, right)) protocol = do
+    written at (EvJoined _ condition symbol (left, right) bottom) protocol = do
       on <- either (pure . labelled protocol) salted condition
-      pure (protocol, Just (indented at (printf "joined %s := %s ? %s : %s" (printFunction (FnSymbol symbol)) on (printFunction (FnSymbol left)) (printFunction (FnSymbol right)))))
+      termination <- render ExTermination
+      pure (protocol, Just (indented at (remarked (printf "joined %s := %s ? %s : %s" (printFunction (FnSymbol symbol)) on (printFunction (FnSymbol left)) (printFunction (FnSymbol right))) [printf "where %s is %s" (printFunction (FnSymbol idx)) termination | Just idx <- [bottom], idx `elem` [left, right]])))
     written at (EvDiverged _ left right path refusal) protocol = do
       one <- sided protocol left
       two <- sided protocol right
@@ -458,13 +468,12 @@
       body <- printed (abbreviatedInside protocol._made term)
       let (index, counted) = numbered protocol
       pure (counted{_made = namedInsert term (alias (opener protocol) index) counted._made}, Just (indented at (printf "fabricated %s·%d := %s and %s  # %s" (labelled protocol answer) index one two body)))
-    written at (EvTaken _ sides term) protocol = do
+    written at (EvTaken _ term) protocol = do
       let (index, counted) = numbered protocol
           naming :: String
           naming = printf "%s·%d" (labelled protocol answer) index
       (protocol', value) <- valued counted naming term
-      remarks <- mapM sourced sides
-      pure (protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, Just (indented at (remarked (printf "%s := %s" naming value) remarks)))
+      pure (protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, Just (indented at (printf "%s := %s" naming value)))
     written _ (EvWorld world) protocol = pure (protocol{_made = namedInsert world ExRoot protocol._made}, Nothing)
     written _ (EvHeader (Header release revision dated command (World file count size tops bindings) table) locator expression) protocol = do
       place <- printed locator
@@ -499,17 +508,18 @@
     explained path refusal = printf "they differ at %s, and %s" (dotted path) (refused refusal)
     sided :: Protocol -> (Expression, Expression) -> IO String
     sided _ (_, term@(ExFormation [BiLambda (FnSymbol _)])) = render term
-    sided protocol (side@(ExMeta _), _) = labelled protocol . T.pack <$> salted side
+    sided protocol (side@(ExMeta _), _) = spoken protocol side
     sided protocol (_, term) = borrowed protocol term
-    commented :: String -> Judgment -> Expression -> IO String
-    commented line judgment operand = printf "%s  # %s(%s)" line (letter judgment) <$> salted operand
-    commented' :: String -> Expression -> IO String
-    commented' line source = printf "%s  # %s" line <$> salted source
-    sourced :: Expression -> IO String
-    sourced side@(ExMeta _) = salted side
-    sourced side = printf "%s(%s)" (letter Morphing) <$> salted side
+    spoken :: Protocol -> Expression -> IO String
+    spoken protocol meta = maybe (labelled protocol . T.pack <$> salted meta) (borrowed protocol) (namedLookup meta (held protocol))
+    commented :: Protocol -> String -> Judgment -> Expression -> IO String
+    commented protocol line judgment operand = printf "%s  # %s(%s)" line (letter judgment) <$> salted (unwritten protocol operand)
+    unwritten :: Protocol -> Expression -> Expression
+    unwritten protocol = abbreviated (held protocol)
+    held :: Protocol -> Named Expression
+    held protocol = Map.findWithDefault Map.empty (opener protocol) protocol._unwritten
     outer :: Int -> Protocol -> Protocol
-    outer depth protocol = protocol{_open = dropWhile ((>= depth) . fst) protocol._open, _answered = dropWhile (\(level, _, _) -> level > depth) protocol._answered}
+    outer depth protocol = protocol{_open = dropWhile ((>= depth) . fst) protocol._open, _answered = dropWhile (\(level, _, _) -> level > depth) protocol._answered, _unwritten = foldr (Map.delete . snd) protocol._unwritten (takeWhile ((>= depth) . fst) protocol._open)}
     labelled :: Protocol -> T.Text -> String
     labelled protocol spelling = printf "%s·%d" (T.unpack spelling) (opener protocol)
     opener :: Protocol -> Int
@@ -558,6 +568,7 @@
     opened' at (nesting, openings) = bimap (forgotten report) (openings ++) <$> elements at report nesting
     beside :: Int -> Evaluation -> Nesting -> Nesting
     beside _ EvStarted{} nesting = nesting
+    beside _ EvBound{} nesting = nesting
     beside at _ nesting = nesting{_heads = dropWhile ((>= at) . fst) nesting._heads, _pending = dropWhile (\(level, _, _) -> level >= at) nesting._pending}
     flushed :: Nesting -> IO (Nesting, [String])
     flushed nesting
@@ -570,8 +581,10 @@
     silent :: Evaluation -> Bool
     silent EvStarted{} = True
     silent EvWorld{} = True
+    silent EvBound{} = True
     silent _ = False
     forgotten :: Evaluation -> Nesting -> Nesting
+    forgotten EvBound{} nesting = nesting
     forgotten EvDelta{} nesting = nesting
     forgotten EvManufactured{} nesting = nesting
     forgotten EvWorld{} nesting = nesting
@@ -657,11 +670,16 @@
         bound :: String -> String
         bound = printf "<bound meta=\"%s\">%s</bound>" (escapeXML (labelled nesting spelling))
     elements at (EvTerm depth spelling _ _ term) nesting = placed at nesting (bind depth nesting spelling term)
-    elements at (EvBound depth spelling _ term) nesting = placed at nesting (bind depth nesting spelling term)
+    elements _ (EvBound _ meta term) nesting = pure (nesting{_unmarked = Map.alter (Just . namedInsert meta term . fromMaybe Map.empty) (opener nesting) nesting._unmarked}, [])
     elements at (EvReshaped depth spelling _ _ term) nesting = placed at nesting (bind depth nesting spelling term)
     elements at (EvSymbolized _ symbol bytes) nesting = do
       datum <- printed (ExBytes bytes)
       placed at nesting (pure (printf "<symbolized symbol=\"%s\"%s>%s</symbolized>" (sigma symbol) (maybe "" (printf " number=\"%s\"" . escapeXML) (ieee bytes) :: String) (escapeXMLText datum)))
+    elements at (EvCast depth spelling source model term) nesting =
+      placed at nesting $ do
+        one <- spoken depth nesting source
+        two <- spoken depth nesting model
+        printf "<cast meta=\"%s\" of=\"%s\" up-to=\"%s\">%s</cast>" (escapeXML (labelled nesting spelling)) (escapeXML one) (escapeXML two) . escapeXMLText <$> leaf depth term
     elements at (EvMinted _ symbol operands) nesting = do
       spelledOperands <- mapM spelled' operands
       placed at nesting (pure (minted spelledOperands))
@@ -695,10 +713,10 @@
         pure (printf "<built meta=\"%s\">%s</built>" (escapeXML naming) (escapeXMLText body))
     elements at (EvAnswer depth term) nesting = placed at nesting (concluded "answered" depth term)
     elements at (EvMorphed depth term) nesting = placed at nesting (concluded "morphed" depth term)
-    elements at (EvJoined _ condition symbol (left, right)) nesting =
+    elements at (EvJoined _ condition symbol (left, right) bottom) nesting =
       placed at nesting $ do
         on <- either (pure . labelled nesting) (lift . traced) condition
-        pure (printf "<joined symbol=\"%s\" on=\"%s\" left=\"%s\" right=\"%s\"/>" (sigma symbol) (escapeXML on) (sigma left) (sigma right))
+        pure (printf "<joined symbol=\"%s\" on=\"%s\" left=\"%s\" right=\"%s\"%s/>" (sigma symbol) (escapeXML on) (sigma left) (sigma right) (concat [printf " terminator=\"%s\"" (sigma idx) :: String | Just idx <- [bottom], idx `elem` [left, right]]))
     elements at (EvDiverged depth left right path refusal) nesting =
       placed at nesting $ do
         one <- sided depth nesting left
@@ -711,7 +729,7 @@
         body <- leaf depth term
         (naming, _) <- counted
         pure (printf "<fabricated meta=\"%s\" left=\"%s\" right=\"%s\">%s</fabricated>" (escapeXML naming) (escapeXML one) (escapeXML two) (escapeXMLText body))
-    elements at (EvTaken depth _ term) nesting = placed at nesting (concluded "answered" depth term)
+    elements at (EvTaken depth term) nesting = placed at nesting (concluded "answered" depth term)
     elements _ (EvWorld world) nesting = pure (known world nesting, [])
     prologue :: Nesting -> [String]
     prologue nesting
@@ -722,10 +740,14 @@
     rooted open = open
     sided :: Int -> Nesting -> (Expression, Expression) -> Naming String
     sided depth _ (_, term@(ExFormation [BiLambda (FnSymbol _)])) = leaf depth term
-    sided _ nesting (side@(ExMeta _), _) = labelled nesting . T.pack <$> lift (spelled side)
+    sided depth nesting (side@(ExMeta _), _) = spoken depth nesting side
     sided depth _ (_, term) = leaf depth term
+    spoken :: Int -> Nesting -> Expression -> Naming String
+    spoken depth nesting meta = maybe (labelled nesting . T.pack <$> lift (spelled meta)) (leaf depth) (namedLookup meta (held nesting))
+    held :: Nesting -> Named Expression
+    held nesting = Map.findWithDefault Map.empty (opener nesting) nesting._unmarked
     outer :: Int -> Nesting -> Nesting
-    outer depth nesting = nesting{_openedAt = dropWhile ((>= depth) . fst) nesting._openedAt, _sources = dropWhile (\(level, _, _) -> level > depth) nesting._sources}
+    outer depth nesting = nesting{_openedAt = dropWhile ((>= depth) . fst) nesting._openedAt, _sources = dropWhile (\(level, _, _) -> level > depth) nesting._sources, _unmarked = foldr (Map.delete . snd) nesting._unmarked (takeWhile ((>= depth) . fst) nesting._openedAt)}
     labelled :: Nesting -> T.Text -> String
     labelled nesting spelling = printf "%s·%d" (T.unpack spelling) (opener nesting)
     stored :: Either Int Bytes -> Nesting -> (String, Nesting)
@@ -764,7 +786,7 @@
     located :: Int -> Expression -> Naming String
     located depth site = do
       (nesting, _) <- get
-      maybe (titled depth site >>= lift . traced) pure (listToMaybe [naming | (_, built, naming) <- nesting._sources, built == site])
+      maybe (titled depth (abbreviated (held nesting) site) >>= lift . traced) pure (listToMaybe [naming | (_, built, naming) <- nesting._sources, built == site])
     taken :: Int -> String -> Int -> Expression -> Nesting -> IO (Nesting, [String])
     taken at tag depth term nesting =
       placed at nesting $ do
diff --git a/src/Emit.hs b/src/Emit.hs
--- a/src/Emit.hs
+++ b/src/Emit.hs
@@ -10,7 +10,7 @@
 import AST
 import Control.Monad (zipWithM)
 import Data.Char (isAlphaNum, isDigit, toLower, toUpper)
-import Data.List (intercalate, nub)
+import Data.List (intercalate, mapAccumL, nub)
 import qualified Data.Map.Strict as Map
 import Data.Maybe (fromMaybe, isJust, isNothing)
 import qualified Data.Set as Set
@@ -173,12 +173,21 @@
     isUpperStart [] = False
 
 named :: [String] -> [String]
-named names = zipWith unique [0 :: Int ..] (map camel names)
+named names = snd (mapAccumL unique (Set.fromList stems) (zip [0 :: Int ..] stems))
   where
-    unique :: Int -> String -> String
-    unique idx name
-      | length (filter (== name) (map camel names)) > 1 = name ++ show idx
-      | otherwise = name
+    stems :: [String]
+    stems = map camel names
+    unique :: Set.Set String -> (Int, String) -> (Set.Set String, String)
+    unique taken (idx, name)
+      | length (filter (== name) stems) > 1 =
+          let chosen = available (name ++ show idx)
+           in (Set.insert chosen taken, chosen)
+      | otherwise = (taken, name)
+      where
+        available :: String -> String
+        available candidate
+          | candidate `Set.member` taken = available (candidate ++ "_")
+          | otherwise = candidate
     camel :: String -> String
     camel name = case filter isAlphaNum (concatMap upper (words (map (\char -> if isAlphaNum char then char else ' ') name))) of
       [] -> "Rule"
diff --git a/src/Evaluate.hs b/src/Evaluate.hs
--- a/src/Evaluate.hs
+++ b/src/Evaluate.hs
@@ -20,9 +20,9 @@
 import Deps (Evaluation (..), Judgment (Evaluation, Morphing), State (..), dontSaveEval, dontSaveStep, resited)
 import Engine (Engine (..))
 import Forks (Refusal (Unnamed), forked, joined)
-import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), emptyLambdas, matched, minted, rewritten, stayed, symbolized)
+import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), cast, emptyLambdas, matched, minted, rewritten, stayed, symbolized)
 import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)
-import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), boxed, charged, counted, deeper, ended, enter, expired, isLambda, lambda, morphing, normalized, opening, recalled, remember, remembered, retained, settled, starved, unparked)
+import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), awaited, boxed, charged, counted, deeper, ended, enter, expired, isLambda, lambda, morphing, normalized, opening, recalled, remember, remembered, retained, settled, starved, unparked)
 import Printer (printFunction)
 import Rule (RuleContext (RuleContext))
 import Text.Printf (printf)
@@ -103,14 +103,15 @@
     line ctx ending held (Evaluated meta source) = evaluated ctx ending held meta source
     line ctx _ (bound, state') (Deferred meta source) = (,state') <$> deferred ctx state' meta source bound
     line ctx _ held (Stayed meta source) = reshaped ctx "stay" (still (pure . stayed)) meta source held
-    line ctx _ held (Rewritten meta source rules) = reshaped ctx "rewrite" (still (rewritten (RuleContext ctx._buildTerm ctx._universe ctx._engine._normal) rules)) meta source held
+    line ctx _ held (Rewritten meta source rules) = reshaped ctx "rewrite" (still (awaited ctx . rewritten (RuleContext ctx._buildTerm ctx._universe ctx._engine._normal) rules)) meta source held
     line ctx _ held (Symbolized meta source) = reshaped ctx "symbolize" (still (masked ctx)) meta source held
     line ctx _ held (Undressed meta source) = reshaped ctx "undress" (peeled ctx) meta source held
+    line ctx _ held (Cast one first two second) = casting ctx held (one, first) (two, second)
     shown :: Int -> Answer -> IO ()
     shown depth (Answer built normal) = do
       caller._saveEval (EvBuilt depth built)
       caller._saveEval (EvAnswer depth normal)
-    shown depth (Joined (left, right) normal) = caller._saveEval (EvTaken depth [left, right] normal)
+    shown depth (Joined normal) = caller._saveEval (EvTaken depth normal)
     kept :: Bool -> ReduceException -> Maybe Kept
     kept _ (Looping term) = Just (Looped term)
     kept _ (LoopingAt term _ _) = Just (Looped term)
@@ -183,10 +184,27 @@
       (term, state'') <- change state' kept
       ctx._saveEval
         ( if term == kept
-            then EvBound ctx._nesting meta._spelling (ExMeta source._name) term
+            then EvBound ctx._nesting (ExMeta meta._name) term
             else EvReshaped ctx._nesting meta._spelling block (ExMeta source._name) term
         )
       (,state'') <$> bind meta (MvExpression term) bound
+    casting :: ReduceContext -> (Subst, State) -> (Meta, Meta) -> (Meta, Meta) -> IO (Subst, State)
+    casting ctx (bound, state') (one, first) (two, second) = do
+      left <- buildExpressionThrows (ExMeta first._name) bound
+      right <- buildExpressionThrows (ExMeta second._name) bound
+      (,state') <$> case (cast left right, cast right left) of
+        (Just made, _) -> molded one first second made bound >>= kept two right
+        (_, Just made) -> kept one left bound >>= molded two second first made
+        _ -> kept one left bound >>= kept two right
+      where
+        kept :: Meta -> Expression -> Subst -> IO Subst
+        kept meta term held = do
+          ctx._saveEval (EvBound ctx._nesting (ExMeta meta._name) term)
+          bind meta (MvExpression term) held
+        molded :: Meta -> Meta -> Meta -> Expression -> Subst -> IO Subst
+        molded meta source shape made held = do
+          ctx._saveEval (EvCast ctx._nesting meta._spelling (ExMeta source._name) (ExMeta shape._name) made)
+          bind meta (MvExpression made) held
     still :: (Expression -> IO Expression) -> State -> Expression -> IO (Expression, State)
     still change state' term = (,state') <$> change term
     peeled :: ReduceContext -> State -> Expression -> IO (Expression, State)
@@ -212,7 +230,11 @@
     evaluated ctx ending (bound, state') meta source = do
       term <- buildExpressionThrows (ExMeta source._name) bound
       (answer, state'') <- kindled ctx ending (ExMeta source._name) state' term
-      ctx._saveEval (EvTerm ctx._nesting meta._spelling Evaluation (ExMeta source._name) answer)
+      ctx._saveEval
+        ( if answer == term
+            then EvBound ctx._nesting (ExMeta meta._name) term
+            else EvTerm ctx._nesting meta._spelling Evaluation (ExMeta source._name) answer
+        )
       bound' <- bind meta (MvExpression answer) bound
       pure (bound', state'')
     kindled :: ReduceContext -> Ending -> Expression -> State -> Expression -> IO (Expression, State)
@@ -273,7 +295,7 @@
       bind meta (MvExpression answer) bound
       where
         kept :: Expression -> IO Expression
-        kept term = term <$ ctx._saveEval (EvBound ctx._nesting meta._spelling (ExMeta source._name) term)
+        kept term = term <$ ctx._saveEval (EvBound ctx._nesting (ExMeta meta._name) term)
     postponing :: ReduceContext -> State -> Expression -> Expression -> IO (Maybe Expression)
     postponing ctx state' site (ExFormation bds)
       | copied bds = do
@@ -352,15 +374,15 @@
       (two, state''') <- reached ctx bound right state''
       spent <- readIORef ctx._minted
       case joined one two spent of
-        Right (term, made, spent') -> do
+        Right (term, made, bottom, spent') -> do
           writeIORef ctx._minted spent'
-          mapM_ (\(fresh, pair) -> ctx._saveEval (EvJoined ctx._nesting (either (Left . _spelling) Right on) fresh pair)) made
-          ctx._saveEval (EvTaken ctx._nesting [left, right] term)
-          pure (Joined (left, right) term, state''')
+          mapM_ (\(fresh, pair) -> ctx._saveEval (EvJoined ctx._nesting (either (Left . _spelling) Right on) fresh pair bottom)) made
+          ctx._saveEval (EvTaken ctx._nesting term)
+          pure (Joined term, state''')
         Left path -> case maybe (Left Unnamed) (\name -> forked name condition one two) fallback of
           Right term -> do
             ctx._saveEval (EvFabricated ctx._nesting (left, one) (right, two) term)
-            pure (Joined (left, right) term, state''')
+            pure (Joined term, state''')
           Left refusal -> do
             ctx._saveEval (EvDiverged ctx._nesting (left, one) (right, two) path refusal)
             throwIO (Diverged func)
diff --git a/src/Filter.hs b/src/Filter.hs
--- a/src/Filter.hs
+++ b/src/Filter.hs
@@ -47,7 +47,7 @@
       Just attrs -> maybe (throwIO (CanNotFindObjectByLocator fqn)) pure (includedFormation expr attrs)
       _ -> throwIO (InvalidLocatorProvided fqn)
     mergeForms :: [Expression] -> Expression
-    mergeForms forms = ExFormation (foldl merged [] (filter ((/= Just AtRho) . attributeFromBinding) (concat [bs | ExFormation bs <- forms])))
+    mergeForms forms = ExFormation (foldl merged [] (concat [bs | ExFormation bs <- forms]))
     merged :: [Binding] -> Binding -> [Binding]
     merged acc bd = case break ((== attributeFromBinding bd) . attributeFromBinding) acc of
       (before, BiTau at (ExFormation old) : after) | BiTau _ (ExFormation new) <- bd -> before ++ BiTau at (mergeForms [ExFormation old, ExFormation new]) : after
diff --git a/src/Forks.hs b/src/Forks.hs
--- a/src/Forks.hs
+++ b/src/Forks.hs
@@ -1,11 +1,13 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
 module Forks (Refusal (..), Side (..), forked, joined) where
 
-import AST (Argument (..), Attribute (AtDelta, AtLabel, AtLambda, AtRho), Binding (..), Bytes, Expression (ExApplication, ExDispatch, ExFormation, ExPhiAgain, ExPhiMeet, ExXi), Function (FnSymbol), attributeFromBinding)
+import AST (Argument (..), Attribute (AtDelta, AtLabel, AtLambda, AtRho), Binding (..), Bytes, Expression (ExApplication, ExDispatch, ExFormation, ExPhiAgain, ExPhiMeet, ExTermination, ExXi), Function (FnSymbol), attributeFromBinding, symbols)
+import Control.Monad.Trans.State.Strict (State, runState, state)
 import Data.Bifunctor (bimap, first)
 import Data.List (nub)
 import Data.Map.Strict (Map)
@@ -14,7 +16,7 @@
 import Data.Text (Text)
 import qualified Data.Text as T
 
-type Joining = (Int, Map (Int, Int) Int, [(Int, (Int, Int))])
+type Joining = (Int, Maybe Int, Map (Int, Int) Int, [(Int, (Int, Int))])
 
 data Side = Lefthand | Righthand
   deriving (Eq, Show)
@@ -25,8 +27,8 @@
   | Holding Side Attribute
   deriving (Eq, Show)
 
-joined :: Expression -> Expression -> Int -> Either [Attribute] (Expression, [(Int, (Int, Int))], Int)
-joined left right spent = (\(term, (spent', _, made)) -> (term, reverse made, spent')) <$> goExpr left right (spent, Map.empty, [])
+joined :: Expression -> Expression -> Int -> Either [Attribute] (Expression, [(Int, (Int, Int))], Maybe Int, Int)
+joined left right spent = (\(term, (spent', bottom, _, made)) -> (term, reverse made, bottom, spent')) <$> goExpr left right (spent, Nothing, Map.empty, [])
   where
     goExpr :: Expression -> Expression -> Joining -> Either [Attribute] (Expression, Joining)
     goExpr (ExFormation one) (ExFormation two) joining = first ExFormation <$> goBindings one two joining
@@ -39,6 +41,9 @@
       | prefix == prefix' && idx == idx' = within (first (ExPhiMeet prefix idx) <$> goExpr one two joining)
     goExpr (ExPhiAgain prefix idx one) (ExPhiAgain prefix' idx' two) joining
       | prefix == prefix' && idx == idx' = within (first (ExPhiAgain prefix idx) <$> goExpr one two joining)
+    goExpr ExTermination ExTermination joining = Right (ExTermination, joining)
+    goExpr ExTermination two joining = faced (,) two joining
+    goExpr one ExTermination joining = faced (flip (,)) one joining
     goExpr one two joining = same one two joining
     goBinding :: Binding -> Binding -> Joining -> Either [Attribute] (Binding, Joining)
     goBinding (BiTau attr one) (BiTau attr' two) joining
@@ -67,10 +72,30 @@
     same one two joining
       | one == two = Right (one, joining)
       | otherwise = Left []
+    faced :: (Int -> Int -> (Int, Int)) -> Expression -> Joining -> Either [Attribute] (Expression, Joining)
+    faced pair side joining@(spent', bottom, names, made)
+      | null (symbols side) = Left []
+      | otherwise = Right (runState (goFaced side) joining')
+      where
+        (termination, joining') = maybe (succ spent', (succ spent', Just (succ spent'), names, made)) (,joining) bottom
+        goFaced :: Expression -> State Joining Expression
+        goFaced (ExFormation bds) = ExFormation <$> mapM goFacedBinding bds
+        goFaced (ExApplication expr arg) = ExApplication <$> goFaced expr <*> goFacedArgument arg
+        goFaced (ExDispatch expr attr) = (`ExDispatch` attr) <$> goFaced expr
+        goFaced (ExPhiMeet prefix idx expr) = ExPhiMeet prefix idx <$> goFaced expr
+        goFaced (ExPhiAgain prefix idx expr) = ExPhiAgain prefix idx <$> goFaced expr
+        goFaced expr = pure expr
+        goFacedBinding :: Binding -> State Joining Binding
+        goFacedBinding (BiTau attr expr) = BiTau attr <$> goFaced expr
+        goFacedBinding (BiLambda (FnSymbol idx)) = BiLambda . FnSymbol <$> state (picked (pair termination idx))
+        goFacedBinding bd = pure bd
+        goFacedArgument :: Argument -> State Joining Argument
+        goFacedArgument (ArTau attr expr) = ArTau attr <$> goFaced expr
+        goFacedArgument (ArAlpha alpha expr) = ArAlpha alpha <$> goFaced expr
     picked :: (Int, Int) -> Joining -> (Int, Joining)
-    picked pair joining@(spent', names, made) = case Map.lookup pair names of
+    picked pair joining@(spent', bottom, names, made) = case Map.lookup pair names of
       Just name -> (name, joining)
-      Nothing -> (succ spent', (succ spent', Map.insert pair (succ spent') names, (succ spent', pair) : made))
+      Nothing -> (succ spent', (succ spent', bottom, Map.insert pair (succ spent') names, (succ spent', pair) : made))
 
 forked :: Function -> Either Int Bytes -> Expression -> Expression -> Either Refusal Expression
 forked func condition left right = fabricated <$> formed Lefthand left <*> formed Righthand right
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -316,7 +316,10 @@
 instance ToLaTeX META where
   toLaTeX META{..} =
     let idx = readMaybe (T.unpack rest) :: Maybe Int
-        rest' = if not (T.null rest) && T.length rest <= 2 && isJust idx then T.cons '_' rest else rest
+        rest'
+          | T.length rest == 1 && isJust idx = T.cons '_' rest
+          | T.length rest == 2 && isJust idx = "_{" <> rest <> "}"
+          | otherwise = rest
      in META NO_EXCL (toLaTeX hd) rest'
 
 instance ToLaTeX META_HEAD where
diff --git a/src/Lambdas.hs b/src/Lambdas.hs
--- a/src/Lambdas.hs
+++ b/src/Lambdas.hs
@@ -13,6 +13,7 @@
   , Lambdas
   , Line (..)
   , Meta (..)
+  , cast
   , emptyLambdas
   , matched
   , minted
@@ -28,6 +29,7 @@
 import AST
 import Builder (buildExpressionThrows)
 import Control.Exception (Exception, throwIO)
+import Control.Monad ((<$!>))
 import Control.Monad.Trans.State.Strict (State, runState, state)
 import Data.Aeson (FromJSON (parseJSON), Key, Object, withObject, (.!=), (.:?))
 import qualified Data.Aeson.Key as Key
@@ -70,6 +72,7 @@
   | Stayed Meta Meta
   | Rewritten Meta Meta [Y.Rule]
   | Symbolized Meta Meta
+  | Cast Meta Meta Meta Meta
 
 data Ending
   = Answering Expression
@@ -119,7 +122,7 @@
         name : _ -> fail (printf "The key '%s' of λ function '%s' is none of the keys an entry reads: %s" (T.unpack name) key (T.unpack (T.intercalate ", " known)))
         where
           known :: [Text]
-          known = ["λ", "dataize", "morph", "undress", "evaluate", "defer", "stay", "rewrite", "symbolize", "join", "𝑛"]
+          known = ["λ", "dataize", "morph", "undress", "evaluate", "defer", "stay", "rewrite", "symbolize", "cast", "join", "𝑛"]
       concluded :: String -> [(Meta, Expression)] -> Object -> Yaml.Parser Ending
       concluded key dataized entry = do
         answer <- entry .:? "𝑛"
@@ -178,11 +181,25 @@
         Right (BtMeta name) -> pure (Meta meta name)
         _ -> fail (printf "The operand '%s' is not a bytes meta, such as '𝛿1'" (T.unpack meta))
       written :: String -> Object -> Yaml.Parser [Line]
-      written key entry = concat <$> sequence [links Evaluated entry "evaluate", links Deferred entry "defer", links Stayed entry "stay", rewrites key entry, links Symbolized entry "symbolize"]
+      written key entry = concat <$> sequence [links Evaluated entry "evaluate", links Deferred entry "defer", links Stayed entry "stay", rewrites key entry, links Symbolized entry "symbolize", casts key entry]
       links :: (Meta -> Meta -> Line) -> Object -> Key -> Yaml.Parser [Line]
       links kind entry name = do
         mapping <- entry .:? name .!= (Map.empty :: Map Text Text)
         mapM (\(meta, source) -> kind <$> expressionMeta meta <*> expressionMeta source) (numbered mapping)
+      casts :: String -> Object -> Yaml.Parser [Line]
+      casts key entry = do
+        mapping <- entry .:? "cast" .!= (Map.empty :: Map Text Text)
+        case numbered mapping of
+          [] -> pure []
+          [(one, first), (two, second)] -> (: []) <$> (Cast <$> expressionMeta one <*> expressionMeta first <*> expressionMeta two <*> expressionMeta second)
+          pairs ->
+            fail
+              ( printf
+                  "The 'cast' block of λ function '%s' holds %d %s, while it casts one pair and takes exactly two"
+                  key
+                  (length pairs)
+                  (if length pairs == 1 then "line" else "lines" :: String)
+              )
       rewrites :: String -> Object -> Yaml.Parser [Line]
       rewrites key entry = do
         mapping <- entry .:? "rewrite" .!= (Map.empty :: Map Text Object)
@@ -202,11 +219,11 @@
             [] -> pure rule
             idx : _ -> fail (printf "The rule '%s' of the 'rewrite' block of λ function '%s' writes the symbol '𝜎%d' into its result, while only a firing mints a symbol" rule.name key idx)
       ordered :: String -> [Text] -> [Line] -> Yaml.Parser [Line]
-      ordered key reduced waiting = mapM_ (bound . source) waiting >> go reduced waiting
+      ordered key reduced waiting = mapM_ bound (concatMap sources waiting) >> go reduced waiting
         where
           bound :: Meta -> Yaml.Parser ()
           bound meta
-            | meta._name `elem` reduced ++ map (_name . binding) waiting = pure ()
+            | meta._name `elem` reduced ++ map _name (concatMap bindings waiting) = pure ()
             | otherwise =
                 fail
                   ( printf
@@ -216,8 +233,8 @@
                   )
           go :: [Text] -> [Line] -> Yaml.Parser [Line]
           go _ [] = pure []
-          go known pending@(first : _) = case break ((`elem` known) . _name . source) pending of
-            (before, line : after) -> (line :) <$> go ((binding line)._name : known) (before ++ after)
+          go known pending@(first : _) = case break (all ((`elem` known) . _name) . sources) pending of
+            (before, line : after) -> (line :) <$> go (map _name (bindings line) ++ known) (before ++ after)
             (_, []) ->
               fail
                 ( printf
@@ -231,16 +248,17 @@
                 | meta._name `elem` seen = meta
                 | otherwise = goCircle (meta._name : seen) (fromMaybe meta (listToMaybe (feeding meta)))
               feeding :: Meta -> [Meta]
-              feeding meta = [source line | line <- pending, meta._name == (binding line)._name, (source line)._name `notElem` known]
-          source :: Line -> Meta
-          source (Dataized _ meta) = meta
-          source (Morphed _ meta) = meta
-          source (Undressed _ meta) = meta
-          source (Evaluated _ meta) = meta
-          source (Deferred _ meta) = meta
-          source (Stayed _ meta) = meta
-          source (Rewritten _ meta _) = meta
-          source (Symbolized _ meta) = meta
+              feeding meta = [source | line <- pending, meta._name `elem` map _name (bindings line), source <- sources line, source._name `notElem` known]
+          sources :: Line -> [Meta]
+          sources (Dataized _ meta) = [meta]
+          sources (Morphed _ meta) = [meta]
+          sources (Undressed _ meta) = [meta]
+          sources (Evaluated _ meta) = [meta]
+          sources (Deferred _ meta) = [meta]
+          sources (Stayed _ meta) = [meta]
+          sources (Rewritten _ meta _) = [meta]
+          sources (Symbolized _ meta) = [meta]
+          sources (Cast _ first _ second) = [first, second]
       binding :: Line -> Meta
       binding (Dataized meta _) = meta
       binding (Morphed meta _) = meta
@@ -250,6 +268,10 @@
       binding (Stayed meta _) = meta
       binding (Rewritten meta _ _) = meta
       binding (Symbolized meta _) = meta
+      binding (Cast meta _ _ _) = meta
+      bindings :: Line -> [Meta]
+      bindings (Cast one _ two _) = [one, two]
+      bindings line = [binding line]
       sigmas :: String -> Expression -> Yaml.Parser ()
       sigmas key answer = case ([kind | Slot kind _ <- slots answer, kind /= "S"], symbols answer) of
         ([], []) -> pure ()
@@ -261,7 +283,7 @@
         Just meta -> fail (printf "The meta '%s' of λ function '%s' is bound by more than one line, while each meta may be bound once" (T.unpack meta._spelling) key)
         where
           bound :: [Meta]
-          bound = map fst (lambda._morphed ++ lambda._undressed) ++ map binding lambda._lines
+          bound = map fst (lambda._morphed ++ lambda._undressed) ++ concatMap bindings lambda._lines
           twice :: [Text] -> [Meta] -> Maybe Meta
           twice _ [] = Nothing
           twice seen (meta : rest)
@@ -290,11 +312,11 @@
           known :: [Text]
           known = map (_name . fst) lambda._dataized ++ reduced
           reduced :: [Text]
-          reduced = map (_name . fst) (lambda._morphed ++ lambda._undressed) ++ map (_name . binding) lambda._lines
+          reduced = map (_name . fst) (lambda._morphed ++ lambda._undressed) ++ map _name (concatMap bindings lambda._lines)
           sided :: String -> Expression -> Yaml.Parser ()
           sided name side = case filter (`notElem` reduced) (metas side) of
             [] -> pure ()
-            meta : _ -> fail (printf "The side '%s' of the 'join' block of λ function '%s' reads the meta '%s' that none of 'morph', 'undress', 'evaluate', 'stay', 'rewrite', 'symbolize' and 'defer' binds" name key (T.unpack meta))
+            meta : _ -> fail (printf "The side '%s' of the 'join' block of λ function '%s' reads the meta '%s' that none of 'morph', 'undress', 'evaluate', 'stay', 'rewrite', 'symbolize', 'cast' and 'defer' binds" name key (T.unpack meta))
       dataless :: String -> Expression -> Yaml.Parser ()
       dataless key answer
         | computes answer = fail (printf "The '𝑛' of λ function '%s' reads data, while a symbolic answer may mention nothing but 𝜎" key)
@@ -418,11 +440,30 @@
     dispatched (ExApplication expr _) = dispatched expr
     dispatched _ = False
 
+cast :: Expression -> Expression -> Maybe Expression
+cast bare@(ExFormation [BiLambda (FnSymbol _)]) shape
+  | length (symbols shape) == 1 = goExpr shape
+  where
+    goExpr :: Expression -> Maybe Expression
+    goExpr (ExFormation bds) = case [body | BiTau AtPhi body <- bds] of
+      [ExFormation [BiLambda (FnSymbol _)]] -> Just (ExFormation (map (placed bare) bds))
+      [body] -> (\made -> ExFormation (map (placed made) bds)) <$> goExpr body
+      _ -> Nothing
+    goExpr _ = Nothing
+    placed :: Expression -> Binding -> Binding
+    placed made (BiTau AtPhi _) = BiTau AtPhi made
+    placed _ bd = bd
+cast _ _ = Nothing
+
 rewritten :: RuleContext -> [Y.Rule] -> Expression -> IO Expression
 rewritten ctx rules = goExpr
   where
     goExpr :: Expression -> IO Expression
-    goExpr expr = goRules expr rules
+    goExpr expr = kept expr <$!> goRules expr rules
+    kept :: Expression -> Expression -> Expression
+    kept expr made
+      | made == expr = expr
+      | otherwise = made
     goRules :: Expression -> [Y.Rule] -> IO Expression
     goRules expr [] = goInside expr
     goRules expr (rule : rest) = do
diff --git a/src/Morph.hs b/src/Morph.hs
--- a/src/Morph.hs
+++ b/src/Morph.hs
@@ -10,7 +10,7 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Morph (Answer (..), Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, boxed, charged, counted, deeper, emptyState, ended, enter, entering, execBuildTerm, expired, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where
+module Morph (Answer (..), Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, awaited, boxed, charged, counted, deeper, emptyState, ended, enter, entering, execBuildTerm, expired, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where
 
 import AST
 import Builder (buildExpressionThrows, nameIn)
@@ -68,11 +68,11 @@
 
 data Answer
   = Answer Expression Expression
-  | Joined (Expression, Expression) Expression
+  | Joined Expression
 
 ended :: Answer -> Expression
 ended (Answer _ normal) = normal
-ended (Joined _ normal) = normal
+ended (Joined normal) = normal
 
 data Firing = Firing T.Text [Either Int Bytes] [Expression]
   deriving (Eq, Ord)
@@ -196,6 +196,13 @@
   ctx._saveEval (EvTimeout ctx._nesting cap ctx._judgment ctx._site)
   throwIO (OutOfTime cap)
 
+awaited :: ReduceContext -> IO a -> IO a
+awaited ctx action = case ctx._deadline of
+  Nothing -> action
+  Just (Deadline cap due) -> do
+    now <- getMonotonicTime
+    maybe (expired ctx cap) pure =<< timeout (ceiling (max 0 (due - now) * 1000000)) action
+
 memoized :: Maybe Acyclic -> IO (Maybe Memo)
 memoized (Just Plausible) = Just <$> (Memo <$> newIORef Map.empty <*> newIORef Map.empty <*> newIORef 0 <*> newIORef 0)
 memoized _ = pure Nothing
@@ -276,13 +283,7 @@
     remembered :: Acyclic -> IO (Either (Acyclic, Expression) ReduceContext)
     remembered mode =
       maybe (Right ctx{_entered = seenInsert (digest mode form) form ctx._entered}) (\before -> Left (mode, before))
-        <$> awaited (listToMaybe (drop ctx._maxLoops (filter (repeated mode form) (Map.findWithDefault [] (digest mode form) ctx._entered))))
-    awaited :: Maybe Expression -> IO (Maybe Expression)
-    awaited found = case ctx._deadline of
-      Nothing -> pure found
-      Just (Deadline cap due) -> do
-        now <- getMonotonicTime
-        maybe (expired ctx cap) pure =<< timeout (ceiling (max 0 (due - now) * 1000000)) (evaluate found)
+        <$> awaited ctx (evaluate (listToMaybe (drop ctx._maxLoops (filter (repeated mode form) (Map.findWithDefault [] (digest mode form) ctx._entered)))))
     digest :: Acyclic -> Expression -> Int
     digest Proven = hashShape
     digest Plausible = hashSkeleton
diff --git a/src/Regexp.hs b/src/Regexp.hs
--- a/src/Regexp.hs
+++ b/src/Regexp.hs
@@ -10,6 +10,7 @@
 import Data.Maybe (fromMaybe)
 import Text.Read (readMaybe)
 import qualified Text.Regex.PCRE.ByteString as R
+import qualified Text.Regex.PCRE.Wrap as W
 
 data Regex = Regex R.Regex R.Regex
 
@@ -87,28 +88,27 @@
       return $ B.concat [before, replacement, after]
 
 replaceAll :: Regex -> B.ByteString -> B.ByteString -> IO B.ByteString
-replaceAll (Regex first continuation) rep input = go True input B.empty
+replaceAll (Regex first _) rep input = go 0 B.empty
   where
-    go :: Bool -> B.ByteString -> B.ByteString -> IO B.ByteString
-    go initial bs acc = do
-      let regex = if initial then first else continuation
-      result <- R.execute regex bs
+    go :: Int -> B.ByteString -> IO B.ByteString
+    go cursor acc = do
+      result <- B.useAsCStringLen input (W.wrapMatch cursor first)
       case result of
         Left err -> regexExecutionFailed err
-        Right Nothing -> return $ B.append acc bs
-        Right (Just arr) -> do
-          let (off, len) = arr ! 0
-              (before, rest1) = B.splitAt off bs
-              (_, rest2) = B.splitAt len rest1
-          groups <- extractGroupsWith regex bs
-          let replacement = substituteGroups rep groups
+        Right (Just offsets@((off, end) : _)) -> do
+          let len = end - off
+              before = B.take (off - cursor) (B.drop cursor input)
+              rest = B.drop end input
+              groups = [if start < 0 then B.empty else B.take (finish - start) (B.drop start input) | (start, finish) <- offsets]
+              replacement = substituteGroups rep groups
           if len == 0
             then
-              let next = B.take (utf8Width rest2) rest2
+              let next = B.take (utf8Width rest) rest
                in if B.null next
                     then return $ B.concat [acc, before, replacement]
-                    else go False (B.drop (B.length next) rest2) (B.concat [acc, before, replacement, next])
-            else go False rest2 (B.concat [acc, before, replacement])
+                    else go (end + B.length next) (B.concat [acc, before, replacement, next])
+            else go end (B.concat [acc, before, replacement])
+        Right _ -> return $ B.append acc (B.drop cursor input)
     utf8Width :: B.ByteString -> Int
     utf8Width bytes =
       case B.uncons bytes of
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -435,11 +435,16 @@
               o <- case doc C.$/ C.element (toName "o") of
                 [single] -> pure single
                 _ -> throwIO (InvalidXMIRFormat "Expected single <o> element in <object>" doc)
-              let pckg =
-                    [ T.unpack t
+              let packages =
+                    [ meta
                     | meta <- doc C.$/ C.element (toName "metas") C.&/ C.element (toName "meta")
                     , let heads = meta C.$/ C.element (toName "head") C.&/ C.content
                     , heads == ["package"]
+                    ]
+              when (length packages > 1) (throwIO (InvalidXMIRFormat "A <metas> can hold only one package meta" doc))
+              let pckg =
+                    [ T.unpack t
+                    | meta <- packages
                     , tail' <- meta C.$/ C.element (toName "tail") C.&/ C.content
                     , t <- T.splitOn "." (T.strip tail')
                     ]
@@ -617,16 +622,10 @@
       let app
             | hasAttr "name" arg = throwIO (InvalidXMIRFormat "Application argument can't have @name attribute" arg)
             | hasAttr "base" arg && hasText arg = throwIO (InvalidXMIRFormat "It's illegal in XMIR to have @base and text() at the same time" arg)
-            | not (hasAttr "base" arg) && not (hasText arg) = do
-                bds <- mapM (\node -> xmirToFormationBinding derived node fqn) (arg C.$/ C.element (toName "o"))
-                key <- asToKey arg idx
-                pure (ExApplication expr (mkArg key (ExFormation bds)))
-            | not (hasAttr "base" arg) && hasText arg = do
+            | not (hasAttr "base" arg) = do
                 key <- asToKey arg idx
-                bytes <- getText arg
-                bds <- mapM (\node -> xmirToFormationBinding derived node fqn) (arg C.$/ C.element (toName "o"))
-                let delta = BiDelta (bytesToBts (T.unpack (T.strip (T.pack bytes))))
-                pure (ExApplication expr (mkArg key (ExFormation (delta : bds))))
+                arg' <- xmirToFormation derived arg fqn
+                pure (ExApplication expr (mkArg key arg'))
             | otherwise = do
                 key <- asToKey arg idx
                 arg' <- xmirToExpression derived arg fqn
@@ -641,9 +640,10 @@
       | hasAttr "as" cur = do
           as <- getAttr "as" cur
           case as of
-            'α' : rest' -> case TR.readMaybe rest' :: Maybe Int of
-              Just idx -> pure (Left (Alpha idx))
-              Nothing -> throwIO (InvalidXMIRFormat "The attribute started with 'α' must be followed by integer" cur)
+            'α' : rest' -> case TR.readMaybe rest' :: Maybe Integer of
+              Just idx
+                | all isDigit rest' && idx <= toInteger (maxBound :: Int) -> pure (Left (Alpha (fromInteger idx)))
+              _ -> throwIO (InvalidXMIRFormat (printf "The attribute started with 'α' must be followed by a non-negative integer that fits into %d" (maxBound :: Int)) cur)
             "ρ" -> throwIO (InvalidXMIRFormat "The 'ρ' in @as attribute is illegal in XMIR" cur)
             _ -> Right <$> toAttr as cur
       | otherwise = pure (Left (Alpha position))
diff --git a/test-resources/evaluate-packs/answers-its-own-sides-on-a-condition-another-join-read.yaml b/test-resources/evaluate-packs/answers-its-own-sides-on-a-condition-another-join-read.yaml
--- a/test-resources/evaluate-packs/answers-its-own-sides-on-a-condition-another-join-read.yaml
+++ b/test-resources/evaluate-packs/answers-its-own-sides-on-a-condition-another-join-read.yaml
@@ -105,7 +105,7 @@
             𝑛·3·8 := 7.0
             𝑛·3·9 := ⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), gt(x) ↦ L_number_gt:λ ⟧
             morphed 𝑛·3·10 := 𝑛·3·9
-          𝑛·3·11 := 𝑛·3·10  # 𝕄(ξ.then), 𝕄(ξ.else)
+          𝑛·3·11 := 𝑛·3·10
         boxed 𝑛·1·10 := 𝑛·3·11.φ
         𝕄(𝑛·1·10):
           𝑛·1·11 := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )
@@ -145,7 +145,7 @@
           𝑛·5·8 := 70.0
           𝑛·5·9 := ⟦ φ ↦ Φ.bytes( φ ↦ 40-51-80-00-00-00-00-00:Δ ), gt(x) ↦ L_number_gt:λ ⟧
           morphed 𝑛·5·10 := 𝑛·5·9
-        𝑛·5·11 := 𝑛·5·10  # 𝕄(ξ.then), 𝕄(ξ.else)
+        𝑛·5·11 := 𝑛·5·10
       𝑛2·1 := 𝑛·5·11  # 𝔼(𝑛1)
       𝑛·1·24 := 𝑛·5·11  # 𝑛
       𝕄(𝑛·1·24):
diff --git a/test-resources/evaluate-packs/binds-a-copy-over-no-bare-symbol-as-it-is.yaml b/test-resources/evaluate-packs/binds-a-copy-over-no-bare-symbol-as-it-is.yaml
--- a/test-resources/evaluate-packs/binds-a-copy-over-no-bare-symbol-as-it-is.yaml
+++ b/test-resources/evaluate-packs/binds-a-copy-over-no-bare-symbol-as-it-is.yaml
@@ -24,7 +24,6 @@
         𝑛·1·2 := ⟦ tup ↦ Φ.items.tail, φ ↦ tup.next ⟧
         morphed 𝑛·1·3 := 𝑛·1·2
       𝑛1·1 := 𝑛·1·3  # 𝕄(ξ.b)
-      𝑛2·1 := 𝑛·1·3  # 𝑛1
       𝑛·1·4 := 𝑛·1·3:φ  # 𝑛
       𝕄(𝑛·1·4):
         morphed 𝑛·1·5 := 𝑛·1·3:φ
diff --git a/test-resources/evaluate-packs/defers-a-copy-a-join-passed-through-stay-and-symbolize.yaml b/test-resources/evaluate-packs/defers-a-copy-a-join-passed-through-stay-and-symbolize.yaml
--- a/test-resources/evaluate-packs/defers-a-copy-a-join-passed-through-stay-and-symbolize.yaml
+++ b/test-resources/evaluate-packs/defers-a-copy-a-join-passed-through-stay-and-symbolize.yaml
@@ -54,15 +54,11 @@
             𝑛·2·3 := ⟦ tup ↦ Φ.items.tail, φ ↦ tup.next ⟧
             morphed 𝑛·2·4 := 𝑛·2·3
           𝑛2·2 := 𝑛·2·4  # 𝕄(ξ.b)
-          𝑛3·2 := 01-:Δ  # 𝑛1
-          𝑛4·2 := 𝑛·2·4  # 𝑛2
           symbolized 𝜎3 := 01-
-          𝑛5·2 := 𝜎3:λ  # symbolize(𝑛3)
-          𝑛7·2 := 𝑛5·2  # 𝑛5
-          𝑛6·2 := 𝑛·2·4  # 𝑛4
-          deferred 𝜎4 := Φ.step( tup ↦ 𝜎1:λ )  # 𝕄(𝑛6.φ)
+          𝑛5·2 := 𝜎3:λ  # symbolize(⟦ Δ ⤍ 01- ⟧)
+          deferred 𝜎4 := Φ.step( tup ↦ 𝜎1:λ )  # 𝕄(𝑛·2·4.φ)
           joined 𝜎5 := 𝛿1·2 ? 𝜎3 : 𝜎4
-          𝑛·2·5 := 𝜎5:λ  # 𝑛7, 𝑛8
+          𝑛·2·5 := 𝜎5:λ
         𝛿·1·1 := 𝔻(𝜎5:λ)
       𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.x)
       𝑛·1·1 := Φ.num( φ ↦ 𝜎6:λ )  # 𝑛
diff --git a/test-resources/evaluate-packs/fires-the-arguments-of-a-copy-a-defer-line-defers.yaml b/test-resources/evaluate-packs/fires-the-arguments-of-a-copy-a-defer-line-defers.yaml
--- a/test-resources/evaluate-packs/fires-the-arguments-of-a-copy-a-defer-line-defers.yaml
+++ b/test-resources/evaluate-packs/fires-the-arguments-of-a-copy-a-defer-line-defers.yaml
@@ -49,7 +49,6 @@
             𝑛·2·5 := ⟦ x ↦ Φ.items.tail, w ↦ Φ.inc( 2A-:Δ ), φ ↦ x.next ⟧
             morphed 𝑛·2·6 := 𝑛·2·5
           𝑛2·2 := 𝑛·2·6  # 𝕄(ξ.b)
-          𝑛3·2 := 𝑛1·2  # 𝑛1
           𝕄(𝑛2.w):
             𝑛·2·7 := Φ.inc( x ↦ 2A-:Δ )
             𝑛·2·8 := ⟦ x ↦ 2A-:Δ, λ ⤍ L_inc ⟧
@@ -66,7 +65,7 @@
             𝑛·3·5 := 𝑛·3·4  # 𝕄(𝑛·3·1)
           deferred 𝜎5 := Φ.box( x ↦ 𝜎1:λ, w ↦ 𝑛·3·5 )  # 𝕄(𝑛2.φ)
           joined 𝜎6 := 𝛿1·2 ? 𝜎3 : 𝜎5
-          𝑛·2·10 := 𝜎6:λ  # 𝑛3, 𝑛4
+          𝑛·2·10 := 𝜎6:λ
         𝛿·1·1 := 𝔻(𝜎6:λ)
       𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.x)
       𝑛·1·1 := Φ.num( φ ↦ 𝜎7:λ )  # 𝑛
diff --git a/test-resources/evaluate-packs/hands-a-named-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml b/test-resources/evaluate-packs/hands-a-named-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml
--- a/test-resources/evaluate-packs/hands-a-named-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml
+++ b/test-resources/evaluate-packs/hands-a-named-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml
@@ -48,5 +48,5 @@
       𝑛·2·5 := ⟦ x ↦ 𝜎2:λ, k ↦ x ⟧
       𝕄(ξ.right🌵):
         morphed 𝑛·2·6 := 𝑛·2·5
-      𝑛·2·7 := 𝑛·2·6  # 𝕄(ξ.left🌵), 𝕄(ξ.right🌵)
+      𝑛·2·7 := 𝑛·2·6
     morphed 𝑛·0·3 := 𝜎2:λ
diff --git a/test-resources/evaluate-packs/hands-a-positional-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml b/test-resources/evaluate-packs/hands-a-positional-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml
--- a/test-resources/evaluate-packs/hands-a-positional-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml
+++ b/test-resources/evaluate-packs/hands-a-positional-argument-to-both-sides-of-an-attribute-of-a-fabricated-formation.yaml
@@ -48,5 +48,5 @@
       𝑛·2·5 := ⟦ x ↦ 𝜎2:λ, k ↦ x ⟧
       𝕄(ξ.right🌵):
         morphed 𝑛·2·6 := 𝑛·2·5
-      𝑛·2·7 := 𝑛·2·6  # 𝕄(ξ.left🌵), 𝕄(ξ.right🌵)
+      𝑛·2·7 := 𝑛·2·6
     morphed 𝑛·0·3 := 𝜎2:λ
diff --git a/test-resources/evaluate-packs/hands-a-side-of-a-fabricated-formation-only-the-voids-its-attribute-leaves.yaml b/test-resources/evaluate-packs/hands-a-side-of-a-fabricated-formation-only-the-voids-its-attribute-leaves.yaml
--- a/test-resources/evaluate-packs/hands-a-side-of-a-fabricated-formation-only-the-voids-its-attribute-leaves.yaml
+++ b/test-resources/evaluate-packs/hands-a-side-of-a-fabricated-formation-only-the-voids-its-attribute-leaves.yaml
@@ -58,5 +58,5 @@
         morphed 𝑛·3·1 := 𝜎2:λ:φ
       𝕄(ξ.right🌵):
         morphed 𝑛·3·2 := 𝑛·3·1
-      𝑛·3·3 := 𝑛·3·1  # 𝕄(ξ.left🌵), 𝕄(ξ.right🌵)
+      𝑛·3·3 := 𝑛·3·1
     morphed 𝑛·0·3 := 𝜎2:λ
diff --git a/test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-down-two-decorators.yaml b/test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-down-two-decorators.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-down-two-decorators.yaml
@@ -0,0 +1,45 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# The bare symbol stands on the left this time, and the right side reaches its
+# data two decorators down, the way 'bool.and' of EO carries its argument 'x'
+# beside the φ of the 'false' it decorates. A 'cast' block finds the bare one
+# of its two terms by itself, casts it into a copy of the other with 𝜎2 in
+# place of 𝜎3 at the end of the φ chain, two steps down, and binds each meta
+# in the order its lines are written, so '𝑛3' takes the cast and '𝑛4' keeps
+# the right side as it is. The cast mints no symbol, and 𝜎2 stays what it
+# was (#2187).
+symbolic: |
+  - λ: L_fork
+    dataize:
+      𝛿1: $.c
+    morph:
+      𝑛1: $.a
+      𝑛2: $.b
+    cast:
+      𝑛3: 𝑛1
+      𝑛4: 𝑛2
+    join:
+      on: 𝛿1
+      left: 𝑛3
+      right: 𝑛4
+location: 'Q.y'
+input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧, λ ⤍ L_fork ⟧.φ ⟧'
+result: '⟦ φ ↦ 𝜎4:λ, if ↦ Φ.zu ⟧'
+protocol: |
+  𝕄(Φ.y):
+    𝔼(L_fork):
+      𝔻(ξ.c):
+        𝛿·1·1 := 𝔻(𝜎1:λ)
+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)
+      𝕄(ξ.a):
+        morphed 𝑛·1·1 := 𝜎2:λ
+      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.a)
+      𝕄(ξ.b):
+        morphed 𝑛·1·2 := ⟦ φ ↦ ⟦ φ ↦ 𝜎3:λ, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧
+      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
+      cast 𝑛3·1 := ⟦ φ ↦ ⟦ φ ↦ 𝜎2:λ, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧  # 𝑛1·1 up to 𝑛2·1
+      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
+      𝑛·1·3 := ⟦ φ ↦ ⟦ φ ↦ 𝜎4:λ, if ↦ Φ.zu ⟧, x ↦ Φ.ty ⟧
+    morphed 𝑛·0·1 := ⟦ φ ↦ 𝜎4:λ, if ↦ Φ.zu ⟧
diff --git a/test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-into-the-shape-of-a-decorator.yaml b/test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-into-the-shape-of-a-decorator.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/joins-a-bare-symbol-a-cast-brought-into-the-shape-of-a-decorator.yaml
@@ -0,0 +1,49 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# The right side is a bare symbol, a branch that already reached its data,
+# while the left side wraps its data in φ and holds 'k' beside it, a branch
+# one step short of its data. As they are, the two differ at .k, the right
+# side has λ, and the join diverges, even under 'otherwise' (#2187). A 'cast'
+# block reads its two metas as one pair and casts the bare symbol into a copy
+# of the left side with 𝜎3 in place of 𝜎2 at the end of its φ chain, so the
+# two sides differ in their symbols alone and the join makes one term of them.
+# The cast mints no symbol. The protocol writes the line of '𝑛20', which took
+# the cast, as 'cast 𝑛20·1 := …' with the meta it read and the meta whose
+# shape it took. The line of '𝑛19' binds its term as it is and writes
+# nothing (#2192).
+symbolic: |
+  - λ: L_fork
+    dataize:
+      𝛿1: $.on🌵
+    morph:
+      𝑛13: $.left🌵
+      𝑛14: $.right🌵
+    cast:
+      𝑛19: 𝑛13
+      𝑛20: 𝑛14
+    join:
+      on: 𝛿1
+      left: 𝑛19
+      right: 𝑛20
+      otherwise: L_fork
+location: 'Q.e1'
+input: '⟦ e1 ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, right🌵 ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧.φ ⟧'
+result: '𝜎4:λ'
+protocol: |
+  𝕄(Φ.e1):
+    𝔼(L_fork):
+      𝔻(ξ.on🌵):
+        𝛿·1·1 := 𝔻(𝜎1:λ)
+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
+      𝕄(ξ.left🌵):
+        morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎2:λ ⟧
+      𝑛13·1 := 𝑛·1·1  # 𝕄(ξ.left🌵)
+      𝕄(ξ.right🌵):
+        morphed 𝑛·1·2 := 𝜎3:λ
+      𝑛14·1 := 𝑛·1·2  # 𝕄(ξ.right🌵)
+      cast 𝑛20·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎3:λ ⟧  # 𝑛14·1 up to 𝑛13·1
+      joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
+      𝑛·1·3 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧
+    morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-a-bool-literal-a-rewrite-line-brought-into-the-shape-of-the-other-side.yaml b/test-resources/evaluate-packs/joins-a-bool-literal-a-rewrite-line-brought-into-the-shape-of-the-other-side.yaml
--- a/test-resources/evaluate-packs/joins-a-bool-literal-a-rewrite-line-brought-into-the-shape-of-the-other-side.yaml
+++ b/test-resources/evaluate-packs/joins-a-bool-literal-a-rewrite-line-brought-into-the-shape-of-the-other-side.yaml
@@ -10,8 +10,8 @@
 # side as it is, since none of its rules matches anything there. The two sides
 # then differ in their symbols alone, and the join makes one term of them.
 # The protocol writes the line of '𝑛3', which a rule changed, commented with
-# the block and the meta it read, and the line of '𝑛4', which changed nothing,
-# as the plain line of a meta bound to what another meta holds.
+# the block and the meta it read. The line of '𝑛4', which changed nothing,
+# writes nothing (#2192).
 symbolic: |
   - λ: L_fork
     dataize:
@@ -53,7 +53,6 @@
         morphed 𝑛·1·2 := ⟦ φ ↦ 𝜎3:λ, kq ↦ Φ.bool( if ↦ 01-:Δ ) ⟧
       𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
       𝑛3·1 := ⟦ φ ↦ 𝜎2:λ, kq ↦ Φ.bool( if ↦ 01-:Δ ) ⟧  # rewrite(𝑛1)
-      𝑛4·1 := 𝑛2·1  # 𝑛2
       joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
-      𝑛·1·3 := ⟦ φ ↦ 𝜎4:λ, kq ↦ Φ.bool( if ↦ 01-:Δ ) ⟧  # 𝑛3, 𝑛4
+      𝑛·1·3 := ⟦ φ ↦ 𝜎4:λ, kq ↦ Φ.bool( if ↦ 01-:Δ ) ⟧
     morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-a-bottom-into-the-shape-of-the-other-side.yaml b/test-resources/evaluate-packs/joins-a-bottom-into-the-shape-of-the-other-side.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/joins-a-bottom-into-the-shape-of-the-other-side.yaml
@@ -0,0 +1,41 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# The left side is ⊥ and the right side wraps its symbol in φ beside 'k', the
+# way the 'bytes' object a branch of EO comes to holds its data. The join
+# keeps the shape of the right side and takes ⊥ for the symbol at its leaf:
+# it mints 𝜎3 to stand for ⊥ and 𝜎4 for 𝜎2 against it, writes 𝜎3 on the
+# left of the condition with a comment saying it is ⊥, and answers the right
+# side with 𝜎4 in place of 𝜎2, so a method the run asks the answer for later
+# is still there (#2195).
+symbolic: |
+  - λ: L_fork
+    dataize:
+      𝛿1: $.on🌵
+    morph:
+      𝑛1: $.left🌵
+      𝑛2: $.right🌵
+    join:
+      on: 𝛿1
+      left: 𝑛1
+      right: 𝑛2
+      otherwise: L_fork
+location: 'Q.e1'
+input: '⟦ e1 ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⊥, right🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ⟧.φ ⟧'
+result: '𝜎4:λ'
+protocol: |
+  𝕄(Φ.e1):
+    𝔼(L_fork):
+      𝔻(ξ.on🌵):
+        𝛿·1·1 := 𝔻(𝜎1:λ)
+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
+      𝕄(ξ.left🌵):
+        morphed 𝑛·1·1 := ⊥
+      𝑛1·1 := ⊥  # 𝕄(ξ.left🌵)
+      𝕄(ξ.right🌵):
+        morphed 𝑛·1·2 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎2:λ ⟧
+      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.right🌵)
+      joined 𝜎4 := 𝛿1·1 ? 𝜎3 : 𝜎2  # where 𝜎3 is ⊥
+      𝑛·1·3 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧
+    morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-a-number-with-a-formation-an-undress-took-the-number-out-of.yaml b/test-resources/evaluate-packs/joins-a-number-with-a-formation-an-undress-took-the-number-out-of.yaml
--- a/test-resources/evaluate-packs/joins-a-number-with-a-formation-an-undress-took-the-number-out-of.yaml
+++ b/test-resources/evaluate-packs/joins-a-number-with-a-formation-an-undress-took-the-number-out-of.yaml
@@ -52,7 +52,7 @@
       symbolized 𝜎3 := 40-1C-00-00-00-00-00-00  # 7.0
       𝑛4·1 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎3:λ ), neg ↦ ρ:φ ⟧  # symbolize(𝑛2)
       joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
-      𝑛·1·9 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ), neg ↦ ρ:φ ⟧  # 𝑛3, 𝑛4
+      𝑛·1·9 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ), neg ↦ ρ:φ ⟧
     𝑛·0·1 := Φ.bytes( φ ↦ 𝜎4:λ )
     𝑛·0·2 := 𝜎4:λ:φ
     morphed 𝑛·0·3 := 𝑛·0·2
diff --git a/test-resources/evaluate-packs/joins-a-side-a-morph-line-brought-down-from-what-a-rewrite-line-unwrapped.yaml b/test-resources/evaluate-packs/joins-a-side-a-morph-line-brought-down-from-what-a-rewrite-line-unwrapped.yaml
--- a/test-resources/evaluate-packs/joins-a-side-a-morph-line-brought-down-from-what-a-rewrite-line-unwrapped.yaml
+++ b/test-resources/evaluate-packs/joins-a-side-a-morph-line-brought-down-from-what-a-rewrite-line-unwrapped.yaml
@@ -51,5 +51,5 @@
         morphed 𝑛·1·3 := 𝜎3:λ:φ
       𝑛4·1 := 𝑛·1·3  # 𝕄(𝑛3)
       joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3
-      𝑛·1·4 := 𝜎4:λ:φ  # 𝑛1, 𝑛4
+      𝑛·1·4 := 𝜎4:λ:φ
     morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-a-side-an-evaluate-line-fired-with-a-bool-it-left-as-it-is.yaml b/test-resources/evaluate-packs/joins-a-side-an-evaluate-line-fired-with-a-bool-it-left-as-it-is.yaml
--- a/test-resources/evaluate-packs/joins-a-side-an-evaluate-line-fired-with-a-bool-it-left-as-it-is.yaml
+++ b/test-resources/evaluate-packs/joins-a-side-an-evaluate-line-fired-with-a-bool-it-left-as-it-is.yaml
@@ -49,7 +49,6 @@
           morphed 𝑛·2·4 := 𝑛·2·3
         𝑛·2·5 := 𝑛·2·4  # 𝕄(𝑛·2·1)
       𝑛3·1 := 𝑛·2·5  # 𝔼(𝑛1)
-      𝑛4·1 := 𝑛2·1  # 𝔼(𝑛2)
       joined 𝜎4 := 𝛿1·1 ? 𝜎3 : 𝜎2
-      𝑛·1·5 := 𝜎4:λ:φ  # 𝑛3, 𝑛4
+      𝑛·1·5 := 𝜎4:λ:φ
     morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-a-side-holding-a-datum-a-symbolize-turned-into-a-symbol.yaml b/test-resources/evaluate-packs/joins-a-side-holding-a-datum-a-symbolize-turned-into-a-symbol.yaml
--- a/test-resources/evaluate-packs/joins-a-side-holding-a-datum-a-symbolize-turned-into-a-symbol.yaml
+++ b/test-resources/evaluate-packs/joins-a-side-holding-a-datum-a-symbolize-turned-into-a-symbol.yaml
@@ -8,9 +8,9 @@
 # value alone, yet no join makes one term of a datum and a symbol (#1968). A
 # 'symbolize' line turns every datum of a term into a fresh symbol, so '𝑛3'
 # holds 𝜎4 where '𝑛1' held the datum, and the protocol writes that 𝜎4 stands
-# for that datum. The line of '𝑛4', whose term holds no datum, is commented
-# with '𝑛2' alone. The join takes the metas the 'symbolize' lines bound and
-# joins 𝜎4 with 𝜎2 into one fresh symbol 𝜎5.
+# for that datum. The line of '𝑛4', whose term holds no datum, writes nothing
+# (#2192). The join takes the metas the 'symbolize' lines bound and joins 𝜎4
+# with 𝜎2 into one fresh symbol 𝜎5.
 symbolic: |
   - λ: L_fork
     dataize:
@@ -42,9 +42,8 @@
       𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
       symbolized 𝜎4 := 3F-F0-00-00-00-00-00-00  # 1.0
       𝑛3·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) ):φ  # symbolize(𝑛1)
-      𝑛4·1 := 𝑛2·1  # 𝑛2
       joined 𝜎5 := 𝛿1·1 ? 𝜎4 : 𝜎2
-      𝑛·1·3 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎5:λ ) ):φ  # 𝑛3, 𝑛4
+      𝑛·1·3 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎5:λ ) ):φ
     𝑛·0·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎5:λ ) )
     𝑛·0·2 := Φ.bytes( φ ↦ 𝜎5:λ ):φ
     morphed 𝑛·0·3 := 𝑛·0·2
diff --git a/test-resources/evaluate-packs/joins-a-side-reading-the-rho-it-binds-in-a-fabricated-formation.yaml b/test-resources/evaluate-packs/joins-a-side-reading-the-rho-it-binds-in-a-fabricated-formation.yaml
--- a/test-resources/evaluate-packs/joins-a-side-reading-the-rho-it-binds-in-a-fabricated-formation.yaml
+++ b/test-resources/evaluate-packs/joins-a-side-reading-the-rho-it-binds-in-a-fabricated-formation.yaml
@@ -46,5 +46,5 @@
       𝕄(ξ.right🌵):
         morphed 𝑛·2·4 := 𝜎3:λ:k
       joined 𝜎4 := ξ.on🌵 ? 𝜎2 : 𝜎3
-      𝑛·2·5 := 𝜎4:λ:k  # 𝕄(ξ.left🌵), 𝕄(ξ.right🌵)
+      𝑛·2·5 := 𝜎4:λ:k
     morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-a-side-whose-void-the-fabricated-formation-holds.yaml b/test-resources/evaluate-packs/joins-a-side-whose-void-the-fabricated-formation-holds.yaml
--- a/test-resources/evaluate-packs/joins-a-side-whose-void-the-fabricated-formation-holds.yaml
+++ b/test-resources/evaluate-packs/joins-a-side-whose-void-the-fabricated-formation-holds.yaml
@@ -47,5 +47,5 @@
       𝕄(ξ.right🌵):
         morphed 𝑛·2·4 := 𝜎3:λ:k
       joined 𝜎4 := ξ.on🌵 ? 𝜎2 : 𝜎3
-      𝑛·2·5 := 𝜎4:λ:k  # 𝕄(ξ.left🌵), 𝕄(ξ.right🌵)
+      𝑛·2·5 := 𝜎4:λ:k
     morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-again-the-attribute-of-a-fabricated-formation.yaml b/test-resources/evaluate-packs/joins-again-the-attribute-of-a-fabricated-formation.yaml
--- a/test-resources/evaluate-packs/joins-again-the-attribute-of-a-fabricated-formation.yaml
+++ b/test-resources/evaluate-packs/joins-again-the-attribute-of-a-fabricated-formation.yaml
@@ -48,5 +48,5 @@
         𝑛·2·5 := ⟦ ke ↦ 𝜎3:λ, φ ↦ ke ⟧
         morphed 𝑛·2·6 := 𝑛·2·5
       joined 𝜎4 := ξ.on🌵 ? 𝜎2 : 𝜎3
-      𝑛·2·7 := ⟦ ke ↦ 𝜎4:λ, φ ↦ ke ⟧  # 𝕄(ξ.left🌵), 𝕄(ξ.right🌵)
+      𝑛·2·7 := ⟦ ke ↦ 𝜎4:λ, φ ↦ ke ⟧
     morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-an-attribute-named-left-of-a-copy-in-a-fabricated-formation.yaml b/test-resources/evaluate-packs/joins-an-attribute-named-left-of-a-copy-in-a-fabricated-formation.yaml
--- a/test-resources/evaluate-packs/joins-an-attribute-named-left-of-a-copy-in-a-fabricated-formation.yaml
+++ b/test-resources/evaluate-packs/joins-an-attribute-named-left-of-a-copy-in-a-fabricated-formation.yaml
@@ -45,5 +45,5 @@
       𝕄(ξ.right🌵):
         morphed 𝑛·2·2 := 𝜎3:λ:left
       joined 𝜎4 := ξ.on🌵 ? 𝜎2 : 𝜎3
-      𝑛·2·3 := 𝜎4:λ:left  # 𝕄(ξ.left🌵), 𝕄(ξ.right🌵)
+      𝑛·2·3 := 𝜎4:λ:left
     morphed 𝑛·0·1 := 𝜎4:λ
diff --git a/test-resources/evaluate-packs/joins-two-numbers-into-one-symbol-keeping-the-constant-a-method-holds.yaml b/test-resources/evaluate-packs/joins-two-numbers-into-one-symbol-keeping-the-constant-a-method-holds.yaml
--- a/test-resources/evaluate-packs/joins-two-numbers-into-one-symbol-keeping-the-constant-a-method-holds.yaml
+++ b/test-resources/evaluate-packs/joins-two-numbers-into-one-symbol-keeping-the-constant-a-method-holds.yaml
@@ -45,9 +45,8 @@
       𝑛2·1 := 𝑛·1·6  # 𝕄(ξ.b)
       symbolized 𝜎4 := 40-45-00-00-00-00-00-00  # 42.0
       𝑛3·1 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ), neg ↦ ρ.times( x ↦ -1.0 ):φ ⟧  # symbolize(𝑛1)
-      𝑛4·1 := 𝑛2·1  # 𝑛2
       joined 𝜎5 := 𝛿1·1 ? 𝜎4 : 𝜎2
-      𝑛·1·7 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎5:λ ), neg ↦ ρ.times( x ↦ -1.0 ):φ ⟧  # 𝑛3, 𝑛4
+      𝑛·1·7 := ⟦ φ ↦ Φ.bytes( φ ↦ 𝜎5:λ ), neg ↦ ρ.times( x ↦ -1.0 ):φ ⟧
     𝑛·0·1 := Φ.bytes( φ ↦ 𝜎5:λ )
     𝑛·0·2 := 𝜎5:λ:φ
     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
@@ -12,7 +12,7 @@
 # symbols alone. The join takes the metas the 'stay' lines bound as they are
 # and makes one term of them with a fresh symbol.
 # The protocol comments the line of '𝑛3', which dropped a tail, with
-# 'stay(𝑛1)', and the line of '𝑛4', which dropped nothing, with '𝑛2' alone.
+# 'stay(𝑛1)'. The line of '𝑛4', which dropped nothing, writes nothing (#2192).
 symbolic: |
   - λ: L_fork
     dataize:
@@ -44,9 +44,8 @@
         morphed 𝑛·1·2 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ):φ
       𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
       𝑛3·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ):φ  # stay(𝑛1)
-      𝑛4·1 := 𝑛2·1  # 𝑛2
       joined 𝜎4 := 𝛿1·1 ? 𝜎1 : 𝜎2
-      𝑛·1·3 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) ):φ  # 𝑛3, 𝑛4
+      𝑛·1·3 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) ):φ
     𝑛·0·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) )
     𝑛·0·2 := Φ.bytes( φ ↦ 𝜎4:λ ):φ
     morphed 𝑛·0·3 := 𝑛·0·2
diff --git a/test-resources/evaluate-packs/joins-two-sides-differing-in-a-datum-a-symbolize-found-off-the-phi-chain.yaml b/test-resources/evaluate-packs/joins-two-sides-differing-in-a-datum-a-symbolize-found-off-the-phi-chain.yaml
--- a/test-resources/evaluate-packs/joins-two-sides-differing-in-a-datum-a-symbolize-found-off-the-phi-chain.yaml
+++ b/test-resources/evaluate-packs/joins-two-sides-differing-in-a-datum-a-symbolize-found-off-the-phi-chain.yaml
@@ -42,9 +42,8 @@
       𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
       symbolized 𝜎3 := FF-
       𝑛3·1 := Φ.bool( if ↦ 𝜎3:λ:φ ):φ  # symbolize(𝑛1)
-      𝑛4·1 := 𝑛·1·2  # 𝑛2
       joined 𝜎4 := 𝛿1·1 ? 𝜎3 : 𝜎2
-      𝑛·1·3 := Φ.bool( if ↦ 𝜎4:λ:φ ):φ  # 𝑛3, 𝑛4
+      𝑛·1·3 := Φ.bool( if ↦ 𝜎4:λ:φ ):φ
     𝑛·0·1 := Φ.bool( if ↦ 𝜎4:λ:φ )
     𝑛·0·2 := ⟦ if ↦ 𝜎4:λ:φ, φ ↦ if ⟧
     morphed 𝑛·0·3 := 𝑛·0·2
diff --git a/test-resources/evaluate-packs/joins-two-sides-that-differ-only-in-symbols.yaml b/test-resources/evaluate-packs/joins-two-sides-that-differ-only-in-symbols.yaml
--- a/test-resources/evaluate-packs/joins-two-sides-that-differ-only-in-symbols.yaml
+++ b/test-resources/evaluate-packs/joins-two-sides-that-differ-only-in-symbols.yaml
@@ -170,7 +170,7 @@
         𝑛·2·17 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧
         morphed 𝑛·2·18 := 𝑛·2·17
       joined 𝜎4 := 𝛿1·2 ? 𝜎2 : 𝜎3
-      𝑛·2·19 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧  # 𝕄(ξ.then), 𝕄(ξ.else)
+      𝑛·2·19 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧
     𝔼(L_number_plus):
       𝔻(ξ.ρ):
         𝕄(ξ.ρ):
diff --git a/test-resources/evaluate-packs/leaves-a-bare-symbol-an-evaluate-line-meets-as-it-is.yaml b/test-resources/evaluate-packs/leaves-a-bare-symbol-an-evaluate-line-meets-as-it-is.yaml
--- a/test-resources/evaluate-packs/leaves-a-bare-symbol-an-evaluate-line-meets-as-it-is.yaml
+++ b/test-resources/evaluate-packs/leaves-a-bare-symbol-an-evaluate-line-meets-as-it-is.yaml
@@ -22,9 +22,8 @@
       𝕄(ξ.x):
         morphed 𝑛·1·1 := 𝜎4:λ
       𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.x)
-      𝑛2·1 := 𝑛1·1  # 𝔼(𝑛1)
       𝑛·1·2 := 𝜎4:λ:φ  # 𝑛
       𝕄(𝑛·1·2):
         morphed 𝑛·1·3 := 𝜎4:λ:φ
       𝑛·1·4 := 𝑛·1·3  # 𝕄(𝑛·1·2)
-    morphed 𝑛·0·1 := 𝑛2·1
+    morphed 𝑛·0·1 := 𝑛1·1
diff --git a/test-resources/evaluate-packs/leaves-a-bare-symbol-uncast-against-a-side-holding-a-symbol-off-its-phi-chain.yaml b/test-resources/evaluate-packs/leaves-a-bare-symbol-uncast-against-a-side-holding-a-symbol-off-its-phi-chain.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/evaluate-packs/leaves-a-bare-symbol-uncast-against-a-side-holding-a-symbol-off-its-phi-chain.yaml
@@ -0,0 +1,39 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# yamllint disable rule:line-length
+# The right side ends its φ chain in a bare symbol, but it holds another one
+# under 'ke', off that chain. A cast would copy that symbol into the left side
+# too, as if the left branch knew it, so a 'cast' block casts nothing here and
+# binds both metas to their terms as they are. The join then diverges as it
+# would with no 'cast' block at all (#2187).
+symbolic: |
+  - λ: L_fork
+    dataize:
+      𝛿1: $.c
+    morph:
+      𝑛1: $.a
+      𝑛2: $.b
+    cast:
+      𝑛3: 𝑛1
+      𝑛4: 𝑛2
+    join:
+      on: 𝛿1
+      left: 𝑛3
+      right: 𝑛4
+location: 'Q.y'
+input: '⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧, ke ↦ ⟦ λ ⤍ 𝜎4 ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'
+fails: "No entry of --symbolic answers the λ function 'L_fork'"
+protocol: |
+  𝕄(Φ.y):
+    𝔼(L_fork):
+      𝔻(ξ.c):
+        𝛿·1·1 := 𝔻(𝜎1:λ)
+      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.c)
+      𝕄(ξ.a):
+        morphed 𝑛·1·1 := 𝜎2:λ
+      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.a)
+      𝕄(ξ.b):
+        morphed 𝑛·1·2 := ⟦ φ ↦ 𝜎3:λ, ke ↦ 𝜎4:λ ⟧
+      𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
+      diverged 𝜎2:λ vs 𝑛2·1  # they differ at .λ, and the join names no otherwise
diff --git a/test-resources/evaluate-packs/passes-a-side-that-is-no-formation-through-an-evaluate-line-to-the-join.yaml b/test-resources/evaluate-packs/passes-a-side-that-is-no-formation-through-an-evaluate-line-to-the-join.yaml
--- a/test-resources/evaluate-packs/passes-a-side-that-is-no-formation-through-an-evaluate-line-to-the-join.yaml
+++ b/test-resources/evaluate-packs/passes-a-side-that-is-no-formation-through-an-evaluate-line-to-the-join.yaml
@@ -49,7 +49,5 @@
         morphed 𝑛·1·2 := Φ.j:φ
       𝑛2·1 := 𝑛·1·2  # 𝕄(ξ.b)
       𝑛3·1 := Φ.k  # rewrite(𝑛1)
-      𝑛5·1 := Φ.k  # 𝔼(𝑛3)
       𝑛4·1 := Φ.j  # rewrite(𝑛2)
-      𝑛6·1 := Φ.j  # 𝔼(𝑛4)
-      diverged 𝑛5·1 vs 𝑛6·1  # the join names no otherwise
+      diverged Φ.k vs Φ.j  # the join names no otherwise
diff --git a/test-resources/evaluate-packs/takes-the-one-term-both-sides-of-a-join-come-to.yaml b/test-resources/evaluate-packs/takes-the-one-term-both-sides-of-a-join-come-to.yaml
--- a/test-resources/evaluate-packs/takes-the-one-term-both-sides-of-a-join-come-to.yaml
+++ b/test-resources/evaluate-packs/takes-the-one-term-both-sides-of-a-join-come-to.yaml
@@ -3,8 +3,7 @@
 ---
 # yamllint disable rule:line-length
 # A join whose two sides come to the same normal form through 𝕄 has
-# nothing to join (#1954): it mints no symbol and answers that one term,
-# commented with both sides it came from.
+# nothing to join (#1954): it mints no symbol and answers that one term.
 symbolic: |
   - λ: L_number_gt
     dataize:
@@ -96,7 +95,7 @@
         𝑛·2·12 := 𝑛·2·10.plus( x ↦ 2.0 )
         𝑛·2·13 := ⟦ x ↦ 2.0, λ ⤍ L_number_plus ⟧
         morphed 𝑛·2·14 := 𝑛·2·13
-      𝑛·2·15 := 𝑛·2·13  # 𝕄(ξ.then), 𝕄(ξ.else)
+      𝑛·2·15 := 𝑛·2·13
     𝔼(L_number_plus):
       𝔻(ξ.ρ):
         𝕄(ξ.ρ):
diff --git a/test-resources/evaluate-packs/writes-no-joined-line-for-a-join-the-memo-answered.yaml b/test-resources/evaluate-packs/writes-no-joined-line-for-a-join-the-memo-answered.yaml
--- a/test-resources/evaluate-packs/writes-no-joined-line-for-a-join-the-memo-answered.yaml
+++ b/test-resources/evaluate-packs/writes-no-joined-line-for-a-join-the-memo-answered.yaml
@@ -173,7 +173,7 @@
         𝑛·2·17 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧
         morphed 𝑛·2·18 := 𝑛·2·17
       joined 𝜎4 := 𝛿1·2 ? 𝜎2 : 𝜎3
-      𝑛·2·19 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧  # 𝕄(ξ.then), 𝕄(ξ.else)
+      𝑛·2·19 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧
     𝔼(L_number_plus):
       𝔻(ξ.ρ):
         𝕄(ξ.ρ):
@@ -228,7 +228,7 @@
           𝑛·6·12 := ⟦ then ↦ 𝑛·3·1.plus( 𝑛·3·9 ).plus( 𝑛·5·5 ), else ↦ 𝑛·4·1.plus( 𝑛·4·9 ).plus( 𝑛·5·5 ), λ ⤍ L_fork ⟧
           morphed 𝑛·6·13 := 𝑛·6·12
         𝔼(L_fork):
-          𝑛·8·1 := ⟦ x ↦ 𝑛·5·5, λ ⤍ L_number_plus ⟧  # 𝕄(ξ.then), 𝕄(ξ.else)
+          𝑛·8·1 := ⟦ x ↦ 𝑛·5·5, λ ⤍ L_number_plus ⟧
         𝔼(L_number_plus):
           𝑛·9·1 := 𝑛·6·1  # 𝑛
           𝑛·9·2 := 𝑛·5·17  # 𝕄(𝑛·9·1)
diff --git a/test-resources/xmir-parsing-packs/alpha-max-int-application-arg.yaml b/test-resources/xmir-parsing-packs/alpha-max-int-application-arg.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/xmir-parsing-packs/alpha-max-int-application-arg.yaml
@@ -0,0 +1,10 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+xmir: |
+  <object>
+    <o name="x" base="Φ.f">
+      <o as="α9223372036854775807" base="Φ.y"/>
+    </o>
+  </object>
+phi: '⟦ x ↦ Φ.f( α9223372036854775807 ↦ Φ.y ) ⟧'
diff --git a/test-resources/xmir-parsing-packs/alpha-negative-application-arg.yaml b/test-resources/xmir-parsing-packs/alpha-negative-application-arg.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/xmir-parsing-packs/alpha-negative-application-arg.yaml
@@ -0,0 +1,11 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+failure: true
+xmir: |
+  <object>
+    <o name="x" base="Φ.f">
+      <o as="α-1" base="Φ.y"/>
+    </o>
+  </object>
+phi: ''
diff --git a/test-resources/xmir-parsing-packs/alpha-overflow-application-arg.yaml b/test-resources/xmir-parsing-packs/alpha-overflow-application-arg.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/xmir-parsing-packs/alpha-overflow-application-arg.yaml
@@ -0,0 +1,11 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+failure: true
+xmir: |
+  <object>
+    <o name="x" base="Φ.f">
+      <o as="α18446744073709551616" base="Φ.y"/>
+    </o>
+  </object>
+phi: ''
diff --git a/test-resources/xmir-parsing-packs/two-package-metas.yaml b/test-resources/xmir-parsing-packs/two-package-metas.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/xmir-parsing-packs/two-package-metas.yaml
@@ -0,0 +1,21 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+failure: true
+xmir: |
+  <object>
+    <metas>
+      <meta>
+        <head>package</head>
+        <tail>a</tail>
+        <part>a</part>
+      </meta>
+      <meta>
+        <head>package</head>
+        <tail>b</tail>
+        <part>b</part>
+      </meta>
+    </metas>
+    <o name="x"/>
+  </object>
+phi: ''
diff --git a/test-resources/xmir-parsing-packs/two-same-package-metas.yaml b/test-resources/xmir-parsing-packs/two-same-package-metas.yaml
new file mode 100644
--- /dev/null
+++ b/test-resources/xmir-parsing-packs/two-same-package-metas.yaml
@@ -0,0 +1,21 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+failure: true
+xmir: |
+  <object>
+    <metas>
+      <meta>
+        <head>package</head>
+        <tail>a</tail>
+        <part>a</part>
+      </meta>
+      <meta>
+        <head>package</head>
+        <tail>a</tail>
+        <part>a</part>
+      </meta>
+    </metas>
+    <o name="x"/>
+  </object>
+phi: ''
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -1433,7 +1433,7 @@
       testCLISucceeded ["dataize", "--help"] ["Dataize the 𝜑-expression"]
 
     it "names every block of a --symbolic entry in its help" $
-      testCLISucceeded ["dataize", "--help"] ["\"dataize\"", "\"morph\"", "\"evaluate\"", "\"defer\"", "\"stay\"", "\"rewrite\"", "\"symbolize\"", "\"join\""]
+      testCLISucceeded ["dataize", "--help"] ["\"dataize\"", "\"morph\"", "\"evaluate\"", "\"defer\"", "\"stay\"", "\"rewrite\"", "\"symbolize\"", "\"cast\"", "\"join\""]
 
     it "dataizes simple expression" $
       withStdin "[[ D> 01- ]]" $
@@ -3093,6 +3093,19 @@
         printed <- dataized "⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧, λ ⤍ L_fork ⟧ ⟧"
         length (lines printed) `shouldBe` 1
 
+      it "dataizes a side and ⊥ into the symbol the join minted for both" $ do
+        printed <- dataized "⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⊥, λ ⤍ L_fork ⟧ ⟧"
+        lines printed `shouldBe` ["40-45-00-00-00-00-00-00"]
+
+      it "writes the symbol a join minted for a side and ⊥ beside a symbol standing for ⊥" $
+        withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
+          hClose stream
+          withLambdasOf joining $ \joins ->
+            withStdin "⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⊥, λ ⤍ L_fork ⟧ ⟧" $
+              testCLISucceeded ["dataize", "--symbolic=" ++ joins, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
+          records <- readProtocol path
+          lines records `shouldContain` ["    joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3  # where 𝜎3 is ⊥"]
+
     describe "--inside" $ do
       let universe = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]"
       it "dataizes an expression the input does not contain" $
@@ -3553,9 +3566,8 @@
                      , "      <morphed meta=\"𝑛·1·4\">𝑛·1·3</morphed>"
                      , "    </morph>"
                      , "    <bound meta=\"𝑛2·1\">𝑛·1·4</bound>"
-                     , "    <bound meta=\"𝑛3·1\">01-</bound>"
                      , "    <deferred symbol=\"𝜎3\" by=\"morph\" at=\"𝑛2.φ\" of=\"Φ.step\"><with><symbol attr=\"tup\">𝜎1</symbol></with></deferred>"
-                     , "    <diverged left=\"𝑛3·1\" right=\"𝜎3\" at=\".Δ\" reason=\"the join names no otherwise\"/>"
+                     , "    <diverged left=\"01-\" right=\"𝜎3\" at=\".Δ\" reason=\"the join names no otherwise\"/>"
                      , "  </evaluate>"
                      , "</dataize>"
                      ]
diff --git a/test/DepsSpec.hs b/test/DepsSpec.hs
--- a/test/DepsSpec.hs
+++ b/test/DepsSpec.hs
@@ -12,7 +12,7 @@
 import Data.List (isInfixOf, isPrefixOf)
 import Data.Time (LocalTime (LocalTime), TimeOfDay (TimeOfDay), ZonedTime (ZonedTime), fromGregorian, hoursToTimeZone)
 import Data.Time.Clock.POSIX (getPOSIXTime)
-import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBound, EvBoxed, EvBuilt, EvData, EvDeferred, EvDelta, EvDiverged, EvFabricated, EvFiring, EvHeader, EvJoined, EvLooped, EvManufactured, EvMorphed, EvReshaped, EvRun, EvStarted, EvStuck, EvStuckOn, EvSymbolized, EvTaken, EvTerm, EvUndressed, EvWorld), Header (Header), Judgment (Dataization, Morphing), Nesting (..), Protocol (..), World (World), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep)
+import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBound, EvBoxed, EvBuilt, EvCast, EvData, EvDeferred, EvDelta, EvDiverged, EvFabricated, EvFiring, EvHeader, EvJoined, EvLooped, EvManufactured, EvMorphed, EvReshaped, EvRun, EvStarted, EvStuck, EvStuckOn, EvSymbolized, EvTaken, EvTerm, EvUndressed, EvWorld), Header (Header), Judgment (Dataization, Evaluation, Morphing), Nesting (..), Protocol (..), World (World), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep)
 import Fixtures (readUtf8, recorded, recordedWhole, recordedXml)
 import Forks (Refusal (..), Side (..))
 import GHC.Clock (getMonotonicTime)
@@ -250,7 +250,7 @@
       (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_выдра" Dataization ExRoot, EvBuilt 2 (ExFormation [BiTau (AtLabel "кот") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "кот"))]), EvMorphed 2 (ExFormation [BiTau (AtLabel "кот") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "кот"))]), EvAnswer 2 (ExFormation [BiTau (AtLabel "кот") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "кот"))]), EvBoxed 1 (ExDispatch (ExFormation [BiTau (AtLabel "кот") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "кот"))]) AtPhi)])
       last (lines written) `shouldBe` "  boxed 𝑛·0·1 := 𝑛·1·3.φ"
     it "names the answer of a join by its line in the box step that takes its φ" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_клёст" Dataization ExRoot, EvTaken 2 [ExDispatch ExXi (AtLabel "then")] (ExFormation [BiTau (AtLabel "жук") (ExFormation [BiLambda (FnSymbol 7)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "жук"))]), EvBoxed 1 (ExDispatch (ExFormation [BiTau (AtLabel "жук") (ExFormation [BiLambda (FnSymbol 7)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "жук"))]) AtPhi)])
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_клёст" Dataization ExRoot, EvTaken 2 (ExFormation [BiTau (AtLabel "жук") (ExFormation [BiLambda (FnSymbol 7)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "жук"))]), EvBoxed 1 (ExDispatch (ExFormation [BiTau (AtLabel "жук") (ExFormation [BiLambda (FnSymbol 7)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "жук"))]) AtPhi)])
       last (lines written) `shouldBe` "  boxed 𝑛·0·1 := 𝑛·1·1.φ"
     it "keeps the mode of a cut made at the site of its block" $ do
       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation []) ExRoot])
@@ -264,18 +264,9 @@
     it "writes a deferred copy as it stands when no object of the world made it" $ do
       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvDeferred 1 9 Morphing (ExFormation [BiTau (AtLabel "щ") (ExFormation [BiLambda (FnSymbol 4)]), BiTau AtPhi (ExDispatch (ExDispatch ExXi (AtLabel "щ")) (AtLabel "й"))]) Nothing ExRoot])
       last (lines written) `shouldBe` "  deferred 𝜎9 := ⟦ щ ↦ 𝜎4:λ, φ ↦ щ.й ⟧"
-    it "writes the term a join came to as the answer of its firing" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 [ExDispatch ExXi (AtLabel "then")] (ExFormation [BiLambda (FnSymbol 3)])])
-      last (lines written) `shouldBe` "    𝑛·1·1 := 𝜎3:λ  # 𝕄(ξ.then)"
-    it "writes the term both sides of a join came to beside both of them" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 [ExDispatch ExXi (AtLabel "then"), ExDispatch ExXi (AtLabel "else")] (ExFormation [BiLambda (FnSymbol 3)])])
-      last (lines written) `shouldBe` "    𝑛·1·1 := 𝜎3:λ  # 𝕄(ξ.then), 𝕄(ξ.else)"
-    it "writes the side a join read from a meta beside that meta alone" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 [ExMeta "n3"] (ExFormation [BiLambda (FnSymbol 3)])])
-      last (lines written) `shouldBe` "    𝑛·1·1 := 𝜎3:λ  # 𝑛3"
-    it "writes the term a path and a meta of a join came to beside the morph of the one and the other alone" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 [ExDispatch ExXi (AtLabel "then"), ExMeta "n4"] (ExFormation [BiLambda (FnSymbol 3)])])
-      last (lines written) `shouldBe` "    𝑛·1·1 := 𝜎3:λ  # 𝕄(ξ.then), 𝑛4"
+    it "writes the term a join came to as the answer of its firing naming neither side" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 (ExFormation [BiLambda (FnSymbol 3)])])
+      last (lines written) `shouldBe` "    𝑛·1·1 := 𝜎3:λ"
     it "writes the term a stay line dropped a ρ from beside the stay of the meta it read" $ do
       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvReshaped 2 "𝑛3" "stay" (ExMeta "n1") (ExFormation [BiLambda (FnSymbol 3)])])
       last (lines written) `shouldBe` "    𝑛3·1 := 𝜎3:λ  # stay(𝑛1)"
@@ -288,12 +279,36 @@
     it "writes the double eight bytes hold beside the symbol a symbolize line minted for them" $ do
       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvSymbolized 2 6 (BtMany ["C0", "09", "1E", "B8", "51", "EB", "85", "1F"])])
       last (lines written) `shouldBe` "    symbolized 𝜎6 := C0-09-1E-B8-51-EB-85-1F  # -3.14"
+    it "writes the meta a cast bound beside the meta it read and the meta whose shape it took" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvCast 2 "𝑛9" (ExMeta "n2") (ExMeta "n4") (ExFormation [BiTau AtPhi (ExFormation [BiLambda (FnSymbol 7)]), BiTau (AtLabel "щ") (ExDispatch ExRoot (AtLabel "ёж"))])])
+      last (lines written) `shouldBe` "    cast 𝑛9·1 := ⟦ φ ↦ 𝜎7:λ, щ ↦ Φ.ёж ⟧  # 𝑛2·1 up to 𝑛4·1"
+    it "writes no line for a meta a line bound to the term it read as it was" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n3") (ExDispatch ExRoot (AtLabel "щука"))])
+      lines written `shouldBe` ["𝕄(Φ):", "  𝔼(L_ф):"]
+    it "names the term a meta that wrote no line holds where a cast read that meta" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n2") (ExDispatch ExRoot (AtLabel "ёрш")), EvCast 2 "𝑛9" (ExMeta "n2") (ExMeta "n4") (ExFormation [BiTau AtPhi (ExFormation [BiLambda (FnSymbol 7)]), BiTau (AtLabel "щ") (ExDispatch ExRoot (AtLabel "ёж"))])])
+      last (lines written) `shouldBe` "    cast 𝑛9·1 := ⟦ φ ↦ 𝜎7:λ, щ ↦ Φ.ёж ⟧  # Φ.ёрш up to 𝑛4·1"
+    it "names a meta a line of another firing left as it was by its own name" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n2") (ExDispatch ExRoot (AtLabel "ёрш")), EvFiring 1 "L_ц" Morphing ExRoot, EvCast 2 "𝑛9" (ExMeta "n2") (ExMeta "n4") (ExFormation [BiTau AtPhi (ExFormation [BiLambda (FnSymbol 7)]), BiTau (AtLabel "щ") (ExDispatch ExRoot (AtLabel "ёж"))])])
+      last (lines written) `shouldBe` "    cast 𝑛9·2 := ⟦ φ ↦ 𝜎7:λ, щ ↦ Φ.ёж ⟧  # 𝑛2·2 up to 𝑛4·2"
+    it "names the term a meta that wrote no line holds in the comment of a line that read that meta" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n1") (ExDispatch ExRoot (AtLabel "щ")), EvReshaped 2 "𝑛3" "stay" (ExMeta "n1") (ExFormation [BiLambda (FnSymbol 3)])])
+      last (lines written) `shouldBe` "    𝑛3·1 := 𝜎3:λ  # stay(Φ.щ)"
+    it "names the term a meta that wrote no line holds at the site of a firing it was read for" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n4") (ExDispatch ExRoot (AtLabel "щ")), EvFiring 2 "L_ю" Evaluation (ExMeta "n4")])
+      last (lines written) `shouldBe` "    𝔼(L_ю):  # 𝔼(Φ.щ)"
+    it "names the term a meta that wrote no line holds where a join could not join the side that meta bound" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n1") (ExDispatch ExRoot (AtLabel "ёж")), EvDiverged 2 (ExMeta "n1", ExDispatch ExRoot (AtLabel "ёж")) (ExMeta "n2", ExDispatch ExRoot (AtLabel "щука")) [] (Unformed Lefthand)])
+      last (lines written) `shouldBe` "    diverged Φ.ёж vs 𝑛2·1  # the left side is no formation"
     it "writes the symbol a join minted beside the meta its condition was bound to and the two it stands for" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9)])
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9) Nothing])
       last (lines written) `shouldBe` "    joined 𝜎12 := 𝛿3·1 ? 𝜎5 : 𝜎9"
     it "writes the symbol a join minted beside the path its condition was read off" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9)])
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9) Nothing])
       last (lines written) `shouldBe` "    joined 𝜎12 := ξ.щит ? 𝜎5 : 𝜎9"
+    it "writes the symbol standing for ⊥ in a join with a comment saying it is ⊥" $ do
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿1") 4 (2, 3) (Just 3)])
+      last (lines written) `shouldBe` "    joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3  # where 𝜎3 is ⊥"
     it "writes two sides a join could not join by the formations applications made" $ do
       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "жук")) (ArTau (AtLabel "w") (ExFormation []))) (ExFormation [BiTau (AtLabel "w") (ExFormation [])]) ExRoot, EvDiverged 2 (ExDispatch ExXi (AtLabel "then"), ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExXi (AtLabel "else"), ExFormation [BiTau (AtLabel "w") (ExFormation [])]) [AtLabel "q"] Unnamed])
       last (lines written) `shouldBe` "    diverged 𝑛·1·2 vs 𝑛·1·4  # they differ at .q, and the join names no otherwise"
@@ -319,8 +334,8 @@
       (_, written) <- recorded (\record -> mapM_ record (EvRun Morphing "Φ" : EvFiring 1 "L_ф" Morphing ExRoot : replicate 2 (EvFabricated 2 (ExMeta "n1", ExFormation [BiTau (AtLabel "ю") (ExDispatch ExRoot (AtLabel "ёж"))]) (ExMeta "n2", ExFormation [BiTau (AtLabel "ю") (ExDispatch ExRoot (AtLabel "щука"))]) (ExFormation [BiTau (AtLabel "ю") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "3F")]), BiTau (AtLabel "left") (ExDispatch ExRoot (AtLabel "ёж")), BiTau (AtLabel "right") (ExDispatch ExRoot (AtLabel "щука"))])]))))
       last (lines written) `shouldBe` "    fabricated 𝑛·1·2 := 𝑛1·1 and 𝑛2·1  # ⟦ λ ⤍ L_ж, on ↦ 3F-:Δ, left ↦ Φ.ёж, right ↦ Φ.щука ⟧:ю"
     it "writes the formation a join fabricated by its name in a later line" $ do
-      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvFabricated 2 (ExMeta "n1", ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (ExMeta "n2", ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (ExFormation [BiTau AtPhi (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) AtPhi), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) AtPhi)]), BiTau (AtLabel "к") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (AtLabel "к")), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (AtLabel "к"))])]), EvTaken 2 [ExMeta "n7"] (ExFormation [BiTau AtPhi (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) AtPhi), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) AtPhi)]), BiTau (AtLabel "к") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (AtLabel "к")), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (AtLabel "к"))])])])
-      last (lines written) `shouldBe` "    𝑛·1·2 := 𝑛·1·1  # 𝑛7"
+      (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvFabricated 2 (ExMeta "n1", ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (ExMeta "n2", ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (ExFormation [BiTau AtPhi (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) AtPhi), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) AtPhi)]), BiTau (AtLabel "к") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (AtLabel "к")), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (AtLabel "к"))])]), EvTaken 2 (ExFormation [BiTau AtPhi (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) AtPhi), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) AtPhi)]), BiTau (AtLabel "к") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (AtLabel "к")), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (AtLabel "к"))])])])
+      last (lines written) `shouldBe` "    𝑛·1·2 := 𝑛·1·1"
     it "opens a heading of its own for every run of the protocol" $ do
       (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvDelta 1 (BtOne "0C"), EvRun Morphing "Φ", EvDelta 1 (BtOne "0D")])
       lines written `shouldBe` ["𝕄(Φ):", "  𝛿·0·1 := 0C-", "𝕄(Φ):", "  𝛿·0·2 := 0D-"]
@@ -475,13 +490,21 @@
     it "spells the datum of an operand by the name the delta rule just gave it in the markup" $ do
       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ж" Dataization ExRoot, EvDelta 3 (BtOne "7F"), EvData 2 "𝛿1" (ExDispatch ExXi (AtLabel "щ")) (Right (BtOne "7F"))])
       lines written `shouldContain` ["    <bound meta=\"𝛿1·1\">𝛿·1·1</bound>"]
-    it "binds the term a stay line dropped a ρ from in the markup as it binds a term passed through" $ do
-      (_, stayed) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ж" Morphing ExRoot, EvReshaped 2 "𝑛3" "stay" (ExMeta "n1") (ExFormation [BiLambda (FnSymbol 3)])])
-      (_, passed) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ж" Morphing ExRoot, EvBound 2 "𝑛3" (ExMeta "n1") (ExFormation [BiLambda (FnSymbol 3)])])
-      stayed `shouldBe` passed
-    it "writes the term a line bound as a bound element in the markup" $ do
-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ж" Morphing ExRoot, EvBound 2 "𝑛3" (ExMeta "n1") (ExDispatch ExRoot (AtLabel "щ"))])
-      lines written `shouldContain` ["    <bound meta=\"𝑛3·1\">Φ.щ</bound>"]
+    it "writes the term a stay line dropped a ρ from as a bound element in the markup" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ж" Morphing ExRoot, EvReshaped 2 "𝑛3" "stay" (ExMeta "n1") (ExFormation [BiLambda (FnSymbol 3)])])
+      lines written `shouldContain` ["    <bound meta=\"𝑛3·1\">𝜎3</bound>"]
+    it "writes no element for a meta a line bound to the term it read as it was" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ж" Morphing ExRoot, EvBound 2 (ExMeta "n3") (ExDispatch ExRoot (AtLabel "щ"))])
+      filter (isInfixOf "𝑛3") (lines written) `shouldBe` []
+    it "names the term a meta that wrote no element holds where a cast read that meta in the markup" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n2") (ExDispatch ExRoot (AtLabel "ёрш")), EvCast 2 "𝑛9" (ExMeta "n2") (ExMeta "n4") (ExFormation [BiTau AtPhi (ExFormation [BiTau AtPhi (ExFormation [BiLambda (FnSymbol 7)])]), BiTau (AtLabel "щ") ExRoot])])
+      lines written `shouldContain` ["    <cast meta=\"𝑛9·1\" of=\"Φ.ёрш\" up-to=\"𝑛4·1\">𝑒·1·2</cast>"]
+    it "names the term a meta that wrote no element holds where a join could not join the side that meta bound in the markup" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n5") (ExDispatch ExRoot (AtLabel "ёж")), EvDiverged 2 (ExMeta "n5", ExDispatch ExRoot (AtLabel "ёж")) (ExMeta "n6", ExDispatch ExRoot (AtLabel "ёрш")) [] (Unformed Lefthand)])
+      lines written `shouldContain` ["    <diverged left=\"Φ.ёж\" right=\"𝑛6·1\" reason=\"the left side is no formation\"/>"]
+    it "names the term a meta that wrote no element holds at the site of a firing it was read for in the markup" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvBound 2 (ExMeta "n4") (ExDispatch ExRoot (AtLabel "щ")), EvFiring 2 "L_ю" Evaluation (ExMeta "n4")])
+      lines written `shouldContain` ["    <evaluate λ=\"L_ю\" by=\"evaluate\" at=\"Φ.щ\">"]
     it "writes the term a morphing came to as an element with its name" $ do
       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvMorphed 1 (ExDispatch ExRoot (AtLabel "щука"))])
       lines written `shouldContain` ["  <morphed meta=\"𝑛·0·1\">Φ.щука</morphed>"]
@@ -573,14 +596,20 @@
       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "кулик")) (ArTau (AtLabel "ш") ExRoot)) (ExFormation [BiTau (AtLabel "ш") ExRoot]) ExRoot, EvDeferred 1 31 Morphing (ExFormation [BiTau (AtLabel "щ") (ExFormation [BiTau (AtLabel "ш") ExRoot]), BiTau AtPhi (ExDispatch ExXi (AtLabel "щ"))]) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "щ") (ExFormation [BiTau (AtLabel "ш") ExRoot])))) ExRoot])
       lines written `shouldContain` ["  <deferred symbol=\"𝜎31\" by=\"morph\" at=\"Φ\" of=\"Φ.ёж\"><with><meta attr=\"щ\">𝑛·0·2</meta></with></deferred>"]
     it "writes the term a join came to as the answer of its firing in the markup" $ do
-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 [ExDispatch ExXi (AtLabel "then")] (ExFormation [BiLambda (FnSymbol 3)])])
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvTaken 2 (ExFormation [BiLambda (FnSymbol 3)])])
       lines written `shouldContain` ["    <answered meta=\"𝑛·1·1\">𝜎3</answered>"]
     it "writes the symbol a join minted as an element naming the meta its condition was bound to and the two it stands for" $ do
-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9)])
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿3") 12 (5, 9) Nothing])
       lines written `shouldContain` ["    <joined symbol=\"𝜎12\" on=\"𝛿3·1\" left=\"𝜎5\" right=\"𝜎9\"/>"]
     it "writes the symbol a join minted as an element naming the path its condition was read off" $ do
-      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9)])
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Right (ExDispatch ExXi (AtLabel "щит"))) 12 (5, 9) Nothing])
       lines written `shouldContain` ["    <joined symbol=\"𝜎12\" on=\"ξ.щит\" left=\"𝜎5\" right=\"𝜎9\"/>"]
+    it "writes the symbol standing for ⊥ in the markup and names it under terminator" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿4") 17 (16, 6) (Just 16)])
+      lines written `shouldContain` ["    <joined symbol=\"𝜎17\" on=\"𝛿4·1\" left=\"𝜎16\" right=\"𝜎6\" terminator=\"𝜎16\"/>"]
+    it "writes no terminator in the markup for a pair of a join that met ⊥ elsewhere" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvJoined 2 (Left "𝛿2") 23 (8, 14) (Just 21)])
+      lines written `shouldContain` ["    <joined symbol=\"𝜎23\" on=\"𝛿2·1\" left=\"𝜎8\" right=\"𝜎14\"/>"]
     it "writes two sides a join could not join as an element naming both" $ do
       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ю")))) (ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ю"))]) ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "жук")) (ArTau (AtLabel "w") (ExDispatch ExRoot (AtLabel "ю")))) (ExFormation [BiTau (AtLabel "w") (ExDispatch ExRoot (AtLabel "ю"))]) ExRoot, EvDiverged 2 (ExDispatch ExXi (AtLabel "then"), ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ю"))]) (ExDispatch ExXi (AtLabel "else"), ExFormation [BiTau (AtLabel "w") (ExDispatch ExRoot (AtLabel "ю"))]) [AtLabel "q"] Unnamed])
       lines written `shouldContain` ["    <diverged left=\"𝑛·1·2\" right=\"𝑛·1·4\" at=\".q\" reason=\"the join names no otherwise\"/>"]
@@ -596,6 +625,9 @@
     it "writes the formation a join fabricated as an element naming both sides in the markup" $ do
       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvFabricated 2 (ExMeta "n3", ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (ExMeta "n4", ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (ExFormation [BiTau AtPhi (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) AtPhi), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) AtPhi)]), BiTau (AtLabel "к") (ExFormation [BiLambda (Function "L_ж"), BiTau (AtLabel "on") (ExFormation [BiDelta (BtOne "05")]), BiTau (AtLabel "left") (ExDispatch (ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "ёж"))]) (AtLabel "к")), BiTau (AtLabel "right") (ExDispatch (ExFormation [BiTau (AtLabel "к") (ExDispatch ExRoot (AtLabel "щука"))]) (AtLabel "к"))])])])
       lines written `shouldContain` ["    <fabricated meta=\"𝑛·1·1\" left=\"𝑛3·1\" right=\"𝑛4·1\">𝑒·1·5</fabricated>"]
+    it "writes the meta a cast bound as an element naming the meta it read and the meta whose shape it took" $ do
+      (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvCast 2 "𝑛9" (ExMeta "n2") (ExMeta "n4") (ExFormation [BiTau AtPhi (ExFormation [BiTau AtPhi (ExFormation [BiLambda (FnSymbol 7)])]), BiTau (AtLabel "щ") ExRoot])])
+      lines written `shouldContain` ["    <cast meta=\"𝑛9·1\" of=\"𝑛2·1\" up-to=\"𝑛4·1\">𝑒·1·2</cast>"]
     it "writes the symbol a symbolize line minted as an element holding the datum it stands for" $ do
       (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ф" Morphing ExRoot, EvSymbolized 2 6 (BtOne "4A")])
       lines written `shouldContain` ["    <symbolized symbol=\"𝜎6\">4A-</symbolized>"]
diff --git a/test/EmitSpec.hs b/test/EmitSpec.hs
--- a/test/EmitSpec.hs
+++ b/test/EmitSpec.hs
@@ -9,7 +9,7 @@
 import AST
 import Control.Monad (forM_)
 import Data.Either (fromRight)
-import Data.List (isInfixOf)
+import Data.List (isInfixOf, isPrefixOf, nub)
 import Emit (emitted)
 import Engine (current)
 import Test.Hspec (Spec, describe, it, shouldBe, shouldNotSatisfy, shouldSatisfy)
@@ -45,6 +45,18 @@
     it "tells two rules of the same name apart" $
       fromRight "" (emitted [] [Y.Rule "ov" Nothing Nothing ExXi ExRoot Nothing Nothing Nothing, Y.Rule "ov" Nothing Nothing ExRoot ExXi Nothing Nothing Nothing] [] [] [] [])
         `shouldSatisfy` (\source -> all (`isInfixOf` source) ["stepOv0 ::", "stepOv1 ::"])
+    forM_
+      [ ["probe-a", "probe a", "probe a0"]
+      , ["probe a0", "probe-a", "probe a"]
+      , ["a1", "a1"] ++ ["unique" ++ show idx | idx <- [0 :: Int .. 7]] ++ ["a", "a"]
+      ]
+      ( \names -> it ("keeps declarations unique for " ++ show names) $ do
+          let rules = [Y.Rule name Nothing Nothing ExXi ExRoot Nothing Nothing Nothing | name <- names]
+              source = fromRight "" (emitted [] rules [] [] [] [])
+              declarations = [name | line <- lines source, name : "::" : _ <- [words line], name /= "steps", any (`isPrefixOf` name) ["step", "rewrite"]]
+          length declarations `shouldBe` 2 * length names
+          length (nub declarations) `shouldBe` length declarations
+      )
     it "keeps the comment of a rule named by a folded scalar on one line" $
       fromRight "" (emitted [] [Y.Rule "folded rule name\n" Nothing Nothing ExXi ExRoot Nothing Nothing Nothing] [] [] [] [])
         `shouldSatisfy` ("-- The rule 'folded rule name'.\n" `isInfixOf`)
diff --git a/test/EvaluateSpec.hs b/test/EvaluateSpec.hs
--- a/test/EvaluateSpec.hs
+++ b/test/EvaluateSpec.hs
@@ -21,16 +21,18 @@
 import Encoding (Encoding (UNICODE))
 import Files (allPathsIn)
 import Fixtures (defaultReduceContext, fixtureLambdas, recorded, recorded', withLambdas, withLambdasOf)
+import GHC.Clock (getMonotonicTime)
 import GHC.Generics (Generic)
 import Lambdas (readLambdas)
 import Lining (LineFormat (SINGLELINE))
 import Margin (defaultMargin)
 import Matcher (substEmpty)
-import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm, memoized, morph, tallied)
+import Morph (Deadline (..), ReduceContext (..), Steps (..), emptyState, execBuildTerm, memoized, morph, tallied)
 import Parser (Form (MONOFORM), parseExpressionThrows')
 import Printer (printExpression, printExpression', printExpressionHidingRho')
 import Sugar (SugarType (SWEET))
 import System.FilePath (makeRelative)
+import System.Timeout (timeout)
 import Tau (seedTaus)
 import Test.Hspec
 import Yaml (ExtraArgument (..))
@@ -159,3 +161,13 @@
       case result of
         TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "FF")]
         _ -> expectationFailure "expected TeExpression"
+
+  describe "stops a line by the clock of --max-seconds" $
+    it "fails a rewrite line that outlasts the deadline" $ do
+      let wide = iterate (\half -> ExFormation [BiTau (AtLabel "lo") half, BiTau (AtLabel "hi") half]) (ExFormation []) !! 18
+          program = ExFormation [BiTau (AtLabel "y") (ExDispatch (ExFormation [BiTau (AtLabel "x") wide, BiLambda (Function "L_wide")]) AtPhi)]
+      table <- withLambdasOf ("- λ: L_wide\n  morph:\n    𝑛1: $.x\n  rewrite:\n    𝑛2:\n      of: 𝑛1\n      rules:\n" <> T.concat (map (\idx -> "        - name: never" <> T.pack (show idx) <> "\n          pattern: 𝑒1.qz\n          result: 𝑒1\n") [1 .. 2000 :: Int]) <> "  𝑛: 𝑛2\n") readLambdas
+      due <- (+ 0.2) <$> getMonotonicTime
+      ctx <- withLambdas table <$> defaultReduceContext (ExDispatch ExRoot (AtLabel "y"))
+      timeout 10000000 (morph program emptyState ctx{_deadline = Just (Deadline 37 due)})
+        `shouldThrow` (\e -> "--max-seconds=37" `isInfixOf` show (e :: SomeException))
diff --git a/test/FilterSpec.hs b/test/FilterSpec.hs
--- a/test/FilterSpec.hs
+++ b/test/FilterSpec.hs
@@ -140,6 +140,11 @@
 
       forM_
         [ ("merges sibling children of one parent into a single binding", "[[ a -> [[ x -> Q, y -> Q ]], b -> Q ]]", ["Q.a.x", "Q.a.y"], "[[ a -> [[ x -> Q, y -> Q ]] ]]")
+        , ("keeps an explicitly selected bound rho", "[[ ^ -> Q, a -> Q ]]", ["Q.^"], "[[ ^ -> Q ]]")
+        , ("keeps an explicitly selected nested rho", "[[ a -> [[ ^ -> Q, x -> Q ]] ]]", ["Q.a.^"], "[[ a -> [[ ^ -> Q ]] ]]")
+        , ("follows a rho formation to a selected child", "[[ ^ -> [[ x -> Q, y -> Q ]], a -> Q ]]", ["Q.^.x"], "[[ ^ -> [[ x -> Q ]] ]]")
+        , ("keeps rho when merging selected sibling children", "[[ a -> [[ ^ -> Q, x -> Q, y -> Q ]] ]]", ["Q.a.^", "Q.a.x"], "[[ a -> [[ ^ -> Q, x -> Q ]] ]]")
+        , ("does not select an unrelated rho", "[[ ^ -> Q, a -> Q ]]", ["Q.a"], "[[ a -> Q ]]")
         , ("merges siblings at several depths", "[[ a -> [[ c -> [[ x -> ?, y -> ? ]], d -> ? ]], b -> ? ]]", ["Q.a.c.x", "Q.a.d", "Q.a.c.y"], "[[ a -> [[ c -> [[ x -> ?, y -> ? ]], d -> ? ]] ]]")
         , ("keeps a single nested child alone", "[[ a -> [[ x -> Q, y -> Q ]], b -> Q ]]", ["Q.a.x"], "[[ a -> [[ x -> Q ]] ]]")
         , ("keeps distinct top-level attributes", "[[ a -> [[ x -> Q ]], b -> Q ]]", ["Q.a", "Q.b"], "[[ a -> [[ x -> Q ]], b -> Q ]]")
diff --git a/test/ForksSpec.hs b/test/ForksSpec.hs
--- a/test/ForksSpec.hs
+++ b/test/ForksSpec.hs
@@ -17,13 +17,13 @@
     let application :: [Int] -> Expression
         application idxs = ExApplication (ExDispatch ExRoot (AtLabel "f")) (ArTau (AtLabel "x") (ExFormation (map (\idx -> BiTau (AtLabel "k") (ExFormation [BiLambda (FnSymbol idx)])) idxs)))
     it "joins two terms that differ in one symbol under a fresh symbol past the count" $
-      joined (application [3]) (application [8]) 11 `shouldBe` Right (application [12], [(12, (3, 8))], 12)
+      joined (application [3]) (application [8]) 11 `shouldBe` Right (application [12], [(12, (3, 8))], Nothing, 12)
     it "names a pair of symbols met twice by one fresh symbol" $
-      joined (application [4, 4]) (application [9, 9]) 17 `shouldBe` Right (application [18, 18], [(18, (4, 9))], 18)
+      joined (application [4, 4]) (application [9, 9]) 17 `shouldBe` Right (application [18, 18], [(18, (4, 9))], Nothing, 18)
     it "names two pairs sharing a symbol by two fresh symbols" $
-      joined (application [5, 5]) (application [6, 7]) 20 `shouldBe` Right (application [21, 22], [(21, (5, 6)), (22, (5, 7))], 22)
+      joined (application [5, 5]) (application [6, 7]) 20 `shouldBe` Right (application [21, 22], [(21, (5, 6)), (22, (5, 7))], Nothing, 22)
     it "mints nothing for two terms that are the same" $
-      joined (application [2, 6]) (application [2, 6]) 13 `shouldBe` Right (application [2, 6], [], 13)
+      joined (application [2, 6]) (application [2, 6]) 13 `shouldBe` Right (application [2, 6], [], Nothing, 13)
     it "tells the datum two formations differ in" $
       joined (ExFormation [BiDelta (BtOne "01"), BiLambda (FnSymbol 4)]) (ExFormation [BiDelta (BtOne "02"), BiLambda (FnSymbol 9)]) 10 `shouldBe` Left [AtDelta]
     it "tells the λ of two formations naming two functions" $
@@ -34,7 +34,7 @@
       joined (ExDispatch (application [3]) (AtLabel "a")) (ExDispatch (application [8]) (AtLabel "b")) 9 `shouldBe` Left []
     it "tells no attribute inside an application whose arguments differ" $
       joined (application [3]) (application [3, 4]) 6 `shouldBe` Left []
-    let apart :: String -> String -> IO (Either [Attribute] (Expression, [(Int, (Int, Int))], Int))
+    let apart :: String -> String -> IO (Either [Attribute] (Expression, [(Int, (Int, Int))], Maybe Int, Int))
         apart left right = (\one two -> joined one two 41) <$> parseExpressionThrows left <*> parseExpressionThrows right
     it "tells every attribute down to the datum two formations differ in" $
       apart "⟦ φ ↦ ⟦ ko ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" "⟦ φ ↦ ⟦ ko ↦ ⟦ Δ ⤍ 02- ⟧ ⟧ ⟧" >>= (`shouldBe` Left [AtPhi, AtLabel "ko", AtDelta])
@@ -52,6 +52,28 @@
       apart "⟦ φ ↦ Φ.fe( ix ↦ ⟦ ke ↦ Φ.ab ⟧ ) ⟧" "⟦ φ ↦ Φ.fe( ix ↦ ⟦ ke ↦ Φ.yo ⟧ ) ⟧" >>= (`shouldBe` Left [AtPhi])
     it "tells no attribute of a dispatch and a formation" $
       apart "Φ.ab.cd" "⟦ φ ↦ Φ.ab ⟧" >>= (`shouldBe` Left [])
+    it "joins a symbol and ⊥ under a fresh symbol, past another fresh one standing for ⊥" $
+      joined (ExFormation [BiLambda (FnSymbol 2)]) ExTermination 5 `shouldBe` Right (ExFormation [BiLambda (FnSymbol 7)], [(7, (2, 6))], Just 6, 7)
+    it "joins ⊥ and a symbol with the symbol standing for ⊥ on the left of the pair" $
+      joined ExTermination (ExFormation [BiLambda (FnSymbol 7)]) 9 `shouldBe` Right (ExFormation [BiLambda (FnSymbol 11)], [(11, (10, 7))], Just 10, 11)
+    it "keeps the shape of the side facing ⊥ and joins the symbol it holds with ⊥" $ do
+      expected <- parseExpressionThrows "⟦ φ ↦ Φ.qo( φ ↦ ⟦ λ ⤍ 𝜎43 ⟧ ), ko ↦ Φ.ze ⟧"
+      apart "⟦ φ ↦ Φ.qo( φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ), ko ↦ Φ.ze ⟧" "⊥" >>= (`shouldBe` Right (expected, [(43, (3, 42))], Just 42, 43))
+    it "names a symbol the side facing ⊥ holds twice by one fresh symbol" $ do
+      expected <- parseExpressionThrows "⟦ ub ↦ ⟦ λ ⤍ 𝜎43 ⟧, xe ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎43 ⟧ ⟧ ⟧"
+      apart "⊥" "⟦ ub ↦ ⟦ λ ⤍ 𝜎8 ⟧, xe ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎8 ⟧ ⟧ ⟧" >>= (`shouldBe` Right (expected, [(43, (42, 8))], Just 42, 43))
+    it "joins ⊥ one formation binds with the symbol the other one binds there" $ do
+      expected <- parseExpressionThrows "⟦ φ ↦ ⟦ λ ⤍ 𝜎43 ⟧, ws ↦ Φ.ug ⟧"
+      apart "⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧, ws ↦ Φ.ug ⟧" "⟦ φ ↦ ⊥, ws ↦ Φ.ug ⟧" >>= (`shouldBe` Right (expected, [(43, (5, 42))], Just 42, 43))
+    it "names every ⊥ a join meets by one fresh symbol" $ do
+      expected <- parseExpressionThrows "⟦ ub ↦ ⟦ λ ⤍ 𝜎43 ⟧, xe ↦ ⟦ λ ⤍ 𝜎44 ⟧ ⟧"
+      apart "⟦ ub ↦ ⊥, xe ↦ ⊥ ⟧" "⟦ ub ↦ ⟦ λ ⤍ 𝜎5 ⟧, xe ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧" >>= (`shouldBe` Right (expected, [(43, (42, 5)), (44, (42, 6))], Just 42, 44))
+    it "mints nothing for two sides of ⊥" $
+      joined ExTermination ExTermination 4 `shouldBe` Right (ExTermination, [], Nothing, 4)
+    it "tells no attribute of ⊥ and a side holding no symbol to stand for ⊥" $
+      apart "⟦ φ ↦ Φ.ab, ko ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" "⊥" >>= (`shouldBe` Left [])
+    it "tells the attribute of a formation binding ⊥ where the other one binds no symbol" $
+      apart "⟦ φ ↦ ⊥ ⟧" "⟦ φ ↦ Φ.ix ⟧" >>= (`shouldBe` Left [AtPhi])
 
   describe "forked" $ do
     let fork :: Text -> Either Int Bytes -> String -> String -> IO (Either Refusal Expression)
diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs
--- a/test/LaTeXSpec.hs
+++ b/test/LaTeXSpec.hs
@@ -164,6 +164,11 @@
       expressionToLaTeX bts defaultLatexContext
         `shouldBe` "\\begin{phiquation}\n\\delta_7 : D{.}\n\\end{phiquation}"
 
+    it "renders a two-digit index of a meta as a whole subscript" $ do
+      metas <- parseExpressionThrows "[[ !B12, !B3, x -> !e10 ]]"
+      expressionToLaTeX metas defaultLatexContext
+        `shouldBe` "\\begin{phiquation}\n[[ B_{12}, B_3, |x| -> e_{10} ]]{.}\n\\end{phiquation}"
+
     it "escapes '@' and '^' in an attribute label, same as '$' and '_'" $ do
       let weird = ExFormation [BiTau (AtLabel "a@b^c") ExRoot]
       expressionToLaTeX weird defaultLatexContext
diff --git a/test/LambdasSpec.hs b/test/LambdasSpec.hs
--- a/test/LambdasSpec.hs
+++ b/test/LambdasSpec.hs
@@ -7,15 +7,16 @@
 module LambdasSpec (spec) where
 
 import AST
-import Control.Exception (SomeException)
+import Control.Exception (SomeException, evaluate)
 import Control.Monad (forM_)
 import Data.List (isInfixOf)
 import Data.Text qualified as T
 import Fixtures (withLambdasOf)
 import Functions (buildTerm)
-import Lambdas (Ending (..), Lambda (..), Lambdas, Line (..), Meta (..), emptyLambdas, matched, minted, readLambdas, rewritten, stayed, symbolized, taken)
+import Lambdas (Ending (..), Lambda (..), Lambdas, Line (..), Meta (..), cast, emptyLambdas, matched, minted, readLambdas, rewritten, stayed, symbolized, taken)
 import Parser (parseExpressionThrows)
 import Rule (RuleContext (..), normal)
+import System.Mem.StableName (makeStableName)
 import Test.Hspec
 import Yaml qualified as Y
 
@@ -35,17 +36,18 @@
 lined known func = maybe [] _lines (matched known func)
 
 order :: Lambdas -> T.Text -> [T.Text]
-order known func = map bound (lined known func)
+order known func = concatMap bound (lined known func)
   where
-    bound :: Line -> T.Text
-    bound (Dataized meta _) = _spelling meta
-    bound (Morphed meta _) = _spelling meta
-    bound (Undressed meta _) = _spelling meta
-    bound (Evaluated meta _) = _spelling meta
-    bound (Deferred meta _) = _spelling meta
-    bound (Stayed meta _) = _spelling meta
-    bound (Symbolized meta _) = _spelling meta
-    bound (Rewritten meta _ _) = _spelling meta
+    bound :: Line -> [T.Text]
+    bound (Dataized meta _) = [_spelling meta]
+    bound (Morphed meta _) = [_spelling meta]
+    bound (Undressed meta _) = [_spelling meta]
+    bound (Evaluated meta _) = [_spelling meta]
+    bound (Deferred meta _) = [_spelling meta]
+    bound (Stayed meta _) = [_spelling meta]
+    bound (Symbolized meta _) = [_spelling meta]
+    bound (Rewritten meta _ _) = [_spelling meta]
+    bound (Cast one _ two _) = [_spelling one, _spelling two]
 
 dataizes :: Lambdas -> T.Text -> [(T.Text, T.Text)]
 dataizes known func = [(_spelling meta, _spelling source) | Dataized meta source <- lined known func]
@@ -68,6 +70,9 @@
 symbolizes :: Lambdas -> T.Text -> [(T.Text, T.Text)]
 symbolizes known func = [(_spelling meta, _spelling source) | Symbolized meta source <- lined known func]
 
+casts :: Lambdas -> T.Text -> [(T.Text, T.Text, T.Text, T.Text)]
+casts known func = [(_spelling one, _spelling first, _spelling two, _spelling second) | Cast one first two second <- lined known func]
+
 rewrites :: Lambdas -> T.Text -> [(T.Text, T.Text, Int)]
 rewrites known func = [(_spelling meta, _spelling source, length rules) | Rewritten meta source rules <- lined known func]
 
@@ -365,6 +370,32 @@
       known <- lambdasOf "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  𝑛: 𝑛1\n"
       rewrites known "L_hold" `shouldBe` []
 
+    it "reads the two lines of 'cast' as one line casting the pair of metas they read" $ do
+      known <- lambdasOf "- λ: L_hold\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n  cast:\n    𝑛4: 𝑛2\n    𝑛3: 𝑛1\n  𝑛: 𝑛3\n"
+      casts known "L_hold" `shouldBe` [("𝑛3", "𝑛1", "𝑛4", "𝑛2")]
+
+    it "runs an 'evaluate' line after the 'cast' block binding the meta it reads" $ do
+      known <- lambdasOf "- λ: L_hold\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n  evaluate:\n    𝑛5: 𝑛4\n  cast:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  𝑛: 𝑛5\n"
+      order known "L_hold" `shouldBe` ["𝑛3", "𝑛4", "𝑛5"]
+
+    it "runs a 'cast' block after the 'defer' lines binding both metas it reads" $ do
+      known <- lambdasOf "- λ: L_hold\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n  cast:\n    𝑛5: 𝑛3\n    𝑛6: 𝑛4\n  defer:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  𝑛: 𝑛5\n"
+      order known "L_hold" `shouldBe` ["𝑛3", "𝑛4", "𝑛5", "𝑛6"]
+
+    it "runs a 'symbolize' line before a 'cast' block no meta orders" $ do
+      known <- lambdasOf "- λ: L_hold\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n  cast:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  symbolize:\n    𝑛5: 𝑛1\n  𝑛: 𝑛3\n"
+      order known "L_hold" `shouldBe` ["𝑛5", "𝑛3", "𝑛4"]
+
+    it "reads a 'join' block whose sides are metas 'cast' bound" $ do
+      known <- lambdasOf "- λ: L_fork\n  dataize:\n    𝛿1: $.c\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n  cast:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  join:\n    on: 𝛿1\n    left: 𝑛3\n    right: 𝑛4\n"
+      left <- parseExpressionThrows "𝑛3"
+      right <- parseExpressionThrows "𝑛4"
+      sides known "L_fork" `shouldBe` Just (left, right)
+
+    it "reads an entry naming no 'cast' block at all" $ do
+      known <- lambdasOf "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  𝑛: 𝑛1\n"
+      casts known "L_hold" `shouldBe` []
+
     it "reads an entry naming no 'defer' block at all" $ do
       known <- lambdasOf "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  𝑛: 𝑛1\n"
       defers known "L_hold" `shouldBe` []
@@ -442,6 +473,12 @@
       , ("a rule of 'rewrite' writing a symbol nobody minted", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  rewrite:\n    𝑛2:\n      of: 𝑛1\n      rules:\n        - name: naming\n          pattern: Φ.true\n          result: ⟦ λ ⤍ 𝜎4 ⟧\n  𝑛: 𝑛2\n", "The rule 'naming' of the 'rewrite' block of λ function 'L_hold' writes the symbol '𝜎4' into its result, while only a firing mints a symbol")
       , ("a rule of 'rewrite' reading a meta it never binds", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  rewrite:\n    𝑛2:\n      of: 𝑛1\n      rules:\n        - name: unbound\n          pattern: ⟦ φ ↦ 𝑒1 ⟧\n          result: ⟦ φ ↦ 𝑒2 ⟧\n  𝑛: 𝑛2\n", "The rule 'unbound' reads the meta 'e2' it never binds")
       , ("a rule of 'rewrite' with no result", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  rewrite:\n    𝑛2:\n      of: 𝑛1\n      rules:\n        - name: empty\n          pattern: Φ.true\n  𝑛: 𝑛2\n", "key \"result\" not found")
+      , ("a 'cast' block holding one line", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  cast:\n    𝑛2: 𝑛1\n  𝑛: 𝑛2\n", "The 'cast' block of λ function 'L_hold' holds 1 line, while it casts one pair and takes exactly two")
+      , ("a 'cast' block holding three lines", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n    𝑛3: $.c\n  cast:\n    𝑛4: 𝑛1\n    𝑛5: 𝑛2\n    𝑛6: 𝑛3\n  𝑛: 𝑛4\n", "The 'cast' block of λ function 'L_hold' holds 3 lines, while it casts one pair and takes exactly two")
+      , ("a 'cast' line reading a term instead of a meta", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  cast:\n    𝑛2: 𝑛1\n    𝑛3: $.b\n  𝑛: 𝑛2\n", "is not an expression meta")
+      , ("a 'cast' line reading a meta the entry never bound", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  cast:\n    𝑛2: 𝑛1\n    𝑛3: 𝑛7\n  𝑛: 𝑛2\n", "The operand '𝑛7' of λ function 'L_hold' names no meta bound by 'morph' or by any line")
+      , ("a meta bound by 'stay' and again by the second line of 'cast'", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n    𝑛2: $.b\n  stay:\n    𝑛4: 𝑛1\n  cast:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  𝑛: 𝑛3\n", "The meta '𝑛4' of λ function 'L_hold' is bound by more than one line")
+      , ("a 'cast' block reading, through another line, a meta it binds", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  evaluate:\n    𝑛2: 𝑛4\n  cast:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  𝑛: 𝑛3\n", "The line binding '𝑛2' of λ function 'L_hold' reads the meta it binds")
       , ("a meta bound by 'morph' and again by 'stay'", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  stay:\n    𝑛1: 𝑛1\n  𝑛: 𝑛1\n", "The meta '𝑛1' of λ function 'L_hold' is bound by more than one line")
       , ("a meta bound by 'morph' and again by 'defer'", "- λ: L_hold\n  morph:\n    𝑛1: $.a\n  defer:\n    𝑛1: 𝑛1\n  𝑛: 𝑛1\n", "The meta '𝑛1' of λ function 'L_hold' is bound by more than one line")
       , ("an entry with both an '𝑛' key and a 'join' block", joint <> "  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "The entry of λ function 'L_fork' has both an '𝑛' key and a 'join' block, while a join answers the term it joins")
@@ -457,7 +494,7 @@
       , ("a 'join' block whose 'otherwise' is no λ name", joint <> "    otherwise: l_join\n", "The 'otherwise' of the 'join' block of λ function 'L_fork' is 'l_join', while it must name a λ function, such as 'L_join'")
       , ("a 'join' block whose 'otherwise' names a symbol", joint <> "    otherwise: 𝜎3\n", "The 'otherwise' of the 'join' block of λ function 'L_fork' is '𝜎3', while it must name a λ function, such as 'L_join'")
       , ("a 'join' block which is no mapping", "- λ: L_fork\n  dataize:\n    𝛿1: $.c\n  join: [𝛿1, $.a, $.b]\n", "join: parsing")
-      , ("a side of a 'join' block naming a meta nothing binds", "- λ: L_fork\n  dataize:\n    𝛿1: $.c\n  join:\n    on: 𝛿1\n    left: 𝑛1\n    right: $.b\n", "The side 'left' of the 'join' block of λ function 'L_fork' reads the meta 'n1' that none of 'morph', 'undress', 'evaluate', 'stay', 'rewrite', 'symbolize' and 'defer' binds")
+      , ("a side of a 'join' block naming a meta nothing binds", "- λ: L_fork\n  dataize:\n    𝛿1: $.c\n  join:\n    on: 𝛿1\n    left: 𝑛1\n    right: $.b\n", "The side 'left' of the 'join' block of λ function 'L_fork' reads the meta 'n1' that none of 'morph', 'undress', 'evaluate', 'stay', 'rewrite', 'symbolize', 'cast' and 'defer' binds")
       , ("a side of a 'join' block reading a meta inside a term", "- λ: L_fork\n  dataize:\n    𝛿1: $.c\n  morph:\n    𝑛1: $.a\n  join:\n    on: 𝛿1\n    left: 𝑛1.x\n    right: $.b\n", "The side 'left' of the 'join' block of λ function 'L_fork' reads the meta 'n1' inside a term, while a side is a path from '$' or a meta alone")
       , ("a side of a 'join' block which is no term of the calculus", "- λ: L_fork\n  dataize:\n    𝛿1: $.c\n  join:\n    on: 𝛿1\n    left: ⟦ λ ⤍\n    right: $.b\n", "cannot be read")
       , ("a 'fork' block, which is gone", "- λ: L_fork\n  dataize:\n    𝛿1: $.c\n  fork:\n    on: 𝛿1\n    left: $.a\n    right: $.b\n", "The key 'fork' of λ function 'L_fork' is none of the keys an entry reads")
@@ -515,6 +552,43 @@
       kept <- parseExpressionThrows "Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) )"
       stayed term `shouldBe` kept
 
+  describe "cast" $ do
+    it "casts a bare symbol into a copy of a decorator whose φ is a bare symbol" $ do
+      bare <- parseExpressionThrows "⟦ λ ⤍ 𝜎5 ⟧"
+      shape <- parseExpressionThrows "⟦ φ ↦ ⟦ λ ⤍ 𝜎8 ⟧, wj ↦ Φ.hu ⟧"
+      made <- parseExpressionThrows "⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧, wj ↦ Φ.hu ⟧"
+      cast bare shape `shouldBe` Just made
+
+    it "casts a bare symbol into a copy of a decorator holding an object beside its φ" $ do
+      bare <- parseExpressionThrows "⟦ λ ⤍ 𝜎13 ⟧"
+      shape <- parseExpressionThrows "⟦ kz ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧"
+      made <- parseExpressionThrows "⟦ kz ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎13 ⟧ ⟧"
+      cast bare shape `shouldBe` Just made
+
+    it "casts a bare symbol down every decorator of the φ chain" $ do
+      bare <- parseExpressionThrows "⟦ λ ⤍ 𝜎2 ⟧"
+      shape <- parseExpressionThrows "⟦ φ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎9 ⟧, if ↦ ξ.ty ⟧, and ↦ ∅ ⟧"
+      made <- parseExpressionThrows "⟦ φ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, if ↦ ξ.ty ⟧, and ↦ ∅ ⟧"
+      cast bare shape `shouldBe` Just made
+
+    forM_
+      [ ("another bare symbol" :: String, "⟦ λ ⤍ 𝜎3 ⟧", "⟦ λ ⤍ 𝜎4 ⟧")
+      , ("a term whose φ chain ends in no symbol", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ Φ.kq ⟧")
+      , ("a term whose φ chain ends in a datum", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ Δ ⤍ 1F- ⟧ ⟧")
+      , ("a term whose φ is void", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ∅, zv ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧")
+      , ("a term whose φ chain ends in a symbol beside other bindings", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6, zv ↦ ∅ ⟧ ⟧")
+      , ("a term holding a symbol off its φ chain", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧, zv ↦ ⟦ λ ⤍ 𝜎7 ⟧ ⟧")
+      , ("a term holding the symbol of its φ chain once more off it", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧, zv ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧")
+      , ("a term whose φ chain runs through an application", "⟦ λ ⤍ 𝜎3 ⟧", "⟦ φ ↦ Φ.kq( φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ) ⟧")
+      , ("a decorator from a term that is no bare symbol", "⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧", "⟦ φ ↦ ⟦ λ ⤍ 𝜎6 ⟧ ⟧")
+      ]
+      ( \(desc, from, into) ->
+          it ("casts nothing into " ++ desc) $ do
+            bare <- parseExpressionThrows from
+            shape <- parseExpressionThrows into
+            cast bare shape `shouldBe` Nothing
+      )
+
   describe "rewritten" $ do
     it "rewrites the term a rule matches as a whole" $ do
       made <- rewrote [("Φ.true", "Φ.bool( if ↦ ⟦ Δ ⤍ 01- ⟧ )")] "Φ.true"
@@ -560,6 +634,12 @@
       term <- parseExpressionThrows "Φ.false( α0 ↦ ⟦ Δ ⤍ 2E- ⟧ )"
       made <- rewrote [("Φ.true", "Φ.vw")] "Φ.false( α0 ↦ ⟦ Δ ⤍ 2E- ⟧ )"
       made `shouldBe` term
+
+    it "hands back the very term no rule matches, so a shared term stays shared" $ do
+      term <- evaluate (iterate (\half -> ExFormation [BiTau (AtLabel "lo") half, BiTau (AtLabel "hi") half]) (ExFormation []) !! 9)
+      rule <- (\from to -> Y.Rule "kq" Nothing Nothing from to Nothing Nothing Nothing) <$> parseExpressionThrows "Φ.true" <*> parseExpressionThrows "Φ.vw"
+      made <- rewritten (RuleContext buildTerm Nothing normal) [rule] term >>= evaluate
+      (==) <$> (makeStableName $! made) <*> (makeStableName $! term) `shouldReturn` True
 
   describe "symbolized" $ do
     it "turns the datum of a formation into a fresh symbol" $ do
diff --git a/test/RegexpSpec.hs b/test/RegexpSpec.hs
--- a/test/RegexpSpec.hs
+++ b/test/RegexpSpec.hs
@@ -150,6 +150,12 @@
       , ("replaces overlapping potential matches correctly", "aa", "X", "aaaa", "XX")
       , ("handles single character replacement", ".", "*", "abc", "***")
       , ("handles word boundary", "\\bword\\b", "WORD", "word in a word", "WORD in a WORD")
+      , ("keeps lookbehind context across matches", "(?<=a)a", "X", "aaa", "aXX")
+      , ("does not invent word boundaries after a match", "\\ba", "X", "aaa", "Xaa")
+      , ("does not restart an absolute-start assertion", "\\Aa", "X", "aaa", "Xaa")
+      , ("keeps captured lookbehind text after previous matches", "(?<=(a))a", "$1X", "aaa", "aaXaX")
+      , ("keeps Unicode lookbehind context", "(?<=é)é", "X", "ééé", "éXX")
+      , ("keeps context after an empty match", "\\b", "X", "éé", "XééX")
       , ("terminates on an empty-match pattern (anchored ^)", "^", "X", "hello", "Xhello")
       , ("terminates on an empty regex pattern", "", "X", "hello", "XhXeXlXlXoX")
       , ("keeps UTF-8 characters together after an empty match", "(?=.)", "X", "é", "Xé")
diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs
--- a/test/XMIRSpec.hs
+++ b/test/XMIRSpec.hs
@@ -305,6 +305,9 @@
       , ("keeps a bare 'Q' bound to a named attribute", "[[ x -> Q ]]")
       , ("keeps a formation bound to φ", "[[ k -> [[ @ -> [[ L> S8 ]] ]] ]]")
       , ("keeps byte data and sibling bindings in an application argument", "[[ x -> Q.y(a -> [[ D> 01-02, b -> Q.z ]]) ]]")
+      , ("keeps data after an application argument's sibling binding", "[[ top -> [[ @ -> ⊥(a -> [[ x -> [[]], D> 00-FF ]]) ]] ]]")
+      , ("keeps data between an application argument's sibling bindings", "[[ top -> [[ @ -> ⊥(a -> [[ x -> [[]], D> 00-FF, y -> [[]] ]]) ]] ]]")
+      , ("keeps data between a positional argument's sibling bindings", "[[ top -> [[ @ -> ⊥(α0 -> [[ x -> [[]], D> 00-FF, y -> [[]] ]]) ]] ]]")
       ]
       ( \(desc, source) -> it desc $ do
           expr <- parseExpressionThrows source