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.40
+version:            0.0.0.41
 license:            MIT
 synopsis:           Command-Line Manipulator of 𝜑-Calculus Expressions
 description:        Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
@@ -37,11 +37,13 @@
     Functions,
     Term,
     Misc,
+    Must,
     Logger,
     Regexp,
     Pretty,
     Random,
-    XMIR
+    XMIR,
+    LaTeX
   hs-source-dirs: src
   other-modules:
     Paths_phino
@@ -102,6 +104,7 @@
     MiscSpec,
     XMIRSpec,
     DataizeSpec,
+    FunctionsSpec,
     Paths_phino
   autogen-modules:
     Paths_phino
diff --git a/src/Ast.hs b/src/Ast.hs
--- a/src/Ast.hs
+++ b/src/Ast.hs
@@ -47,7 +47,16 @@
   | AtLambda -- λ, used only in yaml conditions
   | AtDelta -- Δ, used only in yaml conditions
   | AtMeta String -- !a
-  deriving (Eq, Show, Generic)
+  deriving (Eq, Generic, Ord)
+
+instance Show Attribute where
+  show (AtLabel label) = label
+  show (AtAlpha idx) = 'α' : show idx
+  show AtRho = "ρ"
+  show AtPhi = "φ"
+  show AtDelta = "Δ"
+  show AtLambda = "λ"
+  show (AtMeta meta) = '!' : meta
 
 countNodes :: Program -> Integer
 countNodes (Program expr) = countNodes' expr
diff --git a/src/Builder.hs b/src/Builder.hs
--- a/src/Builder.hs
+++ b/src/Builder.hs
@@ -26,20 +26,23 @@
 import Control.Exception (Exception, throwIO)
 import qualified Data.Map.Strict as Map
 import Matcher
-import Pretty (prettyAttribute, prettyBinding, prettyExpression, prettySubst, prettyBytes)
+import Misc (uniqueBindings)
+import Pretty (prettyAttribute, prettyBinding, prettyBytes, prettyExpression, prettySubst)
 import Text.Printf (printf)
 import Yaml (ExtraArgument (..))
 
 data BuildException
-  = CouldNotBuildExpression {_expr :: Expression, _meta :: String}
-  | CouldNotBuildAttribute {_attr :: Attribute, _meta :: String}
-  | CouldNotBuildBinding {_bd :: Binding, _meta :: String}
-  | CouldNotBuildBytes {_bts :: Bytes, _meta :: String}
+  = CouldNotBuildExpression {_expr :: Expression, _msg :: String}
+  | CouldNotBuildAttribute {_attr :: Attribute, _msg :: String}
+  | CouldNotBuildBinding {_bd :: Binding, _msg :: String}
+  | CouldNotBuildBytes {_bts :: Bytes, _msg :: String}
   deriving (Exception)
 
 metaMsg :: String -> String
 metaMsg = printf "meta '%s' is either does not exist or refers to an inappropriate term"
 
+type Built a = Either String a
+
 -- @todo #277:30min Error messages are too verbose. Now, if we can't build expression or binding, we
 --  throw an exception and just print whole expression or binding to console.
 --  If this elements are big, it's just a mess and error message became unreadable. It would be nice to
@@ -48,23 +51,23 @@
   show CouldNotBuildExpression {..} =
     printf
       "Couldn't build expression, %s\n--Expression: %s"
-      (metaMsg _meta)
+      _msg
       (prettyExpression _expr)
   show CouldNotBuildAttribute {..} =
     printf
       "Couldn't build attribute '%s', %s"
       (prettyAttribute _attr)
-      (metaMsg _meta)
+      _msg
   show CouldNotBuildBinding {..} =
     printf
       "Couldn't build binding, %s\n--Binding: %s"
-      (metaMsg _meta)
+      _msg
       (prettyBinding _bd)
   show CouldNotBuildBytes {..} =
     printf
       "Couldn't build bytes '%s', %s"
       (prettyBytes _bts)
-      (metaMsg _meta)
+      _msg
 
 contextualize :: Expression -> Expression -> Program -> Expression
 contextualize ExGlobal _ (Program expr) = expr
@@ -77,22 +80,22 @@
       bexpr' = contextualize bexpr context prog
    in ExApplication expr' (BiTau attr bexpr')
 
-buildAttribute :: Attribute -> Subst -> Either String Attribute
+buildAttribute :: Attribute -> Subst -> Built Attribute
 buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup meta mp of
   Just (MvAttribute attr) -> Right attr
-  _ -> Left meta
+  _ -> Left (metaMsg meta)
 buildAttribute attr _ = Right attr
 
-buildBytes :: Bytes -> Subst -> Either String Bytes
+buildBytes :: Bytes -> Subst -> Built Bytes
 buildBytes (BtMeta meta) (Subst mp) = case Map.lookup meta mp of
   Just (MvBytes bytes) -> Right bytes
-  _ -> Left meta
+  _ -> Left (metaMsg meta)
 buildBytes bts _ = Right bts
 
 -- Build binding
 -- The function returns [Binding] because the BiMeta is always attached
 -- to the list of bindings
-buildBinding :: Binding -> Subst -> Either String [Binding]
+buildBinding :: Binding -> Subst -> Built [Binding]
 buildBinding (BiTau attr expr) subst = do
   attribute <- buildAttribute attr subst
   (expression, _) <- buildExpression expr subst
@@ -101,18 +104,18 @@
   attribute <- buildAttribute attr subst
   Right [BiVoid attribute]
 buildBinding (BiMeta meta) (Subst mp) = case Map.lookup meta mp of
-  Just (MvBindings bds) -> Right bds
-  _ -> Left meta
+  Just (MvBindings bds) -> uniqueBindings bds
+  _ -> Left (metaMsg meta)
 buildBinding (BiDelta bytes) subst = do
   bts <- buildBytes bytes subst
   Right [BiDelta bts]
 buildBinding (BiMetaLambda meta) (Subst mp) = case Map.lookup meta mp of
   Just (MvFunction func) -> Right [BiLambda func]
-  _ -> Left meta
+  _ -> Left (metaMsg meta)
 buildBinding binding _ = Right [binding]
 
 -- Build bindings that may contain meta binding (BiMeta)
-buildBindings :: [Binding] -> Subst -> Either String [Binding]
+buildBindings :: [Binding] -> Subst -> Built [Binding]
 buildBindings [] _ = Right []
 buildBindings (bd : rest) subst = do
   first <- buildBinding bd subst
@@ -130,7 +133,7 @@
 -- where X is built expression and Y is context of X
 -- If meta expression is built from MvExpression, is has
 -- context from original Program. It have default context otherwise
-buildExpression :: Expression -> Subst -> Either String (Expression, Expression)
+buildExpression :: Expression -> Subst -> Built (Expression, Expression)
 buildExpression (ExDispatch expr attr) subst = do
   (dispatched, scope) <- buildExpression expr subst
   attr <- buildAttribute attr subst
@@ -140,38 +143,42 @@
   bds <- buildBinding (BiTau battr bexpr) subst
   Right (ExApplication applied (head bds), scope)
 buildExpression (ExFormation bds) subst = do
-  bds' <- buildBindings bds subst
+  bds' <- buildBindings bds subst >>= uniqueBindings
   Right (ExFormation bds', defaultScope)
 buildExpression (ExMeta meta) (Subst mp) = case Map.lookup meta mp of
-  Just (MvExpression expr scope) -> Right (expr, scope)
-  _ -> Left meta
+  Just (MvExpression expr scope) ->
+    let res = Right (expr, scope)
+     in case expr of
+          ExFormation bds -> uniqueBindings bds >> res
+          _ -> res
+  _ -> Left (metaMsg meta)
 buildExpression (ExMetaTail expr meta) subst = do
   let (Subst mp) = subst
   (expression, scope) <- buildExpression expr subst
   case Map.lookup meta mp of
     Just (MvTail tails) -> Right (buildExpressionWithTails expression tails subst, scope)
-    _ -> Left meta
+    _ -> Left (metaMsg meta)
 buildExpression expr _ = Right (expr, defaultScope)
 
 buildBytesThrows :: Bytes -> Subst -> IO Bytes
 buildBytesThrows bytes subst = case buildBytes bytes subst of
   Right bts -> pure bts
-  Left meta -> throwIO (CouldNotBuildBytes bytes meta)
+  Left msg -> throwIO (CouldNotBuildBytes bytes msg)
 
 buildBindingThrows :: Binding -> Subst -> IO [Binding]
 buildBindingThrows bd subst = case buildBinding bd subst of
   Right bds -> pure bds
-  Left meta -> throwIO (CouldNotBuildBinding bd meta)
+  Left msg -> throwIO (CouldNotBuildBinding bd msg)
 
 buildAttributeThrows :: Attribute -> Subst -> IO Attribute
 buildAttributeThrows attr subst = case buildAttribute attr subst of
   Right attr' -> pure attr'
-  Left meta -> throwIO (CouldNotBuildAttribute attr meta)
+  Left msg -> throwIO (CouldNotBuildAttribute attr msg)
 
 buildExpressionThrows :: Expression -> Subst -> IO (Expression, Expression)
 buildExpressionThrows expr subst = case buildExpression expr subst of
   Right built -> pure built
-  Left meta -> throwIO (CouldNotBuildExpression expr meta)
+  Left msg -> throwIO (CouldNotBuildExpression expr msg)
 
 -- Build a several expression from one expression and several substitutions
 buildExpressions :: Expression -> [Subst] -> IO [(Expression, Expression)]
diff --git a/src/CLI.hs b/src/CLI.hs
--- a/src/CLI.hs
+++ b/src/CLI.hs
@@ -15,17 +15,20 @@
 import Control.Monad (when)
 import Data.Char (toLower, toUpper)
 import Data.List (intercalate)
+import Data.Maybe (isJust, isNothing)
 import Data.Version (showVersion)
 import Dataize (DataizeContext (DataizeContext), dataize)
 import Functions (buildTerm)
 import qualified Functions
+import LaTeX (explainRules, programToLaTeX)
 import Logger
 import Misc (ensuredFile)
 import qualified Misc
+import Must (Must (..))
 import Options.Applicative
 import Parser (parseProgramThrows)
 import Paths_phino (version)
-import Pretty (PrintMode (SALTY, SWEET), prettyBytes, prettyProgram')
+import Pretty (PrintMode (SALTY, SWEET), prettyBytes, prettyProgram', Encoding (UNICODE))
 import Rewriter (RewriteContext (RewriteContext), rewrite')
 import System.Exit (ExitCode (..), exitFailure)
 import System.IO (getContents')
@@ -48,22 +51,33 @@
 data Command
   = CmdRewrite OptsRewrite
   | CmdDataize OptsDataize
+  | CmdExplain OptsExplain
 
-data IOFormat = XMIR | PHI
+data IOFormat = XMIR | PHI | LATEX
   deriving (Eq)
 
 instance Show IOFormat where
   show XMIR = "xmir"
   show PHI = "phi"
+  show LATEX = "latex"
 
 data OptsDataize = OptsDataize
   { logLevel :: LogLevel,
     inputFormat :: IOFormat,
     maxDepth :: Integer,
     maxCycles :: Integer,
+    depthSensitive :: Bool,
     inputFile :: Maybe FilePath
   }
 
+data OptsExplain = OptsExplain
+  { logLevel :: LogLevel,
+    rules :: [FilePath],
+    normalize :: Bool,
+    shuffle :: Bool,
+    targetFile :: Maybe FilePath
+  }
+
 data OptsRewrite = OptsRewrite
   { logLevel :: LogLevel,
     rules :: [FilePath],
@@ -71,22 +85,24 @@
     outputFormat :: IOFormat,
     printMode :: PrintMode,
     normalize :: Bool,
-    nothing :: Bool,
     shuffle :: Bool,
     omitListing :: Bool,
     omitComments :: Bool,
-    must :: Integer,
+    depthSensitive :: Bool,
+    must :: Must,
     maxDepth :: Integer,
     maxCycles :: Integer,
+    inPlace :: Bool,
     targetFile :: Maybe FilePath,
     inputFile :: Maybe FilePath
   }
 
 parseIOFormat :: String -> ReadM IOFormat
-parseIOFormat type' = eitherReader $ \format -> case map toLower format of
-  "xmir" -> Right XMIR
-  "phi" -> Right PHI
-  _ -> Left (printf "invalid %s format: expected '%s' or '%s'" type' (show PHI) (show XMIR))
+parseIOFormat type' = eitherReader $ \format -> case (map toLower format, type') of
+  ("xmir", _) -> Right XMIR
+  ("phi", _) -> Right PHI
+  ("latex", "output") -> Right LATEX
+  _ -> Left (printf "The value '%s' can't be used for '--%s' option, use --help to check possible values" format type')
 
 argInputFile :: Parser (Maybe FilePath)
 argInputFile = optional (argument str (metavar "FILE" <> help "Path to input file"))
@@ -98,8 +114,11 @@
 optMaxCycles = option auto (long "max-cycles" <> metavar "CYCLES" <> help "Maximum number of rewriting cycles across all rules" <> value 25 <> showDefault)
 
 optInputFormat :: Parser IOFormat
-optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Program input format (phi, xmir)" <> value PHI <> showDefault)
+optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Program input format (phi, xmir, latex)" <> value PHI <> showDefault)
 
+optDepthSensitive :: Parser Bool
+optDepthSensitive = switch (long "depth-sensitive" <> help "Fail if rewriting is not finished after reaching max attempts (see --max-cycles or --max-depth)")
+
 optLogLevel :: Parser LogLevel
 optLogLevel =
   option
@@ -122,6 +141,29 @@
       "NONE" -> Right NONE
       _ -> Left $ "unknown log-level: " <> lvl
 
+optRule :: Parser [FilePath]
+optRule = many (strOption (long "rule" <> metavar "FILE" <> help "Path to custom rule"))
+
+optNormalize :: Parser Bool
+optNormalize = switch (long "normalize" <> help "Use built-in normalization rules")
+
+optTarget :: Parser (Maybe FilePath)
+optTarget = optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to"))
+
+optShuffle :: Parser Bool
+optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying")
+
+explainParser :: Parser Command
+explainParser =
+  CmdExplain
+    <$> ( OptsExplain
+            <$> optLogLevel
+            <*> optRule
+            <*> optNormalize
+            <*> optShuffle
+            <*> optTarget
+        )
+
 dataizeParser :: Parser Command
 dataizeParser =
   CmdDataize
@@ -130,6 +172,7 @@
             <*> optInputFormat
             <*> optMaxDepth
             <*> optMaxCycles
+            <*> optDepthSensitive
             <*> argInputFile
         )
 
@@ -138,29 +181,36 @@
   CmdRewrite
     <$> ( OptsRewrite
             <$> optLogLevel
-            <*> many (strOption (long "rule" <> metavar "FILE" <> help "Path to custom rule"))
+            <*> optRule
             <*> optInputFormat
             <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help "Program output format (phi, xmir)" <> value PHI <> showDefault)
             <*> flag SALTY SWEET (long "sweet" <> help "Print 𝜑-program using syntax sugar")
-            <*> switch (long "normalize" <> help "Use built-in normalization rules")
-            <*> switch (long "nothing" <> help "Just desugar provided 𝜑-program")
-            <*> switch (long "shuffle" <> help "Shuffle rules before applying")
+            <*> optNormalize
+            <*> optShuffle
             <*> switch (long "omit-listing" <> help "Omit full program listing in XMIR output")
             <*> switch (long "omit-comments" <> help "Omit comments in XMIR output")
-            <*> ( flag' 1 (long "must" <> help "Enable must-rewrite with default value 1")
-                    <|> option auto (long "must" <> metavar "N" <> help "Must-rewrite, stops execution if not exactly N rules applied (default 1 when specified without value, if 0 - flag is disabled)" <> value 0)
-                )
+            <*> optDepthSensitive
+            <*> option
+              auto
+              ( long "must"
+                  <> metavar "RANGE"
+                  <> help "Must-rewrite range (e.g., '3', '..5', '3..', '3..5'). Stops execution if number of rules applied is not in range. Use 0 to disable."
+                  <> value MtDisabled
+                  <> showDefaultWith show
+              )
             <*> optMaxDepth
             <*> optMaxCycles
-            <*> optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to"))
+            <*> switch (long "in-place" <> help "Edit file in-place instead of printing to output")
+            <*> optTarget
             <*> argInputFile
         )
 
 commandParser :: Parser Command
 commandParser =
   hsubparser
-    ( command "rewrite" (info (rewriteParser <**> helper) (progDesc "Rewrite the program"))
-        <> command "dataize" (info (dataizeParser <**> helper) (progDesc "Dataize the program"))
+    ( command "rewrite" (info rewriteParser (progDesc "Rewrite the program"))
+        <> command "dataize" (info dataizeParser (progDesc "Dataize the program"))
+        <> command "explain" (info explainParser (progDesc "Explain rules in LaTeX format"))
     )
 
 parserInfo :: ParserInfo Command
@@ -181,6 +231,7 @@
   let level = case cmd of
         CmdRewrite OptsRewrite {logLevel} -> logLevel
         CmdDataize OptsDataize {logLevel} -> logLevel
+        CmdExplain OptsExplain {logLevel} -> logLevel
    in setLogLevel level
 
 runCLI :: [String] -> IO ()
@@ -188,65 +239,72 @@
   cmd <- handleParseResult (execParserPure defaultPrefs parserInfo args)
   setLogLevel' cmd
   case cmd of
-    CmdRewrite OptsRewrite {..} -> do
-      validateMaxDepth maxDepth
-      validateMaxCycles maxCycles
-      validateMust must
-      logDebug (printf "Amount of rewriting cycles: %d" maxDepth)
+    CmdRewrite opts@OptsRewrite {..} -> do
+      validateOpts
+      logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" maxCycles maxDepth)
       input <- readInput inputFile
-      rules' <- getRules
+      rules' <- getRules normalize shuffle rules
       program <- parseProgram input inputFormat
-      rewritten <- rewrite' program rules' (RewriteContext program maxDepth maxCycles buildTerm must)
+      rewritten <- rewrite' program rules' (RewriteContext program maxDepth maxCycles depthSensitive buildTerm must)
       logDebug (printf "Printing rewritten 𝜑-program as %s" (show outputFormat))
-      prog <- printProgram rewritten outputFormat printMode
-      output prog
+      prog <- printProgram rewritten outputFormat printMode input
+      output targetFile prog
       where
-        getRules :: IO [Y.Rule]
-        getRules = do
-          ordered <-
-            if nothing
-              then do
-                logDebug "The --nothing option is provided, no rules are used"
-                pure []
-              else
-                if normalize
-                  then do
-                    let rules' = normalizationRules
-                    logDebug (printf "The --normalize option is provided, %d built-it normalization rules are used" (length rules'))
-                    pure rules'
-                  else
-                    if null rules
-                      then throwIO (InvalidRewriteArguments "no --rule, no --normalize, no --nothing are provided")
-                      else do
-                        logDebug (printf "Using rules from files: [%s]" (intercalate ", " rules))
-                        yamls <- mapM ensuredFile rules
-                        mapM Y.yamlRule yamls
-          if shuffle
-            then do
-              logDebug "The --shuffle option is provided, rules are used in random order"
-              Misc.shuffle ordered
-            else pure ordered
-        printProgram :: Program -> IOFormat -> PrintMode -> IO String
-        printProgram prog PHI mode = pure (prettyProgram' prog mode)
-        printProgram prog XMIR mode = do
-          xmir <- programToXMIR prog (XmirContext omitListing omitComments printMode)
+        validateOpts :: IO ()
+        validateOpts = do
+          when
+            (printMode == SWEET && outputFormat == XMIR)
+            (throwIO (InvalidRewriteArguments "The --sweet and --output=xmir can't stay together"))
+          when
+            (inPlace && isNothing inputFile)
+            (throwIO (InvalidRewriteArguments "--in-place requires an input file"))
+          when
+            (inPlace && isJust targetFile)
+            (throwIO (InvalidRewriteArguments "--in-place and --target cannot be used together"))
+          validateMaxDepth maxDepth
+          validateMaxCycles maxCycles
+          validateMust must
+        printProgram :: Program -> IOFormat -> PrintMode -> String -> IO String
+        printProgram prog PHI mode _ = pure (prettyProgram' prog mode UNICODE)
+        printProgram prog XMIR _ listing = do
+          xmir <- programToXMIR prog (XmirContext omitListing omitComments listing)
           pure (printXMIR xmir)
-        output :: String -> IO ()
-        output prog = case targetFile of
-          Nothing -> do
-            logDebug "The option '--target' is not specified, printing to console..."
-            putStrLn prog
-          Just file -> do
+        printProgram prog LATEX mode _ = pure (programToLaTeX prog mode)
+        output :: Maybe FilePath -> String -> IO ()
+        output target prog = case (inPlace, target, inputFile) of
+          (True, _, Just file) -> do
+            logDebug (printf "The option '--in-place' is specified, writing back to '%s'..." file)
+            writeFile file prog
+            logInfo (printf "The file '%s' was modified in-place" file)
+          (False, Just file, _) -> do
             logDebug (printf "The option '--target' is specified, printing to '%s'..." file)
             writeFile file prog
-            logInfo (printf "The result program was saved in '%s'" file)
-    CmdDataize OptsDataize {..} -> do
-      validateMaxDepth maxDepth
-      validateMaxCycles maxCycles
+            logInfo (printf "The command result was saved in '%s'" file)
+          (False, Nothing, _) -> do
+            logDebug "The option '--target' is not specified, printing to console..."
+            putStrLn prog
+    CmdDataize opts@OptsDataize {..} -> do
+      validateOpts
       input <- readInput inputFile
       prog <- parseProgram input inputFormat
-      dataized <- dataize prog (DataizeContext prog maxDepth maxCycles buildTerm)
+      dataized <- dataize prog (DataizeContext prog maxDepth maxCycles depthSensitive buildTerm)
       maybe (throwIO CouldNotDataize) (putStrLn . prettyBytes) dataized
+      where
+        validateOpts :: IO ()
+        validateOpts = do
+          validateMaxDepth maxDepth
+          validateMaxCycles maxCycles
+    CmdExplain opts@OptsExplain {..} -> do
+      validateOpts
+      rules' <- getRules normalize shuffle rules
+      let latex = explainRules rules'
+      output targetFile (explainRules rules')
+      where
+        validateOpts :: IO ()
+        validateOpts =
+          when
+            (null rules && not normalize)
+            (throwIO (InvalidRewriteArguments "Either --rule or --normalize must be specified"))
   where
     validateIntArgument :: Integer -> (Integer -> Bool) -> String -> IO ()
     validateIntArgument num cmp msg =
@@ -257,8 +315,20 @@
     validateMaxDepth depth = validateIntArgument depth (<= 0) "--max-depth must be positive"
     validateMaxCycles :: Integer -> IO ()
     validateMaxCycles cycles = validateIntArgument cycles (<= 0) "--max-cycles must be positive"
-    validateMust :: Integer -> IO ()
-    validateMust must = validateIntArgument must (< 0) "--must must be positive"
+    validateMust :: Must -> IO ()
+    validateMust MtDisabled = pure ()
+    validateMust (MtExact n) = validateIntArgument n (<= 0) "--must exact value must be positive"
+    validateMust (MtRange minVal maxVal) = do
+      maybe (pure ()) (\n -> validateIntArgument n (< 0) "--must minimum must be non-negative") minVal
+      maybe (pure ()) (\n -> validateIntArgument n (< 0) "--must maximum must be non-negative") maxVal
+      case (minVal, maxVal) of
+        (Just min, Just max)
+          | min > max ->
+              throwIO
+                ( InvalidRewriteArguments
+                    (printf "--must range invalid: minimum (%d) is greater than maximum (%d)" min max)
+                )
+        _ -> pure ()
     readInput :: Maybe FilePath -> IO String
     readInput inputFile' = case inputFile' of
       Just pth -> do
@@ -272,3 +342,34 @@
     parseProgram xmir XMIR = do
       doc <- parseXMIRThrows xmir
       xmirToPhi doc
+    getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule]
+    getRules normalize shuffle rules = do
+      ordered <-
+        if normalize
+          then do
+            let rules' = normalizationRules
+            logDebug (printf "The --normalize option is provided, %d built-it normalization rules are used" (length rules'))
+            pure rules'
+          else
+            if null rules
+              then do
+                logDebug "No --rule and no --normalize options are provided, no rules are used"
+                pure []
+              else do
+                logDebug (printf "Using rules from files: [%s]" (intercalate ", " rules))
+                yamls <- mapM ensuredFile rules
+                mapM Y.yamlRule yamls
+      if shuffle
+        then do
+          logDebug "The --shuffle option is provided, rules are used in random order"
+          Misc.shuffle ordered
+        else pure ordered
+    output :: Maybe FilePath -> String -> IO ()
+    output target content = case target of
+      Nothing -> do
+        logDebug "The option '--target' is not specified, printing to console..."
+        putStrLn content
+      Just file -> do
+        logDebug (printf "The option '--target' is specified, printing to '%s'..." file)
+        writeFile file content
+        logInfo (printf "The command result was saved in '%s'" file)
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -11,6 +11,7 @@
 import Control.Exception (throwIO)
 import Data.List (partition)
 import Misc
+import Must (Must (..))
 import Rewriter (RewriteContext (RewriteContext), rewrite')
 import Rule (RuleContext (RuleContext), isNF)
 import Term (BuildTermFunc)
@@ -22,11 +23,12 @@
   { _program :: Program,
     _maxDepth :: Integer,
     _maxCycles :: Integer,
+    _depthSensitive :: Bool,
     _buildTerm :: BuildTermFunc
   }
 
 switchContext :: DataizeContext -> RewriteContext
-switchContext DataizeContext {..} = RewriteContext _program _maxDepth _maxCycles _buildTerm 0
+switchContext DataizeContext {..} = RewriteContext _program _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled
 
 maybeBinding :: (Binding -> Bool) -> [Binding] -> (Maybe Binding, [Binding])
 maybeBinding _ [] = (Nothing, [])
diff --git a/src/Functions.hs b/src/Functions.hs
--- a/src/Functions.hs
+++ b/src/Functions.hs
@@ -14,6 +14,7 @@
 import Data.Functor
 import Data.Set (Set)
 import qualified Data.Set
+import qualified Data.Set as Set
 import GHC.IO (unsafePerformIO)
 import Matcher
 import Misc
@@ -40,6 +41,7 @@
 buildTerm "string" = _string
 buildTerm "number" = _number
 buildTerm "sum" = _sum
+buildTerm "join" = _join
 buildTerm func = _unsupported func
 
 argToBytes :: Y.ExtraArgument -> Subst -> Program -> IO Bytes
@@ -85,17 +87,8 @@
       Y.ArgBinding bd -> do
         bds <- buildBindingThrows bd subst
         rest' <- argsToAttrs rest
-        pure (attrsFromBindings bds ++ rest')
+        pure (map show (attributesFromBindings bds) ++ rest')
       Y.ArgBytes _ -> throwIO (userError "Bytes can't be argument of random-tau() function")
-    attrsFromBindings :: [Binding] -> [String]
-    attrsFromBindings [] = []
-    attrsFromBindings (bd : bds) =
-      let attr = case bd of
-            BiTau attr _ -> attr
-            BiDelta _ -> AtDelta
-            BiLambda _ -> AtLambda
-            BiVoid attr -> attr
-       in prettyAttribute attr : attrsFromBindings bds
     randomTau :: [String] -> IO String
     randomTau attrs = do
       tau <- randomString "a🌵%d"
@@ -216,6 +209,38 @@
 _sum args subst prog = do
   nums <- traverse (\arg -> argToNumber arg subst prog) args
   pure (TeExpression (DataNumber (numToBts (sum nums))))
+
+_join :: BuildTermMethod
+_join [] _ _ = pure (TeBindings [])
+_join args subst _ = do
+  bds <- buildBindings args
+  pure (TeBindings (join' bds Set.empty))
+  where
+    buildBindings :: [Y.ExtraArgument] -> IO [Binding]
+    buildBindings [] = pure []
+    buildBindings (Y.ArgBinding bd : args') = do
+      bds <- buildBindingThrows bd subst
+      next <- buildBindings args'
+      pure (bds ++ next)
+    buildBindings _ = throwIO (userError "Function 'join' can work with bindings only")
+    join' :: [Binding] -> Set.Set Attribute -> [Binding]
+    join' [] _ = []
+    join' (bd : bds) attrs =
+      let [attr] = attributesFromBindings [bd]
+       in if Set.member attr attrs
+            then
+              if attr == AtRho || attr == AtDelta || attr == AtLambda
+                then join' bds attrs
+                else
+                  let new = case bd of
+                        BiTau attr expr -> BiTau (updated attr attrs) expr
+                        BiVoid attr -> BiVoid (updated attr attrs)
+                   in new : join' bds attrs
+            else bd : join' bds (Set.insert attr attrs)
+    updated :: Attribute -> Set.Set Attribute -> Attribute
+    updated attr attrs =
+      let (TeAttribute attr') = unsafePerformIO (_randomTau (map Y.ArgAttribute (Set.toList attrs)) subst (Program ExGlobal))
+       in attr'
 
 _unsupported :: BuildTermFunc
 _unsupported func _ _ _ = throwIO (userError (printf "Function %s() is not supported or does not exist" func))
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
new file mode 100644
--- /dev/null
+++ b/src/LaTeX.hs
@@ -0,0 +1,44 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module LaTeX (explainRules, programToLaTeX) where
+
+import Data.List (intercalate)
+import Data.Maybe (fromMaybe)
+import qualified Yaml as Y
+import Ast (Program)
+import Pretty (PrintMode, prettyProgram', Encoding (ASCII))
+
+programToLaTeX :: Program -> PrintMode -> String
+programToLaTeX prog mode = unlines
+  [
+    "\\documentclass{article}",
+    "\\usepackage{eolang}",
+    "\\begin{document}",
+    "\\begin{phiquation}",
+    prettyProgram' prog mode ASCII,
+    "\\end{phiquation}",
+    "\\end{document}"
+  ]
+
+-- @todo #114:30min Implement LaTeX conversion for rules.
+--  Convert Rule data structure to LaTeX inference rule format.
+--  Each rule should be formatted as a LaTeX inference rule with
+--  pattern, result, and optional conditions.
+--  Tests must be added for LaTeX conversion logic.
+explainRule :: Y.Rule -> String
+explainRule rule = "\\rule{" ++ fromMaybe "unnamed" (Y.name rule) ++ "}"
+
+-- @todo #114:30min Create LaTeX document wrapper.
+--  Generate proper LaTeX document with tabular format for rules.
+--  Each rule should be   in its own tabular environment.
+--  Include tests for document structure generation.
+explainRules :: [Y.Rule] -> String
+explainRules rules' =
+  unlines
+    [ "\\documentclass{article}",
+      "\\usepackage{amsmath}",
+      "\\begin{document}"
+    ]
+    ++ unlines (map explainRule rules')
+    ++ "\\end{document}"
diff --git a/src/Misc.hs b/src/Misc.hs
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -20,6 +20,10 @@
     shuffle,
     toDouble,
     btsToUnescapedStr,
+    attributesFromBindings,
+    uniqueBindings,
+    uniqueBindings',
+    validateYamlObject,
     pattern DataObject,
     pattern DataString,
     pattern DataNumber,
@@ -38,6 +42,7 @@
 import qualified Data.ByteString.Lazy.UTF8 as U
 import Data.Char (chr, isPrint, ord)
 import Data.List (intercalate)
+import qualified Data.Set as Set
 import qualified Data.Text as T
 import qualified Data.Text.Encoding as T
 import qualified Data.Vector as V
@@ -48,6 +53,9 @@
 import System.FilePath ((</>))
 import System.Random.Stateful
 import Text.Printf (printf)
+import Data.Aeson (Object)
+import qualified Data.Aeson.KeyMap as KeyMap
+import qualified Data.Aeson.Key as Key
 
 data FsException
   = FileDoesNotExist {file :: FilePath}
@@ -99,6 +107,52 @@
             )
         )
 
+-- Extract attributes from bindings
+attributesFromBindings :: [Binding] -> [Attribute]
+attributesFromBindings [] = []
+attributesFromBindings (bd : bds) =
+  let attr = case bd of
+        BiTau attr _ -> Just attr
+        BiDelta _ -> Just AtDelta
+        BiLambda _ -> Just AtLambda
+        BiVoid attr -> Just attr
+        BiMeta _ -> Nothing
+        BiMetaLambda _ -> Just AtLambda
+   in case attr of
+        Just attr' -> attr' : attributesFromBindings bds
+        _ -> attributesFromBindings bds
+
+uniqueBindings' :: [Binding] -> IO [Binding]
+uniqueBindings' bds = case uniqueBindings bds of
+  Left msg -> throwIO (userError msg)
+  Right _ -> pure bds
+
+-- Check if given binding list consists of unique attributes
+uniqueBindings :: [Binding] -> Either String [Binding]
+uniqueBindings bds = case maybeDuplicatedAttribute bds Set.empty of
+  Just attr ->
+    Left
+      ( printf
+          "Duplicated attribute '%s' found in %s"
+          (show attr)
+          (intercalate ", " (map show (attributesFromBindings bds)))
+      )
+  _ -> Right bds
+  where
+    maybeDuplicatedAttribute :: [Binding] -> Set.Set Attribute -> Maybe Attribute
+    maybeDuplicatedAttribute [] = const Nothing
+    maybeDuplicatedAttribute ((BiTau attr _) : rest) = checkAttr attr rest
+    maybeDuplicatedAttribute (BiVoid attr : rest) = checkAttr attr rest
+    maybeDuplicatedAttribute (BiLambda _ : rest) = checkAttr AtLambda rest
+    maybeDuplicatedAttribute (BiMetaLambda _ : rest) = checkAttr AtLambda rest
+    maybeDuplicatedAttribute (BiDelta _ : rest) = checkAttr AtDelta rest
+    maybeDuplicatedAttribute (BiMeta _ : rest) = maybeDuplicatedAttribute rest
+
+    checkAttr :: Attribute -> [Binding] -> Set.Set Attribute -> Maybe Attribute
+    checkAttr attr rest acc
+      | attr `Set.member` acc = Just attr
+      | otherwise = maybeDuplicatedAttribute rest (Set.insert attr acc)
+
 -- 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
@@ -295,3 +349,14 @@
     j <- uniformRM (0, i) gen
     M.swap v i j
   V.toList <$> V.freeze v
+
+validateYamlObject :: (Applicative a, MonadFail a) => Object -> [String] -> a ()
+validateYamlObject v keys = do
+  let present = filter (`KeyMap.member` v) (map Key.fromString keys)
+      current = KeyMap.keys v
+  when
+    (length current > 1)
+    (fail ("Exactly one condition type is expected, when multiple condition types specified: " ++ show current))
+  when
+    (null present)
+    (fail (printf "Unknown condition type '%s', expected one of: %s" (show current) (show keys)))
diff --git a/src/Must.hs b/src/Must.hs
new file mode 100644
--- /dev/null
+++ b/src/Must.hs
@@ -0,0 +1,65 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module Must (Must (..), inRange, exceedsUpperBound) where
+
+import Data.List (isInfixOf)
+import Text.Read (readMaybe)
+
+data Must
+  = MtDisabled
+  | MtExact Integer
+  | MtRange (Maybe Integer) (Maybe Integer)
+  deriving (Eq)
+
+instance Show Must where
+  show MtDisabled = "0"
+  show (MtExact n) = show n
+  show (MtRange Nothing Nothing) = ".."
+  show (MtRange Nothing (Just max)) = ".." ++ show max
+  show (MtRange (Just min) Nothing) = show min ++ ".."
+  show (MtRange (Just min) (Just max)) = show min ++ ".." ++ show max
+
+instance Read Must where
+  readsPrec _ "0" = [(MtDisabled, "")]
+  readsPrec _ s
+    | ".." `isInfixOf` s = parseRange s
+    | otherwise = parseExact s
+    where
+      parseRange :: String -> [(Must, String)]
+      parseRange str = case break (== '.') str of
+        (minStr, '.' : '.' : maxStr) ->
+          let minPart = if null minStr then Nothing else readMaybe minStr
+              maxPart = if null maxStr then Nothing else readMaybe maxStr
+           in case (minPart, maxPart, null minStr, null maxStr) of
+                (Nothing, Nothing, False, False) -> [] -- Invalid range: non-numeric values
+                (Nothing, Nothing, True, True) -> [] -- Invalid range: empty range '..'
+                (Nothing, Just max, True, False) ->
+                  [(MtRange Nothing (Just max), "") | max >= 0]
+                (Just min, Nothing, False, True) ->
+                  [(MtRange (Just min) Nothing, "") | min >= 0]
+                (Just min, Just max, False, False) ->
+                  [(MtRange (Just min) (Just max), "") | min >= 0 && max >= 0 && min <= max]
+                _ -> [] -- Invalid range format
+        _ -> [] -- Invalid range: expected format like '3..5', '3..', or '..5'
+      parseExact :: String -> [(Must, String)]
+      parseExact str = case readMaybe str of
+        Just n | n >= 0 -> [(if n == 0 then MtDisabled else MtExact n, "")]
+        Just _ -> [] -- Invalid value: must be non-negative
+        Nothing -> [] -- Invalid value: expected integer
+
+inRange :: Must -> Integer -> Bool
+inRange MtDisabled _ = True
+inRange (MtExact expected) actual = actual == expected
+inRange (MtRange minVal maxVal) actual =
+  checkMin && checkMax
+  where
+    checkMin = maybe True (<= actual) minVal
+    checkMax = maybe True (>= actual) maxVal
+
+-- | Check if a value exceeds the upper bound of the range
+exceedsUpperBound :: Must -> Integer -> Bool
+exceedsUpperBound MtDisabled _ = False
+exceedsUpperBound (MtExact n) current = current > n
+exceedsUpperBound (MtRange _ (Just max)) current = current > max
+exceedsUpperBound (MtRange _ Nothing) _ = False
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -22,7 +22,9 @@
 import Ast
 import Control.Exception (Exception, throwIO)
 import Control.Monad (guard)
+import Control.Monad.IO.Class (MonadIO (liftIO))
 import Data.Char (isAsciiLower, isDigit, isLower)
+import Data.List (intercalate)
 import Data.Scientific (toRealFloat)
 import Data.Sequence (mapWithIndex)
 import Data.Text.Internal.Fusion.Size (lowerBound)
@@ -82,7 +84,7 @@
     'f' -> return '\f'
     'u' -> unicodeEscape
     'x' -> hexEscape
-    _ -> fail $ "Unknown escape: \\" ++ [c]
+    _ -> fail ("Unknown escape: \\" ++ [c])
   where
     unicodeEscape :: Parser Char
     unicodeEscape = do
@@ -115,7 +117,7 @@
       digits <- count 2 hexDigitChar
       case readHex digits of
         [(n, "")] -> return (chr n)
-        _ -> fail $ "Invalid hex escape: \\x" ++ digits
+        _ -> fail ("Invalid hex escape: \\x" ++ digits)
 
 function :: Parser String
 function = lexeme $ do
@@ -230,8 +232,9 @@
         voids <- map BiVoid <$> void' `sepBy` symbol ","
         _ <- symbol ")"
         _ <- arrow
-        ExFormation bs <- formation
-        return (BiTau attr' (ExFormation (withVoidRho (voids ++ bs))))
+        bs <- formationBindings
+        bds <- validatedBindings (voids ++ bs)
+        return (BiTau attr' (ExFormation (withVoidRho bds)))
     ]
 
 metaBinding :: Parser Binding
@@ -312,13 +315,18 @@
     ]
     <?> "full attribute"
 
+validatedBindings :: [Binding] -> Parser [Binding]
+validatedBindings bds = case uniqueBindings bds of
+  Left msg -> fail msg
+  Right bds' -> return bds'
+
 -- formation
-formation :: Parser Expression
-formation = do
+formationBindings :: Parser [Binding]
+formationBindings = do
   _ <- choice [symbol "[[", symbol "⟦"]
   bs <- binding `sepBy` symbol ","
   _ <- choice [symbol "]]", symbol "⟧"]
-  return (ExFormation bs)
+  return bs
 
 -- head part of expression
 -- 1. formation
@@ -331,7 +339,7 @@
 exHead =
   choice
     [ do
-        ExFormation bs <- formation
+        bs <- formationBindings >>= validatedBindings
         return (ExFormation (withVoidRho bs)),
       do
         _ <- choice [symbol "$", symbol "ξ"]
@@ -351,7 +359,7 @@
         str <- manyTill (choice [escapedChar, noneOf ['\\', '"']]) (char '"')
         return (DataString (strToBts str)),
       try (ExMeta <$> meta' 'e' "𝑒"),
-      ExDispatch ExThis <$> fullAttribute
+      ExDispatch ExThis <$> attribute
     ]
     <?> "expression head"
 
@@ -370,7 +378,7 @@
           choice
             [ do
                 _ <- symbol "."
-                ExDispatch expr <$> fullAttribute,
+                ExDispatch expr <$> attribute,
               do
                 guard
                   ( case expr of
diff --git a/src/Pretty.hs b/src/Pretty.hs
--- a/src/Pretty.hs
+++ b/src/Pretty.hs
@@ -16,6 +16,7 @@
     prettyBytes,
     prettyExtraArg,
     PrintMode (SWEET, SALTY),
+    Encoding (ASCII, UNICODE),
   )
 where
 
@@ -35,27 +36,43 @@
   show SWEET = "sweet"
   show SALTY = "salty"
 
-newtype Formatted a = Formatted {unFormatted :: (PrintMode, a)}
+data Encoding = ASCII | UNICODE
 
+newtype Formatted a = Formatted {unFormatted :: (PrintMode, Encoding, a)}
+
+formatted :: a -> Formatted a
+formatted x = Formatted (SALTY, UNICODE, x)
+
 prettyMeta :: String -> Doc ann
 prettyMeta meta = pretty "!" <> pretty meta
 
-prettyArrow :: Doc ann
-prettyArrow = pretty "↦"
+prettyArrow :: Encoding -> Doc ann
+prettyArrow UNICODE = pretty "↦"
+prettyArrow ASCII = pretty "->"
 
-prettyLsb :: Doc ann
-prettyLsb = pretty "⟦"
+prettyLsb :: Encoding -> Doc ann
+prettyLsb UNICODE = pretty "⟦"
+prettyLsb ASCII = pretty "[["
 
-prettyRsb :: Doc ann
-prettyRsb = pretty "⟧"
+prettyRsb :: Encoding -> Doc ann
+prettyRsb UNICODE = pretty "⟧"
+prettyRsb ASCII = pretty "]]"
 
 prettyDashedArrow :: Doc ann
 prettyDashedArrow = pretty "⤍"
 
+prettyLambda :: Encoding -> Doc ann
+prettyLambda UNICODE = pretty "λ" <+> prettyDashedArrow
+prettyLambda ASCII = pretty "L>"
+
+prettyDelta :: Encoding -> Doc ann
+prettyDelta UNICODE = pretty "Δ" <+> prettyDashedArrow
+prettyDelta ASCII = pretty "D>"
+
 instance Pretty ExtraArgument where
-  pretty (ArgExpression expr) = pretty (Formatted (SWEET, expr))
-  pretty (ArgBinding bd) = pretty (Formatted (SWEET, bd))
-  pretty (ArgAttribute attr) = pretty attr
+  pretty (ArgExpression expr) = pretty (Formatted (SWEET, UNICODE, expr))
+  pretty (ArgBinding bd) = pretty (Formatted (SWEET, UNICODE, bd))
+  pretty (ArgAttribute attr) = pretty (formatted attr)
   pretty (ArgBytes bytes) = pretty bytes
 
 instance Pretty Bytes where
@@ -64,24 +81,22 @@
   pretty (BtMany bts) = pretty (intercalate "-" bts)
   pretty (BtMeta meta) = prettyMeta meta
 
-instance Pretty Attribute where
-  pretty (AtLabel name) = pretty name
-  pretty (AtAlpha index) = pretty "α" <> pretty index
-  pretty AtRho = pretty "ρ"
-  pretty AtPhi = pretty "φ"
-  pretty AtDelta = pretty "Δ"
-  pretty AtLambda = pretty "λ"
-  pretty (AtMeta meta) = prettyMeta meta
+instance Pretty (Formatted Attribute) where
+  pretty (Formatted (_, _, AtMeta meta)) = prettyMeta meta
+  pretty (Formatted (_, ASCII, AtAlpha idx)) = pretty "~" <> pretty idx
+  pretty (Formatted (_, ASCII, AtPhi)) = pretty "@"
+  pretty (Formatted (_, ASCII, AtRho)) = pretty "^"
+  pretty (Formatted (_, _, attr)) = pretty (show attr)
 
 instance Pretty (Formatted Binding) where
-  pretty (Formatted (SWEET, BiTau attr (ExFormation bindings))) =
+  pretty (Formatted (SWEET, encoding, BiTau attr (ExFormation bindings))) =
     let voids' = voids bindings
      in if null voids'
-          then pretty attr <+> prettyArrow <+> pretty (Formatted (SWEET, ExFormation bindings))
+          then pretty (Formatted (SWEET, encoding, attr)) <+> prettyArrow encoding <+> pretty (Formatted (SWEET, encoding, 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)))
+              then inlineVoids (init voids') <+> prettyLsb encoding <> prettyRsb encoding
+              else inlineVoids voids' <+> pretty (Formatted (SWEET, encoding, ExFormation (drop (length voids') bindings)))
     where
       voids :: [Binding] -> [Attribute]
       voids [] = []
@@ -89,19 +104,27 @@
         BiVoid attr -> attr : voids bds
         _ -> []
       inlineVoids :: [Attribute] -> Doc ann
-      inlineVoids [] = pretty attr <+> prettyArrow
-      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
-  pretty (Formatted (_, BiMetaLambda meta)) = pretty "λ" <+> prettyDashedArrow <+> prettyMeta meta
-  pretty (Formatted (_, BiVoid attr)) = pretty attr <+> prettyArrow <+> pretty "∅"
-  pretty (Formatted (_, BiLambda func)) = pretty "λ" <+> prettyDashedArrow <+> pretty func
+      inlineVoids [] = pretty (Formatted (SWEET, encoding, attr)) <+> prettyArrow encoding
+      inlineVoids voids' =
+        pretty (Formatted (SWEET, encoding, attr))
+          <> lparen
+          <> hsep (punctuate comma (map (\attr -> pretty (Formatted (SWEET, encoding, attr))) voids'))
+          <> rparen
+          <+> prettyArrow encoding
+  pretty (Formatted (mode, encoding, BiTau attr expr)) = pretty (Formatted (mode, encoding, attr)) <+> prettyArrow encoding <+> pretty (Formatted (mode, encoding, expr))
+  pretty (Formatted (_, _, BiMeta meta)) = prettyMeta meta
+  pretty (Formatted (_, encoding, BiDelta bytes)) = prettyDelta encoding <+> pretty bytes
+  pretty (Formatted (_, encoding, BiLambda func)) = prettyLambda encoding <+> pretty func
+  pretty (Formatted (_, encoding, BiMetaLambda meta)) = prettyLambda encoding <+> prettyMeta meta
+  pretty (Formatted (mode, UNICODE, BiVoid attr)) = pretty (Formatted (mode, UNICODE, attr)) <+> prettyArrow UNICODE <+> pretty "∅"
+  pretty (Formatted (mode, ASCII, BiVoid attr)) = pretty (Formatted (mode, ASCII, attr)) <+> prettyArrow ASCII <+> pretty "?"
 
--- >>> render (Formatted (SWEET, [BiVoid AtRho]))
+-- >>> render (Formatted (SWEET, UNICODE, [BiVoid AtRho]))
 -- ""
+-- >>> render (Formatted (SWEET, UNICODE, [BiTau (AtLabel "x") ExGlobal, BiVoid AtPhi]))
+-- "x \8614 \934,\n\966 \8614 \8709"
 instance {-# OVERLAPPING #-} Pretty (Formatted [Binding]) where
-  pretty (Formatted (SWEET, bds)) = vsep (punctuate comma (excludeVoidRho (\bd -> pretty (Formatted (SWEET, bd))) [] bds))
+  pretty (Formatted (SWEET, encoding, bds)) = vsep (punctuate comma (excludeVoidRho (\bd -> pretty (Formatted (SWEET, encoding, bd))) [] bds))
     where
       excludeVoidRho :: (Binding -> Doc ann) -> [Doc ann] -> [Binding] -> [Doc ann]
       excludeVoidRho func acc [bd] = case bd of
@@ -109,7 +132,7 @@
         _ -> 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))
+  pretty (Formatted (SALTY, encoding, bds)) = vsep (punctuate comma (map (\bd -> pretty (Formatted (SALTY, encoding, bd))) bds))
 
 complexApplication :: Expression -> (Expression, [Binding], [Expression])
 complexApplication (ExApplication (ExApplication expr tau) tau') =
@@ -129,51 +152,57 @@
 -- >>> render (Formatted (SWEET, ExFormation [BiVoid AtRho]))
 -- "\10214\10215"
 instance Pretty (Formatted Expression) where
-  pretty (Formatted (SWEET, ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))) = pretty "Φ̇"
-  pretty (Formatted (SWEET, DataString bytes)) = pretty "\"" <> pretty (btsToStr bytes) <> pretty "\""
-  pretty (Formatted (SWEET, DataNumber bytes)) = either pretty pretty (btsToNum bytes)
-  pretty (Formatted (SWEET, DataObject other bytes)) = pretty (Formatted (SALTY, DataObject other bytes))
-  pretty (Formatted (SWEET, ExFormation [BiVoid AtRho])) = pretty "⟦⟧"
-  pretty (Formatted (mode, ExFormation [binding])) = case binding of
-    BiTau _ _ -> vsep [pretty "⟦", indent 2 (pretty (Formatted (mode, binding))), pretty "⟧"]
-    _ -> pretty "⟦" <+> pretty (Formatted (mode, binding)) <+> pretty "⟧"
-  pretty (Formatted (_, ExFormation [])) = pretty "⟦⟧"
-  pretty (Formatted (mode, ExFormation bindings)) = vsep [pretty "⟦", indent 2 (pretty (Formatted (mode, bindings))), pretty "⟧"]
-  pretty (Formatted (_, ExThis)) = pretty "ξ"
-  pretty (Formatted (_, ExGlobal)) = pretty "Φ"
-  pretty (Formatted (_, ExTermination)) = pretty "⊥"
-  pretty (Formatted (_, ExMeta meta)) = prettyMeta meta
-  pretty (Formatted (SWEET, ExApplication (ExApplication expr tau) tau')) =
+  pretty (Formatted (SWEET, UNICODE, ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))) = pretty "Φ̇"
+  pretty (Formatted (SWEET, ASCII, ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))) = pretty "QQ"
+  pretty (Formatted (SWEET, _, DataString bytes)) = pretty "\"" <> pretty (btsToStr bytes) <> pretty "\""
+  pretty (Formatted (SWEET, _, DataNumber bytes)) = either pretty pretty (btsToNum bytes)
+  pretty (Formatted (SWEET, encoding, DataObject other bytes)) = pretty (Formatted (SALTY, encoding, DataObject other bytes))
+  pretty (Formatted (SWEET, UNICODE, ExFormation [BiVoid AtRho])) = pretty "⟦⟧"
+  pretty (Formatted (SWEET, ASCII, ExFormation [BiVoid AtRho])) = pretty "[[]]"
+  pretty (Formatted (mode, encoding, ExFormation [binding])) = case binding of
+    BiTau _ _ -> vsep [prettyLsb encoding, indent 2 (pretty (Formatted (mode, encoding, binding))), prettyRsb encoding]
+    _ -> prettyLsb encoding <+> pretty (Formatted (mode, encoding, binding)) <+> prettyRsb encoding
+  pretty (Formatted (_, UNICODE, ExFormation [])) = pretty "⟦⟧"
+  pretty (Formatted (_, ASCII, ExFormation [])) = pretty "[[]]"
+  pretty (Formatted (mode, encoding, ExFormation bindings)) = vsep [prettyLsb encoding, indent 2 (pretty (Formatted (mode, encoding, bindings))), prettyRsb encoding]
+  pretty (Formatted (_, UNICODE, ExThis)) = pretty "ξ"
+  pretty (Formatted (_, ASCII, ExThis)) = pretty "$"
+  pretty (Formatted (_, UNICODE, ExGlobal)) = pretty "Φ"
+  pretty (Formatted (_, ASCII, ExGlobal)) = pretty "Q"
+  pretty (Formatted (_, UNICODE, ExTermination)) = pretty "⊥"
+  pretty (Formatted (_, ASCII, ExTermination)) = pretty "T"
+  pretty (Formatted (_, _, ExMeta meta)) = prettyMeta meta
+  pretty (Formatted (SWEET, encoding, 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)))
-     in pretty (Formatted (SWEET, expr')) <> vsep [lparen, indent 2 args, rparen]
-  pretty (Formatted (SWEET, ExApplication expr tau)) =
+            then pretty (Formatted (SWEET, encoding, reverse taus))
+            else vsep (punctuate comma (map (\exp -> pretty (Formatted (SWEET, encoding, exp))) (reverse exprs)))
+     in pretty (Formatted (SWEET, encoding, expr')) <> vsep [lparen, indent 2 args, rparen]
+  pretty (Formatted (SWEET, encoding, ExApplication expr tau)) =
     let arg = case tau of
-          BiTau (AtAlpha 0) expr' -> pretty (Formatted (SWEET, expr'))
-          _ -> pretty (Formatted (SWEET, tau))
-     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
+          BiTau (AtAlpha 0) expr' -> pretty (Formatted (SWEET, encoding, expr'))
+          _ -> pretty (Formatted (SWEET, encoding, tau))
+     in pretty (Formatted (SWEET, encoding, expr)) <> vsep [lparen, indent 2 arg, rparen]
+  pretty (Formatted (mode, encoding, ExApplication expr tau)) = pretty (Formatted (mode, encoding, expr)) <> vsep [lparen, indent 2 (pretty (Formatted (mode, encoding, tau))), rparen]
+  pretty (Formatted (mode, encoding, ExDispatch expr attr)) = pretty (Formatted (mode, encoding, expr)) <> pretty "." <> pretty (Formatted (mode, encoding, attr))
+  pretty (Formatted (mode, encoding, ExMetaTail expr meta)) = pretty (Formatted (mode, encoding, expr)) <+> pretty "*" <+> prettyMeta meta
 
 instance Pretty (Formatted Program) where
-  pretty (Formatted (SALTY, Program expr)) = pretty "Φ" <+> prettyArrow <+> pretty (Formatted (SALTY, expr))
-  pretty (Formatted (SWEET, Program expr)) = pretty "{" <> pretty (Formatted (SWEET, expr)) <> pretty "}"
+  pretty (Formatted (SALTY, encoding, Program expr)) = pretty "Φ" <+> prettyArrow encoding <+> pretty (Formatted (SALTY, encoding, expr))
+  pretty (Formatted (SWEET, encoding, Program expr)) = pretty "{" <> pretty (Formatted (SWEET, encoding, expr)) <> pretty "}"
 
 instance Pretty Tail where
-  pretty (TaApplication tau) = vsep [lparen, indent 2 (pretty (Formatted (SALTY, tau))), rparen]
-  pretty (TaDispatch attr) = pretty "." <> pretty attr
+  pretty (TaApplication tau) = vsep [lparen, indent 2 (pretty (formatted tau)), rparen]
+  pretty (TaDispatch attr) = pretty "." <> pretty (formatted attr)
 
 instance Pretty MetaValue where
-  pretty (MvAttribute attr) = pretty attr
+  pretty (MvAttribute attr) = pretty (formatted attr)
   pretty (MvBytes bytes) = pretty bytes
   pretty (MvBindings []) = pretty "[]"
-  pretty (MvBindings bindings) = vsep [pretty "[", indent 2 (pretty (Formatted (SALTY, bindings))), pretty "]"]
+  pretty (MvBindings bindings) = vsep [pretty "[", indent 2 (pretty (formatted bindings)), pretty "]"]
   pretty (MvFunction func) = pretty func
-  pretty (MvExpression expr _) = pretty (Formatted (SALTY, expr))
+  pretty (MvExpression expr _) = pretty (formatted expr)
   pretty (MvTail tails) = vsep (punctuate comma (map pretty tails))
 
 instance Pretty Subst where
@@ -195,14 +224,14 @@
       ]
 
 instance {-# OVERLAPPING #-} Pretty (Formatted [Subst]) where
-  pretty (Formatted (_, [])) = pretty "[]"
-  pretty (Formatted (mode, substs)) = vsep [pretty "[", indent 2 (vsep (punctuate comma (map pretty substs))), pretty "]"]
+  pretty (Formatted (_, _, [])) = pretty "[]"
+  pretty (Formatted (mode, _, substs)) = vsep [pretty "[", indent 2 (vsep (punctuate comma (map pretty substs))), pretty "]"]
 
 render :: (Pretty a) => a -> String
 render printable = renderString (layoutPretty defaultLayoutOptions (pretty printable))
 
 prettyBinding :: Binding -> String
-prettyBinding binding = render (Formatted (SALTY, binding))
+prettyBinding binding = render (formatted binding)
 
 prettyExtraArg :: ExtraArgument -> String
 prettyExtraArg = render
@@ -211,7 +240,7 @@
 prettyBytes = render
 
 prettyAttribute :: Attribute -> String
-prettyAttribute = render
+prettyAttribute attr = render (formatted attr)
 
 prettySubst :: Subst -> String
 prettySubst = render
@@ -219,17 +248,17 @@
 prettySubsts :: [Subst] -> String
 prettySubsts = render
 
-prettySubsts' :: [Subst] -> PrintMode -> String
-prettySubsts' substs mode = render (Formatted (mode, substs))
+prettySubsts' :: [Subst] -> PrintMode -> Encoding -> String
+prettySubsts' substs mode encoding = render (Formatted (mode, encoding, substs))
 
 prettyExpression :: Expression -> String
-prettyExpression expr = render (Formatted (SALTY, expr))
+prettyExpression expr = render (formatted expr)
 
 prettyExpression' :: Expression -> String
-prettyExpression' expr = render (Formatted (SWEET, expr))
+prettyExpression' expr = render (Formatted (SWEET, UNICODE, expr))
 
 prettyProgram :: Program -> String
-prettyProgram prog = render (Formatted (SALTY, prog))
+prettyProgram prog = render (formatted prog)
 
-prettyProgram' :: Program -> PrintMode -> String
-prettyProgram' prog mode = render (Formatted (mode, prog))
+prettyProgram' :: Program -> PrintMode -> Encoding -> String
+prettyProgram' prog mode encoding = render (Formatted (mode, encoding, prog))
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -17,6 +17,7 @@
 import Logger (logDebug)
 import Matcher (MetaValue (MvAttribute, MvBindings, MvBytes, MvExpression), Subst (Subst), combine, combineMany, defaultScope, matchProgram, substEmpty, substSingle)
 import Misc (ensuredFile)
+import Must (Must (..), exceedsUpperBound, inRange)
 import Parser (parseProgram, parseProgramThrows)
 import Pretty (PrintMode (SWEET), prettyAttribute, prettyBytes, prettyExpression, prettyExpression', prettyProgram, prettyProgram', prettySubsts)
 import Replacer (ReplaceProgramContext (ReplaceProgramContext), ReplaceProgramThrowsFunc, replaceProgramFastThrows, replaceProgramThrows)
@@ -31,27 +32,35 @@
   { _program :: Program,
     _maxDepth :: Integer,
     _maxCycles :: Integer,
+    _depthSensitive :: Bool,
     _buildTerm :: BuildTermFunc,
-    _must :: Integer
+    _must :: Must
   }
 
-data MustException
-  = StoppedBefore {must :: Integer, count :: Integer}
-  | ContinueAfter {must :: Integer}
+data RewriteException
+  = MustBeGoing {must :: Must, count :: Integer}
+  | MustStopBefore {must :: Must, count :: Integer}
+  | StoppedOnLimit {flag :: String, limit :: Integer}
   deriving (Exception)
 
-instance Show MustException where
-  show StoppedBefore {..} =
+instance Show RewriteException where
+  show MustBeGoing {..} =
     printf
-      "With option --must=%d it's expected exactly %d rewriting cycles happened, but rewriting stopped after %d"
-      must
-      must
+      "With option --must=%s it's expected rewriting cycles to be in range [%s], but rewriting stopped after %d cycles"
+      (show must)
+      (show must)
       count
-  show ContinueAfter {..} =
+  show MustStopBefore {..} =
     printf
-      "With option --must=%d it's expected exactly %d rewriting cycles happened, but rewriting is still going"
-      must
-      must
+      "With option --must=%s it's expected rewriting cycles to be in range [%s], but rewriting has already reached %d cycles and is still going"
+      (show must)
+      (show must)
+      count
+  show StoppedOnLimit {..} =
+    printf
+      "With option --depth-sensitive it's expected rewriting iterations amount does not reach the limit: --%s=%d"
+      flag
+      limit
 
 -- Build pattern and result expression and replace patterns to results in given program
 buildAndReplace' :: Expression -> Expression -> [Subst] -> ReplaceProgramThrowsFunc -> ReplaceProgramContext -> IO Program
@@ -115,7 +124,9 @@
        in if count - 1 == depth
             then do
               logDebug (printf "Max amount of rewriting cycles (%d) for rule '%s' has been reached, rewriting is stopped" depth ruleName)
-              pure prog
+              if _depthSensitive ctx
+                then throwIO (StoppedOnLimit "max-depth" depth)
+                else pure prog
             else do
               logDebug (printf "Starting rewriting cycle for rule '%s': %d out of %d" ruleName count depth)
               matched <- R.matchProgramWithRule prog rule (RuleContext (_program ctx) (_buildTerm ctx))
@@ -154,20 +165,23 @@
     _rewrite prog count = do
       let cycles = _maxCycles ctx
           must = _must ctx
-      if must /= 0 && count - 1 > must
-        then throwIO (ContinueAfter must)
+          current = count - 1
+      if not (inRange must current) && current > 0 && exceedsUpperBound must current
+        then throwIO (MustStopBefore must current)
         else
-          if count - 1 == cycles
+          if current == cycles
             then do
               logDebug (printf "Max amount of rewriting cycles for all rules (%d) has been reached, rewriting is stopped" cycles)
-              pure prog
+              if _depthSensitive ctx
+                then throwIO (StoppedOnLimit "max-cycles" cycles)
+                else pure prog
             else do
               logDebug (printf "Starting rewriting cycle for all rules: %d out of %d" count cycles)
               rewritten <- rewrite prog rules ctx
               if rewritten == prog
                 then do
                   logDebug "No rule matched, rewriting is stopped"
-                  if must /= 0 && count - 1 /= must
-                    then throwIO (StoppedBefore must (count - 1))
+                  if not (inRange must current)
+                    then throwIO (MustBeGoing must current)
                     else pure rewritten
                 else _rewrite rewritten (count + 1)
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -19,7 +19,7 @@
 import Logger (logDebug)
 import Matcher
 import Misc (allPathsIn, btsToUnescapedStr)
-import Pretty (prettyAttribute, prettyBytes, prettyExpression, prettyExpression', prettySubsts)
+import Pretty (prettyAttribute, prettyBytes, prettyExpression, prettyExpression', prettySubsts, prettyBinding)
 import Regexp (match)
 import Term (BuildTermFunc, Term (..))
 import Text.Printf (printf)
@@ -258,6 +258,9 @@
                   TeBytes bytes -> do
                     logDebug (printf "Function %s() returned bytes: %s" func (prettyBytes bytes))
                     pure (MvBytes bytes)
+                  TeBindings bds -> do
+                    logDebug (printf "Function %s return bindings: %s" func (prettyExpression' (ExFormation bds)))
+                    pure (MvBindings bds)
                 case maybeName of
                   Just name -> pure (combine (substSingle name meta) subst')
                   _ -> pure Nothing
diff --git a/src/Term.hs b/src/Term.hs
--- a/src/Term.hs
+++ b/src/Term.hs
@@ -13,7 +13,11 @@
 import Matcher
 import Ast
 
-data Term = TeExpression Expression | TeAttribute Attribute | TeBytes Bytes
+data Term
+  = TeExpression Expression
+  | TeAttribute Attribute
+  | TeBytes Bytes
+  | TeBindings [Binding]
 
 type BuildTermMethod = [ExtraArgument] -> Subst -> Program -> IO Term
 
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -6,7 +6,17 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module XMIR (programToXMIR, printXMIR, toName, parseXMIR, parseXMIRThrows, xmirToPhi, XmirContext (XmirContext)) where
+module XMIR
+  ( programToXMIR,
+    printXMIR,
+    toName,
+    parseXMIR,
+    parseXMIRThrows,
+    xmirToPhi,
+    defaultXmirContext,
+    XmirContext (XmirContext),
+  )
+where
 
 import Ast
 import Control.Exception (Exception (displayException), SomeException, throwIO)
@@ -26,11 +36,11 @@
 import Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds)
 import Data.Time.Format (defaultTimeLocale, formatTime)
 import Data.Version (showVersion)
+import Debug.Trace
 import Misc
 import Paths_phino (version)
-import Pretty (PrintMode, prettyAttribute, prettyBinding, prettyBytes, prettyExpression, prettyProgram')
+import Pretty (PrintMode (SWEET), prettyAttribute, prettyBinding, prettyBytes, prettyExpression, prettyProgram)
 import Text.Printf (printf)
-import Text.Read (readMaybe)
 import qualified Text.Read as TR
 import Text.XML
 import qualified Text.XML.Cursor as C
@@ -38,22 +48,23 @@
 data XmirContext = XmirContext
   { omitListing :: Bool,
     omitComments :: Bool,
-    printMode :: PrintMode
+    listing :: String
   }
 
--- @todo #116:30min Refactor XMIR module. This module became so big and hard to read.
---  Now it's responsible for 3 different operations: 1) converting Phi AST to XML Document Ast,
---  2) printing XML Document, 3) parsing XMIR to Phi AST. I think we should separate the logic
---  in order to keep modules as little as possible.
+defaultXmirContext :: XmirContext
+defaultXmirContext = XmirContext True True ""
+
 data XMIRException
-  = UnsupportedExpression {expr :: Expression}
+  = UnsupportedProgram {prog :: Program}
+  | UnsupportedExpression {expr :: Expression}
   | UnsupportedBinding {binding :: Binding}
   | CouldNotParseXMIR {message :: String}
   | InvalidXMIRFormat {message :: String, cursor :: C.Cursor}
   deriving (Exception)
 
 instance Show XMIRException where
-  show UnsupportedExpression {..} = printf "XMIR does not support such expression: %s" (prettyExpression expr)
+  show UnsupportedProgram {..} = printf "XMIR does not support such program:\n%s" (prettyProgram prog)
+  show UnsupportedExpression {..} = printf "XMIR does not support such expression:\n%s" (prettyExpression expr)
   show UnsupportedBinding {..} = printf "XMIR does not support such bindings: %s" (prettyBinding binding)
   show CouldNotParseXMIR {..} = printf "Couldn't parse given XMIR, cause: %s" message
   show InvalidXMIRFormat {..} =
@@ -78,9 +89,9 @@
 object attrs children = NodeElement (element "o" attrs children)
 
 -- @todo #278:30min Remove xmirAttributure and replace to prettyAttribute. Right now XMIR does not
---  support "ρ" and "φ" in @base and @name attributes. When it's done, we should also generate 
+--  support "ρ" and "φ" in @base and @name attributes. When it's done, we should also generate
 --  such valid XMIR. To achieve that we should get rid of xmirAttribute function and use prettyAttribute
---  instead. Also we should use "@" in formationBinding. Don't forget to remove the puzzle. 
+--  instead. Also we should use "@" in formationBinding. Don't forget to remove the puzzle.
 xmirAttribute :: Attribute -> String
 xmirAttribute AtPhi = "@"
 xmirAttribute AtRho = "^"
@@ -141,9 +152,6 @@
 expression (ExApplication (ExFormation bds) tau) _ = throwIO (UnsupportedExpression (ExApplication (ExFormation bds) tau))
 expression expr _ = throwIO (UnsupportedExpression expr)
 
-nestedBindings :: [Binding] -> XmirContext -> IO [Node]
-nestedBindings bds ctx = catMaybes <$> mapM (`formationBinding` ctx) bds
-
 formationBinding :: Binding -> XmirContext -> IO (Maybe Node)
 formationBinding (BiTau (AtLabel label) (ExFormation bds)) ctx = do
   inners <- nestedBindings bds ctx
@@ -162,86 +170,102 @@
 formationBinding (BiVoid (AtLabel label)) _ = pure (Just (object [("name", label), ("base", "∅")] []))
 formationBinding binding _ = throwIO (UnsupportedBinding binding)
 
-rootExpression :: Expression -> XmirContext -> IO Node
-rootExpression (ExFormation [bd, BiVoid AtRho]) ctx = do
-  [bd'] <- nestedBindings [bd] ctx
-  pure bd'
-rootExpression expr _ = throwIO (UnsupportedExpression expr)
-
--- Extract package from given expression
--- The function returns tuple (X, Y), where
--- - X: list of package parts
--- - Y: root object expression
-getPackage :: Expression -> IO ([String], Expression)
-getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiVoid AtRho]) = do
-  (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])
-  pure (label : pckg, expr')
-getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiLambda "Package", BiVoid AtRho]) = do
-  (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])
-  pure (label : pckg, expr')
-getPackage (ExFormation [BiTau attr expr, BiLambda "Package", BiVoid AtRho]) = pure ([], ExFormation [BiTau attr expr, BiVoid AtRho])
-getPackage (ExFormation [bd, BiVoid AtRho]) = pure ([], ExFormation [bd, BiVoid AtRho])
-getPackage expr = throwIO (userError (printf "Can't extract package from given expression:\n %s" (prettyExpression expr)))
+nestedBindings :: [Binding] -> XmirContext -> IO [Node]
+nestedBindings bds ctx = catMaybes <$> mapM (`formationBinding` ctx) bds
 
-metasWithPackage :: String -> Node
-metasWithPackage pckg =
-  NodeElement
-    ( element
-        "metas"
-        []
-        [ NodeElement
+programToXMIR :: Program -> XmirContext -> IO Document
+programToXMIR prog@(Program expr@(ExFormation [BiTau (AtLabel _) arg, BiVoid AtRho])) ctx@XmirContext {..} = case arg of
+  ExFormation _ -> programToXMIR'
+  ExApplication _ _ -> programToXMIR'
+  ExDispatch _ _ -> programToXMIR'
+  ExGlobal -> programToXMIR'
+  _ -> throwIO (UnsupportedProgram prog)
+  where
+    programToXMIR' :: IO Document
+    programToXMIR' = do
+      (pckg, expr') <- getPackage expr
+      root <- rootExpression expr' ctx
+      now <- getCurrentTime
+      let listingContent =
+            if omitListing
+              then show (length (lines listing)) ++ " line(s)"
+              else listing
+          listing' = NodeElement (element "listing" [] [NodeContent (T.pack listingContent)])
+          metas = metasWithPackage (intercalate "." pckg)
+      pure
+        ( Document
+            (Prologue [] Nothing [])
             ( element
-                "meta"
-                []
-                [ NodeElement (element "head" [] [NodeContent (T.pack "package")]),
-                  NodeElement (element "tail" [] [NodeContent (T.pack pckg)]),
-                  NodeElement (element "part" [] [NodeContent (T.pack pckg)])
+                "object"
+                [ ("dob", formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now),
+                  ("ms", "0"),
+                  ("revision", "1234567"),
+                  ("time", time now),
+                  ("version", showVersion version),
+                  ("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
+                  ("xsi:noNamespaceSchemaLocation", "https://raw.githubusercontent.com/objectionary/eo/refs/heads/gh-pages/XMIR.xsd")
                 ]
+                ( if null pckg
+                    then [listing', root]
+                    else [listing', metas, root]
+                )
             )
-        ]
-    )
-
-time :: UTCTime -> String
-time now = do
-  let base = formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now
-      posix = utcTimeToPOSIXSeconds now
-      fractional :: Double
-      fractional = realToFrac posix - fromInteger (floor posix)
-      nanos = floor (fractional * 1_000_000_000) :: Int
-  base ++ "." ++ printf "%09d" nanos ++ "Z"
-
-programToXMIR :: Program -> XmirContext -> IO Document
-programToXMIR (Program expr) ctx = do
-  (pckg, expr') <- getPackage expr
-  root <- rootExpression expr' ctx
-  now <- getCurrentTime
-  let phi = prettyProgram' (Program expr) (printMode ctx)
-      listing =
-        if omitListing ctx
-          then show (length (lines phi)) ++ " lines of phi"
-          else phi
-      listing' = NodeElement (element "listing" [] [NodeContent (T.pack listing)])
-      metas = metasWithPackage (intercalate "." pckg)
-  pure
-    ( Document
-        (Prologue [] Nothing [])
+            []
+        )
+    -- Extract package from given expression
+    -- The function returns tuple (X, Y), where
+    -- - X: list of package parts
+    -- - Y: root object expression
+    getPackage :: Expression -> IO ([String], Expression)
+    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiVoid AtRho]) = do
+      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])
+      pure (label : pckg, expr')
+    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda "Package", BiVoid AtRho]), BiLambda "Package", BiVoid AtRho]) = do
+      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda "Package", BiVoid AtRho])
+      pure (label : pckg, expr')
+    getPackage (ExFormation [BiTau attr expr, BiLambda "Package", BiVoid AtRho]) = pure ([], ExFormation [BiTau attr expr, BiVoid AtRho])
+    getPackage (ExFormation [bd, BiVoid AtRho]) = pure ([], ExFormation [bd, BiVoid AtRho])
+    getPackage expr = throwIO (userError (printf "Can't extract package from given expression:\n %s" (prettyExpression expr)))
+    -- Convert root Expression to Node
+    rootExpression :: Expression -> XmirContext -> IO Node
+    rootExpression (ExFormation [bd, BiVoid AtRho]) ctx = do
+      [bd'] <- nestedBindings [bd] ctx
+      pure bd'
+    rootExpression expr _ = throwIO (UnsupportedExpression expr)
+    -- Returns metas Node with package:
+    -- <metas>
+    --   <meta>
+    --     <head>package</head>
+    --     <tail><!-- package here --></tail>
+    --     <part><!-- package here --></part>
+    --   </meta>
+    -- </metas>
+    metasWithPackage :: String -> Node
+    metasWithPackage pckg =
+      NodeElement
         ( element
-            "object"
-            [ ("dob", formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now),
-              ("ms", "0"),
-              ("revision", "1234567"),
-              ("time", time now),
-              ("version", showVersion version),
-              ("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
-              ("xsi:noNamespaceSchemaLocation", "https://raw.githubusercontent.com/objectionary/eo/refs/heads/gh-pages/XMIR.xsd")
+            "metas"
+            []
+            [ NodeElement
+                ( element
+                    "meta"
+                    []
+                    [ NodeElement (element "head" [] [NodeContent (T.pack "package")]),
+                      NodeElement (element "tail" [] [NodeContent (T.pack pckg)]),
+                      NodeElement (element "part" [] [NodeContent (T.pack pckg)])
+                    ]
+                )
             ]
-            ( if null pckg
-                then [listing', root]
-                else [listing', metas, root]
-            )
         )
-        []
-    )
+    time :: UTCTime -> String
+    time now = do
+      let base = formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now
+          posix = utcTimeToPOSIXSeconds now
+          fractional :: Double
+          fractional = realToFrac posix - fromInteger (floor posix)
+          nanos = floor (fractional * 1_000_000_000) :: Int
+      base ++ "." ++ printf "%09d" nanos ++ "Z"
+programToXMIR prog _ = throwIO (UnsupportedProgram prog)
 
 -- Add indentation (2 spaces per level).
 indent :: Int -> TB.Builder
@@ -361,7 +385,7 @@
   | not (hasAttr "name" cur) = throwIO (InvalidXMIRFormat "Formation children must have @name attribute" cur)
   | not (hasAttr "base" cur) = do
       name <- getAttr "name" cur
-      bds <- mapM (`xmirToFormationBinding` (name : fqn)) (cur C.$/ C.element (toName "o"))
+      bds <- mapM (`xmirToFormationBinding` (name : fqn)) (cur C.$/ C.element (toName "o")) >>= uniqueBindings'
       case name of
         "λ" -> pure (BiLambda (intercalate "_" ("L" : reverse fqn)))
         ('α' : _) -> throwIO (InvalidXMIRFormat "Formation child @name can't start with α" cur)
@@ -409,7 +433,7 @@
         '$' : '.' : rest -> xmirToExpression' ExThis "$" rest cur fqn
         _ -> throwIO (InvalidXMIRFormat "The @base attribute must be either ['∅'|'Q'] or start with ['Q.'|'$.'|'.']" cur)
   | otherwise = do
-      bds <- mapM (`xmirToFormationBinding` fqn) (cur C.$/ C.element (toName "o"))
+      bds <- mapM (`xmirToFormationBinding` fqn) (cur C.$/ C.element (toName "o")) >>= uniqueBindings'
       pure (ExFormation (withVoidRho bds))
   where
     xmirToExpression' :: Expression -> String -> String -> C.Cursor -> [String] -> IO Expression
@@ -422,8 +446,7 @@
               (\acc part -> ExDispatch acc <$> toAttr (T.unpack part) cur)
               start
               (T.splitOn "." (T.pack rest))
-          let args = cur C.$/ C.element (toName "o")
-          xmirToApplication head' args fqn
+          xmirToApplication head' (cur C.$/ C.element (toName "o")) fqn
 
 xmirToApplication :: Expression -> [C.Cursor] -> [String] -> IO Expression
 xmirToApplication = xmirToApplication' 0
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -17,7 +17,7 @@
 import Data.Yaml (Parser)
 import qualified Data.Yaml as Yaml
 import GHC.Generics
-import Misc (allPathsIn)
+import Misc (allPathsIn, validateYamlObject)
 import Parser
 
 parseJSON' :: String -> (String -> Either String a) -> Value -> Parser a
@@ -52,7 +52,8 @@
 
 instance FromJSON Number where
   parseJSON v = case v of
-    Object o ->
+    Object o -> do
+      validateYamlObject o ["ordinal", "length"]
       asum
         [ Ordinal <$> o .: "ordinal",
           Length <$> o .: "length"
@@ -73,7 +74,8 @@
   parseJSON =
     withObject
       "Condition"
-      ( \v ->
+      ( \v -> do
+          validateYamlObject v ["and", "or", "not", "alpha", "nf", "xi", "eq", "in", "matches", "part-of"]
           asum
             [ And <$> v .: "and",
               Or <$> v .: "or",
diff --git a/test/BuilderSpec.hs b/test/BuilderSpec.hs
--- a/test/BuilderSpec.hs
+++ b/test/BuilderSpec.hs
@@ -8,7 +8,8 @@
 import Control.Monad
 import Data.Map.Strict qualified as Map
 import Matcher
-import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, anyException, describe, it, shouldBe, shouldThrow)
+import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, anyException, describe, it, shouldBe, shouldThrow, shouldSatisfy)
+import Data.Either (isLeft)
 
 test :: (Show a, Eq a) => (a -> Subst -> Either String (a, a)) -> [(String, a, [(String, MetaValue)], Either String (a, a))] -> SpecWith (Arg Expectation)
 test function useCases =
@@ -50,7 +51,7 @@
         ( "Q.!a => () => X",
           ExDispatch ExGlobal (AtMeta "a"),
           [],
-          Left "a"
+          Left "meta 'a' is either does not exist or refers to an inappropriate term"
         ),
         ( "!e0(!a1 -> !e1, !a2 => !e2) => (!e0 >> [[]], !a1 >> x, !e1 >> Q, !a2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)",
           ExApplication (ExApplication (ExMeta "e0") (BiTau (AtMeta "a1") (ExMeta "e1"))) (BiTau (AtMeta "a2") (ExMeta "e2")),
@@ -94,3 +95,9 @@
         (ExMeta "e")
         [substSingle "e1" (MvExpression (ExDispatch ExGlobal (AtLabel "x")) defaultScope)]
         `shouldThrow` anyException
+  
+  describe "build with duplicate attributes in bindings" $ do
+    it "build binding with duplicates" $
+      buildBinding (BiMeta "B") (substSingle "B" (MvBindings [BiVoid AtRho, BiVoid AtRho])) `shouldSatisfy` isLeft
+    it "build formation with duplicates" $
+      buildExpression (ExMeta "e") (substSingle "e" (MvExpression (ExFormation [BiVoid AtRho, BiVoid AtRho]) ExThis)) `shouldSatisfy` isLeft
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -16,7 +16,6 @@
 import System.Directory (removeFile)
 import System.Exit (ExitCode (ExitFailure))
 import System.IO
-import System.IO.Silently (capture_)
 import Test.Hspec
 import Text.Printf (printf)
 
@@ -64,6 +63,12 @@
   where
     cleanup (fp, _) = removeFile fp
 
+withTempFile :: String -> ((FilePath, Handle) -> IO a) -> IO a
+withTempFile pattern =
+  bracket
+    (openTempFile "." pattern)
+    (\(path, _) -> removeFile path)
+
 testCLI :: [String] -> [String] -> Expectation
 testCLI args outputs = do
   (out, _) <- withStdout (try (runCLI args) :: IO (Either ExitCode ()))
@@ -86,24 +91,24 @@
   it "prints version" $
     testCLI ["--version"] [showVersion version]
 
-  it "prints help" $ do
-    output <- capture_ (runCLI ["--help"])
-    output `shouldContain` "Phino - CLI Manipulator of 𝜑-Calculus Expressions"
-    output `shouldContain` "Usage:"
+  it "prints help" $
+    testCLI
+      ["--help"]
+      ["Phino - CLI Manipulator of 𝜑-Calculus Expressions", "Usage:"]
 
   it "prints debug info with --log-level=DEBUG" $
     withStdin "Q -> [[]]" $
-      testCLI ["rewrite", "--nothing", "--log-level=DEBUG"] ["[DEBUG]:"]
+      testCLI ["rewrite", "--log-level=DEBUG"] ["[DEBUG]:"]
 
   describe "rewrites" $ do
-    it "desugares with --nothing flag from file" $
+    it "desugares without any rules flag from file" $
       testCLI
-        ["rewrite", "--nothing", "test-resources/cli/desugar.phi"]
+        ["rewrite", "test-resources/cli/desugar.phi"]
         ["Φ ↦ ⟦\n  foo ↦ Φ.org.eolang,\n  ρ ↦ ∅\n⟧"]
 
-    it "desugares with --nothing flag from stdin" $
+    it "desugares with without any rules flag from stdin" $
       withStdin "{[[foo ↦ QQ]]}" $
-        testCLI ["rewrite", "--nothing"] ["Φ ↦ ⟦\n  foo ↦ Φ.org.eolang,\n  ρ ↦ ∅\n⟧"]
+        testCLI ["rewrite"] ["Φ ↦ ⟦\n  foo ↦ Φ.org.eolang,\n  ρ ↦ ∅\n⟧"]
 
     it "rewrites with single rule" $
       withStdin "{T(x -> Q.y)}" $
@@ -125,13 +130,13 @@
             ]
         ]
 
-    it "fails with negative --max-depth" $
+    it "fails with --input=latex" $
       withStdin "" $
-        testCLIFailed ["rewrite", "--max-depth=-1"] "--max-depth must be positive"
+        testCLIFailed ["rewrite", "--input=latex"] "The value 'latex' can't be used for '--input' option"
 
-    it "fails with no rewriting options provided" $
+    it "fails with negative --max-depth" $
       withStdin "" $
-        testCLIFailed ["rewrite"] "no --rule, no --normalize, no --nothing are provided"
+        testCLIFailed ["rewrite", "--max-depth=-1"] "--max-depth must be positive"
 
     it "normalizes from stdin" $
       withStdin "Φ ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ [[ ]]) ⟧" $
@@ -151,19 +156,37 @@
     it "rewrites with --sweet flag" $
       withStdin "Q -> [[ x -> 5]]" $
         testCLI
-          ["rewrite", "--nothing", "--sweet"]
+          ["rewrite", "--sweet"]
           ["{⟦\n  x ↦ 5\n⟧}"]
 
     it "rewrites as XMIR" $
       withStdin "Q -> [[ x -> Q.y ]]" $
         testCLI
-          ["rewrite", "--nothing", "--output=xmir"]
+          ["rewrite", "--output=xmir"]
           ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "  <o base=\"Q.y\" name=\"x\"/>"]
 
+    it "rewrites as LaTeX" $
+      withStdin "Q -> [[ x -> QQ.z(y -> 5), q -> T ]]" $
+        testCLI
+          ["rewrite", "--output=latex", "--sweet"]
+          [ "\\documentclass{article}",
+            "\\usepackage{eolang}",
+            "\\begin{document}",
+            "\\begin{phiquation}",
+            "{[[",
+            "  x -> QQ.z(",
+            "    y -> 5",
+            "  ),",
+            "  q -> T",
+            "]]}",
+            "\\end{phiquation}",
+            "\\end{document}"
+          ]
+
     it "rewrites with XMIR as input" $
       withStdin "<object><o name=\"app\"><o name=\"x\" base=\"Q.number\"/></o></object>" $
         testCLI
-          ["rewrite", "--nothing", "--input=xmir", "--sweet"]
+          ["rewrite", "--input=xmir", "--sweet"]
           [ unlines
               [ "{⟦",
                 "  app ↦ ⟦",
@@ -176,8 +199,8 @@
     it "rewrites as XMIR with omit-listing flag" $
       withStdin "Q -> [[ x -> Q.y ]]" $
         testCLI
-          ["rewrite", "--nothing", "--output=xmir", "--omit-listing"]
-          ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "<listing>4 lines of phi</listing>", "  <o base=\"Q.y\" name=\"x\"/>"]
+          ["rewrite", "--output=xmir", "--omit-listing"]
+          ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "<listing>1 line(s)</listing>", "  <o base=\"Q.y\" name=\"x\"/>"]
 
     it "does not fail on exactly 1 rewriting" $
       withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
@@ -185,41 +208,122 @@
           ["rewrite", "--rule=test-resources/cli/simple.yaml", "--must=1", "--sweet"]
           ["x ↦ \"bar\""]
 
-    it "fails with --nothing and --must" $
-      withStdin "Q -> [[ ]]" $
-        testCLIFailed ["rewrite", "--nothing", "--must"] "it's expected exactly 1 rewriting cycles happened, but rewriting stopped after 0"
-
-    it "fails with --normalize and --must" $
+    it "fails with --normalize and --must=1" $
       withStdin "Q -> [[ x -> [[ y -> 5 ]].y ]].x" $
-        testCLIFailed ["rewrite", "--max-depth=2", "--normalize", "--must"] "it's expected exactly 1 rewriting cycles happened, but rewriting is still going"
+        testCLIFailed ["rewrite", "--max-depth=2", "--normalize", "--must=1"] "it's expected rewriting cycles to be in range [1], but rewriting has already reached 2"
 
+    describe "must range tests" $ do
+      it "accepts range ..5 (0 to 5 cycles)" $
+        withStdin "Q -> [[ ]]" $
+          testCLI ["rewrite", "--must=..5", "--sweet"] ["{⟦⟧}"]
+
+      it "accepts range 0..0 (exactly 0 cycles)" $
+        withStdin "Q -> [[ ]]" $
+          testCLI ["rewrite", "--must=0..0", "--sweet"] ["{⟦⟧}"]
+
+      it "accepts range 1..1 (exactly 1 cycle)" $
+        withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
+          testCLI
+            ["rewrite", "--rule=test-resources/cli/simple.yaml", "--must=1..1", "--sweet"]
+            ["x ↦ \"bar\""]
+
+      it "accepts range 1..3 when 1 cycle happens" $
+        withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
+          testCLI
+            ["rewrite", "--rule=test-resources/cli/simple.yaml", "--must=1..3", "--sweet"]
+            ["x ↦ \"bar\""]
+
+      it "accepts range 0.. (0 or more)" $
+        withStdin "Q -> [[ ]]" $
+          testCLI ["rewrite", "--must=0..", "--sweet"] ["{⟦⟧}"]
+
+      it "fails when cycles exceed range ..1" $
+        withStdin "Q -> [[ x -> [[ y -> 5 ]].y ]].x" $
+          testCLIFailed
+            ["rewrite", "--max-depth=2", "--normalize", "--must=..1"]
+            "it's expected rewriting cycles to be in range [..1], but rewriting has already reached 2"
+
+      it "fails when cycles below range 2.." $
+        withStdin "{⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧}" $
+          testCLIFailed
+            ["rewrite", "--rule=test-resources/cli/simple.yaml", "--must=2.."]
+            "it's expected rewriting cycles to be in range [2..], but rewriting stopped after 1"
+
+      it "fails with invalid range 5..3" $
+        withStdin "Q -> [[ ]]" $
+          testCLIFailed
+            ["rewrite", "--must=5..3"]
+            "cannot parse value `5..3'"
+
+      it "fails with negative in range -1..5" $
+        withStdin "Q -> [[ ]]" $
+          testCLIFailed
+            ["rewrite", "--must=-1..5"]
+            "cannot parse value `-1..5'"
+
+      it "fails with malformed range syntax" $
+        withStdin "Q -> [[ ]]" $
+          testCLIFailed
+            ["rewrite", "--must=3...5"]
+            "cannot parse value `3...5'"
+
     it "prints to target file" $
       withStdin "Q -> [[ ]]" $
-        bracket
-          (openTempFile "." "targetXXXXXX.tmp")
-          (\(path, _) -> removeFile path)
-          ( \(path, h) -> do
-              hClose h
-              testCLI
-                ["rewrite", "--nothing", "--sweet", printf "--target=%s" path]
-                [printf "The result program was saved in '%s'" path]
-              content <- readFile path
-              content `shouldBe` "{⟦⟧}"
-          )
+        withTempFile "targetXXXXXX.tmp" $ \(path, h) -> do
+          hClose h
+          testCLI
+            ["rewrite", "--sweet", printf "--target=%s" path]
+            [printf "The command result was saved in '%s'" path]
+          content <- readFile path
+          content `shouldBe` "{⟦⟧}"
 
+    it "modifies file in-place" $
+      withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
+        hPutStr h "Q -> [[ x -> \"foo\" ]]"
+        hClose h
+        testCLI
+          ["rewrite", "--rule=test-resources/cli/simple.yaml", "--in-place", "--sweet", path]
+          [printf "The file '%s' was modified in-place" path]
+        content <- readFile path
+        content `shouldBe` "{⟦\n  x ↦ \"bar\"\n⟧}"
+
+    it "fails when --in-place is used without input file" $
+      withStdin "Q -> [[ ]]" $
+        testCLIFailed
+          ["rewrite", "--in-place"]
+          "--in-place requires an input file"
+
+    it "fails when --in-place is used with --target" $
+      withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
+        hPutStr h "Q -> [[ ]]"
+        hClose h
+        testCLIFailed
+          ["rewrite", "--in-place", "--target=output.phi", path]
+          "--in-place and --target cannot be used together"
+
     it "rewrites with cycles" $
-      withStdin "Q -> [[ x -> 1 ]]" $
+      withStdin "Q -> [[ x -> \"x\" ]]" $
         testCLI
           ["rewrite", "--sweet", "--rule=test-resources/cli/infinite.yaml", "--max-depth=1", "--max-cycles=2"]
           [ unlines
               [ "{⟦",
-                "  x ↦ 1,",
-                "  x ↦ 1,",
-                "  x ↦ 1",
+                "  x ↦ \"x_hi_hi\"",
                 "⟧}"
               ]
           ]
 
+    it "fails with --depth-sensitive" $
+      withStdin "Q -> [[ x -> \"x\"]]" $
+        testCLIFailed
+          ["rewrite", "--depth-sensitive", "--max-depth=1", "--max-cycles=1", "--rule=test-resources/cli/infinite.yaml"]
+          "[ERROR]: With option --depth-sensitive it's expected rewriting iterations amount does not reach the limit: --max-depth=1"
+
+    it "fails on --sweet and --output=xmir together" $
+      withStdin "Q -> [[ ]]" $
+        testCLIFailed
+          ["rewrite", "--sweet", "--output=xmir"]
+          "The --sweet and --output=xmir can't stay together"
+
   describe "dataize" $ do
     it "dataizes simple program" $
       withStdin "Q -> [[ D> 01- ]]" $
@@ -228,3 +332,38 @@
     it "fails to dataize" $
       withStdin "Q -> [[ ]]" $
         testCLIFailed ["dataize"] "[ERROR]: Could not dataize given program"
+
+  describe "explain" $ do
+    it "explains single rule" $
+      testCLI
+        ["explain", "--rule=resources/copy.yaml"]
+        ["\\documentclass{article}", "\\usepackage{amsmath}", "\\begin{document}", "\\rule{COPY}", "\\end{document}"]
+
+    it "explains multiple rules" $
+      testCLI
+        ["explain", "--rule=resources/copy.yaml", "--rule=resources/alpha.yaml"]
+        ["\\documentclass{article}", "\\rule{COPY}", "\\rule{ALPHA}"]
+
+    it "explains normalization rules" $
+      testCLI
+        ["explain", "--normalize"]
+        ["\\documentclass{article}", "\\begin{document}", "\\end{document}"]
+
+    it "fails with no rules specified" $
+      testCLIFailed
+        ["explain"]
+        "Either --rule or --normalize must be specified"
+
+    it "writes to target file" $
+      bracket
+        (openTempFile "." "explainXXXXXX.tex")
+        (\(path, _) -> removeFile path)
+        ( \(path, h) -> do
+            hClose h
+            testCLI
+              ["explain", "--normalize", printf "--target=%s" path]
+              [printf "was saved in '%s'" path]
+            content <- readFile path
+            content `shouldContain` "\\documentclass{article}"
+            content `shouldContain` "\\begin{document}"
+        )
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -11,7 +11,7 @@
 import Functions (buildTerm)
 
 defaultDataizeContext :: Program -> DataizeContext
-defaultDataizeContext prog = DataizeContext prog 25 1 buildTerm
+defaultDataizeContext prog = DataizeContext prog 25 1 False buildTerm
 
 test :: (Eq a, Show a) => (Expression -> DataizeContext -> IO (Maybe a)) -> [(String, Expression, Expression, Maybe a)] -> Spec
 test func useCases =
diff --git a/test/FunctionsSpec.hs b/test/FunctionsSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/FunctionsSpec.hs
@@ -0,0 +1,28 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module FunctionsSpec where
+
+import Ast
+import Data.Map.Strict qualified as Map
+import Functions (buildTerm)
+import Logger (logDebug)
+import Matcher (MetaValue (MvBindings), Subst (Subst))
+import Misc (uniqueBindings')
+import Pretty (prettyExpression')
+import Term (Term (TeBindings))
+import Test.Hspec (Spec, describe, it, shouldBe)
+import Text.Printf (printf)
+import Yaml (ExtraArgument (ArgBinding))
+
+spec :: Test.Hspec.Spec
+spec = describe "Functions" $
+  Test.Hspec.it "contains only unique bindings after 'join'" $ do
+    let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExGlobal, BiVoid (AtAlpha 0)])
+        second = ("B2", MvBindings [BiTau AtRho ExThis, BiLambda "Func", BiDelta (BtOne "00"), BiVoid (AtAlpha 1)])
+        third = ("B3", MvBindings [BiLambda "Some", BiTau (AtLabel "y") ExThis, BiTau (AtLabel "x") ExThis, BiVoid (AtAlpha 0)])
+        subst = Subst (Map.fromList [first, second, third])
+    TeBindings bds <- buildTerm "join" [ArgBinding (BiMeta "B1"), ArgBinding (BiMeta "B2"), ArgBinding (BiMeta "B3")] subst (Program ExGlobal)
+    bds' <- uniqueBindings' bds
+    logDebug (printf "Joined bindings:\n%s" (prettyExpression' (ExFormation bds')))
+    length bds' `shouldBe` 9
diff --git a/test/MiscSpec.hs b/test/MiscSpec.hs
--- a/test/MiscSpec.hs
+++ b/test/MiscSpec.hs
@@ -4,9 +4,10 @@
 module MiscSpec where
 
 import Control.Monad (forM_)
-import Misc (withVoidRho)
-import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, shouldBe)
+import Misc (withVoidRho, uniqueBindings)
+import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, shouldBe, shouldSatisfy)
 import Ast
+import Data.Either (isLeft, isRight)
 
 testWithVoidRho :: [(String, [Binding], [Binding])] -> SpecWith (Arg Expectation)
 testWithVoidRho useCases =
@@ -14,7 +15,7 @@
     it desc $ withVoidRho before `shouldBe` after
 
 spec :: Spec
-spec =
+spec = do
   describe "with void rho binding" $
     testWithVoidRho
       [ ( "[[x -> ?]] => [[x -> ?, ^ -> ?]]",
@@ -48,3 +49,9 @@
           [BiTau (AtMeta "a") (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
         )
       ]
+
+  describe "unique bindings" $ do
+    it "fails with duplicate attribute" $
+      uniqueBindings [BiVoid AtRho, BiVoid AtRho] `shouldSatisfy` isLeft
+    it "does not fail on different attributes" $
+      uniqueBindings [BiVoid AtPhi, BiVoid AtRho] `shouldSatisfy` isRight
diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs
--- a/test/ParserSpec.hs
+++ b/test/ParserSpec.hs
@@ -99,16 +99,13 @@
                 )
             )
         ),
-        ( "[[x -> y.z, a -> ~1, w -> ^, u -> @, p -> !a, q -> !e]]",
+        ( "[[x -> y.z, w -> ^, u -> @, p -> !a, q -> !e]]",
           Just
             ( ExFormation
                 [ BiTau
                     (AtLabel "x")
                     (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z")),
                   BiTau
-                    (AtLabel "a")
-                    (ExDispatch ExThis (AtAlpha 1)),
-                  BiTau
                     (AtLabel "w")
                     (ExDispatch ExThis AtRho),
                   BiTau
@@ -124,21 +121,18 @@
                 ]
             )
         ),
-        ( "Q.x(~1, y, [[]].z, Q.y(^,@))",
+        ( "Q.x(y, [[]].z, Q.y(^,@))",
           Just
             ( ExApplication
                 ( ExApplication
                     ( ExApplication
-                        ( ExApplication
-                            (ExDispatch ExGlobal (AtLabel "x"))
-                            (BiTau (AtAlpha 0) (ExDispatch ExThis (AtAlpha 1)))
-                        )
-                        (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "y")))
+                        (ExDispatch ExGlobal (AtLabel "x"))
+                        (BiTau (AtAlpha 0) (ExDispatch ExThis (AtLabel "y")))
                     )
-                    (BiTau (AtAlpha 2) (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "z")))
+                    (BiTau (AtAlpha 1) (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "z")))
                 )
                 ( BiTau
-                    (AtAlpha 3)
+                    (AtAlpha 2)
                     ( ExApplication
                         ( ExApplication
                             (ExDispatch ExGlobal (AtLabel "y"))
@@ -229,17 +223,15 @@
         "Q.x(y() -> [[]])",
         "Q.x(y(q) -> [[w -> !e]])",
         "Q.x(~1(^,@) -> [[]])",
-        "Q.x.~1.^.@.!a0",
+        "Q.x.^.@.!a0",
         "[[x -> y.z]]",
-        "[[x -> ~1]]",
         "[[x -> ^, y -> @, z -> !a]]",
         "Q.x(a.b.c, Q.a(b), [[]])",
-        "Q.x(~1, y, [[]].z, Q.y(^,@))",
+        "Q.x(y, [[]].z, Q.y(^,@))",
         "[[x -> 5.plus(5), y -> \"hello\", z -> 42.5]]",
-        "[[w -> x(~1)]]",
         "[[\n  x -> \"Hi\",\n  y -> 42\n]]",
         "[[x -> -42, y -> +34]]",
-        "⟦x ↦ Φ.org.eolang(z ↦ ξ.f, x ↦ α0, φ ↦ ρ, t ↦ φ, first ↦ ⟦ λ ⤍ Function_name, Δ ⤍ 42- ⟧)⟧",
+        "⟦x ↦ Φ.org.eolang(z ↦ ξ.f, φ ↦ ρ, t ↦ φ, first ↦ ⟦ λ ⤍ Function_name, Δ ⤍ 42- ⟧)⟧",
         "[[x -> 1.00e+3, y -> 2.32e-4]]",
         "[[ x -> \"\\u0001\\u0001\"]]",
         "[[ x -> \"\\uD835\\uDF11\"]]",
@@ -269,11 +261,15 @@
             "[[z(w) -> Q.x]]",
             "Q.x(y(~1) -> [[]])",
             "Q.x(1, 2, !B)",
+            "Q.x.~0",
             "Q.x(~1 -> Q.y, x -> 5, !B1)",
             "Q.x(𝐵1, 𝜏0 -> $, x -> 𝑒)",
             "[[ x -> \"\\uD800\"]]",
             "[[ x -> \"\\uDFFF\"]]",
-            "[[ x -> \"\\uD835\\u0041\"]]"
+            "[[ x -> \"\\uD835\\u0041\"]]",
+            "[[ x -> 1, x -> 2 ]]",
+            "⟦ k ↦ ⟦ λ ⤍ Foo, λ ⤍ Bar ⟧ ⟧",
+            "⟦ k ↦ ⟦ Δ ⤍ 42-, Δ ⤍ 55- ⟧ ⟧"
           ]
       )
 
@@ -284,4 +280,13 @@
       ( \pack -> do
           content <- runIO (readFile pack)
           it (takeBaseName pack) (parseProgram content `shouldSatisfy` isRight)
+      )
+
+  describe "process typo packs" $ do
+    packs <- runIO (allPathsIn "test-resources/phi-typos-packs")
+    forM_
+      packs
+      ( \pack -> do
+          content <- runIO (readFile pack)
+          it (takeBaseName pack) (parseProgram content `shouldSatisfy` isLeft)
       )
diff --git a/test/PrettySpec.hs b/test/PrettySpec.hs
--- a/test/PrettySpec.hs
+++ b/test/PrettySpec.hs
@@ -10,10 +10,10 @@
 import Pretty
 import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, runIO, shouldBe)
 
-test :: (a -> PrintMode -> String) -> [(String, String, a, PrintMode)] -> SpecWith (Arg Expectation)
+test :: (a -> PrintMode -> Encoding -> String) -> [(String, String, a, PrintMode)] -> SpecWith (Arg Expectation)
 test function useCases =
   forM_ useCases $ \(input, output, arg, mode) ->
-    it input $ function arg mode `shouldBe` output
+    it input $ function arg mode UNICODE `shouldBe` output
 
 prep :: PrintMode -> (String, String) -> IO (String, String, Program, PrintMode)
 prep mode (input, output) = do
diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs
--- a/test/RewriterSpec.hs
+++ b/test/RewriterSpec.hs
@@ -15,8 +15,9 @@
 import Functions (buildTerm)
 import GHC.Generics
 import Misc (allPathsIn, ensuredFile)
+import Must (Must(..))
 import Parser (parseProgramThrows)
-import Pretty (PrintMode (SWEET), prettyProgram')
+import Pretty (PrintMode (SWEET), prettyProgram', Encoding (UNICODE))
 import Rewriter (RewriteContext (RewriteContext), rewrite')
 import System.FilePath (makeRelative, replaceExtension, (</>))
 import Test.Hspec (Spec, describe, expectationFailure, it, pending, runIO)
@@ -74,8 +75,8 @@
                     Just num -> num
                     _ -> 1
               must' = case must pack of
-                Just num -> num
-                _ -> 0
+                Just num -> MtExact num
+                _ -> MtDisabled
           case skip pack of
             Just True -> pending
             _ -> do
@@ -96,13 +97,13 @@
                   if normalize'
                     then pure normalizationRules
                     else pure []
-              rewritten <- rewrite' program rules' (RewriteContext program repeat' repeat' buildTerm must')
+              rewritten <- rewrite' program rules' (RewriteContext program repeat' repeat' False buildTerm must')
               result' <- parseProgramThrows (output pack)
               unless (rewritten == result') $
                 expectationFailure
                   ( "Wrong rewritten program. Expected:\n"
-                      ++ prettyProgram' result' SWEET
+                      ++ prettyProgram' result' SWEET UNICODE
                       ++ "\nGot:\n"
-                      ++ prettyProgram' rewritten SWEET
+                      ++ prettyProgram' rewritten SWEET UNICODE
                   )
       )
diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs
--- a/test/XMIRSpec.hs
+++ b/test/XMIRSpec.hs
@@ -1,45 +1,123 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DuplicateRecordFields #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
 module XMIRSpec where
 
-import Control.Monad (forM_)
+import Ast
+import Control.Exception (bracket)
+import Control.Monad (filterM, forM_, unless)
 import Data.Aeson
+import Data.List (intercalate)
 import Data.Yaml qualified as Yaml
 import GHC.Generics (Generic)
+import GHC.IO (unsafePerformIO)
 import Misc (allPathsIn)
-import Parser (parseProgramThrows)
+import Parser (parseExpressionThrows, parseProgramThrows)
+import System.Directory (removeFile)
+import System.Exit (ExitCode (ExitSuccess))
 import System.FilePath (makeRelative)
-import Test.Hspec (Spec, describe, it, runIO, shouldBe)
-import XMIR (parseXMIRThrows, xmirToPhi)
+import System.IO (hClose, hPutStr, openTempFile)
+import System.Process (readProcessWithExitCode)
+import Test.Hspec (Spec, anyException, describe, expectationFailure, it, pendingWith, runIO, shouldBe, shouldThrow)
+import XMIR (defaultXmirContext, parseXMIRThrows, printXMIR, programToXMIR, xmirToPhi)
 
-data XMIRPack = XMIRPack
-  { xmir :: String,
+data ParsePack = ParsePack
+  { failure :: Maybe Bool,
+    xmir :: String,
     phi :: String
   }
   deriving (Generic, Show, FromJSON)
 
-xmirPack :: FilePath -> IO XMIRPack
-xmirPack = Yaml.decodeFileThrow
+data PrintPack = PrintPack
+  { phi :: String,
+    xpaths :: [String]
+  }
+  deriving (Generic, Show, FromJSON)
 
--- @todo #126:30min Introduce XMIR printing test. It's not possible anymore to compare XMIRs like strings
---  because they contain random data, e.g. system time. We need to introduce some convenient
---  test system for testing XML and use it here here.
+parsePack :: FilePath -> IO ParsePack
+parsePack = Yaml.decodeFileThrow
+
+printPack :: FilePath -> IO PrintPack
+printPack = Yaml.decodeFileThrow
+
+-- Check if xmllint is available on the system
+isXmllintAvailable :: Bool
+isXmllintAvailable =
+  let (exitCode, _, _) = unsafePerformIO (readProcessWithExitCode "xmllint" ["--version"] "")
+   in (exitCode == ExitSuccess)
+
 spec :: Spec
-spec =
+spec = do
   describe "XMIR parsing packs" $ do
     let resources = "test-resources/xmir-parsing-packs"
     packs <- runIO (allPathsIn resources)
     forM_
       packs
       ( \pth -> it (makeRelative resources pth) $ do
-          pack <- xmirPack pth
-          xmir' <- do
-            doc <- parseXMIRThrows (xmir pack)
-            xmirToPhi doc
-          phi' <- parseProgramThrows (phi pack)
-          xmir' `shouldBe` phi'
+          pack <- parsePack pth
+          let ParsePack {phi = phi'} = pack
+              xmir' = do
+                doc <- parseXMIRThrows (xmir pack)
+                xmirToPhi doc
+          case failure pack of
+            Just True -> xmir' `shouldThrow` anyException
+            _ -> do
+              xmir'' <- xmir'
+              phi'' <- parseProgramThrows phi'
+              xmir'' `shouldBe` phi''
+      )
+
+  describe "prohibit to convert to XMIR" $
+    forM_
+      [ "[[ ]]",
+        "T",
+        "[[ x -> ? ]]",
+        "[[ ^ -> 5 ]]",
+        "Q.x.y.z",
+        "\"Hello\"",
+        "Q",
+        "$"
+      ]
+      ( \phi' -> it phi' $ do
+          expr <- parseExpressionThrows phi'
+          programToXMIR (Program expr) defaultXmirContext `shouldThrow` anyException
+      )
+
+  describe "XMIR printing packs" $ do
+    let resources = "test-resources/xmir-printing-packs"
+        available = isXmllintAvailable
+    packs <- runIO (allPathsIn resources)
+    forM_
+      packs
+      ( \pth ->
+          it (makeRelative resources pth) $
+            if not available
+              then pendingWith "The 'xmllint' is not available"
+              else do
+                pack <- printPack pth
+                let PrintPack {phi = phi', xpaths = xpaths'} = pack
+                prog <- parseProgramThrows phi'
+                xmir' <- programToXMIR prog defaultXmirContext
+                let xml = printXMIR xmir'
+                bracket
+                  (openTempFile "." "xmirXXXXXX.tmp")
+                  (\(fp, _) -> removeFile fp)
+                  ( \(path, hTmp) -> do
+                      hPutStr hTmp xml
+                      hClose hTmp
+                      failed <-
+                        filterM
+                          ( \xpath -> do
+                              (code, _, _) <- readProcessWithExitCode "xmllint" ["--xpath", xpath, path] ""
+                              pure (code /= ExitSuccess)
+                          )
+                          xpaths'
+                      unless
+                        (null failed)
+                        (expectationFailure ("Failed xpaths:\n - " ++ intercalate "\n - " failed ++ "\nXMIR is:\n" ++ xml))
+                  )
       )
diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs
--- a/test/YamlSpec.hs
+++ b/test/YamlSpec.hs
@@ -3,14 +3,16 @@
 
 module YamlSpec where
 
+import Control.Exception (Exception (displayException), SomeException)
 import Control.Monad
+import Data.List (isInfixOf)
 import Misc
 import System.FilePath
-import Test.Hspec (Spec, describe, it, runIO, shouldReturn)
+import Test.Hspec (Spec, describe, it, runIO, shouldReturn, shouldThrow)
 import Yaml (yamlRule)
 
 spec :: Spec
-spec =
+spec = do
   describe "parses yaml rule" $ do
     let resources = "test-resources/yaml-packs"
     packs <- runIO (allPathsIn resources)
@@ -19,4 +21,19 @@
       ( \pth -> it (makeRelative resources pth) $ do
           _ <- yamlRule pth
           pure () `shouldReturn` ()
+      )
+
+  describe "fails on yaml typos" $ do
+    let resources = "test-resources/yaml-typos"
+    packs <- runIO (allPathsIn resources)
+    forM_
+      packs
+      ( \pth ->
+          it (makeRelative resources pth) $
+            shouldThrow
+              (yamlRule pth)
+              ( \e ->
+                  let msg = displayException (e :: SomeException)
+                   in "Unknown" `isInfixOf` msg || "Exactly one" `isInfixOf` msg
+              )
       )