diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,7 +1,7 @@
 cabal-version:      3.0
 
 name:               phino
-version:            0.0.0.12
+version:            0.0.0.13
 license:            MIT
 synopsis:           Command-Line Manipulator of 𝜑-Calculus Expressions
 description:        Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/resources/copy.yaml b/resources/copy.yaml
--- a/resources/copy.yaml
+++ b/resources/copy.yaml
@@ -16,7 +16,7 @@
 pattern: ⟦ 𝐵1, 𝜏1 ↦ ⟦ 𝐵2, 𝜏2 ↦ ∅, 𝐵3 ⟧(𝜏2 ↦ 𝑒1) * !t, 𝐵4 ⟧
 result: ⟦ 𝐵1, 𝜏1 ↦ ⟦ 𝐵2, 𝜏2 ↦ 𝑒2, 𝐵3 ⟧ * !t, 𝐵4 ⟧
 when:
-  fn: 𝑒1
+  xi: 𝑒1
 where:
   - meta: 𝑒2
     function: contextualize
diff --git a/src/Builder.hs b/src/Builder.hs
--- a/src/Builder.hs
+++ b/src/Builder.hs
@@ -23,10 +23,10 @@
 contextualize ExTermination _ _ = ExTermination
 contextualize (ExFormation bds) _ _ = ExFormation bds
 contextualize (ExDispatch expr attr) context prog = ExDispatch (contextualize expr context prog) attr
-contextualize (ExApplication expr (BiTau attr bexpr)) context prog = do
+contextualize (ExApplication expr (BiTau attr bexpr)) context prog =
   let expr' = contextualize expr context prog
       bexpr' = contextualize bexpr context prog
-  ExApplication expr' (BiTau attr bexpr')
+   in ExApplication expr' (BiTau attr bexpr')
 
 buildAttribute :: Attribute -> Subst -> Maybe Attribute
 buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup meta mp of
diff --git a/src/Condition.hs b/src/Condition.hs
--- a/src/Condition.hs
+++ b/src/Condition.hs
@@ -46,28 +46,25 @@
 numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of
   Just (MvBindings bds) -> Just (toInteger (length bds))
   _ -> Nothing
-numToInt (Y.Add left right) subst = case (numToInt left subst, numToInt right subst) of
-  (Just left_, Just right_) -> Just (left_ + right_)
-  _ -> Nothing
 numToInt (Y.Literal num) subst = Just num
 numToInt _ _ = Nothing
 
 meetCondition' :: Y.Condition -> Subst -> [Subst]
 meetCondition' (Y.Or []) subst = [subst]
-meetCondition' (Y.Or (cond : rest)) subst = do
+meetCondition' (Y.Or (cond : rest)) subst =
   let met = meetCondition' cond subst
-  if null met
-    then meetCondition' (Y.Or rest) subst
-    else met
+   in if null met
+        then meetCondition' (Y.Or rest) subst
+        else met
 meetCondition' (Y.And []) subst = [subst]
-meetCondition' (Y.And (cond : rest)) subst = do
+meetCondition' (Y.And (cond : rest)) subst =
   let met = meetCondition' cond subst
-  if null met
-    then []
-    else meetCondition' (Y.And rest) subst
-meetCondition' (Y.Not cond) subst = do
+   in if null met
+        then []
+        else meetCondition' (Y.And rest) subst
+meetCondition' (Y.Not cond) subst =
   let met = meetCondition' cond subst
-  [subst | null met]
+   in [subst | null met]
 meetCondition' (Y.In attr binding) subst =
   case (buildAttribute attr subst, buildBinding binding subst) of
     (Just attr, Just bds) -> [subst | attrInBindings attr bds] -- if attrInBindings attr bd then [subst] else []
@@ -82,23 +79,20 @@
   (_, _) -> []
 meetCondition' (Y.Eq (Y.CmpAttr left) (Y.CmpAttr right)) subst = [subst | compareAttrs left right subst]
 meetCondition' (Y.Eq _ _) _ = []
--- @todo #89:30min Extend list of expressions. There are expressions where we can definitely say
---  if this expression in normal form or not. In common case the expression in normal form if
---  it does not match with any of normalization rules. But it's quite expensive operation comparing to
---  simple list filtering and pattern matching. For example if expression is formation where all bindings are
---  void, lambda, or delta - this expression in normal form and there's no need to try to match it with normalization
---  rules. So we need find more such cases and introduce them.
 meetCondition' (Y.NF (ExMeta meta)) (Subst mp) = case M.lookup meta mp of
-  Just (MvExpression expr) -> case expr of
-    ExThis -> [Subst mp]
-    ExGlobal -> [Subst mp]
-    ExTermination -> [Subst mp]
-    ExDispatch ExThis _ -> [Subst mp]
-    ExDispatch ExGlobal _ -> [Subst mp]
-    ExDispatch ExTermination _ -> [] -- dd rule
-    ExApplication ExTermination _ -> [] -- dc rule
-    ExFormation [] -> [Subst mp]
-    _ -> [Subst mp | not (matchesAnyNormalizationRule expr normalizationRules)]
+  Just (MvExpression expr) ->
+    let isNf = not (matchesAnyNormalizationRule expr normalizationRules)
+     in case expr of
+          ExThis -> [Subst mp]
+          ExGlobal -> [Subst mp]
+          ExTermination -> [Subst mp]
+          ExDispatch ExThis _ -> [Subst mp]
+          ExDispatch ExGlobal _ -> [Subst mp]
+          ExDispatch ExTermination _ -> [] -- dd rule
+          ExApplication ExTermination _ -> [] -- dc rule
+          ExFormation [] -> [Subst mp]
+          ExFormation bds -> [Subst mp | normalBindings bds || isNf]
+          _ -> [Subst mp | isNf]
   _ -> []
   where
     -- Returns True if given expression matches with any of given normalization rules
@@ -108,30 +102,39 @@
       case matchProgramWithCondition (Y.pattern rule) (Y.when rule) (Program expr) of
         Just matched -> not (null matched) || matchesAnyNormalizationRule expr rules
         Nothing -> matchesAnyNormalizationRule expr rules
+    normalBindings :: [Binding] -> Bool
+    normalBindings [] = True
+    normalBindings (bd : bds) =
+      let next = normalBindings bds
+       in case bd of
+            BiDelta _ -> next
+            BiVoid _ -> next
+            BiLambda _ -> next
+            _ -> False
 meetCondition' (Y.NF _) _ = []
-meetCondition' (Y.FN (ExMeta meta)) (Subst mp) = case M.lookup meta mp of
-  Just (MvExpression expr) -> meetCondition' (Y.FN expr) (Subst mp)
+meetCondition' (Y.XI (ExMeta meta)) (Subst mp) = case M.lookup meta mp of
+  Just (MvExpression expr) -> meetCondition' (Y.XI expr) (Subst mp)
   _ -> []
-meetCondition' (Y.FN (ExFormation _)) subst = [subst]
-meetCondition' (Y.FN ExThis) subst = []
-meetCondition' (Y.FN ExGlobal) subst = [subst]
-meetCondition' (Y.FN (ExApplication expr (BiTau attr texpr))) subst = do
-  let onExpr = meetCondition' (Y.FN expr) subst
-      onTau = meetCondition' (Y.FN texpr) subst
-  [subst | not (null onExpr) && not (null onTau)]
-meetCondition' (Y.FN (ExDispatch expr _)) subst = meetCondition' (Y.FN expr) subst
+meetCondition' (Y.XI (ExFormation _)) subst = [subst]
+meetCondition' (Y.XI ExThis) subst = []
+meetCondition' (Y.XI ExGlobal) subst = [subst]
+meetCondition' (Y.XI (ExApplication expr (BiTau attr texpr))) subst =
+  let onExpr = meetCondition' (Y.XI expr) subst
+      onTau = meetCondition' (Y.XI texpr) subst
+   in [subst | not (null onExpr) && not (null onTau)]
+meetCondition' (Y.XI (ExDispatch expr _)) subst = meetCondition' (Y.XI expr) subst
 
 -- For each substitution check if it meetCondition to given condition
 -- If substitution does not meet the condition - it's thrown out
 -- and is not used in replacement
 meetCondition :: Y.Condition -> [Subst] -> [Subst]
 meetCondition _ [] = []
-meetCondition cond (subst : rest) = do
+meetCondition cond (subst : rest) =
   let first = meetCondition' cond subst
-  let next = meetCondition cond rest
-  if null first
-    then next
-    else head first : next
+      next = meetCondition cond rest
+   in if null first
+        then next
+        else head first : next
 
 -- Returns Just [...] if
 -- 1. program matches pattern and
@@ -139,14 +142,14 @@
 -- 2.2. condition is present and met
 -- Otherwise returns Nothing
 matchProgramWithCondition :: Expression -> Maybe Y.Condition -> Program -> Maybe [Subst]
-matchProgramWithCondition ptn condition program = do
+matchProgramWithCondition ptn condition program =
   let matched = matchProgram ptn program
-  if null matched
-    then Nothing
-    else case condition of
-      Nothing -> Just matched
-      Just cond -> do
-        let met = meetCondition cond matched
-        if null met
-          then Nothing
-          else Just met
+   in if null matched
+        then Nothing
+        else case condition of
+          Nothing -> Just matched
+          Just cond ->
+            let met = meetCondition cond matched
+             in if null met
+                  then Nothing
+                  else Just met
diff --git a/src/Matcher.hs b/src/Matcher.hs
--- a/src/Matcher.hs
+++ b/src/Matcher.hs
@@ -80,13 +80,13 @@
 matchBindings :: [Binding] -> [Binding] -> [Subst]
 matchBindings [] [] = [substEmpty]
 matchBindings [] _ = []
-matchBindings ((BiMeta name) : pbs) tbs = do
+matchBindings ((BiMeta name) : pbs) tbs =
   let splits = [splitAt idx tbs | idx <- [0 .. length tbs]]
-  catMaybes
-    [ combine (substSingle name (MvBindings before)) subst
-      | (before, after) <- splits,
-        subst <- matchBindings pbs after
-    ]
+   in catMaybes
+        [ combine (substSingle name (MvBindings before)) subst
+          | (before, after) <- splits,
+            subst <- matchBindings pbs after
+        ]
 matchBindings (pb : pbs) (tb : tbs) = combineMany (matchBinding pb tb) (matchBindings pbs tbs)
 matchBindings _ _ = []
 
@@ -95,19 +95,19 @@
 -- If there's one - build the list of all the tail operations after head expression.
 -- The tail operations may be only dispatches or applications
 tailExpressions :: Expression -> Expression -> ([Subst], [Tail])
-tailExpressions ptn tgt = do
+tailExpressions ptn tgt =
   let (substs, tails) = tailExpressionsReversed ptn tgt
-  (substs, reverse tails)
+   in (substs, reverse tails)
   where
     tailExpressionsReversed :: Expression -> Expression -> ([Subst], [Tail])
     tailExpressionsReversed ptn' tgt' = case matchExpression ptn' tgt' of
       [] -> case tgt' of
-        ExDispatch expr attr -> do
+        ExDispatch expr attr ->
           let (substs, tails) = tailExpressionsReversed ptn' expr
-          (substs, TaDispatch attr : tails)
-        ExApplication expr tau -> do
+           in (substs, TaDispatch attr : tails)
+        ExApplication expr tau ->
           let (substs, tails) = tailExpressionsReversed ptn' expr
-          (substs, TaApplication tau : tails)
+           in (substs, TaApplication tau : tails)
         _ -> ([], [])
       substs -> (substs, [])
 
@@ -131,14 +131,14 @@
 
 -- Match expression with deep nested expression(s) matching
 matchExpressionDeep :: Expression -> Expression -> [Subst]
-matchExpressionDeep ptn tgt = do
+matchExpressionDeep ptn tgt =
   let matched = matchExpression ptn tgt
       deep = case tgt of
         ExFormation bds -> concatMap (`matchBindingExpression` ptn) bds
         ExDispatch exp _ -> matchExpressionDeep ptn exp
         ExApplication exp tau -> matchExpressionDeep ptn exp ++ matchBindingExpression tau ptn
         _ -> []
-  matched ++ deep
+   in matched ++ deep
 
 matchProgram :: Expression -> Program -> [Subst]
 matchProgram ptn (Program exp) = matchExpressionDeep ptn exp
diff --git a/src/Misc.hs b/src/Misc.hs
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -1,11 +1,24 @@
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ViewPatterns #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
 -- This module provides commonly used helper functions for other modules
-module Misc where
+module Misc
+  ( numToHex,
+    strToHex,
+    hexToStr,
+    hexToNum,
+    withVoidRho,
+    allPathsIn,
+    ensuredFile,
+    shuffle,
+    pattern DataObject,
+  )
+where
 
 import Ast
 import Control.Exception
@@ -39,6 +52,41 @@
   show FileDoesNotExist {..} = printf "File '%s' does not exist" file
   show DirectoryDoesNotExist {..} = printf "Directory '%s' does not exist" dir
 
+-- Minimal matcher function (required for view pattern)
+matchDataoObject :: Expression -> Maybe (String, String)
+matchDataoObject
+  ( ExApplication
+      (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel label))
+      ( BiTau
+          (AtAlpha 0)
+          ( ExApplication
+              (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
+              ( BiTau
+                  (AtAlpha 0)
+                  (ExFormation [BiDelta bts, BiVoid AtRho])
+                )
+            )
+        )
+    ) = Just (label, bts)
+matchDataoObject _ = Nothing
+
+pattern DataObject :: String -> String -> Expression
+pattern DataObject label bts <- (matchDataoObject -> Just (label, bts))
+  where
+    DataObject label bts =
+      ExApplication
+        (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel label))
+        ( BiTau
+            (AtAlpha 0)
+            ( ExApplication
+                (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
+                ( BiTau
+                    (AtAlpha 0)
+                    (ExFormation [BiDelta bts, BiVoid AtRho])
+                )
+            )
+        )
+
 -- Add void rho binding to the end of the list of any rho binding is not present
 withVoidRho :: [Binding] -> [Binding]
 withVoidRho bds = withVoidRho' bds False
@@ -101,16 +149,16 @@
 -- >>> hexToNum "40-45"
 -- Expected 8 bytes for conversion, got 2
 hexToNum :: String -> Either Integer Double
-hexToNum hx = do
+hexToNum hx =
   let bytes = hexToBts hx
-  if length bytes /= 8
-    then error $ "Expected 8 bytes for conversion, got " ++ show (length bytes)
-    else do
-      let word = toWord64BE bytes
-          val = wordToDouble word
-      case properFraction val of
-        (n, 0.0) -> Left n
-        _ -> Right val
+   in if length bytes /= 8
+        then error $ "Expected 8 bytes for conversion, got " ++ show (length bytes)
+        else
+          let word = toWord64BE bytes
+              val = wordToDouble word
+           in case properFraction val of
+                (n, 0.0) -> Left n
+                _ -> Right val
   where
     toWord64BE :: [Word8] -> Word64
     toWord64BE [a, b, c, d, e, f, g, h] =
@@ -175,7 +223,7 @@
     escapeStr :: String -> String
     escapeStr = concatMap escapeChar
       where
-        escapeChar '"'  = "\\\""
+        escapeChar '"' = "\\\""
         escapeChar '\\' = "\\\\"
         escapeChar '\n' = "\\n"
         escapeChar '\t' = "\\t"
diff --git a/src/Pretty.hs b/src/Pretty.hs
--- a/src/Pretty.hs
+++ b/src/Pretty.hs
@@ -1,6 +1,4 @@
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ViewPatterns #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
@@ -22,7 +20,7 @@
 import Matcher
 import Prettyprinter
 import Prettyprinter.Render.String (renderString)
-import Misc (hexToStr, hexToNum)
+import Misc
 
 data PrintMode = SWEET | SALTY
   deriving (Eq)
@@ -33,41 +31,6 @@
 
 newtype Formatted a = Formatted {unFormatted :: (PrintMode, a)}
 
--- Minimal matcher function (required for view pattern)
-matchDataoObject :: Expression -> Maybe (String, String)
-matchDataoObject
-  ( ExApplication
-      (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel label))
-      ( BiTau
-          (AtAlpha 0)
-          ( ExApplication
-              (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
-              ( BiTau
-                  (AtAlpha 0)
-                  (ExFormation [BiDelta bts, BiVoid AtRho])
-                )
-            )
-        )
-    ) = Just (label, bts)
-matchDataoObject _ = Nothing
-
-pattern DataObject :: String -> String -> Expression
-pattern DataObject label bts <- (matchDataoObject -> Just (label, bts))
-  where
-    DataObject label bts =
-      ExApplication
-        (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel label))
-        ( BiTau
-            (AtAlpha 0)
-            ( ExApplication
-                (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
-                ( BiTau
-                    (AtAlpha 0)
-                    (ExFormation [BiDelta bts, BiVoid AtRho])
-                )
-            )
-        )
-
 prettyMeta :: String -> Doc ann
 prettyMeta meta = pretty "!" <> pretty meta
 
@@ -91,23 +54,22 @@
   pretty (AtMeta meta) = prettyMeta meta
 
 instance Pretty (Formatted Binding) where
-  pretty (Formatted (SWEET, BiTau attr (ExFormation bindings))) = do
+  pretty (Formatted (SWEET, BiTau attr (ExFormation bindings))) =
     let voids' = voids bindings
-    if null voids'
-      then pretty attr <+> prettyArrow <+> pretty (Formatted (SWEET, ExFormation bindings))
-      else
-        pretty attr
-          <> lparen
-          <> hsep (punctuate comma (map pretty voids'))
-          <> rparen
-          <+> prettyArrow
-          <+> pretty (Formatted (SWEET, ExFormation (drop (length voids') bindings)))
+     in if null voids'
+          then pretty attr <+> prettyArrow <+> pretty (Formatted (SWEET, ExFormation bindings))
+          else
+            if length voids' == length bindings && last voids' == AtRho
+              then inlineVoids (init voids') <+> prettyLsb <> prettyRsb
+              else inlineVoids voids' <+> pretty (Formatted (SWEET, ExFormation (drop (length voids') bindings)))
     where
       voids :: [Binding] -> [Attribute]
       voids [] = []
       voids (bd : bds) = case bd of
         BiVoid attr -> attr : voids bds
         _ -> []
+      inlineVoids :: [Attribute] -> Doc ann
+      inlineVoids voids' = pretty attr <> lparen <> hsep (punctuate comma (map pretty voids')) <> rparen <+> prettyArrow
   pretty (Formatted (mode, BiTau attr expr)) = pretty attr <+> prettyArrow <+> pretty (Formatted (mode, expr))
   pretty (Formatted (_, BiMeta meta)) = prettyMeta meta
   pretty (Formatted (_, BiDelta bytes)) = pretty "Δ" <+> prettyDashedArrow <+> pretty bytes
@@ -117,19 +79,28 @@
   pretty (Formatted (_, BiLambda func)) = pretty "λ" <+> prettyDashedArrow <+> pretty func
 
 instance {-# OVERLAPPING #-} Pretty (Formatted [Binding]) where
-  pretty (Formatted (mode, bds)) = vsep (punctuate comma (map (\bd -> pretty (Formatted (mode, bd))) bds))
+  pretty (Formatted (SWEET, bds)) = vsep (punctuate comma (excludeVoidRho (\bd -> pretty (Formatted (SWEET, bd))) [] bds))
+    where
+      excludeVoidRho :: (Binding -> Doc ann) -> [Doc ann] -> [Binding] -> [Doc ann]
+      excludeVoidRho func acc [bd] = case bd of
+        BiVoid AtRho -> reverse acc
+        _ -> reverse (func bd : acc)
+      excludeVoidRho func acc (x : xs) = excludeVoidRho func (func x : acc) xs
+      excludeVoidRho func acc [] = reverse acc
+  pretty (Formatted (SALTY, bds)) = vsep (punctuate comma (map (\bd -> pretty (Formatted (SALTY, bd))) bds))
 
 complexApplication :: Expression -> (Expression, [Binding], [Expression])
-complexApplication (ExApplication (ExApplication expr tau) tau') = do
+complexApplication (ExApplication (ExApplication expr tau) tau') =
   let (before, taus, exprs) = complexApplication (ExApplication expr tau)
       taus' = tau' : taus
-  if null exprs
-    then (before, taus', [])
-    else case tau' of
-      BiTau (AtAlpha idx) expr' -> if idx == fromIntegral (length exprs)
-        then (before, taus', expr' : exprs)
-        else (before, taus', [])
-      _ -> (before, taus', [])
+   in if null exprs
+        then (before, taus', [])
+        else case tau' of
+          BiTau (AtAlpha idx) expr' ->
+            if idx == fromIntegral (length exprs)
+              then (before, taus', expr' : exprs)
+              else (before, taus', [])
+          _ -> (before, taus', [])
 complexApplication (ExApplication expr (BiTau (AtAlpha 0) expr')) = (expr, [BiTau (AtAlpha 0) expr'], [expr'])
 complexApplication (ExApplication expr tau) = (expr, [tau], [])
 
@@ -147,17 +118,18 @@
   pretty (Formatted (_, ExGlobal)) = pretty "Φ"
   pretty (Formatted (_, ExTermination)) = pretty "⊥"
   pretty (Formatted (_, ExMeta meta)) = prettyMeta meta
-  pretty (Formatted (SWEET, ExApplication (ExApplication expr tau) tau')) = do
+  pretty (Formatted (SWEET, ExApplication (ExApplication expr tau) tau')) =
     let (expr', taus, exprs) = complexApplication (ExApplication (ExApplication expr tau) tau')
-        args = if null exprs
-          then pretty (Formatted (SWEET, reverse taus))
-          else vsep (punctuate comma (map (\exp -> pretty (Formatted (SWEET, exp))) (reverse exprs)))
-    pretty (Formatted (SWEET, expr')) <> vsep [lparen, indent 2 args, rparen]
-  pretty (Formatted (SWEET, ExApplication expr tau)) = do
+        args =
+          if null exprs
+            then pretty (Formatted (SWEET, reverse taus))
+            else vsep (punctuate comma (map (\exp -> pretty (Formatted (SWEET, exp))) (reverse exprs)))
+     in pretty (Formatted (SWEET, expr')) <> vsep [lparen, indent 2 args, rparen]
+  pretty (Formatted (SWEET, ExApplication expr tau)) =
     let arg = case tau of
           BiTau (AtAlpha 0) expr' -> pretty (Formatted (SWEET, expr'))
           _ -> pretty (Formatted (SWEET, tau))
-    pretty (Formatted (SWEET, expr)) <> vsep [lparen, indent 2 arg, rparen]
+     in pretty (Formatted (SWEET, expr)) <> vsep [lparen, indent 2 arg, rparen]
   pretty (Formatted (mode, ExApplication expr tau)) = pretty (Formatted (mode, expr)) <> vsep [lparen, indent 2 (pretty (Formatted (mode, tau))), rparen]
   pretty (Formatted (mode, ExDispatch expr attr)) = pretty (Formatted (mode, expr)) <> pretty "." <> pretty attr
   pretty (Formatted (mode, ExMetaTail expr meta)) = pretty (Formatted (mode, expr)) <+> pretty "*" <+> prettyMeta meta
diff --git a/src/Replacer.hs b/src/Replacer.hs
--- a/src/Replacer.hs
+++ b/src/Replacer.hs
@@ -11,37 +11,37 @@
 replaceBindings :: [Binding] -> [Expression] -> [Expression] -> ([Binding], [Expression], [Expression])
 replaceBindings bds [] [] = (bds, [], [])
 replaceBindings [] ptns repls = ([], ptns, repls)
-replaceBindings (BiTau attr expr : bds) ptns repls = do
+replaceBindings (BiTau attr expr : bds) ptns repls =
   let (expr', ptns', repls') = replaceExpression expr ptns repls
-  let (bds', ptns'', repls'') = replaceBindings bds ptns' repls'
-  (BiTau attr expr' : bds', ptns'', repls'')
-replaceBindings (bd : bds) ptns repls = do
+      (bds', ptns'', repls'') = replaceBindings bds ptns' repls'
+   in (BiTau attr expr' : bds', ptns'', repls'')
+replaceBindings (bd : bds) ptns repls =
   let (bds', ptns', repls') = replaceBindings bds ptns repls
-  (bd : bds', ptns', repls')
+   in (bd : bds', ptns', repls')
 
 replaceExpression :: Expression -> [Expression] -> [Expression] -> (Expression, [Expression], [Expression])
 replaceExpression expr [] [] = (expr, [], [])
-replaceExpression expr ptns repls = do
+replaceExpression expr ptns repls =
   let (ptn : ptnsRest) = ptns
-  let (repl : replsRest) = repls
-  if expr == ptn
-    then replaceExpression repl ptnsRest replsRest
-    else case expr of
-      ExDispatch inner attr -> do
-        let (expr', ptns', repls') = replaceExpression inner ptns repls
-        (ExDispatch expr' attr, ptns', repls')
-      ExApplication inner tau -> do
-        let (expr', ptns', repls') = replaceExpression inner ptns repls
-        let ([tau'], ptns'', repls'') = replaceBindings [tau] ptns' repls'
-        (ExApplication expr' tau', ptns'', repls'')
-      ExFormation bds -> do
-        let (bds', ptns', repls') = replaceBindings bds ptns repls
-        (ExFormation bds', ptns', repls')
-      _ -> (expr, ptns, repls)
+      (repl : replsRest) = repls
+   in if expr == ptn
+        then replaceExpression repl ptnsRest replsRest
+        else case expr of
+          ExDispatch inner attr ->
+            let (expr', ptns', repls') = replaceExpression inner ptns repls
+             in (ExDispatch expr' attr, ptns', repls')
+          ExApplication inner tau ->
+            let (expr', ptns', repls') = replaceExpression inner ptns repls
+                ([tau'], ptns'', repls'') = replaceBindings [tau] ptns' repls'
+             in (ExApplication expr' tau', ptns'', repls'')
+          ExFormation bds ->
+            let (bds', ptns', repls') = replaceBindings bds ptns repls
+             in (ExFormation bds', ptns', repls')
+          _ -> (expr, ptns, repls)
 
 replaceProgram :: Program -> [Expression] -> [Expression] -> Maybe Program
 replaceProgram (Program expr) ptns repls
-  | length ptns == length repls = do
+  | length ptns == length repls =
       let (expr', _, _) = replaceExpression expr ptns repls
-      Just (Program expr')
+       in Just (Program expr')
   | otherwise = Nothing
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -26,7 +26,7 @@
 import Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds)
 import Data.Time.Format (defaultTimeLocale, formatTime)
 import Data.Version (showVersion)
-import Misc (withVoidRho)
+import Misc
 import Paths_phino (version)
 import Pretty (PrintMode, prettyAttribute, prettyBinding, prettyExpression, prettyProgram')
 import Text.Printf (printf)
@@ -86,6 +86,24 @@
       if head base == '.' || not (null children)
         then pure ('.' : attr', [object [("base", base)] children])
         else pure (base ++ ('.' : attr'), children)
+expression (DataObject "number" bytes) =
+  pure
+    ( "Q.org.eolang.number",
+      [ NodeComment (T.pack (either show show (hexToNum bytes))),
+        object
+          [("base", "Q.org.eolang.bytes")]
+          [object [] [NodeContent (T.pack bytes)]]
+      ]
+    )
+expression (DataObject "string" bytes) =
+  pure
+    ( "Q.org.eolang.string",
+      [ NodeComment (T.pack ('"' : hexToStr bytes ++ "\"")),
+        object
+          [("base", "Q.org.eolang.bytes")]
+          [object [] [NodeContent (T.pack bytes)]]
+      ]
+    )
 expression (ExApplication expr (BiTau attr texpr)) = do
   (base, children) <- expression expr
   (base', children') <- expression texpr
@@ -172,9 +190,10 @@
   root <- rootExpression expr'
   now <- getCurrentTime
   let phi = prettyProgram' (Program expr) mode
-      listing = if omitListing
-        then show (length (lines phi)) ++ " lines of phi"
-        else phi
+      listing =
+        if omitListing
+          then show (length (lines phi)) ++ " lines of phi"
+          else phi
   pure
     ( Document
         (Prologue [] Nothing [])
@@ -211,6 +230,7 @@
         <> TB.fromText (nameLocalName name)
         <> attrsText
         <> TB.fromString "/>"
+        <> newline
   | all isTextNode nodes =
       indent indentLevel
         <> TB.fromString "<"
@@ -221,25 +241,28 @@
         <> TB.fromString "</"
         <> TB.fromText (nameLocalName name)
         <> TB.fromString ">"
+        <> newline
   | otherwise =
       indent indentLevel
         <> TB.fromString "<"
         <> TB.fromText (nameLocalName name)
         <> attrsText
         <> TB.fromString ">"
+        <> newline
         <> mconcat (map (printNode (indentLevel + 1)) nodes)
         <> indent indentLevel
         <> TB.fromString "</"
         <> TB.fromText (nameLocalName name)
         <> TB.fromString ">"
+        <> newline
   where
-    attrsText = do
+    attrsText =
       let attrs' = M.toList attrs
           first = if length attrs' > 4 then newline <> indent (indentLevel + 1) else TB.fromString " "
-      mconcat
-        [ first <> TB.fromText (nameLocalName k) <> TB.fromString "=\"" <> TB.fromText v <> TB.fromString "\""
-          | (k, v) <- attrs'
-        ]
+       in mconcat
+            [ first <> TB.fromText (nameLocalName k) <> TB.fromString "=\"" <> TB.fromText v <> TB.fromString "\""
+              | (k, v) <- attrs'
+            ]
 
     isTextNode (NodeContent _) = True
     isTextNode _ = False
@@ -274,29 +297,29 @@
   Left err -> throwIO (CouldNotParseXMIR err)
 
 xmirToPhi :: Document -> IO Program
-xmirToPhi xmir = do
+xmirToPhi xmir =
   let doc = C.fromDocument xmir
-  case C.node doc of
-    NodeElement el
-      | nameLocalName (elementName el) == "object" -> do
-          obj <- case doc C.$/ C.element (toName "o") of
-            [o] -> xmirToFormationBinding o []
-            _ -> throwIO (InvalidXMIRFormat "Expected single <o> element in <object>" doc)
-          let pckg =
-                [ T.unpack t
-                  | 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"],
-                    tail' <- meta C.$/ C.element (toName "tail") C.&/ C.content,
-                    t <- T.splitOn "." tail'
-                ]
-          if null pckg
-            then pure (Program (ExFormation [obj, BiVoid AtRho]))
-            else do
-              let bd = foldr (\part acc -> BiTau (AtLabel part) (ExFormation [acc, BiLambda "Package", BiVoid AtRho])) obj pckg
-              pure (Program (ExFormation [bd, BiVoid AtRho]))
-      | otherwise -> throwIO (InvalidXMIRFormat "Expected single <object> element" doc)
-    _ -> throwIO (InvalidXMIRFormat "NodeElement is expected as root element" doc)
+   in case C.node doc of
+        NodeElement el
+          | nameLocalName (elementName el) == "object" -> do
+              obj <- case doc C.$/ C.element (toName "o") of
+                [o] -> xmirToFormationBinding o []
+                _ -> throwIO (InvalidXMIRFormat "Expected single <o> element in <object>" doc)
+              let pckg =
+                    [ T.unpack t
+                      | 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"],
+                        tail' <- meta C.$/ C.element (toName "tail") C.&/ C.content,
+                        t <- T.splitOn "." tail'
+                    ]
+              if null pckg
+                then pure (Program (ExFormation [obj, BiVoid AtRho]))
+                else
+                  let bd = foldr (\part acc -> BiTau (AtLabel part) (ExFormation [acc, BiLambda "Package", BiVoid AtRho])) obj pckg
+                   in pure (Program (ExFormation [bd, BiVoid AtRho]))
+          | otherwise -> throwIO (InvalidXMIRFormat "Expected single <object> element" doc)
+        _ -> throwIO (InvalidXMIRFormat "NodeElement is expected as root element" doc)
 
 xmirToFormationBinding :: C.Cursor -> [String] -> IO Binding
 xmirToFormationBinding cur fqn
@@ -330,20 +353,20 @@
         '.' : rest ->
           if null rest
             then throwIO (InvalidXMIRFormat "The @base attribute can't be just '.'" cur)
-            else do
+            else
               let args = cur C.$/ C.element (toName "o")
-              if null args
-                then throwIO (InvalidXMIRFormat (printf "Element with @base='%s' must have at least one child" base) cur)
-                else do
-                  expr <- xmirToExpression (head args) fqn
-                  attr <- toAttr rest cur
-                  let disp = ExDispatch expr attr
-                  xmirToApplication disp (tail args) fqn
-        "$" -> do
+               in if null args
+                    then throwIO (InvalidXMIRFormat (printf "Element with @base='%s' must have at least one child" base) cur)
+                    else do
+                      expr <- xmirToExpression (head args) fqn
+                      attr <- toAttr rest cur
+                      let disp = ExDispatch expr attr
+                      xmirToApplication disp (tail args) fqn
+        "$" ->
           if null (cur C.$/ C.element (toName "o"))
             then pure ExThis
             else throwIO (InvalidXMIRFormat "Application of '$' is illegal in XMIR" cur)
-        "Q" -> do
+        "Q" ->
           if null (cur C.$/ C.element (toName "o"))
             then pure ExGlobal
             else throwIO (InvalidXMIRFormat "Application of 'Q' is illegal in XMIR" cur)
@@ -403,7 +426,7 @@
 
 toAttr :: String -> C.Cursor -> IO Attribute
 toAttr attr cur = case attr of
-  'α' : rest' -> do
+  'α' : rest' ->
     case TR.readMaybe rest' :: Maybe Integer of
       Just idx -> pure (AtAlpha idx)
       Nothing -> throwIO (InvalidXMIRFormat "The attribute started with 'α' must be followed by integer" cur)
@@ -418,15 +441,15 @@
 hasAttr key cur = not (null (C.attribute (toName key) cur))
 
 getAttr :: String -> C.Cursor -> IO String
-getAttr key cur = do
+getAttr key cur =
   let attrs = C.attribute (toName key) cur
-  if null attrs
-    then throwIO (InvalidXMIRFormat (printf "Couldn't find attribute '%s'" key) cur)
-    else do
-      let attr = (T.unpack . head) attrs
-      if null attr
-        then throwIO (InvalidXMIRFormat (printf "The attribute '%s' is not expected to be empty" attr) cur)
-        else pure attr
+   in if null attrs
+        then throwIO (InvalidXMIRFormat (printf "Couldn't find attribute '%s'" key) cur)
+        else
+          let attr = (T.unpack . head) attrs
+           in if null attr
+                then throwIO (InvalidXMIRFormat (printf "The attribute '%s' is not expected to be empty" attr) cur)
+                else pure attr
 
 hasText :: C.Cursor -> Bool
 hasText cur = any isNonEmptyTextNode (C.child cur)
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -52,15 +52,7 @@
     Object o ->
       asum
         [ Ordinal <$> o .: "ordinal",
-          Length <$> o .: "length",
-          do
-            vals <- o .: "add"
-            case vals of
-              [first_, second_] -> do
-                first <- parseJSON first_
-                second <- parseJSON second_
-                pure (Add first second)
-              _ -> fail "'add' requires exactly two elements"
+          Length <$> o .: "length"
         ]
     Number num -> pure (Literal (round num))
     _ ->
@@ -84,7 +76,7 @@
               Not <$> v .: "not",
               Alpha <$> v .: "alpha",
               NF <$> v .: "nf",
-              FN <$> v .: "fn",
+              XI <$> v .: "xi",
               do
                 vals <- v .: "eq"
                 case vals of
@@ -116,7 +108,6 @@
 data Number
   = Ordinal Attribute
   | Length Binding
-  | Add Number Number
   | Literal Integer
   deriving (Generic, Show)
 
@@ -133,7 +124,7 @@
   | Alpha Attribute
   | Eq Comparable Comparable
   | NF Expression
-  | FN Expression
+  | XI Expression
   deriving (Generic, Show)
 
 data Extra = Extra
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -153,7 +153,7 @@
       withStdin "Q -> [[ x -> 5]]" $
         testCLI
           ["rewrite", "--nothing", "--sweet"]
-          ["{⟦\n  x ↦ 5,\n  ρ ↦ ∅\n⟧}"]
+          ["{⟦\n  x ↦ 5\n⟧}"]
 
     it "rewrites as XMIR" $
       withStdin "Q -> [[ x -> Q.y ]]" $
@@ -168,10 +168,8 @@
           [ unlines
               [ "{⟦",
                 "  app ↦ ⟦",
-                "    x ↦ Φ.number,",
-                "    ρ ↦ ∅",
-                "  ⟧,",
-                "  ρ ↦ ∅",
+                "    x ↦ Φ.number",
+                "  ⟧",
                 "⟧}"
               ]
           ]
diff --git a/test/PrettySpec.hs b/test/PrettySpec.hs
--- a/test/PrettySpec.hs
+++ b/test/PrettySpec.hs
@@ -45,9 +45,10 @@
           (prep SWEET)
           [ ("Q -> $", "{ξ}"),
             ("Q -> Q.org.eolang(x -> Q.x)", "{Φ̇(\n  x ↦ Φ.x\n)}"),
-            ("Q -> [[ x -> [[ y -> ?, z -> ? ]] ]]", "{⟦\n  x(y, z, ρ) ↦ ⟦⟧,\n  ρ ↦ ∅\n⟧}"),
+            ("Q -> [[ x -> [[ y -> ?, z -> ? ]] ]]", "{⟦\n  x(y, z) ↦ ⟦⟧\n⟧}"),
             ("Q -> 5", "{5}"),
-            ("Q -> [[ x -> \"hello\"]]", "{⟦\n  x ↦ \"hello\",\n  ρ ↦ ∅\n⟧}"),
+            ("Q -> [[ x -> \"hello\"]]", "{⟦\n  x ↦ \"hello\"\n⟧}"),
+            ("Q -> [[ x -> \"hello\", y -> 5]]", "{⟦\n  x ↦ \"hello\",\n  y ↦ 5\n⟧}"),
             ("Q -> Q.x(x -> 1)(y -> 2)(z -> 3)", "{Φ.x(\n  x ↦ 1,\n  y ↦ 2,\n  z ↦ 3\n)}"),
             ("Q -> Q.x(~0 -> Q.y)", "{Φ.x(\n  Φ.y\n)}"),
             ("Q -> Q.x(~0 -> 1)(~1 -> 2)(~2 -> 3)", "{Φ.x(\n  1,\n  2,\n  3\n)}"),