diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@
 
 ```bash
 cabal update
-cabal install --overwrite-policy=always phino-0.0.0.59
+cabal install --overwrite-policy=always phino-0.0.0.60
 phino --version
 ```
 
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.0.60
+version: 0.0.0.61
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
@@ -38,6 +38,11 @@
     Builder
     Canonizer
     CLI
+    CLI.Helpers
+    CLI.Parsers
+    CLI.Runners
+    CLI.Types
+    CLI.Validators
     Condition
     CST
     Dataize
@@ -125,7 +130,6 @@
     FilterSpec
     FunctionsSpec
     LaTeXSpec
-    LiningSpec
     LocatorSpec
     MatcherSpec
     MergeSpec
diff --git a/resources/copy.yaml b/resources/copy.yaml
--- a/resources/copy.yaml
+++ b/resources/copy.yaml
@@ -5,7 +5,9 @@
 pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒1)
 result: ⟦ 𝐵1, 𝜏 ↦ 𝑒3, 𝐵2 ⟧
 when:
-  xi: 𝑒1
+  and:
+    - xi: 𝑒1
+    - nf: 𝑒1
 where:
   - meta: 𝑒2
     function: scope
diff --git a/src/CLI.hs b/src/CLI.hs
--- a/src/CLI.hs
+++ b/src/CLI.hs
@@ -1,7 +1,5 @@
-{-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
@@ -9,508 +7,14 @@
 
 module CLI (runCLI) where
 
-import AST
-import qualified Canonizer as C
-import Condition (parseConditionThrows)
-import Control.Exception.Base (Exception (displayException), SomeException, catch, fromException, handle, throwIO)
-import Control.Monad (forM_, unless, when, (>=>))
-import Data.Char (toLower, toUpper)
-import Data.Foldable (for_)
-import Data.Functor ((<&>))
-import Data.List (intercalate)
-import Data.Maybe (fromJust, fromMaybe, isJust, isNothing)
-import Data.Version (showVersion)
-import Dataize (DataizeContext (DataizeContext), dataize)
-import Deps (SaveStepFunc, saveStep)
-import Encoding (Encoding (UNICODE))
-import qualified Filter as F
-import Functions (buildTerm)
-import LaTeX (LatexContext (LatexContext), defaultMeetLength, defaultMeetPopularity, explainRules, expressionToLaTeX, programToLaTeX, rewrittensToLatex)
-import Lining (LineFormat (MULTILINE, SINGLELINE))
-import Locator (locatedExpression)
+import CLI.Parsers
+import CLI.Runners
+import CLI.Types
+import Control.Exception.Base (Exception (displayException), SomeException, fromException, handle)
 import Logger
-import Margin (defaultMargin)
-import Merge (merge)
-import Misc (ensuredFile)
-import qualified Misc
-import Must (Must (..), validateMust)
 import Options.Applicative
-import Parser (parseExpressionThrows, parseProgramThrows)
-import Paths_phino (version)
-import qualified Printer as P
-import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)
-import Rule (RuleContext (RuleContext), matchProgramWithRule)
-import Sugar
 import System.Exit (ExitCode (..), exitFailure)
-import System.IO (getContents')
-import Text.Printf (printf)
-import XMIR (XmirContext (XmirContext), defaultXmirContext, parseXMIRThrows, printXMIR, programToXMIR, xmirToPhi)
-import Yaml (normalizationRules)
-import qualified Yaml as Y
 
-data PrintProgramContext = PrintProgCtx
-  { _sugar :: SugarType
-  , _line :: LineFormat
-  , _margin :: Int
-  , _xmirCtx :: XmirContext
-  , _nonumber :: Bool
-  , _compress :: Bool
-  , _sequence :: Bool
-  , _meetPopularity :: Int
-  , _meetLength :: Int
-  , _focus :: Expression
-  , _expression :: Maybe String
-  , _label :: Maybe String
-  , _meetPrefix :: Maybe String
-  , _outputFormat :: IOFormat
-  }
-
-data CmdException
-  = InvalidCLIArguments String
-  | CouldNotReadFromStdin String
-  | CouldNotDataize
-  | CouldNotPrintExpressionInXMIR
-  deriving (Exception)
-
-instance Show CmdException where
-  show (InvalidCLIArguments msg) = printf "Invalid set of arguments: %s" msg
-  show (CouldNotReadFromStdin msg) = printf "Could not read input from stdin\nReason: %s" msg
-  show CouldNotDataize = "Could not dataize given program"
-  show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only program printing is allowed"
-
-data Command
-  = CmdRewrite OptsRewrite
-  | CmdDataize OptsDataize
-  | CmdExplain OptsExplain
-  | CmdMerge OptsMerge
-  | CmdMatch OptsMatch
-
-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
-  , _logLines :: Int
-  , _inputFormat :: IOFormat
-  , _outputFormat :: IOFormat
-  , _sugarType :: SugarType
-  , _flat :: LineFormat
-  , _omitListing :: Bool
-  , _omitComments :: Bool
-  , _nonumber :: Bool
-  , _sequence :: Bool
-  , _canonize :: Bool
-  , _depthSensitive :: Bool
-  , _quiet :: Bool
-  , _compress :: Bool
-  , _maxDepth :: Int
-  , _maxCycles :: Int
-  , _margin :: Int
-  , _meetPopularity :: Maybe Int
-  , _meetLength :: Maybe Int
-  , _hide :: [String]
-  , _show :: [String]
-  , _locator :: String
-  , _focus :: String
-  , _expression :: Maybe String
-  , _label :: Maybe String
-  , _meetPrefix :: Maybe String
-  , _stepsDir :: Maybe FilePath
-  , _inputFile :: Maybe FilePath
-  }
-
-data OptsExplain = OptsExplain
-  { _logLevel :: LogLevel
-  , _logLines :: Int
-  , _rules :: [FilePath]
-  , _normalize :: Bool
-  , _shuffle :: Bool
-  , _targetFile :: Maybe FilePath
-  }
-
-data OptsRewrite = OptsRewrite
-  { _logLevel :: LogLevel
-  , _logLines :: Int
-  , _inputFormat :: IOFormat
-  , _outputFormat :: IOFormat
-  , _sugarType :: SugarType
-  , _flat :: LineFormat
-  , _must :: Must
-  , _normalize :: Bool
-  , _shuffle :: Bool
-  , _omitListing :: Bool
-  , _omitComments :: Bool
-  , _depthSensitive :: Bool
-  , _nonumber :: Bool
-  , _inPlace :: Bool
-  , _sequence :: Bool
-  , _canonize :: Bool
-  , _compress :: Bool
-  , _maxDepth :: Int
-  , _maxCycles :: Int
-  , _margin :: Int
-  , _meetPopularity :: Maybe Int
-  , _meetLength :: Maybe Int
-  , _rules :: [FilePath]
-  , _hide :: [String]
-  , _show :: [String]
-  , _locator :: String
-  , _focus :: String
-  , _expression :: Maybe String
-  , _label :: Maybe String
-  , _meetPrefix :: Maybe String
-  , _targetFile :: Maybe FilePath
-  , _stepsDir :: Maybe FilePath
-  , _inputFile :: Maybe FilePath
-  }
-
-data OptsMerge = OptsMerge
-  { _logLevel :: LogLevel
-  , _logLines :: Int
-  , _inputFormat :: IOFormat
-  , _outputFormat :: IOFormat
-  , _sugarType :: SugarType
-  , _flat :: LineFormat
-  , _omitListing :: Bool
-  , _omitComments :: Bool
-  , _margin :: Int
-  , _targetFile :: Maybe FilePath
-  , _inputs :: [FilePath]
-  }
-
-data OptsMatch = OptsMatch
-  { _logLevel :: LogLevel
-  , _logLines :: Int
-  , _sugarType :: SugarType
-  , _flat :: LineFormat
-  , _pattern :: Maybe String
-  , _when :: Maybe String
-  , _inputFile :: Maybe FilePath
-  }
-
-validateIntOption :: (Int -> Bool) -> String -> Int -> ReadM Int
-validateIntOption cmp msg num
-  | cmp num = return num
-  | otherwise = readerError msg
-
-optLogLevel :: Parser LogLevel
-optLogLevel =
-  option
-    parseLogLevel
-    ( long "log-level"
-        <> metavar "LEVEL"
-        <> help ("Log level (" <> intercalate ", " (map show [DEBUG, ERROR, NONE]) <> ")")
-        <> value ERROR
-        <> showDefault
-    )
-  where
-    parseLogLevel :: ReadM LogLevel
-    parseLogLevel = eitherReader $ \lvl -> case map toUpper lvl of
-      "DEBUG" -> Right DEBUG
-      "ERROR" -> Right ERROR
-      "ERR" -> Right ERROR
-      "NONE" -> Right NONE
-      _ -> Left $ "unknown log-level: " <> lvl
-
-optLogLines :: Parser Int
-optLogLines =
-  option
-    (auto >>= validateIntOption (>= -1) "--log-lines must be >= -1")
-    (long "log-lines" <> metavar "LINES" <> help "Amount of lines printed to console per each log operation (0 - print nothing, -1 - no limits)" <> value 25 <> showDefault)
-
-optRule :: Parser [FilePath]
-optRule = many (strOption (long "rule" <> metavar "[FILE]" <> help "Path to custom rule"))
-
-optInputFormat :: Parser IOFormat
-optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Program input format (phi, xmir)" <> value PHI <> showDefault)
-
-parseIOFormat :: String -> ReadM IOFormat
-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')
-
-optOutputFormat :: Parser IOFormat
-optOutputFormat =
-  option
-    (parseIOFormat "output")
-    (long "output" <> metavar "FORMAT" <> help (printf "Result and intermediate (see %s option(s)) programs output format (phi, xmir, latex)" _intermediateOptions) <> value PHI <> showDefault)
-
-argInputFile :: Parser (Maybe FilePath)
-argInputFile = optional (argument str (metavar "FILE" <> help "Path to input file"))
-
-optMaxDepth :: Parser Int
-optMaxDepth =
-  option
-    (auto >>= validateIntOption (> 0) "--max-depth must be positive")
-    (long "max-depth" <> metavar "DEPTH" <> help "Maximum number of rewriting iterations per rule" <> value 25 <> showDefault)
-
-optMaxCycles :: Parser Int
-optMaxCycles =
-  option
-    (auto >>= validateIntOption (> 0) "--max-cycles must be positive")
-    (long "max-cycles" <> metavar "CYCLES" <> help "Maximum number of rewriting cycles across all rules" <> value 25 <> showDefault)
-
-optMargin :: Parser Int
-optMargin =
-  option
-    (auto >>= validateIntOption (> 0) "--margin must be positive")
-    (long "margin" <> help "The maximum right margin for the printed 𝜑-programs or 𝜑-expressions" <> value defaultMargin <> showDefault)
-
-optMeetPopularity :: Parser (Maybe Int)
-optMeetPopularity =
-  optional
-    ( option
-        ( auto
-            >>= validateIntOption (> 0) "--meet-popularity must be positive"
-            >>= validateIntOption (< 100) "--meet-popularity must be <= 100"
-        )
-        ( long "meet-popularity"
-            <> metavar "PERCENTAGE"
-            <> help (printf "The minimum popularity of an expression in order to be suitable for \\phiMeet{}, in percentage (default: %d)" defaultMeetPopularity)
-        )
-    )
-
-optMeetLength :: Parser (Maybe Int)
-optMeetLength =
-  optional
-    ( option
-        (auto >>= validateIntOption (> 0) "--meet-length must be positive")
-        ( long "meet-length"
-            <> metavar "NODES"
-            <> help (printf "The minimum length of an expression that fits into \\phiMeet{}, in AST nodes (default: %d)" defaultMeetLength)
-        )
-    )
-
-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)")
-
-optNonumber :: Parser Bool
-optNonumber = switch (long "nonumber" <> help "Turn off equation auto numbering in LaTeX rendering (see --output option)")
-
-optSequence :: Parser Bool
-optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-programs concatenated with EOL")
-
-optCanonize :: Parser Bool
-optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with F1, F2, etc.")
-
-optExpression :: Parser (Maybe String)
-optExpression = optional (strOption (long "expression" <> metavar "NAME" <> help "Name for 'phiExpression' element when rendering to LaTeX (see --output option)"))
-
-optLabel :: Parser (Maybe String)
-optLabel = optional (strOption (long "label" <> metavar "NAME" <> help "Name for 'label' element when rendering to LaTeX (see --output option)"))
-
-optMeetPrefix :: Parser (Maybe String)
-optMeetPrefix = optional (strOption (long "meet-prefix" <> metavar "PREFIX" <> help "Prefix to be inserted before index in \\phiMeet{} and \\phiAgain{} LaTeX functions, e.g. \\phiMeet{foo:1}"))
-
-optHide :: Parser [String]
-optHide = many (strOption (long "hide" <> metavar "FQN" <> help "Location of object to exclude from result and intermediate programs after rewriting. Must be a valid dispatch expression; e.g. Q.org.eolang"))
-
-optShow :: Parser [String]
-optShow =
-  many
-    ( strOption
-        ( long "show"
-            <> metavar "FQN"
-            <> help
-              "Location of object to include to result and intermediate programs after rewriting. \
-              \Must be a valid dispatch expression; e.g. Q.org.eolang. Unlike --hide, can be used only once"
-        )
-    )
-
-optLocator :: Parser String
-optLocator = strOption (long "locator" <> metavar "FQN" <> help "Location of object to dataize. Must be a valid dispatch expression; e.g. Q.foo.bar" <> value "Q" <> showDefault)
-
-optFocus :: Parser String
-optFocus =
-  strOption
-    ( long "focus"
-        <> metavar "FQN"
-        <> help "Location of only object to be printed in entire program. Must be a valid dispatch expression; e.g. Q.foo.bar"
-        <> value "Q"
-        <> showDefault
-    )
-
-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"))
-
-optStepsDir :: Parser (Maybe FilePath)
-optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing"))
-
-optShuffle :: Parser Bool
-optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying")
-
-optSugar :: Parser SugarType
-optSugar = flag SALTY SWEET (long "sweet" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs using syntax sugar" _intermediateOptions))
-
-optSugar' :: Parser SugarType
-optSugar' = flag SALTY SWEET (long "sweet" <> help "Print result 𝜑-program using syntax sugar")
-
-optLineFormat :: Parser LineFormat
-optLineFormat = flag MULTILINE SINGLELINE (long "flat" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs in one line" _intermediateOptions))
-
-optLineFormat' :: Parser LineFormat
-optLineFormat' = flag MULTILINE SINGLELINE (long "flat" <> help "Print result 𝜑-program in one line")
-
-optOmitListing :: Parser Bool
-optOmitListing = switch (long "omit-listing" <> help "Omit full program listing in XMIR output")
-
-optOmitComments :: Parser Bool
-optOmitComments = switch (long "omit-comments" <> help "Omit comments in XMIR output")
-
-optCompress :: Parser Bool
-optCompress = switch (long "compress" <> help "Compress expressions in LaTeX output using \\phiMeet{} and \\phiAgain{} functions")
-
-_intermediateOptions :: String
-_intermediateOptions = intercalate ", " ["--sequence", "--steps-dir"]
-
-explainParser :: Parser Command
-explainParser =
-  CmdExplain
-    <$> ( OptsExplain
-            <$> optLogLevel
-            <*> optLogLines
-            <*> optRule
-            <*> optNormalize
-            <*> optShuffle
-            <*> optTarget
-        )
-
-dataizeParser :: Parser Command
-dataizeParser =
-  CmdDataize
-    <$> ( OptsDataize
-            <$> optLogLevel
-            <*> optLogLines
-            <*> optInputFormat
-            <*> optOutputFormat
-            <*> optSugar
-            <*> optLineFormat
-            <*> optOmitListing
-            <*> optOmitComments
-            <*> optNonumber
-            <*> optSequence
-            <*> optCanonize
-            <*> optDepthSensitive
-            <*> switch (long "quiet" <> help "Don't print the result of dataization")
-            <*> optCompress
-            <*> optMaxDepth
-            <*> optMaxCycles
-            <*> optMargin
-            <*> optMeetPopularity
-            <*> optMeetLength
-            <*> optHide
-            <*> optShow
-            <*> optLocator
-            <*> optFocus
-            <*> optExpression
-            <*> optLabel
-            <*> optMeetPrefix
-            <*> optStepsDir
-            <*> argInputFile
-        )
-
-rewriteParser :: Parser Command
-rewriteParser =
-  CmdRewrite
-    <$> ( OptsRewrite
-            <$> optLogLevel
-            <*> optLogLines
-            <*> optInputFormat
-            <*> optOutputFormat
-            <*> optSugar
-            <*> optLineFormat
-            <*> 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
-              )
-            <*> optNormalize
-            <*> optShuffle
-            <*> optOmitListing
-            <*> optOmitComments
-            <*> optDepthSensitive
-            <*> optNonumber
-            <*> switch (long "in-place" <> help "Edit file in-place instead of printing to output")
-            <*> optSequence
-            <*> optCanonize
-            <*> optCompress
-            <*> optMaxDepth
-            <*> optMaxCycles
-            <*> optMargin
-            <*> optMeetPopularity
-            <*> optMeetLength
-            <*> optRule
-            <*> optHide
-            <*> optShow
-            <*> optLocator
-            <*> optFocus
-            <*> optExpression
-            <*> optLabel
-            <*> optMeetPrefix
-            <*> optTarget
-            <*> optStepsDir
-            <*> argInputFile
-        )
-
-mergeParser :: Parser Command
-mergeParser =
-  CmdMerge
-    <$> ( OptsMerge
-            <$> optLogLevel
-            <*> optLogLines
-            <*> optInputFormat
-            <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help (printf "Result program output format (phi, xmir, latex)") <> value PHI <> showDefault)
-            <*> optSugar'
-            <*> optLineFormat'
-            <*> optOmitListing
-            <*> optOmitComments
-            <*> optMargin
-            <*> optTarget
-            <*> many (argument str (metavar "[FILE]" <> help "Paths to input files"))
-        )
-
-matchParser :: Parser Command
-matchParser =
-  CmdMatch
-    <$> ( OptsMatch
-            <$> optLogLevel
-            <*> optLogLines
-            <*> optSugar
-            <*> optLineFormat
-            <*> optional (strOption (long "pattern" <> metavar "EXPRESSION" <> help "Pattern expression to match against"))
-            <*> optional (strOption (long "when" <> metavar "CONDITION" <> help "Predicate for matched substitutions"))
-            <*> argInputFile
-        )
-
-commandParser :: Parser Command
-commandParser =
-  hsubparser
-    ( 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"))
-        <> command "merge" (info mergeParser (progDesc "Merge 𝜑-programs into single one by merging their top level formations"))
-        <> command "match" (info matchParser (progDesc "Match 𝜑-program against provided pattern and build matched substitutions"))
-    )
-
-parserInfo :: ParserInfo Command
-parserInfo =
-  info
-    (commandParser <**> helper <**> simpleVersioner (showVersion version))
-    (fullDesc <> header "Phino - CLI Manipulator of 𝜑-Calculus Expressions")
-
 handler :: SomeException -> IO ()
 handler e = case fromException e of
   Just ExitSuccess -> pure () -- prevent printing error on --version etc.
@@ -528,333 +32,13 @@
         CmdMatch OptsMatch{_logLevel, _logLines} -> (_logLevel, _logLines)
    in setLogConfig level lns
 
-invalidCLIArguments :: String -> IO a
-invalidCLIArguments msg = throwIO (InvalidCLIArguments msg)
-
 runCLI :: [String] -> IO ()
 runCLI args = handle handler $ do
   cmd <- handleParseResult (execParserPure defaultPrefs parserInfo args)
   setLogger cmd
   case cmd of
-    CmdRewrite OptsRewrite{..} -> do
-      validateOpts
-      excluded <- validatedDispatches "hide" _hide
-      included <- validatedDispatches "show" _show
-      [loc] <- validatedDispatches "locator" [_locator]
-      [foc] <- validatedDispatches "focus" [_focus]
-      logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)
-      input <- readInput _inputFile
-      rules <- getRules _normalize _shuffle _rules
-      program <- parseProgram input _inputFormat
-      let listing = if null rules then const input else (\prog -> P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))
-          xmirCtx = XmirContext _omitListing _omitComments listing
-          printCtx = printProgCtx xmirCtx foc
-          canonize = if _canonize then C.canonize else id
-          exclude = (`F.exclude` excluded)
-          include = (`F.include` included)
-      rewrittens <- rewrite program rules (context loc printCtx) <&> canonize . exclude . include
-      let rewrittens' = if _sequence then rewrittens else [last rewrittens]
-      logDebug (printf "Printing rewritten 𝜑-program as %s" (show _outputFormat))
-      progs <- printRewrittens printCtx rewrittens'
-      output _targetFile progs
-      where
-        validateOpts :: IO ()
-        validateOpts = do
-          when
-            (_inPlace && isNothing _inputFile)
-            (invalidCLIArguments "The option --in-place requires an input file")
-          when
-            (_inPlace && isJust _targetFile)
-            (invalidCLIArguments "The options --in-place and --target cannot be used together")
-          when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
-          validateLatexOptions
-            _outputFormat
-            [(_nonumber, "nonumber"), (_compress, "compress")]
-            [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]
-            [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]
-          validateMust' _must
-          validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
-        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
-            logDebug (printf "The file '%s' was modified in-place" file)
-          (True, _, Nothing) ->
-            error "The option --in-place requires an input file"
-          (False, Just file, _) -> do
-            logDebug (printf "The option '--target' is specified, printing to '%s'..." file)
-            writeFile file prog
-            logDebug (printf "The command result was saved in '%s'" file)
-          (False, Nothing, _) -> do
-            logDebug "The option '--target' is not specified, printing to console..."
-            putStrLn prog
-        context :: Expression -> PrintProgramContext -> RewriteContext
-        context loc ctx =
-          RewriteContext
-            loc
-            _maxDepth
-            _maxCycles
-            _depthSensitive
-            buildTerm
-            _must
-            (saveStepFunc _stepsDir ctx)
-        printProgCtx :: XmirContext -> Expression -> PrintProgramContext
-        printProgCtx xmirCtx focus =
-          PrintProgCtx
-            _sugarType
-            _flat
-            _margin
-            xmirCtx
-            _nonumber
-            _compress
-            _sequence
-            (justMeetPopularity _meetPopularity)
-            (justMeetLength _meetLength)
-            focus
-            _expression
-            _label
-            _meetPrefix
-            _outputFormat
-    CmdDataize OptsDataize{..} -> do
-      validateOpts
-      excluded <- validatedDispatches "hide" _hide
-      included <- validatedDispatches "show" _show
-      [loc] <- validatedDispatches "locator" [_locator]
-      [foc] <- validatedDispatches "focus" [_focus]
-      input <- readInput _inputFile
-      prog <- parseProgram input _inputFormat
-      let printCtx = printProgCtx foc
-          canonize = if _canonize then C.canonize else id
-          exclude = (`F.exclude` excluded)
-          include = (`F.include` included)
-      (maybeBytes, chain) <- dataize (context loc prog printCtx)
-      when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain) >>= putStrLn)
-      unless _quiet (putStrLn (maybe (P.printExpression ExTermination) P.printBytes maybeBytes))
-      where
-        validateOpts :: IO ()
-        validateOpts = do
-          validateLatexOptions
-            _outputFormat
-            [(_nonumber, "nonumber"), (_compress, "compress")]
-            [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]
-            [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]
-          validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
-          when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
-        context :: Expression -> Program -> PrintProgramContext -> DataizeContext
-        context loc prog ctx =
-          DataizeContext
-            loc
-            prog
-            _maxDepth
-            _maxCycles
-            _depthSensitive
-            buildTerm
-            (saveStepFunc _stepsDir ctx)
-        printProgCtx :: Expression -> PrintProgramContext
-        printProgCtx focus =
-          PrintProgCtx
-            _sugarType
-            _flat
-            _margin
-            defaultXmirContext
-            _nonumber
-            _compress
-            _sequence
-            (justMeetPopularity _meetPopularity)
-            (justMeetLength _meetLength)
-            focus
-            _expression
-            _label
-            _meetPrefix
-            _outputFormat
-    CmdExplain OptsExplain{..} -> do
-      validateOpts
-      rules <- getRules _normalize _shuffle _rules
-      printOut _targetFile (explainRules rules)
-      where
-        validateOpts :: IO ()
-        validateOpts =
-          when
-            (null _rules && not _normalize)
-            (throwIO (InvalidCLIArguments "Either --rule or --normalize must be specified"))
-    CmdMerge OptsMerge{..} -> do
-      validateOpts
-      inputs' <- traverse (readInput . Just) _inputs
-      progs <- traverse (`parseProgram` _inputFormat) inputs'
-      prog <- merge progs
-      let listing = const (P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))
-          xmirCtx = XmirContext _omitListing _omitComments listing
-          printCtx = printProgCtx xmirCtx
-      prog' <- printProgram printCtx prog
-      printOut _targetFile prog'
-      where
-        validateOpts :: IO ()
-        validateOpts = do
-          when
-            (null _inputs)
-            (throwIO (InvalidCLIArguments "At least one input file must be specified for 'merge' command"))
-          validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] "Q"
-        printProgCtx :: XmirContext -> PrintProgramContext
-        printProgCtx xmirCtx =
-          PrintProgCtx
-            _sugarType
-            _flat
-            _margin
-            xmirCtx
-            False
-            False
-            False
-            (justMeetPopularity Nothing)
-            (justMeetLength Nothing)
-            ExGlobal
-            Nothing
-            Nothing
-            Nothing
-            _outputFormat
-    CmdMatch OptsMatch{..} -> do
-      input <- readInput _inputFile
-      prog <- parseProgram input PHI
-      if isNothing _pattern
-        then logDebug "The --pattern is not provided, no substitutions are built"
-        else do
-          ptn <- parseExpressionThrows (fromJust _pattern)
-          condition <- traverse parseConditionThrows _when
-          substs <- matchProgramWithRule prog (rule ptn condition) (RuleContext buildTerm)
-          if null substs
-            then logDebug "Provided pattern was not matched, no substitutions are built"
-            else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin))
-      where
-        rule :: Expression -> Maybe Y.Condition -> Y.Rule
-        rule ptn cnd = Y.Rule Nothing Nothing ptn ExGlobal cnd Nothing Nothing
-
-justMeetPopularity :: Maybe Int -> Int
-justMeetPopularity = fromMaybe defaultMeetPopularity
-
-justMeetLength :: Maybe Int -> Int
-justMeetLength = fromMaybe defaultMeetLength
-
--- Prepare saveStepFunc
-saveStepFunc :: Maybe FilePath -> PrintProgramContext -> SaveStepFunc
-saveStepFunc stepsDir ctx@PrintProgCtx{..} = saveStep stepsDir ioToExt (printProgram ctx)
-  where
-    ioToExt :: String
-    ioToExt
-      | _outputFormat == LATEX = "tex"
-      | otherwise = show _outputFormat
-
--- Validate given expressions as valid dispatches
-validatedDispatches :: String -> [String] -> IO [Expression]
-validatedDispatches opt = traverse (parseExpressionThrows >=> asDispatch)
-  where
-    asDispatch :: Expression -> IO Expression
-    asDispatch expr = asDispatch' expr
-      where
-        asDispatch' :: Expression -> IO Expression
-        asDispatch' ex@ExGlobal = pure ex
-        asDispatch' disp@(ExDispatch ex _) = asDispatch' ex >> pure disp
-        asDispatch' _ =
-          invalidCLIArguments
-            ( printf
-                "Only dispatch expression started with Φ (or Q) can be used in --%s, but given: %s"
-                opt
-                (P.printExpression' expr P.logPrintConfig)
-            )
-
--- Validate LaTeX options
-validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> [(Maybe Int, String)] -> IO ()
-validateLatexOptions LATEX _ _ _ = pure ()
-validateLatexOptions _ bools strings ints = do
-  let (bools', opts) = unzip bools
-      msg = "The --%s option can stay together with --output=latex only"
-      callback (maybe', opt) = when (isJust maybe') (invalidCLIArguments (printf msg opt))
-  validateBoolOpts (zip bools' (map (printf msg) opts))
-  forM_ strings callback
-  forM_ ints callback
-
--- Validate 'must' option
-validateMust' :: Must -> IO ()
-validateMust' must = for_ (validateMust must) invalidCLIArguments
-
--- Validate options for output to XMIR
-validateXmirOptions :: IOFormat -> [(Bool, String)] -> String -> IO ()
-validateXmirOptions XMIR _ focus = when (focus /= "Q") (invalidCLIArguments "Only --focus=Q is allowed to be used with --output=xmir")
-validateXmirOptions _ bools _ =
-  let (bools', opts) = unzip bools
-   in validateBoolOpts (zip bools' (map (printf "The --%s can be used only with --output=xmir") opts))
-
-validateBoolOpts :: [(Bool, String)] -> IO ()
-validateBoolOpts bools = forM_ bools (\(bool, msg) -> when bool (invalidCLIArguments msg))
-
--- Read input from file or stdin
-readInput :: Maybe FilePath -> IO String
-readInput inputFile' = case inputFile' of
-  Just pth -> do
-    logDebug (printf "Reading from file: '%s'" pth)
-    readFile =<< ensuredFile pth
-  Nothing -> do
-    logDebug "Reading from stdin"
-    getContents' `catch` (\(e :: SomeException) -> throwIO (CouldNotReadFromStdin (show e)))
-
--- Parse program from String input depending on input IO format
-parseProgram :: String -> IOFormat -> IO Program
-parseProgram phi PHI = parseProgramThrows phi
-parseProgram xmir XMIR = do
-  doc <- parseXMIRThrows xmir
-  xmirToPhi doc
-parseProgram _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format"
-
-printRewrittens :: PrintProgramContext -> [Rewritten] -> IO String
-printRewrittens ctx@PrintProgCtx{..} rewrittens
-  | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix)
-  | _focus == ExGlobal = mapM (printProgram ctx . fst) rewrittens <&> intercalate "\n"
-  | otherwise = mapM (\(prog, _) -> locatedExpression _focus prog >>= printExpression ctx) rewrittens <&> intercalate "\n"
-
-printExpression :: PrintProgramContext -> Expression -> IO String
-printExpression PrintProgCtx{..} ex = case _outputFormat of
-  PHI -> pure (P.printExpression' ex (_sugar, UNICODE, _line, _margin))
-  XMIR -> throwIO CouldNotPrintExpressionInXMIR
-  LATEX -> pure (expressionToLaTeX ex (LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix))
-
--- Convert
--- Convert program to corresponding String format
-printProgram :: PrintProgramContext -> Program -> IO String
-printProgram PrintProgCtx{..} prog = case _outputFormat of
-  PHI -> pure (P.printProgram' prog (_sugar, UNICODE, _line, _margin))
-  XMIR -> programToXMIR prog _xmirCtx <&> printXMIR
-  LATEX -> pure (programToLaTeX prog (LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix))
-
--- Get rules for rewriting depending on provided flags
-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 content
-printOut :: Maybe FilePath -> String -> IO ()
-printOut 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
-    logDebug (printf "The command result was saved in '%s'" file)
+    CmdRewrite opts -> runRewrite opts
+    CmdDataize opts -> runDataize opts
+    CmdExplain opts -> runExplain opts
+    CmdMerge opts -> runMerge opts
+    CmdMatch opts -> runMatch opts
diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs
new file mode 100644
--- /dev/null
+++ b/src/CLI/Helpers.hs
@@ -0,0 +1,118 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module CLI.Helpers where
+
+import AST
+import CLI.Types
+import CLI.Validators (invalidCLIArguments)
+import Control.Exception
+import Data.Functor ((<&>))
+import Data.List (intercalate)
+import Data.Maybe
+import Deps (SaveStepFunc, saveStep)
+import Encoding
+import LaTeX (LatexContext (..), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, programToLaTeX, rewrittensToLatex)
+import Locator (locatedExpression)
+import Logger
+import qualified Misc as M
+import Parser (parseProgramThrows)
+import qualified Printer as P
+import Rewriter (Rewrittens)
+import System.IO (getContents')
+import Text.Printf (printf)
+import XMIR (parseXMIRThrows, printXMIR, programToXMIR, xmirToPhi)
+import Yaml (normalizationRules)
+import qualified Yaml as Y
+
+justMeetPopularity :: Maybe Int -> Int
+justMeetPopularity = fromMaybe defaultMeetPopularity
+
+justMeetLength :: Maybe Int -> Int
+justMeetLength = fromMaybe defaultMeetLength
+
+-- Prepare saveStepFunc
+saveStepFunc :: Maybe FilePath -> PrintProgramContext -> SaveStepFunc
+saveStepFunc stepsDir ctx@PrintProgCtx{..} = saveStep stepsDir ioToExt (printProgram ctx)
+  where
+    ioToExt :: String
+    ioToExt
+      | _outputFormat == LATEX = "tex"
+      | otherwise = show _outputFormat
+
+-- Read input from file or stdin
+readInput :: Maybe FilePath -> IO String
+readInput inputFile' = case inputFile' of
+  Just pth -> do
+    logDebug (printf "Reading from file: '%s'" pth)
+    readFile =<< M.ensuredFile pth
+  Nothing -> do
+    logDebug "Reading from stdin"
+    getContents' `catch` (\(e :: SomeException) -> throwIO (CouldNotReadFromStdin (show e)))
+
+-- Parse program from String input depending on input IO format
+parseProgram :: String -> IOFormat -> IO Program
+parseProgram phi PHI = parseProgramThrows phi
+parseProgram xmir XMIR = parseXMIRThrows xmir >>= xmirToPhi
+parseProgram _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format"
+
+printRewrittens :: PrintProgramContext -> Rewrittens -> IO String
+printRewrittens ctx@PrintProgCtx{..} rewrittens@(chain, _)
+  | _outputFormat == LATEX && _sequence = rewrittensToLatex rewrittens (printCtxToLatexCtx ctx)
+  | _focus == ExGlobal = mapM (printProgram ctx . fst) chain <&> intercalate "\n"
+  | otherwise = mapM (\(prog, _) -> locatedExpression _focus prog >>= printExpression ctx) chain <&> intercalate "\n"
+
+printExpression :: PrintProgramContext -> Expression -> IO String
+printExpression ctx@PrintProgCtx{..} ex = case _outputFormat of
+  PHI -> pure (P.printExpression' ex (_sugar, UNICODE, _line, _margin))
+  XMIR -> throwIO CouldNotPrintExpressionInXMIR
+  LATEX -> pure (expressionToLaTeX ex (printCtxToLatexCtx ctx))
+
+-- Convert
+-- Convert program to corresponding String format
+printProgram :: PrintProgramContext -> Program -> IO String
+printProgram ctx@PrintProgCtx{..} prog = case _outputFormat of
+  PHI -> pure (P.printProgram' prog (_sugar, UNICODE, _line, _margin))
+  XMIR -> programToXMIR prog _xmirCtx <&> printXMIR
+  LATEX -> pure (programToLaTeX prog (printCtxToLatexCtx ctx))
+
+printCtxToLatexCtx :: PrintProgramContext -> LatexContext
+printCtxToLatexCtx PrintProgCtx{..} =
+  LatexContext _sugar _line _margin _nonumber _compress _meetPopularity _meetLength _focus _expression _label _meetPrefix
+
+-- Get rules for rewriting depending on provided flags
+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 M.ensuredFile rules
+            mapM Y.yamlRule yamls
+  if shuffle
+    then do
+      logDebug "The --shuffle option is provided, rules are used in random order"
+      M.shuffle ordered
+    else pure ordered
+
+-- Output content
+printOut :: Maybe FilePath -> String -> IO ()
+printOut 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
+    logDebug (printf "The command result was saved in '%s'" file)
diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs
new file mode 100644
--- /dev/null
+++ b/src/CLI/Parsers.hs
@@ -0,0 +1,343 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module CLI.Parsers where
+
+import CLI.Types
+import Data.Char (toLower, toUpper)
+import Data.List (intercalate)
+import Data.Version (showVersion)
+import LaTeX (defaultMeetLength, defaultMeetPopularity)
+import Lining (LineFormat (..))
+import Logger
+import Margin (defaultMargin)
+import Must
+import Options.Applicative
+import Paths_phino (version)
+import Sugar (SugarType (..))
+import Text.Printf (printf)
+
+validateIntOption :: (Int -> Bool) -> String -> Int -> ReadM Int
+validateIntOption cmp msg num
+  | cmp num = return num
+  | otherwise = readerError msg
+
+optLogLevel :: Parser LogLevel
+optLogLevel =
+  option
+    parseLogLevel
+    ( long "log-level"
+        <> metavar "LEVEL"
+        <> help ("Log level (" <> intercalate ", " (map show [DEBUG, ERROR, NONE]) <> ")")
+        <> value ERROR
+        <> showDefault
+    )
+  where
+    parseLogLevel :: ReadM LogLevel
+    parseLogLevel = eitherReader $ \lvl -> case map toUpper lvl of
+      "DEBUG" -> Right DEBUG
+      "ERROR" -> Right ERROR
+      "ERR" -> Right ERROR
+      "NONE" -> Right NONE
+      _ -> Left $ "unknown log-level: " <> lvl
+
+optLogLines :: Parser Int
+optLogLines =
+  option
+    (auto >>= validateIntOption (>= -1) "--log-lines must be >= -1")
+    (long "log-lines" <> metavar "LINES" <> help "Amount of lines printed to console per each log operation (0 - print nothing, -1 - no limits)" <> value 25 <> showDefault)
+
+optRule :: Parser [FilePath]
+optRule = many (strOption (long "rule" <> metavar "[FILE]" <> help "Path to custom rule"))
+
+optInputFormat :: Parser IOFormat
+optInputFormat = option (parseIOFormat "input") (long "input" <> metavar "FORMAT" <> help "Program input format (phi, xmir)" <> value PHI <> showDefault)
+
+parseIOFormat :: String -> ReadM IOFormat
+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')
+
+optOutputFormat :: Parser IOFormat
+optOutputFormat =
+  option
+    (parseIOFormat "output")
+    (long "output" <> metavar "FORMAT" <> help (printf "Result and intermediate (see %s option(s)) programs output format (phi, xmir, latex)" _intermediateOptions) <> value PHI <> showDefault)
+
+argInputFile :: Parser (Maybe FilePath)
+argInputFile = optional (argument str (metavar "FILE" <> help "Path to input file"))
+
+optMaxDepth :: Parser Int
+optMaxDepth =
+  option
+    (auto >>= validateIntOption (> 0) "--max-depth must be positive")
+    (long "max-depth" <> metavar "DEPTH" <> help "Maximum number of rewriting iterations per rule" <> value 25 <> showDefault)
+
+optMaxCycles :: Parser Int
+optMaxCycles =
+  option
+    (auto >>= validateIntOption (> 0) "--max-cycles must be positive")
+    (long "max-cycles" <> metavar "CYCLES" <> help "Maximum number of rewriting cycles across all rules" <> value 25 <> showDefault)
+
+optMargin :: Parser Int
+optMargin =
+  option
+    (auto >>= validateIntOption (> 0) "--margin must be positive")
+    (long "margin" <> help "The maximum right margin for the printed 𝜑-programs or 𝜑-expressions" <> value defaultMargin <> showDefault)
+
+optMeetPopularity :: Parser (Maybe Int)
+optMeetPopularity =
+  optional
+    ( option
+        ( auto
+            >>= validateIntOption (> 0) "--meet-popularity must be positive"
+            >>= validateIntOption (<= 100) "--meet-popularity must be <= 100"
+        )
+        ( long "meet-popularity"
+            <> metavar "PERCENTAGE"
+            <> help (printf "The minimum popularity of an expression in order to be suitable for \\phiMeet{}, in percentage (default: %d)" defaultMeetPopularity)
+        )
+    )
+
+optMeetLength :: Parser (Maybe Int)
+optMeetLength =
+  optional
+    ( option
+        (auto >>= validateIntOption (> 0) "--meet-length must be positive")
+        ( long "meet-length"
+            <> metavar "NODES"
+            <> help (printf "The minimum length of an expression that fits into \\phiMeet{}, in AST nodes (default: %d)" defaultMeetLength)
+        )
+    )
+
+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)")
+
+optNonumber :: Parser Bool
+optNonumber = switch (long "nonumber" <> help "Turn off equation auto numbering in LaTeX rendering (see --output option)")
+
+optSequence :: Parser Bool
+optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-programs concatenated with EOL")
+
+optCanonize :: Parser Bool
+optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with F1, F2, etc.")
+
+optExpression :: Parser (Maybe String)
+optExpression = optional (strOption (long "expression" <> metavar "NAME" <> help "Name for 'phiExpression' element when rendering to LaTeX (see --output option)"))
+
+optLabel :: Parser (Maybe String)
+optLabel = optional (strOption (long "label" <> metavar "NAME" <> help "Name for 'label' element when rendering to LaTeX (see --output option)"))
+
+optMeetPrefix :: Parser (Maybe String)
+optMeetPrefix = optional (strOption (long "meet-prefix" <> metavar "PREFIX" <> help "Prefix to be inserted before index in \\phiMeet{} and \\phiAgain{} LaTeX functions, e.g. \\phiMeet{foo:1}"))
+
+optHide :: Parser [String]
+optHide =
+  many
+    ( strOption
+        ( long "hide"
+            <> metavar "FQN"
+            <> help "Location of object to exclude from result and intermediate programs after rewriting. Must be a valid dispatch expression; e.g. Q.org.eolang"
+        )
+    )
+
+optShow :: Parser [String]
+optShow =
+  many
+    ( strOption
+        ( long "show"
+            <> metavar "FQN"
+            <> help
+              "Location of object to include to result and intermediate programs after rewriting. \
+              \Must be a valid dispatch expression; e.g. Q.org.eolang. Unlike --hide, can be used only once"
+        )
+    )
+
+optLocator :: Parser String
+optLocator = strOption (long "locator" <> metavar "FQN" <> help "Location of object to dataize. Must be a valid dispatch expression; e.g. Q.foo.bar" <> value "Q" <> showDefault)
+
+optFocus :: Parser String
+optFocus =
+  strOption
+    ( long "focus"
+        <> metavar "FQN"
+        <> help "Location of only object to be printed in entire program. Must be a valid dispatch expression; e.g. Q.foo.bar"
+        <> value "Q"
+        <> showDefault
+    )
+
+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"))
+
+optStepsDir :: Parser (Maybe FilePath)
+optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing"))
+
+optShuffle :: Parser Bool
+optShuffle = switch (long "shuffle" <> help "Shuffle rules before applying")
+
+optSugar :: Parser SugarType
+optSugar = flag SALTY SWEET (long "sweet" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs using syntax sugar" _intermediateOptions))
+
+optSugar' :: Parser SugarType
+optSugar' = flag SALTY SWEET (long "sweet" <> help "Print result 𝜑-program using syntax sugar")
+
+optLineFormat :: Parser LineFormat
+optLineFormat = flag MULTILINE SINGLELINE (long "flat" <> help (printf "Print result and intermediate (see %s option(s)) 𝜑-programs in one line" _intermediateOptions))
+
+optLineFormat' :: Parser LineFormat
+optLineFormat' = flag MULTILINE SINGLELINE (long "flat" <> help "Print result 𝜑-program in one line")
+
+optOmitListing :: Parser Bool
+optOmitListing = switch (long "omit-listing" <> help "Omit full program listing in XMIR output")
+
+optOmitComments :: Parser Bool
+optOmitComments = switch (long "omit-comments" <> help "Omit comments in XMIR output")
+
+optCompress :: Parser Bool
+optCompress = switch (long "compress" <> help "Compress expressions in LaTeX output using \\phiMeet{} and \\phiAgain{} functions")
+
+_intermediateOptions :: String
+_intermediateOptions = intercalate ", " ["--sequence", "--steps-dir"]
+
+explainParser :: Parser Command
+explainParser =
+  CmdExplain
+    <$> ( OptsExplain
+            <$> optLogLevel
+            <*> optLogLines
+            <*> optRule
+            <*> optNormalize
+            <*> optShuffle
+            <*> optTarget
+        )
+
+dataizeParser :: Parser Command
+dataizeParser =
+  CmdDataize
+    <$> ( OptsDataize
+            <$> optLogLevel
+            <*> optLogLines
+            <*> optInputFormat
+            <*> optOutputFormat
+            <*> optSugar
+            <*> optLineFormat
+            <*> optOmitListing
+            <*> optOmitComments
+            <*> optNonumber
+            <*> optSequence
+            <*> optCanonize
+            <*> optDepthSensitive
+            <*> switch (long "quiet" <> help "Don't print the result of dataization")
+            <*> optCompress
+            <*> optMaxDepth
+            <*> optMaxCycles
+            <*> optMargin
+            <*> optMeetPopularity
+            <*> optMeetLength
+            <*> optHide
+            <*> optShow
+            <*> optLocator
+            <*> optFocus
+            <*> optExpression
+            <*> optLabel
+            <*> optMeetPrefix
+            <*> optStepsDir
+            <*> argInputFile
+        )
+
+rewriteParser :: Parser Command
+rewriteParser =
+  CmdRewrite
+    <$> ( OptsRewrite
+            <$> optLogLevel
+            <*> optLogLines
+            <*> optInputFormat
+            <*> optOutputFormat
+            <*> optSugar
+            <*> optLineFormat
+            <*> 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
+              )
+            <*> optNormalize
+            <*> optShuffle
+            <*> optOmitListing
+            <*> optOmitComments
+            <*> optDepthSensitive
+            <*> optNonumber
+            <*> switch (long "in-place" <> help "Edit file in-place instead of printing to output")
+            <*> optSequence
+            <*> optCanonize
+            <*> optCompress
+            <*> optMaxDepth
+            <*> optMaxCycles
+            <*> optMargin
+            <*> optMeetPopularity
+            <*> optMeetLength
+            <*> optRule
+            <*> optHide
+            <*> optShow
+            <*> optLocator
+            <*> optFocus
+            <*> optExpression
+            <*> optLabel
+            <*> optMeetPrefix
+            <*> optTarget
+            <*> optStepsDir
+            <*> argInputFile
+        )
+
+mergeParser :: Parser Command
+mergeParser =
+  CmdMerge
+    <$> ( OptsMerge
+            <$> optLogLevel
+            <*> optLogLines
+            <*> optInputFormat
+            <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help (printf "Result program output format (phi, xmir, latex)") <> value PHI <> showDefault)
+            <*> optSugar'
+            <*> optLineFormat'
+            <*> optOmitListing
+            <*> optOmitComments
+            <*> optMargin
+            <*> optTarget
+            <*> many (argument str (metavar "[FILE]" <> help "Paths to input files"))
+        )
+
+matchParser :: Parser Command
+matchParser =
+  CmdMatch
+    <$> ( OptsMatch
+            <$> optLogLevel
+            <*> optLogLines
+            <*> optSugar
+            <*> optLineFormat
+            <*> optional (strOption (long "pattern" <> metavar "EXPRESSION" <> help "Pattern expression to match against"))
+            <*> optional (strOption (long "when" <> metavar "CONDITION" <> help "Predicate for matched substitutions"))
+            <*> argInputFile
+        )
+
+commandParser :: Parser Command
+commandParser =
+  hsubparser
+    ( 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"))
+        <> command "merge" (info mergeParser (progDesc "Merge 𝜑-programs into single one by merging their top level formations"))
+        <> command "match" (info matchParser (progDesc "Match 𝜑-program against provided pattern and build matched substitutions"))
+    )
+
+parserInfo :: ParserInfo Command
+parserInfo =
+  info
+    (commandParser <**> helper <**> simpleVersioner (showVersion version))
+    (fullDesc <> header "Phino - CLI Manipulator of 𝜑-Calculus Expressions")
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
new file mode 100644
--- /dev/null
+++ b/src/CLI/Runners.hs
@@ -0,0 +1,208 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module CLI.Runners where
+
+import AST
+import CLI.Helpers
+import CLI.Types
+import CLI.Validators
+import qualified Canonizer as C
+import Condition (parseConditionThrows)
+import Control.Exception
+import Control.Monad (unless, when)
+import Data.Maybe (fromJust, isJust, isNothing)
+import Dataize
+import Encoding
+import qualified Filter as F
+import Functions (buildTerm)
+import LaTeX (explainRules)
+import Logger
+import Margin (defaultMargin)
+import Merge (merge)
+import Parser (parseExpressionThrows)
+import qualified Printer as P
+import Rewriter
+import Rule (RuleContext (..), matchProgramWithRule)
+import Text.Printf (printf)
+import XMIR
+import qualified Yaml as Y
+
+runRewrite :: OptsRewrite -> IO ()
+runRewrite OptsRewrite{..} = do
+  validateOpts
+  excluded <- validatedDispatches "hide" _hide
+  included <- validatedDispatches "show" _show
+  [loc] <- validatedDispatches "locator" [_locator]
+  [foc] <- validatedDispatches "focus" [_focus]
+  logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)
+  input <- readInput _inputFile
+  rules <- getRules _normalize _shuffle _rules
+  program <- parseProgram input _inputFormat
+  let listing = if null rules then const input else (\prog -> P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))
+      xmirCtx = XmirContext _omitListing _omitComments listing
+      printCtx = printProgCtx xmirCtx foc
+      canonize = if _canonize then C.canonize else id
+      exclude = (`F.exclude` excluded)
+      include = (`F.include` included)
+  (rewrittens, exceeded) <- rewrite program rules (context loc printCtx)
+  let rewrittens' = canonize $ exclude $ include (if _sequence then rewrittens else [last rewrittens])
+  logDebug (printf "Printing rewritten 𝜑-program as %s" (show _outputFormat))
+  progs <- printRewrittens printCtx (rewrittens', exceeded)
+  output _targetFile progs
+  where
+    validateOpts :: IO ()
+    validateOpts = do
+      when (_inPlace && isNothing _inputFile) (invalidCLIArguments "The option --in-place requires an input file")
+      when (_inPlace && isJust _targetFile) (invalidCLIArguments "The options --in-place and --target cannot be used together")
+      when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
+      validateLatexOptions
+        _outputFormat
+        [(_nonumber, "nonumber"), (_compress, "compress")]
+        [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]
+        [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]
+      validateMust' _must
+      validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
+    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
+        logDebug (printf "The file '%s' was modified in-place" file)
+      (True, _, Nothing) ->
+        error "The option --in-place requires an input file"
+      (False, Just file, _) -> do
+        logDebug (printf "The option '--target' is specified, printing to '%s'..." file)
+        writeFile file prog
+        logDebug (printf "The command result was saved in '%s'" file)
+      (False, Nothing, _) -> do
+        logDebug "The option '--target' is not specified, printing to console..."
+        putStrLn prog
+    context :: Expression -> PrintProgramContext -> RewriteContext
+    context loc ctx = RewriteContext loc _maxDepth _maxCycles _depthSensitive buildTerm _must (saveStepFunc _stepsDir ctx)
+    printProgCtx :: XmirContext -> Expression -> PrintProgramContext
+    printProgCtx xmirCtx focus =
+      PrintProgCtx
+        _sugarType
+        _flat
+        _margin
+        xmirCtx
+        _nonumber
+        _compress
+        _sequence
+        (justMeetPopularity _meetPopularity)
+        (justMeetLength _meetLength)
+        focus
+        _expression
+        _label
+        _meetPrefix
+        _outputFormat
+
+runDataize :: OptsDataize -> IO ()
+runDataize OptsDataize{..} = do
+  validateOpts
+  excluded <- validatedDispatches "hide" _hide
+  included <- validatedDispatches "show" _show
+  [loc] <- validatedDispatches "locator" [_locator]
+  [foc] <- validatedDispatches "focus" [_focus]
+  input <- readInput _inputFile
+  prog <- parseProgram input _inputFormat
+  let printCtx = printProgCtx foc
+      canonize = if _canonize then C.canonize else id
+      exclude = (`F.exclude` excluded)
+      include = (`F.include` included)
+  (maybeBytes, chain) <- dataize (context loc prog printCtx)
+  when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain, False) >>= putStrLn)
+  unless _quiet (putStrLn (maybe (P.printExpression ExTermination) P.printBytes maybeBytes))
+  where
+    validateOpts :: IO ()
+    validateOpts = do
+      validateLatexOptions
+        _outputFormat
+        [(_nonumber, "nonumber"), (_compress, "compress")]
+        [(_expression, "expression"), (_label, "label"), (_meetPrefix, "meet-prefix")]
+        [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]
+      validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus
+      when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")
+    context :: Expression -> Program -> PrintProgramContext -> DataizeContext
+    context loc prog ctx = DataizeContext loc prog _maxDepth _maxCycles _depthSensitive buildTerm (saveStepFunc _stepsDir ctx)
+    printProgCtx :: Expression -> PrintProgramContext
+    printProgCtx focus =
+      PrintProgCtx
+        _sugarType
+        _flat
+        _margin
+        defaultXmirContext
+        _nonumber
+        _compress
+        _sequence
+        (justMeetPopularity _meetPopularity)
+        (justMeetLength _meetLength)
+        focus
+        _expression
+        _label
+        _meetPrefix
+        _outputFormat
+
+runExplain :: OptsExplain -> IO ()
+runExplain OptsExplain{..} = do
+  validateOpts
+  rules <- getRules _normalize _shuffle _rules
+  printOut _targetFile (explainRules rules)
+  where
+    validateOpts :: IO ()
+    validateOpts = when (null _rules && not _normalize) (invalidCLIArguments "Either --rule or --normalize must be specified")
+
+runMerge :: OptsMerge -> IO ()
+runMerge OptsMerge{..} = do
+  validateOpts
+  inputs' <- traverse (readInput . Just) _inputs
+  progs <- traverse (`parseProgram` _inputFormat) inputs'
+  prog <- merge progs
+  let listing = const (P.printProgram' prog (_sugarType, UNICODE, _flat, _margin))
+      xmirCtx = XmirContext _omitListing _omitComments listing
+      printCtx = printProgCtx xmirCtx
+  prog' <- printProgram printCtx prog
+  printOut _targetFile prog'
+  where
+    validateOpts :: IO ()
+    validateOpts = do
+      when (null _inputs) (throwIO (InvalidCLIArguments "At least one input file must be specified for 'merge' command"))
+      validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] "Q"
+    printProgCtx :: XmirContext -> PrintProgramContext
+    printProgCtx xmirCtx =
+      PrintProgCtx
+        _sugarType
+        _flat
+        _margin
+        xmirCtx
+        False
+        False
+        False
+        (justMeetPopularity Nothing)
+        (justMeetLength Nothing)
+        ExGlobal
+        Nothing
+        Nothing
+        Nothing
+        _outputFormat
+
+runMatch :: OptsMatch -> IO ()
+runMatch OptsMatch{..} = do
+  input <- readInput _inputFile
+  prog <- parseProgram input PHI
+  if isNothing _pattern
+    then logDebug "The --pattern is not provided, no substitutions are built"
+    else do
+      ptn <- parseExpressionThrows (fromJust _pattern)
+      condition <- traverse parseConditionThrows _when
+      substs <- matchProgramWithRule prog (rule ptn condition) (RuleContext buildTerm)
+      if null substs
+        then logDebug "Provided pattern was not matched, no substitutions are built"
+        else putStrLn (P.printSubsts' substs (_sugarType, UNICODE, _flat, defaultMargin))
+  where
+    rule :: Expression -> Maybe Y.Condition -> Y.Rule
+    rule ptn cnd = Y.Rule Nothing Nothing ptn ExGlobal cnd Nothing Nothing
diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/CLI/Types.hs
@@ -0,0 +1,161 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module CLI.Types where
+
+import AST
+import Control.Exception (Exception)
+import Lining (LineFormat)
+import Logger (LogLevel)
+import Must (Must)
+import Sugar (SugarType)
+import Text.Printf (printf)
+import XMIR (XmirContext)
+
+data PrintProgramContext = PrintProgCtx
+  { _sugar :: SugarType
+  , _line :: LineFormat
+  , _margin :: Int
+  , _xmirCtx :: XmirContext
+  , _nonumber :: Bool
+  , _compress :: Bool
+  , _sequence :: Bool
+  , _meetPopularity :: Int
+  , _meetLength :: Int
+  , _focus :: Expression
+  , _expression :: Maybe String
+  , _label :: Maybe String
+  , _meetPrefix :: Maybe String
+  , _outputFormat :: IOFormat
+  }
+
+data CmdException
+  = InvalidCLIArguments String
+  | CouldNotReadFromStdin String
+  | CouldNotDataize
+  | CouldNotPrintExpressionInXMIR
+  deriving (Exception)
+
+instance Show CmdException where
+  show (InvalidCLIArguments msg) = printf "Invalid set of arguments: %s" msg
+  show (CouldNotReadFromStdin msg) = printf "Could not read input from stdin\nReason: %s" msg
+  show CouldNotDataize = "Could not dataize given program"
+  show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only program printing is allowed"
+
+data Command
+  = CmdRewrite OptsRewrite
+  | CmdDataize OptsDataize
+  | CmdExplain OptsExplain
+  | CmdMerge OptsMerge
+  | CmdMatch OptsMatch
+
+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
+  , _logLines :: Int
+  , _inputFormat :: IOFormat
+  , _outputFormat :: IOFormat
+  , _sugarType :: SugarType
+  , _flat :: LineFormat
+  , _omitListing :: Bool
+  , _omitComments :: Bool
+  , _nonumber :: Bool
+  , _sequence :: Bool
+  , _canonize :: Bool
+  , _depthSensitive :: Bool
+  , _quiet :: Bool
+  , _compress :: Bool
+  , _maxDepth :: Int
+  , _maxCycles :: Int
+  , _margin :: Int
+  , _meetPopularity :: Maybe Int
+  , _meetLength :: Maybe Int
+  , _hide :: [String]
+  , _show :: [String]
+  , _locator :: String
+  , _focus :: String
+  , _expression :: Maybe String
+  , _label :: Maybe String
+  , _meetPrefix :: Maybe String
+  , _stepsDir :: Maybe FilePath
+  , _inputFile :: Maybe FilePath
+  }
+
+data OptsExplain = OptsExplain
+  { _logLevel :: LogLevel
+  , _logLines :: Int
+  , _rules :: [FilePath]
+  , _normalize :: Bool
+  , _shuffle :: Bool
+  , _targetFile :: Maybe FilePath
+  }
+
+data OptsRewrite = OptsRewrite
+  { _logLevel :: LogLevel
+  , _logLines :: Int
+  , _inputFormat :: IOFormat
+  , _outputFormat :: IOFormat
+  , _sugarType :: SugarType
+  , _flat :: LineFormat
+  , _must :: Must
+  , _normalize :: Bool
+  , _shuffle :: Bool
+  , _omitListing :: Bool
+  , _omitComments :: Bool
+  , _depthSensitive :: Bool
+  , _nonumber :: Bool
+  , _inPlace :: Bool
+  , _sequence :: Bool
+  , _canonize :: Bool
+  , _compress :: Bool
+  , _maxDepth :: Int
+  , _maxCycles :: Int
+  , _margin :: Int
+  , _meetPopularity :: Maybe Int
+  , _meetLength :: Maybe Int
+  , _rules :: [FilePath]
+  , _hide :: [String]
+  , _show :: [String]
+  , _locator :: String
+  , _focus :: String
+  , _expression :: Maybe String
+  , _label :: Maybe String
+  , _meetPrefix :: Maybe String
+  , _targetFile :: Maybe FilePath
+  , _stepsDir :: Maybe FilePath
+  , _inputFile :: Maybe FilePath
+  }
+
+data OptsMerge = OptsMerge
+  { _logLevel :: LogLevel
+  , _logLines :: Int
+  , _inputFormat :: IOFormat
+  , _outputFormat :: IOFormat
+  , _sugarType :: SugarType
+  , _flat :: LineFormat
+  , _omitListing :: Bool
+  , _omitComments :: Bool
+  , _margin :: Int
+  , _targetFile :: Maybe FilePath
+  , _inputs :: [FilePath]
+  }
+
+data OptsMatch = OptsMatch
+  { _logLevel :: LogLevel
+  , _logLines :: Int
+  , _sugarType :: SugarType
+  , _flat :: LineFormat
+  , _pattern :: Maybe String
+  , _when :: Maybe String
+  , _inputFile :: Maybe FilePath
+  }
diff --git a/src/CLI/Validators.hs b/src/CLI/Validators.hs
new file mode 100644
--- /dev/null
+++ b/src/CLI/Validators.hs
@@ -0,0 +1,61 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module CLI.Validators where
+
+import AST
+import CLI.Types
+import Control.Exception
+import Control.Monad (forM_, when, (>=>))
+import Data.Foldable (for_)
+import Data.Maybe (isJust)
+import Must
+import Parser (parseExpressionThrows)
+import Printer
+import Text.Printf (printf)
+
+invalidCLIArguments :: String -> IO a
+invalidCLIArguments msg = throwIO (InvalidCLIArguments msg)
+
+-- Validate given expressions as valid dispatches
+validatedDispatches :: String -> [String] -> IO [Expression]
+validatedDispatches opt = traverse (parseExpressionThrows >=> asDispatch)
+  where
+    asDispatch :: Expression -> IO Expression
+    asDispatch expr = asDispatch' expr
+      where
+        asDispatch' :: Expression -> IO Expression
+        asDispatch' ex@ExGlobal = pure ex
+        asDispatch' disp@(ExDispatch ex _) = asDispatch' ex >> pure disp
+        asDispatch' _ =
+          invalidCLIArguments
+            ( printf
+                "Only dispatch expression started with Φ (or Q) can be used in --%s, but given: %s"
+                opt
+                (printExpression' expr logPrintConfig)
+            )
+
+-- Validate LaTeX options
+validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> [(Maybe Int, String)] -> IO ()
+validateLatexOptions LATEX _ _ _ = pure ()
+validateLatexOptions _ bools strings ints = do
+  let (bools', opts) = unzip bools
+      msg = "The --%s option can stay together with --output=latex only"
+      callback (maybe', opt) = when (isJust maybe') (invalidCLIArguments (printf msg opt))
+  validateBoolOpts (zip bools' (map (printf msg) opts))
+  forM_ strings callback
+  forM_ ints callback
+
+-- Validate 'must' option
+validateMust' :: Must -> IO ()
+validateMust' must = for_ (validateMust must) invalidCLIArguments
+
+-- Validate options for output to XMIR
+validateXmirOptions :: IOFormat -> [(Bool, String)] -> String -> IO ()
+validateXmirOptions XMIR _ focus = when (focus /= "Q") (invalidCLIArguments "Only --focus=Q is allowed to be used with --output=xmir")
+validateXmirOptions _ bools _ =
+  let (bools', opts) = unzip bools
+   in validateBoolOpts (zip bools' (map (printf "The --%s can be used only with --output=xmir") opts))
+
+validateBoolOpts :: [(Bool, String)] -> IO ()
+validateBoolOpts bools = forM_ bools (\(bool, msg) -> when bool (invalidCLIArguments msg))
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# OPTIONS_GHC -Wno-partial-fields -Wno-name-shadowing #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
@@ -11,6 +12,7 @@
 import AST
 import Data.Maybe (isJust)
 import Misc
+import qualified Yaml as Y
 
 data LCB = LCB | BIG_LCB
   deriving (Eq, Show)
@@ -48,7 +50,7 @@
 data XI = XI | DOLLAR
   deriving (Eq, Show)
 
-data LAMBDA = LAMBDA
+data LAMBDA = LAMBDA | LAMBDA'
   deriving (Eq, Show)
 
 data GLOBAL = Φ | Q
@@ -63,6 +65,9 @@
 data EOL = EOL | NO_EOL
   deriving (Eq, Show)
 
+data DOTS = DOTS | DOTS'
+  deriving (Eq, Show)
+
 data BYTES
   = BT_EMPTY
   | BT_ONE String
@@ -70,19 +75,26 @@
   | BT_META META
   deriving (Eq, Show)
 
-data META
-  = MT_EXPRESSION {rest :: String}
-  | MT_EXPRESSION' {rest :: String}
-  | MT_ATTRIBUTE {rest :: String}
-  | MT_ATTRIBUTE' {rest :: String}
-  | MT_BINDING {rest :: String}
-  | MT_BINDING' {rest :: String}
-  | MT_BYTES {rest :: String}
-  | MT_BYTES' {rest :: String}
-  | MT_TAIL {rest :: String}
-  | MT_FUNCTION {rest :: String}
+data META_HEAD
+  = E -- 𝑒
+  | E' -- e
+  | A -- a
+  | TAU -- 𝜏
+  | TAU' -- \tau
+  | B -- 𝐵
+  | B' -- B
+  | D -- δ
+  | D' -- d
+  | TAIL -- t
+  | F -- F
   deriving (Eq, Show)
 
+data EXCLAMATION = EXCL | NO_EXCL
+  deriving (Eq, Show)
+
+data META = META {excl :: EXCLAMATION, hd :: META_HEAD, rest :: String}
+  deriving (Eq, Show)
+
 data TAB
   = TAB {indent :: Int}
   | TAB'
@@ -162,14 +174,92 @@
   | AT_LAMBDA {lambda :: LAMBDA}
   | AT_DELTA {delta :: DELTA}
   | AT_META {meta :: META}
+  | AT_REST {dots :: DOTS}
   deriving (Eq, Show)
 
+data BELONGING
+  = IN
+  | NOT_IN
+  deriving (Eq, Show)
+
+data SET
+  = ST_BINDING {binding :: BINDING}
+  | ST_ATTRIBUTES {attrs :: [ATTRIBUTE]}
+  deriving (Eq, Show)
+
+data LOGIC_OPERATOR
+  = AND
+  | OR
+  deriving (Eq, Show)
+
+data EQUAL
+  = EQUAL
+  | NOT_EQUAL
+  deriving (Eq, Show)
+
+data NUMBER
+  = ORDINAL {attr :: ATTRIBUTE}
+  | LENGTH {binding :: BINDING}
+  | LITERAL {num :: Int}
+  deriving (Eq, Show)
+
+data COMPARABLE
+  = CMP_ATTR {attr :: ATTRIBUTE}
+  | CMP_EXPR {expr :: EXPRESSION}
+  | CMP_NUM {num :: NUMBER}
+  deriving (Eq, Show)
+
+data CONDITION
+  = CO_EMPTY
+  | CO_BELONGS {attr :: ATTRIBUTE, belongs :: BELONGING, set :: SET}
+  | CO_LOGIC {conditions :: [CONDITION], operator :: LOGIC_OPERATOR}
+  | CO_NF {expr :: EXPRESSION}
+  | CO_NOT {condition :: CONDITION}
+  | CO_COMPARE {left :: COMPARABLE, equal :: EQUAL, right :: COMPARABLE}
+  | CO_MATCHES {regex :: String, expr :: EXPRESSION}
+  | CO_PART_OF {expr :: EXPRESSION, binding :: BINDING}
+  deriving (Eq, Show)
+
+data EXTRA_ARG
+  = ARG_EXPR {expr :: EXPRESSION}
+  | ARG_ATTR {attr :: ATTRIBUTE}
+  | ARG_BINDING {binding :: BINDING}
+  | ARG_BYTES {bytes :: BYTES}
+  deriving (Eq, Show)
+
+data EXTRA = EXTRA {meta :: EXTRA_ARG, func :: String, args :: [EXTRA_ARG]}
+  deriving (Eq, Show)
+
 programToCST :: Program -> PROGRAM
-programToCST prog = toCST prog (0, EOL)
+programToCST = toCST'
 
 expressionToCST :: Expression -> EXPRESSION
-expressionToCST ex = toCST ex (0, EOL)
+expressionToCST = toCST'
 
+attributeToCST :: Attribute -> ATTRIBUTE
+attributeToCST = toCST'
+
+bindingsToCST :: [Binding] -> BINDING
+bindingsToCST = toCST'
+
+conditionToCST :: Y.Condition -> CONDITION
+conditionToCST = toCST'
+
+comparableToCST :: Y.Comparable -> COMPARABLE
+comparableToCST = toCST'
+
+numberToCST :: Y.Number -> NUMBER
+numberToCST = toCST'
+
+extraToCST :: Y.Extra -> EXTRA
+extraToCST = toCST'
+
+toCST' :: ToCST a b => a -> b
+toCST' = (`toCST` (0, EOL))
+
+metaTail :: String -> String
+metaTail = tail
+
 -- This class is used to convert AST to CST
 -- CST is created with sugar and unicode
 -- All further transformations must consider that
@@ -182,8 +272,8 @@
 instance ToCST Expression EXPRESSION where
   toCST ExGlobal _ = EX_GLOBAL Φ
   toCST ExThis _ = EX_XI XI
-  toCST (ExMeta mt) _ = EX_META (MT_EXPRESSION (tail mt))
-  toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (MT_TAIL (tail mt))
+  toCST (ExMeta mt) _ = EX_META (META NO_EXCL E (metaTail mt))
+  toCST (ExMetaTail expr mt) ctx = EX_META_TAIL (toCST expr ctx) (META EXCL TAIL (metaTail mt))
   toCST ExTermination _ = EX_TERMINATION DEAD
   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)
   toCST (ExPhiAgain prefix idx expr) ctx = EX_PHI_AGAIN prefix idx (toCST expr ctx)
@@ -304,12 +394,12 @@
 
 instance ToCST [Binding] BINDING where
   toCST [] (tabs, _) = BI_EMPTY (TAB tabs)
-  toCST (BiMeta mt : bds) ctx@(tabs, _) = BI_META (MT_BINDING (tail mt)) (toCST bds ctx) (TAB tabs)
+  toCST (BiMeta mt : bds) ctx@(tabs, _) = BI_META (META NO_EXCL B (metaTail mt)) (toCST bds ctx) (TAB tabs)
   toCST (bd : bds) ctx@(tabs, _) = BI_PAIR (toCST bd ctx) (toCST bds ctx) (TAB tabs)
 
 instance ToCST [Binding] BINDINGS where
   toCST [] (tabs, _) = BDS_EMPTY (TAB tabs)
-  toCST (BiMeta mt : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (MT_BINDING (tail mt)) (toCST bds ctx)
+  toCST (BiMeta mt : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (META NO_EXCL B (metaTail mt)) (toCST bds ctx)
   toCST (bd : bds) ctx@(tabs, eol) = BDS_PAIR eol (TAB tabs) (toCST bd ctx) (toCST bds ctx)
 
 instance ToCST Binding PAIR where
@@ -335,7 +425,7 @@
   toCST (BiVoid attr) ctx = PA_VOID (toCST attr ctx) ARROW EMPTY
   toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)
   toCST (BiLambda func) _ = PA_LAMBDA func
-  toCST (BiMetaLambda mt) _ = PA_META_LAMBDA (MT_FUNCTION (tail mt))
+  toCST (BiMetaLambda mt) _ = PA_META_LAMBDA (META EXCL F (metaTail mt))
   toCST (BiMeta mt) _ = error $ "BiMeta binding " ++ mt ++ " cannot be converted to PAIR"
 
 instance ToCST Binding APP_BINDING where
@@ -346,7 +436,7 @@
   toCST BtEmpty _ = BT_EMPTY
   toCST (BtOne byte) _ = BT_ONE byte
   toCST (BtMany bts) _ = BT_MANY bts
-  toCST (BtMeta mt) _ = BT_META (MT_BYTES (tail mt))
+  toCST (BtMeta mt) _ = BT_META (META NO_EXCL D (metaTail mt))
 
 instance ToCST Attribute ATTRIBUTE where
   toCST (AtLabel label) _ = AT_LABEL label
@@ -355,4 +445,52 @@
   toCST AtRho _ = AT_RHO RHO
   toCST AtDelta _ = AT_DELTA DELTA
   toCST AtLambda _ = AT_LAMBDA LAMBDA
-  toCST (AtMeta mt) _ = AT_META (MT_ATTRIBUTE (tail mt))
+  toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt))
+
+withoutXi :: [Y.Condition] -> [Y.Condition]
+withoutXi conds = [cond | cond <- conds, not (singleXi cond)]
+  where
+    singleXi :: Y.Condition -> Bool
+    singleXi (Y.Xi _) = True
+    singleXi (Y.Not (Y.Xi _)) = True
+    singleXi (Y.And [cond]) = singleXi cond
+    singleXi (Y.Or [cond]) = singleXi cond
+    singleXi _ = False
+
+instance ToCST Y.Condition CONDITION where
+  toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))
+  toCST (Y.Not (Y.Eq left right)) _ = CO_COMPARE (comparableToCST left) NOT_EQUAL (comparableToCST right)
+  toCST (Y.Not (Y.Alpha attr)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])
+  toCST (Y.In attr binding) _ = CO_BELONGS (attributeToCST attr) IN (ST_BINDING (bindingsToCST [binding]))
+  toCST (Y.And conds) _ = case withoutXi conds of
+    [] -> CO_EMPTY
+    conds' -> CO_LOGIC (map toCST' (withoutXi conds')) AND
+  toCST (Y.Or conds) _ = case withoutXi conds of
+    [] -> CO_EMPTY
+    conds' -> CO_LOGIC (map toCST' (withoutXi conds')) OR
+  toCST (Y.Alpha attr) _ = CO_BELONGS (attributeToCST attr) IN (ST_ATTRIBUTES [attributeToCST (AtAlpha 0), attributeToCST (AtAlpha 1), AT_REST DOTS])
+  toCST (Y.NF expr) _ = CO_NF (expressionToCST expr)
+  toCST (Y.Not cond) _ = CO_NOT (conditionToCST cond)
+  toCST (Y.Eq left right) _ = CO_COMPARE (comparableToCST left) EQUAL (comparableToCST right)
+  toCST (Y.Matches regex expr) _ = CO_MATCHES regex (expressionToCST expr)
+  toCST (Y.PartOf expr binding) _ = CO_PART_OF (expressionToCST expr) (bindingsToCST [binding])
+  toCST (Y.Xi _) _ = CO_EMPTY
+
+instance ToCST Y.Comparable COMPARABLE where
+  toCST (Y.CmpAttr attr) _ = CMP_ATTR (attributeToCST attr)
+  toCST (Y.CmpExpr expr) _ = CMP_EXPR (expressionToCST expr)
+  toCST (Y.CmpNum num) _ = CMP_NUM (numberToCST num)
+
+instance ToCST Y.Number NUMBER where
+  toCST (Y.Ordinal attr) _ = ORDINAL (attributeToCST attr)
+  toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])
+  toCST (Y.Literal num) _ = LITERAL num
+
+instance ToCST Y.ExtraArgument EXTRA_ARG where
+  toCST (Y.ArgAttribute attr) _ = ARG_ATTR (attributeToCST attr)
+  toCST (Y.ArgExpression expr) _ = ARG_EXPR (expressionToCST expr)
+  toCST (Y.ArgBinding binding) _ = ARG_BINDING (bindingsToCST [binding])
+  toCST (Y.ArgBytes bytes) _ = ARG_BYTES (toCST' bytes)
+
+instance ToCST Y.Extra EXTRA where
+  toCST Y.Extra{..} _ = EXTRA (toCST' meta) function (map toCST' args)
diff --git a/src/Condition.hs b/src/Condition.hs
--- a/src/Condition.hs
+++ b/src/Condition.hs
@@ -124,7 +124,7 @@
         _ <- symbol "xi" >> lparen
         expr <- _expression phiParser
         _ <- rparen
-        return (Y.XI expr)
+        return (Y.Xi expr)
     , do
         _ <- symbol "matches" >> lparen
         ptn <- _string phiParser
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -154,7 +154,7 @@
         then morph (ExTermination, seq) ctx -- PRIM
         else do
           prog' <- withLocatedExpression _locator expr _program
-          rewrittens' <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ todo
+          (rewrittens', _) <- rewrite prog' normalizationRules (switchContext ctx) -- NMZ todo
           let seq' = reverse rewrittens' <> tail seq
           expr' <- locatedExpression _locator (fst (head seq'))
           morph (expr', seq') ctx
diff --git a/src/Encoding.hs b/src/Encoding.hs
--- a/src/Encoding.hs
+++ b/src/Encoding.hs
@@ -31,8 +31,8 @@
   toASCII EX_APPLICATION{..} = EX_APPLICATION (toASCII expr) eol tab (toASCII tau) eol' tab' indent
   toASCII EX_APPLICATION_TAUS{..} = EX_APPLICATION_TAUS (toASCII expr) eol tab (toASCII taus) eol' tab' indent
   toASCII EX_APPLICATION_EXPRS{..} = EX_APPLICATION_EXPRS (toASCII expr) eol tab (toASCII args) eol' tab' indent
-  toASCII EX_META{..} = EX_META (MT_EXPRESSION' (rest meta))
-  toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) (MT_TAIL (rest meta))
+  toASCII EX_META{..} = EX_META (META EXCL E' (rest meta))
+  toASCII EX_META_TAIL{..} = EX_META_TAIL (toASCII expr) meta
   toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr)
   toASCII EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toASCII expr)
   toASCII expr = expr
@@ -42,12 +42,12 @@
 
 instance ToASCII BINDING where
   toASCII BI_PAIR{..} = BI_PAIR (toASCII pair) (toASCII bindings) tab
-  toASCII BI_META{..} = BI_META (MT_BINDING' (rest meta)) (toASCII bindings) tab
+  toASCII BI_META{meta = META{..}, ..} = BI_META (META EXCL B' rest) (toASCII bindings) tab
   toASCII bd = bd
 
 instance ToASCII BINDINGS where
   toASCII BDS_PAIR{..} = BDS_PAIR eol tab (toASCII pair) (toASCII bindings)
-  toASCII BDS_META{..} = BDS_META eol tab (MT_BINDING' (rest meta)) (toASCII bindings)
+  toASCII BDS_META{..} = BDS_META eol tab (META EXCL B' (rest meta)) (toASCII bindings)
   toASCII bds = bds
 
 instance ToASCII APP_ARG where
@@ -64,12 +64,45 @@
   toASCII PA_LAMBDA{..} = PA_LAMBDA' func
   toASCII PA_DELTA{..} = PA_DELTA' bytes
   toASCII PA_META_LAMBDA{..} = PA_META_LAMBDA' meta
-  toASCII PA_META_DELTA{..} = PA_META_DELTA' (MT_BYTES' (rest meta))
+  toASCII PA_META_DELTA{..} = PA_META_DELTA' (META EXCL D' (rest meta))
   toASCII pair = pair
 
 instance ToASCII ATTRIBUTE where
   toASCII AT_ALPHA{..} = AT_ALPHA ALPHA' idx
   toASCII AT_PHI{} = AT_PHI AT
   toASCII AT_RHO{} = AT_RHO CARET
-  toASCII AT_META{..} = AT_META (MT_ATTRIBUTE' (rest meta))
+  toASCII AT_META{..} = AT_META (META EXCL A (rest meta))
   toASCII attr = attr
+
+instance ToASCII SET where
+  toASCII ST_BINDING{..} = ST_BINDING (toASCII binding)
+  toASCII ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toASCII attrs)
+
+instance ToASCII NUMBER where
+  toASCII ORDINAL{..} = ORDINAL (toASCII attr)
+  toASCII LENGTH{..} = LENGTH (toASCII binding)
+  toASCII literal@LITERAL{} = literal
+
+instance ToASCII COMPARABLE where
+  toASCII CMP_ATTR{..} = CMP_ATTR (toASCII attr)
+  toASCII CMP_EXPR{..} = CMP_EXPR (toASCII expr)
+  toASCII CMP_NUM{..} = CMP_NUM (toASCII num)
+
+instance ToASCII CONDITION where
+  toASCII CO_BELONGS{..} = CO_BELONGS (toASCII attr) belongs (toASCII set)
+  toASCII CO_LOGIC{..} = CO_LOGIC (map toASCII conditions) operator
+  toASCII CO_NF{..} = CO_NF (toASCII expr)
+  toASCII CO_NOT{..} = CO_NOT (toASCII condition)
+  toASCII CO_COMPARE{..} = CO_COMPARE (toASCII left) equal (toASCII right)
+  toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr)
+  toASCII CO_PART_OF{..} = CO_PART_OF (toASCII expr) (toASCII binding)
+  toASCII CO_EMPTY = CO_EMPTY
+
+instance ToASCII EXTRA_ARG where
+  toASCII ARG_ATTR{..} = ARG_ATTR (toASCII attr)
+  toASCII ARG_EXPR{..} = ARG_EXPR (toASCII expr)
+  toASCII ARG_BINDING{..} = ARG_BINDING (toASCII binding)
+  toASCII bts@ARG_BYTES{} = bts
+
+instance ToASCII EXTRA where
+  toASCII EXTRA{..} = EXTRA (toASCII meta) func (map toASCII args)
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -23,15 +23,15 @@
 import CST
 import Data.List (intercalate, nub)
 import Data.Maybe (fromMaybe)
-import Encoding (Encoding (ASCII), ToASCII, withEncoding)
-import Lining (LineFormat (MULTILINE), ToSingleLine, withLineFormat)
+import Encoding
+import Lining
 import Locator (locatedExpression)
 import Margin (WithMargin, defaultMargin, withMargin)
 import Matcher
 import Misc
 import Render (Render (render))
 import Replacer (replaceProgram)
-import Rewriter (Rewritten)
+import Rewriter (Rewritten, Rewrittens)
 import Sugar (SugarType (SWEET), ToSalty, withSugarType)
 import Text.Printf (printf)
 import qualified Yaml as Y
@@ -51,7 +51,7 @@
   }
 
 defaultLatexContext :: LatexContext
-defaultLatexContext = LatexContext SWEET MULTILINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExGlobal Nothing Nothing Nothing
+defaultLatexContext = LatexContext SWEET SINGLELINE defaultMargin False False defaultMeetPopularity defaultMeetLength ExGlobal Nothing Nothing Nothing
 
 defaultMeetPopularity :: Int
 defaultMeetPopularity = 50
@@ -149,31 +149,32 @@
         printed
     )
 
-ending :: LatexContext -> String
-ending ctx = printf "{.}\n\\end{%s}" (phiquation ctx)
+ending :: Bool -> LatexContext -> String
+ending True ctx = printf " \\leadsto\n  \\leadsto \\dots\n\\end{%s}" (phiquation ctx)
+ending False ctx = printf "{.}\n\\end{%s}" (phiquation ctx)
 
 compressedRewrittens :: [Rewritten] -> LatexContext -> [Rewritten]
 compressedRewrittens rewrittens ctx@LatexContext{..} =
   let (progs, rules) = unzip rewrittens
    in if _compress then zip (meetInPrograms progs ctx) rules else rewrittens
 
-rewrittensToLatex :: [Rewritten] -> LatexContext -> IO String
-rewrittensToLatex rewrittens ctx@LatexContext{_focus = ExGlobal} =
+rewrittensToLatex :: Rewrittens -> LatexContext -> IO String
+rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{_focus = ExGlobal} =
   pure
     ( concat
         [ preamble ctx
         , body (compressedRewrittens rewrittens ctx) (\prog -> renderToLatex (programToCST prog) ctx)
-        , ending ctx
+        , ending exceeded ctx
         ]
     )
-rewrittensToLatex rewrittens ctx@LatexContext{..} = do
+rewrittensToLatex (rewrittens, exceeded) ctx@LatexContext{..} = do
   let (progs, rules) = unzip (compressedRewrittens rewrittens ctx)
   exprs <- mapM (locatedExpression _focus) progs
   pure
     ( concat
         [ preamble ctx
         , body (zip exprs rules) (\expr -> renderToLatex (expressionToCST expr) ctx)
-        , ending ctx
+        , ending exceeded ctx
         ]
     )
 
@@ -182,7 +183,7 @@
   concat
     [ preamble ctx
     , renderToLatex (programToCST prog) ctx
-    , ending ctx
+    , ending False ctx
     ]
 
 expressionToLaTeX :: Expression -> LatexContext -> String
@@ -190,7 +191,7 @@
   concat
     [ preamble ctx
     , renderToLatex (expressionToCST ex) ctx
-    , ending ctx
+    , ending False ctx
     ]
 
 piped :: String -> String
@@ -212,10 +213,14 @@
   toLaTeX EX_DISPATCH{..} = EX_DISPATCH (toLaTeX expr) (toLaTeX attr)
   toLaTeX EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toLaTeX expr)
   toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)
+  toLaTeX EX_META{..} = EX_META (META NO_EXCL E' (rest meta))
   toLaTeX expr = expr
 
 instance ToLaTeX ATTRIBUTE where
   toLaTeX AT_LABEL{..} = AT_LABEL (piped (toLaTeX label))
+  toLaTeX AT_META{..} = AT_META (META NO_EXCL TAU' (rest meta))
+  toLaTeX AT_LAMBDA{} = AT_LAMBDA LAMBDA'
+  toLaTeX AT_REST{} = AT_REST DOTS'
   toLaTeX attr = attr
 
 instance ToLaTeX APP_BINDING where
@@ -223,10 +228,12 @@
 
 instance ToLaTeX BINDING where
   toLaTeX BI_PAIR{..} = BI_PAIR (toLaTeX pair) (toLaTeX bindings) tab
+  toLaTeX BI_META{..} = BI_META (META NO_EXCL B' (rest meta)) (toLaTeX bindings) tab
   toLaTeX bd = bd
 
 instance ToLaTeX BINDINGS where
   toLaTeX BDS_PAIR{..} = BDS_PAIR eol tab (toLaTeX pair) (toLaTeX bindings)
+  toLaTeX BDS_META{..} = BDS_META eol tab (META NO_EXCL B' (rest meta)) (toLaTeX bindings)
   toLaTeX bds = bds
 
 instance ToLaTeX PAIR where
@@ -236,6 +243,10 @@
   toLaTeX PA_VOID{..} = PA_VOID (toLaTeX attr) arrow void
   toLaTeX PA_TAU{..} = PA_TAU (toLaTeX attr) arrow (toLaTeX expr)
   toLaTeX PA_FORMATION{..} = PA_FORMATION (toLaTeX attr) (map toLaTeX voids) arrow (toLaTeX expr)
+  toLaTeX PA_META_DELTA{..} = toLaTeX (PA_META_DELTA' meta)
+  toLaTeX PA_META_DELTA'{..} = PA_META_DELTA' (META NO_EXCL D' (rest meta))
+  toLaTeX PA_META_LAMBDA{..} = toLaTeX (PA_META_LAMBDA' meta)
+  toLaTeX PA_META_LAMBDA'{..} = PA_META_LAMBDA' (META NO_EXCL F (rest meta))
   toLaTeX pair = pair
 
 instance ToLaTeX APP_ARG where
@@ -257,24 +268,74 @@
         '_' -> "\\char95{}" <> escapeUnprintedChars rest
         _ -> ch : escapeUnprintedChars rest
 
--- @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.
+instance ToLaTeX SET where
+  toLaTeX ST_BINDING{..} = ST_BINDING (toLaTeX binding)
+  toLaTeX ST_ATTRIBUTES{..} = ST_ATTRIBUTES (map toLaTeX attrs)
+
+instance ToLaTeX NUMBER where
+  toLaTeX ORDINAL{..} = ORDINAL (toLaTeX attr)
+  toLaTeX LENGTH{..} = LENGTH (toLaTeX binding)
+  toLaTeX literal@LITERAL{} = literal
+
+instance ToLaTeX COMPARABLE where
+  toLaTeX CMP_EXPR{..} = CMP_EXPR (toLaTeX expr)
+  toLaTeX CMP_ATTR{..} = CMP_ATTR (toLaTeX attr)
+  toLaTeX CMP_NUM{..} = CMP_NUM (toLaTeX num)
+
+instance ToLaTeX CONDITION where
+  toLaTeX CO_BELONGS{..} = CO_BELONGS (toLaTeX attr) belongs (toLaTeX set)
+  toLaTeX CO_LOGIC{..} = CO_LOGIC (map toLaTeX conditions) operator
+  toLaTeX CO_NF{..} = CO_NF (toLaTeX expr)
+  toLaTeX CO_NOT{..} = CO_NOT (toLaTeX condition)
+  toLaTeX CO_COMPARE{..} = CO_COMPARE (toLaTeX left) equal (toLaTeX right)
+  toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr)
+  toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding)
+  toLaTeX CO_EMPTY = CO_EMPTY
+
+instance ToLaTeX EXTRA_ARG where
+  toLaTeX ARG_ATTR{..} = ARG_ATTR (toLaTeX attr)
+  toLaTeX ARG_EXPR{..} = ARG_EXPR (toLaTeX expr)
+  toLaTeX ARG_BINDING{..} = ARG_BINDING (toLaTeX binding)
+  toLaTeX bts@ARG_BYTES{} = bts
+
+instance ToLaTeX EXTRA where
+  toLaTeX EXTRA{..} = EXTRA (toLaTeX meta) func (map toLaTeX args)
+
 explainRule :: Y.Rule -> String
-explainRule rule = "\\rule{" ++ fromMaybe "unnamed" (Y.name rule) ++ "}"
+explainRule rule =
+  intercalate
+    "\n  "
+    [ "\\trrule{" ++ fromMaybe "unknown" (Y.name rule) ++ "}"
+    , braced (renderToLatex (expressionToCST (Y.pattern rule)) defaultLatexContext)
+    , braced (renderToLatex (expressionToCST (Y.result rule)) defaultLatexContext)
+    , conditionToLatex (joinedConditions (Y.when rule) (Y.having rule))
+    , extraArgumentsToLatex (Y.where_ rule)
+    ]
+  where
+    conditionToLatex :: Maybe Y.Condition -> String
+    conditionToLatex Nothing = "{ }"
+    conditionToLatex (Just cond) = case conditionToCST cond of
+      CO_EMPTY -> "{ }"
+      cond' -> braced ("if " <> renderToLatex cond' defaultLatexContext)
+    extraArgumentsToLatex :: Maybe [Y.Extra] -> String
+    extraArgumentsToLatex Nothing = "{ }"
+    extraArgumentsToLatex (Just extras) =
+      let extras' = map ((`renderToLatex` defaultLatexContext) . extraToCST) extras
+       in braced ("where " <> intercalate "; " extras')
+    braced :: String -> String
+    braced = printf "{ %s }"
+    -- Join two maybe conditions into single one using Y.And if at least one is just.
+    joinedConditions :: Maybe Y.Condition -> Maybe Y.Condition -> Maybe Y.Condition
+    joinedConditions Nothing Nothing = Nothing
+    joinedConditions first@(Just _) Nothing = first
+    joinedConditions Nothing second@(Just _) = second
+    joinedConditions (Just first) (Just second) = Just (Y.And [first, second])
 
--- @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}"
+explainRules rules =
+  intercalate
+    "\n"
+    [ "\\begin{tabular}{rl}"
+    , intercalate "\n" (map explainRule rules)
+    , "\\end{tabular}"
     ]
-    ++ unlines (map explainRule rules')
-    ++ "\\end{document}"
diff --git a/src/Lining.hs b/src/Lining.hs
--- a/src/Lining.hs
+++ b/src/Lining.hs
@@ -57,3 +57,35 @@
 instance ToSingleLine APP_ARGS where
   toSingleLine AAS_EXPR{..} = AAS_EXPR NO_EOL TAB' (toSingleLine expr) (toSingleLine args)
   toSingleLine args = args
+
+instance ToSingleLine SET where
+  toSingleLine ST_BINDING{..} = ST_BINDING (toSingleLine binding)
+  toSingleLine st = st
+
+instance ToSingleLine NUMBER where
+  toSingleLine LENGTH{..} = LENGTH (toSingleLine binding)
+  toSingleLine num = num
+
+instance ToSingleLine COMPARABLE where
+  toSingleLine comp@CMP_ATTR{} = comp
+  toSingleLine CMP_EXPR{..} = CMP_EXPR (toSingleLine expr)
+  toSingleLine CMP_NUM{..} = CMP_NUM (toSingleLine num)
+
+instance ToSingleLine CONDITION where
+  toSingleLine CO_BELONGS{..} = CO_BELONGS attr belongs (toSingleLine set)
+  toSingleLine CO_LOGIC{..} = CO_LOGIC (map toSingleLine conditions) operator
+  toSingleLine CO_NF{..} = CO_NF (toSingleLine expr)
+  toSingleLine CO_NOT{..} = CO_NOT (toSingleLine condition)
+  toSingleLine CO_COMPARE{..} = CO_COMPARE (toSingleLine left) equal (toSingleLine right)
+  toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr)
+  toSingleLine CO_PART_OF{..} = CO_PART_OF (toSingleLine expr) (toSingleLine binding)
+  toSingleLine CO_EMPTY = CO_EMPTY
+
+instance ToSingleLine EXTRA_ARG where
+  toSingleLine ARG_EXPR{..} = ARG_EXPR (toSingleLine expr)
+  toSingleLine ARG_BINDING{..} = ARG_BINDING (toSingleLine binding)
+  toSingleLine at@ARG_ATTR{} = at
+  toSingleLine bts@ARG_BYTES{} = bts
+
+instance ToSingleLine EXTRA where
+  toSingleLine EXTRA{..} = EXTRA (toSingleLine meta) func (map toSingleLine args)
diff --git a/src/Margin.hs b/src/Margin.hs
--- a/src/Margin.hs
+++ b/src/Margin.hs
@@ -111,5 +111,11 @@
      in if lengthOf single + extra <= margin then single else pa'
   withMargin' _ pa = pa
 
+instance WithMargin CONDITION where
+  withMargin' _ co = co
+
+instance WithMargin EXTRA where
+  withMargin' _ = id
+
 lengthOf :: Render a => a -> Int
 lengthOf renderable = length (render renderable)
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -9,6 +9,7 @@
 
 import CST
 import Data.List (intercalate)
+import Text.Printf (printf)
 
 class Render a where
   render :: a -> String
@@ -76,6 +77,7 @@
 
 instance Render LAMBDA where
   render LAMBDA = "λ"
+  render LAMBDA' = "\\lambda"
 
 instance Render GLOBAL where
   render Φ = "Φ"
@@ -92,23 +94,35 @@
   render EOL = "\n"
   render NO_EOL = ""
 
+instance Render DOTS where
+  render DOTS = "..."
+  render DOTS' = "\\dots"
+
 instance Render BYTES where
   render BT_EMPTY = "--"
   render (BT_ONE bte) = render bte <> "-"
   render (BT_MANY bts) = intercalate "-" bts
   render (BT_META mt) = render mt
 
+instance Render EXCLAMATION where
+  render EXCL = "!"
+  render NO_EXCL = ""
+
+instance Render META_HEAD where
+  render E = "𝑒"
+  render E' = "e"
+  render A = "a"
+  render TAU = "𝜏"
+  render TAU' = "\\tau"
+  render B = "𝐵"
+  render B' = "B"
+  render D = "δ"
+  render D' = "d"
+  render TAIL = "t"
+  render F = "F"
+
 instance Render META where
-  render MT_EXPRESSION{..} = '𝑒' : rest
-  render MT_EXPRESSION'{..} = "!e" <> rest
-  render MT_ATTRIBUTE{..} = '𝜏' : rest
-  render MT_ATTRIBUTE'{..} = "!a" <> rest
-  render MT_BINDING{..} = '𝐵' : rest
-  render MT_BINDING'{..} = "!B" <> rest
-  render MT_BYTES{..} = 'δ' : rest
-  render MT_BYTES'{..} = "!d" <> rest
-  render MT_TAIL{..} = "!t" <> rest
-  render MT_FUNCTION{..} = "!F" <> rest
+  render META{..} = render excl <> render hd <> render rest
 
 instance Render ALPHA where
   render ALPHA = "α"
@@ -185,3 +199,53 @@
   render AT_LAMBDA{..} = render lambda
   render AT_DELTA{..} = render delta
   render AT_META{..} = render meta
+  render AT_REST{..} = render dots
+
+instance Render BELONGING where
+  render IN = "\\in"
+  render NOT_IN = "\\notin"
+
+instance Render SET where
+  render ST_BINDING{..} = render binding
+  render ST_ATTRIBUTES{..} = printf "[ %s ]" (intercalate ", " (map render attrs))
+
+instance Render LOGIC_OPERATOR where
+  render AND = "and"
+  render OR = "or"
+
+instance Render NUMBER where
+  render ORDINAL{..} = renderFunc "ordinal" attr
+  render LENGTH{..} = renderFunc "length" binding
+  render LITERAL{..} = show num
+
+instance Render COMPARABLE where
+  render CMP_ATTR{..} = render attr
+  render CMP_EXPR{..} = render expr
+  render CMP_NUM{..} = render num
+
+instance Render EQUAL where
+  render EQUAL = "="
+  render NOT_EQUAL = "\\not="
+
+instance Render CONDITION where
+  render CO_BELONGS{..} = render attr <> render SPACE <> render belongs <> render SPACE <> render set
+  render CO_LOGIC{conditions = [cond]} = render cond
+  render CO_LOGIC{..} = printf "\\( %s \\)" (intercalate (printf " \\) %s \\( " (render operator)) (map render conditions))
+  render CO_NF{..} = renderFunc "NF" expr
+  render CO_NOT{..} = renderFunc "not" condition
+  render CO_COMPARE{..} = render left <> render SPACE <> render equal <> render SPACE <> render right
+  render CO_MATCHES{..} = printf "matches( %s, %s )" regex (render expr)
+  render CO_PART_OF{..} = printf "part-of( %s, %s )" (render expr) (render binding)
+  render CO_EMPTY = ""
+
+renderFunc :: Render a => String -> a -> String
+renderFunc func renderable = printf "%s( %s )" func (render renderable)
+
+instance Render EXTRA_ARG where
+  render ARG_ATTR{..} = render attr
+  render ARG_EXPR{..} = render expr
+  render ARG_BINDING{..} = render binding
+  render ARG_BYTES{..} = render bytes
+
+instance Render EXTRA where
+  render EXTRA{..} = render meta <> " <- " <> printf "%s( %s )" func (intercalate ", " (map render args))
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -8,13 +8,12 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Rewriter (rewrite, RewriteContext (..), Rewritten) where
+module Rewriter (rewrite, RewriteContext (..), Rewritten, Rewrittens) where
 
 import AST
 import Builder
 import Control.Exception (Exception, throwIO)
 import Data.Char (toLower)
-import Data.Functor ((<&>))
 import Data.Maybe (fromMaybe)
 import qualified Data.Set as Set
 import Deps
@@ -33,6 +32,8 @@
 
 type Rewritten = (Program, Maybe String)
 
+type Rewrittens = ([Rewritten], Bool)
+
 type ToReplace = (Expression, Expression, Expression, [Subst])
 
 data RewriteContext = RewriteContext
@@ -183,17 +184,19 @@
           [] -> [(_prog, Nothing)]
 
 -- Rewrite program by provided locator from RewriteContext
-rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO [Rewritten]
-rewrite prog rules ctx@RewriteContext{..} = _rewrite ([(prog, Nothing)], Set.empty) 0 <&> reverse
+rewrite :: Program -> [Y.Rule] -> RewriteContext -> IO Rewrittens
+rewrite prog rules ctx@RewriteContext{..} = do
+  (rewrittens, exceeded) <- _rewrite ([(prog, Nothing)], Set.empty) 0
+  pure (reverse rewrittens, exceeded)
   where
-    _rewrite :: RewriteState -> Int -> IO [Rewritten]
+    _rewrite :: RewriteState -> Int -> IO Rewrittens
     _rewrite state@(rewrittens, _) count
       | not (inRange _must count) && count > 0 && exceedsUpperBound _must count = throwIO (MustStopBefore _must count)
       | count == _maxCycles = do
           logDebug (printf "Max amount of rewriting cycles for all rules (%d) has been reached, rewriting is stopped" _maxCycles)
           if _depthSensitive
             then throwIO (StoppedOnLimit "max-cycles" _maxCycles)
-            else pure rewrittens
+            else pure (rewrittens, True)
       | otherwise = do
           logDebug (printf "Starting rewriting cycle for all rules: %d out of %d" count _maxCycles)
           state'@(rewrittens', _) <- rewrite' state rules count ctx
@@ -204,5 +207,5 @@
               logDebug "Rewriting is stopped since it has no effect"
               if not (inRange _must count)
                 then throwIO (MustBeGoing _must count)
-                else pure rewrittens'
+                else pure (rewrittens', False)
             else _rewrite state' (count + 1)
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -208,7 +208,7 @@
 meetCondition' (Y.Alpha attr) = _alpha attr
 meetCondition' (Y.Eq left right) = _eq left right
 meetCondition' (Y.NF expr) = _nf expr
-meetCondition' (Y.XI expr) = _xi expr
+meetCondition' (Y.Xi expr) = _xi expr
 meetCondition' (Y.Matches pat expr) = _matches pat expr
 meetCondition' (Y.PartOf expr bd) = _partOf expr bd
 
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -166,3 +166,35 @@
       joinToBindings [] BI_META{} = error "BI_META unexpected in joinToBindings"
       joinToBindings (attr : rest) bd = BDS_PAIR eol tab (PA_VOID attr arrow EMPTY) (joinToBindings rest bd)
   toSalty pair = pair
+
+instance ToSalty SET where
+  toSalty ST_BINDING{..} = ST_BINDING (toSalty binding)
+  toSalty st = st
+
+instance ToSalty NUMBER where
+  toSalty LENGTH{..} = LENGTH (toSalty binding)
+  toSalty num = num
+
+instance ToSalty COMPARABLE where
+  toSalty comp@CMP_ATTR{} = comp
+  toSalty CMP_EXPR{..} = CMP_EXPR (toSalty expr)
+  toSalty CMP_NUM{..} = CMP_NUM (toSalty num)
+
+instance ToSalty CONDITION where
+  toSalty CO_BELONGS{..} = CO_BELONGS attr belongs (toSalty set)
+  toSalty CO_LOGIC{..} = CO_LOGIC (map toSalty conditions) operator
+  toSalty CO_NF{..} = CO_NF (toSalty expr)
+  toSalty CO_NOT{..} = CO_NOT (toSalty condition)
+  toSalty CO_COMPARE{..} = CO_COMPARE (toSalty left) equal (toSalty right)
+  toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr)
+  toSalty CO_PART_OF{..} = CO_PART_OF (toSalty expr) (toSalty binding)
+  toSalty CO_EMPTY = CO_EMPTY
+
+instance ToSalty EXTRA_ARG where
+  toSalty ARG_EXPR{..} = ARG_EXPR (toSalty expr)
+  toSalty ARG_BINDING{..} = ARG_BINDING (toSalty binding)
+  toSalty at@ARG_ATTR{} = at
+  toSalty bts@ARG_BYTES{} = bts
+
+instance ToSalty EXTRA where
+  toSalty EXTRA{..} = EXTRA (toSalty meta) func (map toSalty args)
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -83,7 +83,7 @@
             , Not <$> v .: "not"
             , Alpha <$> v .: "alpha"
             , NF <$> v .: "nf"
-            , XI <$> v .: "xi"
+            , Xi <$> v .: "xi"
             , do
                 vals <- v .: "eq"
                 case vals of
@@ -151,7 +151,7 @@
   | Alpha Attribute
   | Eq Comparable Comparable
   | NF Expression
-  | XI Expression
+  | Xi Expression
   | Matches String Expression
   | PartOf Expression Binding
   deriving (Eq, Generic, Show)
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -559,6 +559,19 @@
               ]
           ]
 
+    it "shows exceeding of limits in latex" $
+      withStdin "{[[ x -> $.y, y -> $.x ]].x}" $
+        testCLISucceeded
+          ["rewrite", "--normalize", "--flat", "--sequence", "--output=latex", "--sweet", "--max-depth=1", "--max-cycles=1"]
+          [ unlines
+              [ "\\begin{phiquation}"
+              , "\\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|x|\\Big\\} \\leadsto_{\\nameref{r:dot}}"
+              , "  \\leadsto \\Big\\{[[ |x| -> |y|, |y| -> |x| ]].|y|( ^ -> [[ |x| -> |y|, |y| -> |x| ]] )\\Big\\} \\leadsto"
+              , "  \\leadsto \\dots"
+              , "\\end{phiquation}"
+              ]
+          ]
+
     it "focuses expression in phi without sequence" $
       withStdin "{[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]]  ]]( y -> [[ t -> 42 ]]) ]].i ]]}" $
         testCLISucceeded
@@ -806,17 +819,85 @@
     it "explains single rule" $
       testCLISucceeded
         ["explain", "--rule=resources/copy.yaml"]
-        ["\\documentclass{article}", "\\usepackage{amsmath}", "\\begin{document}", "\\rule{COPY}", "\\end{document}"]
+        [ unlines
+            [ "\\begin{tabular}{rl}"
+            , "\\trrule{COPY}"
+            , "  { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"
+            , "  { [[ B1, \\tau -> e3, B2 ]] }"
+            , "  { if NF( e1 ) }"
+            , "  { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"
+            , "\\end{tabular}"
+            ]
+        ]
 
     it "explains multiple rules" $
       testCLISucceeded
         ["explain", "--rule=resources/copy.yaml", "--rule=resources/alpha.yaml"]
-        ["\\documentclass{article}", "\\rule{COPY}", "\\rule{ALPHA}"]
+        ["\\begin{tabular}{rl}", "\\trrule{COPY}", "\\trrule{ALPHA}"]
 
     it "explains normalization rules" $
       testCLISucceeded
         ["explain", "--normalize"]
-        ["\\documentclass{article}", "\\begin{document}", "\\end{document}"]
+        [ unlines
+            [ "\\begin{tabular}{rl}"
+            , "\\trrule{ALPHA}"
+            , "  { [[ B1, \\tau1 -> ?, B2 ]]( \\tau2 -> e ) }"
+            , "  { [[ B1, \\tau1 -> ?, B2 ]]( \\tau1 -> e ) }"
+            , "  { if ordinal( \\tau2 ) = length( B1 ) }"
+            , "  { }"
+            , "\\trrule{COPY}"
+            , "  { [[ B1, \\tau -> ?, B2 ]]( \\tau -> e1 ) }"
+            , "  { [[ B1, \\tau -> e3, B2 ]] }"
+            , "  { if NF( e1 ) }"
+            , "  { where e2 <- scope( e1 ); e3 <- contextualize( e1, e2 ) }"
+            , "\\trrule{DC}"
+            , "  { T( \\tau -> e ) }"
+            , "  { T }"
+            , "  { }"
+            , "  { }"
+            , "\\trrule{DD}"
+            , "  { T.\\tau }"
+            , "  { T }"
+            , "  { }"
+            , "  { }"
+            , "\\trrule{DOT}"
+            , "  { [[ B1, \\tau -> e1, B2 ]].\\tau }"
+            , "  { e2( ^ -> [[ B1, \\tau -> e1, B2 ]] ) }"
+            , "  { if NF( e1 ) }"
+            , "  { where e2 <- contextualize( e1, [[ B1, \\tau -> e1, B2 ]] ) }"
+            , "\\trrule{MISS}"
+            , "  { [[ B ]]( \\tau -> e ) }"
+            , "  { T }"
+            , "  { if \\( \\tau \\notin B \\) and \\( \\tau \\notin [ ~0, ~1, \\dots ] \\) }"
+            , "  { }"
+            , "\\trrule{NULL}"
+            , "  { [[ B1, \\tau -> ?, B2 ]].\\tau }"
+            , "  { T }"
+            , "  { }"
+            , "  { }"
+            , "\\trrule{OVER}"
+            , "  { [[ B1, \\tau -> e1, B2 ]]( \\tau -> e2 ) }"
+            , "  { T }"
+            , "  { if \\tau \\not= ^ }"
+            , "  { }"
+            , "\\trrule{PHI}"
+            , "  { [[ B ]].\\tau }"
+            , "  { [[ B ]].@.\\tau }"
+            , "  { if \\( @ \\in B \\) and \\( \\tau \\notin B \\) }"
+            , "  { }"
+            , "\\trrule{STAY}"
+            , "  { [[ B1, ^ -> e1, B2 ]]( ^ -> e2 ) }"
+            , "  { [[ B1, ^ -> e1, B2 ]] }"
+            , "  { }"
+            , "  { }"
+            , "\\trrule{STOP}"
+            , "  { [[ B ]].\\tau }"
+            , "  { T }"
+            , "  { if \\( \\tau \\notin B \\) and \\( @ \\notin B \\) and \\( \\lambda \\notin B \\) }"
+            , "  { }"
+            , "\\end{tabular}"
+            ]
+        ]
 
     it "fails with no rules specified" $
       testCLIFailed
@@ -837,8 +918,8 @@
             testCLISucceeded ["explain", "--normalize", printf "--target=%s" path] []
             content <- readFile path
             _ <- evaluate (length content)
-            content `shouldContain` "\\documentclass{article}"
-            content `shouldContain` "\\begin{document}"
+            content `shouldContain` "\\begin{tabular}{rl}"
+            content `shouldContain` "\\end{tabular}"
         )
 
   describe "merge" $ do
diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs
--- a/test/ConditionSpec.hs
+++ b/test/ConditionSpec.hs
@@ -36,7 +36,7 @@
       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))
       , ("eq(ordinal(z),length(!B1))", Y.Eq (Y.CmpNum (Y.Ordinal (AtLabel "z"))) (Y.CmpNum (Y.Length (BiMeta "B1"))))
       , ("eq(!a1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "a1")) (Y.CmpExpr (ExMeta "e2")))
-      , ("or(xi(!e1), nf(Q.x))", Y.Or [Y.XI (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])
+      , ("or(xi(!e1), nf(Q.x))", Y.Or [Y.Xi (ExMeta "e1"), Y.NF (ExDispatch ExGlobal (AtLabel "x"))])
       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])
       ]
       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res))
diff --git a/test/LiningSpec.hs b/test/LiningSpec.hs
deleted file mode 100644
--- a/test/LiningSpec.hs
+++ /dev/null
@@ -1,193 +0,0 @@
--- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
--- SPDX-License-Identifier: MIT
-
-{- | Tests for the Lining module that converts CST to single-line format.
-The module provides functions to remove line breaks and indentation from
-phi-calculus concrete syntax trees while preserving structural semantics.
--}
-module LiningSpec (spec) where
-
-import CST
-import Control.Monad (forM_)
-import Lining (LineFormat (..), toSingleLine, withLineFormat)
-import Test.Hspec (Spec, describe, it, shouldBe, shouldNotBe)
-
-spec :: Spec
-spec = do
-  describe "withLineFormat preserves multiline programs" $
-    it "returns program unchanged" $
-      let prog = PR_SWEET LCB (EX_GLOBAL Φ) RCB
-       in withLineFormat MULTILINE prog `shouldBe` prog
-
-  describe "withLineFormat converts to singleline" $
-    it "applies toSingleLine transformation" $
-      let prog = PR_SWEET LCB (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) RCB
-          result = withLineFormat SINGLELINE prog
-       in result `shouldBe` PR_SWEET LCB (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) RCB
-
-  describe "LineFormat Eq instance" $
-    forM_
-      [ ("SINGLELINE equals SINGLELINE", SINGLELINE, SINGLELINE, True)
-      , ("MULTILINE equals MULTILINE", MULTILINE, MULTILINE, True)
-      , ("SINGLELINE differs from MULTILINE", SINGLELINE, MULTILINE, False)
-      ]
-      ( \(desc, fmt1, fmt2, expected) ->
-          it desc $
-            if expected
-              then fmt1 `shouldBe` fmt2
-              else fmt1 `shouldNotBe` fmt2
-      )
-
-  describe "LineFormat Show instance" $
-    forM_
-      [ ("SINGLELINE shows correctly", SINGLELINE, "SINGLELINE")
-      , ("MULTILINE shows correctly", MULTILINE, "MULTILINE")
-      ]
-      ( \(desc, fmt, expected) ->
-          it desc (show fmt `shouldBe` expected)
-      )
-
-  describe "toSingleLine PROGRAM for PR_SWEET" $
-    it "removes newlines from expression" $
-      let prog = PR_SWEET LCB (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) RCB
-       in toSingleLine prog `shouldBe` PR_SWEET LCB (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) RCB
-
-  describe "toSingleLine PROGRAM for PR_SALTY" $
-    it "converts salty program to singleline" $
-      let prog = PR_SALTY Φ ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)
-       in toSingleLine prog `shouldBe` PR_SALTY Φ ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)
-
-  describe "toSingleLine EXPRESSION for EX_FORMATION with empty binding" $
-    it "removes tabs and newlines" $
-      let ex = EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB
-       in toSingleLine ex `shouldBe` EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB
-
-  describe "toSingleLine EXPRESSION for EX_FORMATION with bindings" $
-    it "converts to singleline with TAB markers" $
-      let bd = BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) (TAB 1)
-          ex = EX_FORMATION LSB EOL (TAB 1) bd EOL (TAB 0) RSB
-          result = toSingleLine ex
-       in result `shouldBe` EX_FORMATION LSB NO_EOL TAB' (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) TAB') NO_EOL TAB' RSB
-
-  describe "toSingleLine EXPRESSION for EX_DISPATCH" $
-    it "converts nested expression" $
-      let ex = EX_DISPATCH (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) (AT_LABEL "attr")
-       in toSingleLine ex `shouldBe` EX_DISPATCH (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) (AT_LABEL "attr")
-
-  describe "toSingleLine EXPRESSION for EX_APPLICATION" $
-    it "converts with proper spacing" $
-      let t = APP_BINDING (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ))
-          ex = EX_APPLICATION (EX_GLOBAL Φ) EOL (TAB 1) t EOL (TAB 0) 1
-       in toSingleLine ex `shouldBe` EX_APPLICATION (EX_GLOBAL Φ) NO_EOL TAB' (APP_BINDING (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ))) NO_EOL TAB' 1
-
-  describe "toSingleLine EXPRESSION for EX_APPLICATION_TAUS" $
-    it "converts taus application" $
-      let ts = BI_PAIR (PA_TAU (AT_LABEL "z") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) (TAB 1)
-          ex = EX_APPLICATION_TAUS (EX_GLOBAL Φ) EOL (TAB 1) ts EOL (TAB 0) 1
-       in toSingleLine ex `shouldBe` EX_APPLICATION_TAUS (EX_GLOBAL Φ) NO_EOL TAB' (BI_PAIR (PA_TAU (AT_LABEL "z") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) TAB') NO_EOL TAB' 1
-
-  describe "toSingleLine EXPRESSION for EX_APPLICATION_EXPRS" $
-    it "converts expressions application" $
-      let as = APP_ARG (EX_GLOBAL Φ) AAS_EMPTY
-          ex = EX_APPLICATION_EXPRS (EX_GLOBAL Φ) EOL (TAB 1) as EOL (TAB 0) 1
-       in toSingleLine ex `shouldBe` EX_APPLICATION_EXPRS (EX_GLOBAL Φ) NO_EOL TAB' (APP_ARG (EX_GLOBAL Φ) AAS_EMPTY) NO_EOL TAB' 1
-
-  describe "toSingleLine EXPRESSION for EX_PHI_MEET" $
-    it "converts meet expression" $
-      let ex = EX_PHI_MEET Nothing 0 (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)
-       in toSingleLine ex `shouldBe` EX_PHI_MEET Nothing 0 (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)
-
-  describe "toSingleLine EXPRESSION for EX_PHI_AGAIN" $
-    it "converts again expression" $
-      let ex = EX_PHI_AGAIN Nothing 1 (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)
-       in toSingleLine ex `shouldBe` EX_PHI_AGAIN Nothing 1 (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)
-
-  describe "toSingleLine EXPRESSION leaves primitives unchanged" $
-    forM_
-      [ ("EX_GLOBAL", EX_GLOBAL Φ)
-      , ("EX_XI", EX_XI XI)
-      , ("EX_ATTR", EX_ATTR (AT_LABEL "attr"))
-      , ("EX_TERMINATION", EX_TERMINATION DEAD)
-      , ("EX_STRING", EX_STRING "тест" (TAB 0) [])
-      , ("EX_NUMBER", EX_NUMBER (Left 42) (TAB 0) [])
-      , ("EX_META", EX_META (MT_EXPRESSION "e"))
-      , ("EX_META_TAIL", EX_META_TAIL (EX_GLOBAL Φ) (MT_TAIL "t"))
-      ]
-      ( \(desc, ex) ->
-          it desc (toSingleLine ex `shouldBe` ex)
-      )
-
-  describe "toSingleLine APP_BINDING" $
-    it "converts nested pair expression" $
-      let bd = APP_BINDING (PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB))
-       in toSingleLine bd `shouldBe` APP_BINDING (PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB))
-
-  describe "toSingleLine BINDING for BI_PAIR" $
-    it "converts to singleline" $
-      let bd = BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) (TAB 1)
-       in toSingleLine bd `shouldBe` BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)) TAB'
-
-  describe "toSingleLine BINDING for BI_META" $
-    it "converts meta binding" $
-      let bd = BI_META (MT_BINDING "B") (BDS_EMPTY (TAB 1)) (TAB 1)
-       in toSingleLine bd `shouldBe` BI_META (MT_BINDING "B") (BDS_EMPTY (TAB 1)) TAB'
-
-  describe "toSingleLine BINDING for BI_EMPTY" $
-    it "returns binding unchanged" $
-      let bd = BI_EMPTY (TAB 1)
-       in toSingleLine bd `shouldBe` bd
-
-  describe "toSingleLine BINDINGS for BDS_PAIR" $
-    it "converts to singleline" $
-      let bds = BDS_PAIR EOL (TAB 1) (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1))
-       in toSingleLine bds `shouldBe` BDS_PAIR NO_EOL TAB' (PA_TAU (AT_LABEL "y") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1))
-
-  describe "toSingleLine BINDINGS for BDS_META" $
-    it "converts meta bindings" $
-      let bds = BDS_META EOL (TAB 1) (MT_BINDING "B") (BDS_EMPTY (TAB 1))
-       in toSingleLine bds `shouldBe` BDS_META NO_EOL TAB' (MT_BINDING "B") (BDS_EMPTY (TAB 1))
-
-  describe "toSingleLine BINDINGS for BDS_EMPTY" $
-    it "returns bindings unchanged" $
-      let bds = BDS_EMPTY (TAB 1)
-       in toSingleLine bds `shouldBe` bds
-
-  describe "toSingleLine PAIR for PA_TAU" $
-    it "converts expression" $
-      let pr = PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)
-       in toSingleLine pr `shouldBe` PA_TAU (AT_LABEL "x") ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)
-
-  describe "toSingleLine PAIR for PA_FORMATION" $
-    it "converts formation pair" $
-      let pr = PA_FORMATION (AT_LABEL "f") [AT_LABEL "v"] ARROW (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB)
-       in toSingleLine pr `shouldBe` PA_FORMATION (AT_LABEL "f") [AT_LABEL "v"] ARROW (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB)
-
-  describe "toSingleLine PAIR leaves non-expression pairs unchanged" $
-    forM_
-      [ ("PA_VOID", PA_VOID (AT_LABEL "v") ARROW EMPTY)
-      , ("PA_LAMBDA", PA_LAMBDA "λфункция")
-      , ("PA_LAMBDA'", PA_LAMBDA' "Function")
-      , ("PA_META_LAMBDA", PA_META_LAMBDA (MT_FUNCTION "F"))
-      , ("PA_META_LAMBDA'", PA_META_LAMBDA' (MT_FUNCTION "F"))
-      , ("PA_DELTA", PA_DELTA (BT_ONE "FF"))
-      , ("PA_DELTA'", PA_DELTA' (BT_MANY ["00", "01"]))
-      , ("PA_META_DELTA", PA_META_DELTA (MT_BYTES "d"))
-      , ("PA_META_DELTA'", PA_META_DELTA' (MT_BYTES "d"))
-      ]
-      ( \(desc, pr) ->
-          it desc (toSingleLine pr `shouldBe` pr)
-      )
-
-  describe "toSingleLine APP_ARG" $
-    it "converts expression and args" $
-      let arg = APP_ARG (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) AAS_EMPTY
-       in toSingleLine arg `shouldBe` APP_ARG (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) AAS_EMPTY
-
-  describe "toSingleLine APP_ARGS for AAS_EXPR" $
-    it "converts nested expression" $
-      let as = AAS_EXPR EOL (TAB 1) (EX_FORMATION LSB EOL (TAB 1) (BI_EMPTY (TAB 1)) EOL (TAB 0) RSB) AAS_EMPTY
-       in toSingleLine as `shouldBe` AAS_EXPR NO_EOL TAB' (EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB) AAS_EMPTY
-
-  describe "toSingleLine APP_ARGS for AAS_EMPTY" $
-    it "returns unchanged" $
-      toSingleLine AAS_EMPTY `shouldBe` AAS_EMPTY
diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs
--- a/test/RewriterSpec.hs
+++ b/test/RewriterSpec.hs
@@ -99,7 +99,7 @@
                   if normalize'
                     then pure normalizationRules
                     else pure []
-              rewrittens <-
+              (rewrittens, _) <-
                 rewrite
                   prog
                   rules'