diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,7 +1,7 @@
 cabal-version:      3.0
 
 name:               phino
-version:            0.0.0.3
+version:            0.0.0.4
 license:            MIT
 synopsis:           Command-Line Manipulator of 𝜑-Calculus Expressions
 description:        Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
@@ -23,13 +23,14 @@
 
 library
   exposed-modules:
-    CLI, Ast, Parser, Matcher, Builder, Replacer, Printer, Rewriter, Yaml, Misc
+    CLI, Ast, Parser, Matcher, Builder, Replacer, Printer, Rewriter, Yaml, Condition, Misc
   hs-source-dirs: src
   other-modules:
     Paths_phino
   autogen-modules:
     Paths_phino
   build-depends:
+    file-embed ^>=0.0.16.0,
     base ^>=4.18.3.0,
     containers,
     megaparsec >= 9.0,
@@ -43,7 +44,9 @@
     bytestring,
     utf8-string,
     prettyprinter,
-    optparse-applicative
+    optparse-applicative,
+    vector,
+    random
   default-language: Haskell2010
 
 -- Executable using the library
@@ -71,7 +74,9 @@
     ReplacerSpec,
     PrinterSpec,
     RewriterSpec,
+    ConditionSpec,
     YamlSpec,
+    MiscSpec,
     Paths_phino
   autogen-modules:
     Paths_phino
diff --git a/src/Builder.hs b/src/Builder.hs
--- a/src/Builder.hs
+++ b/src/Builder.hs
@@ -7,17 +7,27 @@
 module Builder
   ( buildExpressions,
     buildExpression,
+    buildExpressionFromFunction,
     buildAttribute,
-    buildBinding
+    buildBinding,
   )
 where
 
 import Ast
-import Data.List (findIndex)
 import qualified Data.Map.Strict as Map
 import Matcher
-import Misc
 
+contextualize :: Expression -> Expression -> Program -> Expression
+contextualize ExGlobal _ (Program expr) = expr
+contextualize ExThis expr _ = expr
+contextualize ExTermination _ _ = ExTermination
+contextualize (ExFormation bds) _ _ = ExFormation bds
+contextualize (ExDispatch expr attr) context prog = ExDispatch (contextualize expr context prog) attr
+contextualize (ExApplication expr (BiTau attr bexpr)) context prog = do
+  let expr' = contextualize expr context prog
+      bexpr' = contextualize bexpr context prog
+  ExApplication expr' (BiTau attr bexpr')
+
 buildAttribute :: Attribute -> Subst -> Maybe Attribute
 buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup meta mp of
   Just (MvAttribute attr) -> Just attr
@@ -81,6 +91,13 @@
     Just (MvTail tails) -> Just (buildExpressionWithTails expression tails subst)
     _ -> Nothing
 buildExpression expr _ = Just expr
+
+buildExpressionFromFunction :: String -> [Expression] -> Subst -> Program -> Maybe Expression
+buildExpressionFromFunction "contextualize" [expr, context] subst prog = do
+  expr' <- buildExpression expr subst
+  context' <- buildExpression context subst
+  return (contextualize expr' context' prog)
+buildExpressionFromFunction _ _ _ _ = Nothing
 
 -- Build a several expression from one expression and several substitutions
 buildExpressions :: Expression -> [Subst] -> Maybe [Expression]
diff --git a/src/CLI.hs b/src/CLI.hs
--- a/src/CLI.hs
+++ b/src/CLI.hs
@@ -7,27 +7,31 @@
 
 module CLI (runCLI) where
 
+import Ast (Program (Program))
 import Control.Exception (Exception (displayException), SomeException, handle, throw, throwIO)
 import Control.Exception.Base
+import Control.Monad (when)
 import Data.Version (showVersion)
 import Misc (ensuredFile)
+import qualified Misc
 import Options.Applicative
+import Parser (parseProgramThrows)
 import Paths_phino (version)
+import Printer (printProgram)
 import Rewriter (rewrite)
-import System.Exit (exitFailure, ExitCode (..))
+import System.Exit (ExitCode (..), exitFailure)
 import System.IO (getContents', hPutStrLn, stderr)
 import Text.Printf (printf)
+import Yaml (normalizationRules)
 import qualified Yaml as Y
 
 data CmdException
-  = InvalidRewriteArguments
-  | NormalizationIsNotSupported
+  = InvalidRewriteArguments {message :: String}
   | CouldNotReadFromStdin {message :: String}
   deriving (Exception)
 
 instance Show CmdException where
-  show InvalidRewriteArguments = "Invalid set of arguments for 'rewrite' command: no --rule, no --normalize, no --nothing are provided"
-  show NormalizationIsNotSupported = "Normalization is not supported yet..."
+  show InvalidRewriteArguments {..} = printf "Invalid set of arguments for 'rewrite' command: %s" message
   show CouldNotReadFromStdin {..} = printf "Could not read 𝜑-expression from stdin\nReason: %s" message
 
 newtype Command = CmdRewrite OptsRewrite
@@ -36,7 +40,9 @@
   { rules :: [FilePath],
     phiInput :: Maybe FilePath,
     normalize :: Bool,
-    nothing :: Bool
+    nothing :: Bool,
+    shuffle :: Bool,
+    maxDepth :: Integer
   }
 
 rewriteParser :: Parser Command
@@ -47,6 +53,8 @@
             <*> optional (strOption (long "phi-input" <> metavar "FILE" <> help "Path .phi file with 𝜑-expression"))
             <*> switch (long "normalize" <> help "Use built-in normalization rules")
             <*> switch (long "nothing" <> help "Desugar provided 𝜑-expression")
+            <*> switch (long "shuffle" <> help "Shuffle rules before applying")
+            <*> option auto (long "max-depth" <> metavar "DEPTH" <> help "Max amount of rewritng cycles" <> value 25 <> showDefault)
         )
 
 commandParser :: Parser Command
@@ -60,7 +68,7 @@
 
 handler :: SomeException -> IO ()
 handler e = case fromException e of
-  Just ExitSuccess -> pure ()  -- prevent printing error on --version etc.
+  Just ExitSuccess -> pure () -- prevent printing error on --version etc.
   _ -> do
     hPutStrLn stderr ("[error] " ++ displayException e)
     exitFailure
@@ -70,20 +78,36 @@
   cmd <- handleParseResult (execParserPure defaultPrefs parserInfo args)
   case cmd of
     CmdRewrite OptsRewrite {..} -> do
+      when (maxDepth < 0) $ throwIO (InvalidRewriteArguments "--max-depth must be non-negative")
       prog <- case phiInput of
         Just pth -> readFile =<< ensuredFile pth
         Nothing -> getContents' `catch` (\(e :: SomeException) -> throwIO (CouldNotReadFromStdin (show e)))
-      rules' <-
-        if nothing
-          then pure []
-          else do
-            paths <-
-              if null rules
-                then
-                  if normalize
-                    then throwIO NormalizationIsNotSupported
-                    else throwIO InvalidRewriteArguments
-                else mapM ensuredFile rules
-            mapM Y.yamlRule paths
-      rewritten <- rewrite prog rules'
-      putStrLn rewritten
+      rules' <- do
+        ordered <-
+          if nothing
+            then pure []
+            else
+              if normalize
+                then pure normalizationRules
+                else
+                  if null rules
+                    then throwIO (InvalidRewriteArguments "no --rule, no --normalize, no --nothing are provided")
+                    else do
+                      yamls <- mapM ensuredFile rules
+                      mapM Y.yamlRule yamls
+        if shuffle
+          then Misc.shuffle ordered
+          else pure ordered
+      program <- parseProgramThrows prog
+      rewritten <- rewrite' program rules' 0
+      putStrLn (printProgram rewritten)
+      where
+        rewrite' :: Program -> [Y.Rule] -> Integer -> IO Program
+        rewrite' prog rules count = do
+          if count == maxDepth
+            then pure prog
+            else do
+              rewritten <- rewrite prog rules
+              if rewritten == prog
+                then pure rewritten
+                else rewrite' rewritten rules (count + 1)
diff --git a/src/Condition.hs b/src/Condition.hs
new file mode 100644
--- /dev/null
+++ b/src/Condition.hs
@@ -0,0 +1,153 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module Condition where
+
+import Ast
+import Builder (buildAttribute, buildBinding)
+import Data.Aeson (FromJSON)
+import qualified Data.Map.Strict as M
+import GHC.Generics
+import GHC.IO (unsafePerformIO)
+import Matcher
+import Misc (allPathsIn)
+import Printer (printCondition, printExpression, printSubstitutions)
+import Yaml (normalizationRules)
+import qualified Yaml as Y
+
+-- Check if given attribute is present in given binding
+attrInBindings :: Attribute -> [Binding] -> Bool
+attrInBindings attr (bd : bds) = attrInBinding attr bd || attrInBindings attr bds
+  where
+    attrInBinding :: Attribute -> Binding -> Bool
+    attrInBinding attr (BiTau battr _) = attr == battr
+    attrInBinding attr (BiVoid battr) = attr == battr
+    attrInBinding AtLambda (BiLambda _) = True
+    attrInBinding AtDelta (BiDelta _) = True
+    attrInBinding _ _ = False
+attrInBindings _ _ = False
+
+-- Apply 'eq' yaml condition to attributes
+compareAttrs :: Attribute -> Attribute -> Subst -> Bool
+compareAttrs (AtMeta left) (AtMeta right) _ = left == right
+compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup meta mp of
+  Just (MvAttribute found) -> attr == found
+  _ -> False
+compareAttrs (AtMeta meta) attr (Subst mp) = case M.lookup meta mp of
+  Just (MvAttribute found) -> attr == found
+  _ -> False
+compareAttrs left right subst = right == left
+
+-- Convert Number to Integer
+numToInt :: Y.Number -> Subst -> Maybe Integer
+numToInt (Y.Ordinal (AtMeta meta)) (Subst mp) = case M.lookup meta mp of
+  Just (MvAttribute (AtAlpha idx)) -> Just idx
+  _ -> Nothing
+numToInt (Y.Ordinal (AtAlpha idx)) subst = Just idx
+numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of
+  Just (MvBindings bds) -> Just (toInteger (length bds))
+  _ -> Nothing
+numToInt (Y.Add left right) subst = case (numToInt left subst, numToInt right subst) of
+  (Just left_, Just right_) -> Just (left_ + right_)
+  _ -> Nothing
+numToInt (Y.Literal num) subst = Just num
+numToInt _ _ = Nothing
+
+meetCondition' :: Y.Condition -> Subst -> [Subst]
+meetCondition' (Y.Or []) subst = [subst]
+meetCondition' (Y.Or (cond : rest)) subst = do
+  let met = meetCondition' cond subst
+  if null met
+    then meetCondition' (Y.Or rest) subst
+    else met
+meetCondition' (Y.And []) subst = [subst]
+meetCondition' (Y.And (cond : rest)) subst = do
+  let met = meetCondition' cond subst
+  if null met
+    then []
+    else meetCondition' (Y.And rest) subst
+meetCondition' (Y.Not cond) subst = do
+  let met = meetCondition' cond subst
+  [subst | null met]
+meetCondition' (Y.In attr binding) subst =
+  case (buildAttribute attr subst, buildBinding binding subst) of
+    (Just attr, Just bds) -> [subst | attrInBindings attr bds] -- if attrInBindings attr bd then [subst] else []
+    (_, _) -> []
+meetCondition' (Y.Alpha (AtAlpha _)) subst = [subst]
+meetCondition' (Y.Alpha (AtMeta name)) (Subst mp) = case M.lookup name mp of
+  Just (MvAttribute (AtAlpha _)) -> [Subst mp]
+  _ -> []
+meetCondition' (Y.Alpha _) _ = []
+meetCondition' (Y.Eq (Y.CmpNum left) (Y.CmpNum right)) subst = case (numToInt left subst, numToInt right subst) of
+  (Just left_, Just right_) -> [subst | left_ == right_]
+  (_, _) -> []
+meetCondition' (Y.Eq (Y.CmpAttr left) (Y.CmpAttr right)) subst = [subst | compareAttrs left right subst]
+meetCondition' (Y.Eq _ _) _ = []
+-- @todo #89:30min Extend list of expressions. There are expressions where we can definitely say
+--  if this expression in normal form or not. In common case the expression in normal form if
+--  it does not match with any of normalization rules. But it's quite expensive operation comparing to
+--  simple list filtering and pattern matching. For example if expression is formation where all bindings are
+--  void, lambda, or delta - this expression in normal form and there's no need to try to match it with normalization
+--  rules. So we need find more such cases and introduce them.
+meetCondition' (Y.NF (ExMeta meta)) (Subst mp) = case M.lookup meta mp of
+  Just (MvExpression expr) -> case expr of
+    ExThis -> [Subst mp]
+    ExGlobal -> [Subst mp]
+    ExTermination -> [Subst mp]
+    ExDispatch ExThis _ -> [Subst mp]
+    ExDispatch ExGlobal _ -> [Subst mp]
+    ExDispatch ExTermination _ -> [] -- dd rule
+    ExApplication ExTermination _ -> [] -- dc rule
+    ExFormation [] -> [Subst mp]
+    _ -> [Subst mp | not (matchesAnyNormalizationRule expr normalizationRules)]
+  _ -> []
+  where
+    -- Returns True if given expression matches with any of given normalization rules
+    matchesAnyNormalizationRule :: Expression -> [Y.Rule] -> Bool
+    matchesAnyNormalizationRule _ [] = False
+    matchesAnyNormalizationRule expr (rule : rules) =
+      case matchProgramWithCondition (Y.pattern rule) (Y.when rule) (Program expr) of
+        Just matched -> not (null matched) || matchesAnyNormalizationRule expr rules
+        Nothing -> matchesAnyNormalizationRule expr rules
+meetCondition' (Y.NF _) _ = []
+meetCondition' (Y.FN (ExMeta meta)) (Subst mp) = case M.lookup meta mp of
+  Just (MvExpression expr) -> meetCondition' (Y.FN expr) (Subst mp)
+  _ -> []
+meetCondition' (Y.FN (ExFormation _)) subst = [subst]
+meetCondition' (Y.FN ExThis) subst = []
+meetCondition' (Y.FN ExGlobal) subst = [subst]
+meetCondition' (Y.FN (ExApplication expr (BiTau attr texpr))) subst = do
+  let onExpr = meetCondition' (Y.FN expr) subst
+      onTau = meetCondition' (Y.FN texpr) subst
+  [subst | not (null onExpr) && not (null onTau)]
+meetCondition' (Y.FN (ExDispatch expr _)) subst = meetCondition' (Y.FN expr) subst
+
+-- For each substitution check if it meetCondition to given condition
+-- If substitution does not meet the condition - it's thrown out
+-- and is not used in replacement
+meetCondition :: Y.Condition -> [Subst] -> [Subst]
+meetCondition _ [] = []
+meetCondition cond (subst : rest) = do
+  let first = meetCondition' cond subst
+  let next = meetCondition cond rest
+  if null first
+    then next
+    else head first : next
+
+-- Returns Just [...] if
+-- 1. program matches pattern and
+-- 2.1. condition is not present, or
+-- 2.2. condition is present and met
+-- Otherwise returns Nothing
+matchProgramWithCondition :: Expression -> Maybe Y.Condition -> Program -> Maybe [Subst]
+matchProgramWithCondition ptn condition program = do
+  let matched = matchProgram ptn program
+  if null matched
+    then Nothing
+    else case condition of
+      Nothing -> Just matched
+      Just cond -> do
+        let met = meetCondition cond matched
+        if null met
+          then Nothing
+          else Just met
diff --git a/src/Matcher.hs b/src/Matcher.hs
--- a/src/Matcher.hs
+++ b/src/Matcher.hs
@@ -133,13 +133,12 @@
 matchExpressionDeep :: Expression -> Expression -> [Subst]
 matchExpressionDeep ptn tgt = do
   let matched = matchExpression ptn tgt
-  if null matched
-    then case tgt of
-      ExFormation bds -> concatMap (`matchBindingExpression` ptn) bds
-      ExDispatch exp _ -> matchExpressionDeep ptn exp
-      ExApplication exp tau -> matchExpressionDeep ptn exp ++ matchBindingExpression tau ptn
-      _ -> []
-    else matched
+      deep = case tgt of
+        ExFormation bds -> concatMap (`matchBindingExpression` ptn) bds
+        ExDispatch exp _ -> matchExpressionDeep ptn exp
+        ExApplication exp tau -> matchExpressionDeep ptn exp ++ matchBindingExpression tau ptn
+        _ -> []
+  matched ++ deep
 
 matchProgram :: Expression -> Program -> [Subst]
 matchProgram ptn (Program exp) = matchExpressionDeep ptn exp
diff --git a/src/Misc.hs b/src/Misc.hs
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -10,15 +10,19 @@
 import Ast
 import Control.Exception
 import Control.Monad
-import System.Directory (doesDirectoryExist, doesFileExist, listDirectory)
-import System.FilePath ((</>))
-import Text.Printf (printf)
 import Data.Binary.IEEE754
-import Data.ByteString.Builder (word64BE, toLazyByteString)
-import Data.List (intercalate)
+import qualified Data.Bits as IOArray
+import Data.ByteString.Builder (toLazyByteString, word64BE)
 import Data.ByteString.Lazy (unpack)
 import qualified Data.ByteString.Lazy.UTF8 as U
+import Data.List (intercalate)
+import qualified Data.Vector as V
+import qualified Data.Vector.Mutable as M
 import Data.Word (Word8)
+import System.Directory (doesDirectoryExist, doesFileExist, listDirectory)
+import System.FilePath ((</>))
+import System.Random.Stateful
+import Text.Printf (printf)
 
 data FsException
   = FileDoesNotExist {file :: FilePath}
@@ -29,6 +33,22 @@
   show FileDoesNotExist {..} = printf "File '%s' does not exist" file
   show DirectoryDoesNotExist {..} = printf "Directory '%s' does not exist" dir
 
+-- Add void rho binding to the end of the list of any rho binding is not present
+withVoidRho :: [Binding] -> [Binding]
+withVoidRho bds = withVoidRho' bds False
+  where
+    withVoidRho' :: [Binding] -> Bool -> [Binding]
+    withVoidRho' [] True = []
+    withVoidRho' [] False = [BiVoid AtRho]
+    withVoidRho' (bd : bds) hasRho = 
+      case bd of
+        BiMeta _ -> bd : bds
+        BiVoid (AtMeta _) -> bd : bds
+        BiTau (AtMeta _) _ -> bd : bds
+        BiVoid AtRho -> bd : withVoidRho' bds True
+        BiTau AtRho _ -> bd : withVoidRho' bds True
+        _ -> bd : withVoidRho' bds hasRho
+
 ensuredFile :: FilePath -> IO FilePath
 ensuredFile pth = do
   exists <- doesFileExist pth
@@ -71,3 +91,18 @@
 -- "77-6F-72-6C-64"
 strToHex :: String -> String
 strToHex str = btsToHex (unpack (U.fromString str))
+
+-- Fast Fisher-Yates with mutable vectors.
+-- The function is generated by ChatGPT and claimed as
+-- fastest approach comparing to usage IOArray.
+-- >>> shuffle [1..20]
+-- [20,5,6,1,12,10,7,8,9,11,14,15,13,2,4,16,3,19,18,17]
+shuffle :: [a] -> IO [a]
+shuffle xs = do
+  gen <- newIOGenM =<< newStdGen
+  let n = length xs
+  v <- V.thaw (V.fromList xs) -- Mutable copy
+  forM_ [n - 1, n - 2 .. 1] $ \i -> do
+    j <- uniformRM (0, i) gen
+    M.swap v i j
+  V.toList <$> V.freeze v
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -23,7 +23,7 @@
 import Data.Sequence (mapWithIndex)
 import Data.Text.Internal.Fusion.Size (lowerBound)
 import Data.Void
-import Misc (numToHex, strToHex)
+import Misc (numToHex, strToHex, withVoidRho)
 import Text.Megaparsec
 import Text.Megaparsec.Char (alphaNumChar, char, digitChar, hexDigitChar, letterChar, lowerChar, space1, string, upperChar)
 import qualified Text.Megaparsec.Char.Lexer as L
@@ -50,7 +50,7 @@
             (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
             ( BiTau
                 (AtAlpha 0)
-                (ExFormation [BiDelta bts])
+                (ExFormation [BiDelta bts, BiVoid AtRho])
             )
         )
     )
@@ -169,7 +169,7 @@
         _ <- symbol ")"
         _ <- arrow
         ExFormation bs <- formation
-        return (BiTau attr' (ExFormation (voids ++ bs)))
+        return (BiTau attr' (ExFormation (withVoidRho (voids ++ bs))))
     ]
 
 metaBinding :: Parser Binding
@@ -271,7 +271,9 @@
 exHead :: Parser Expression
 exHead =
   choice
-    [ formation,
+    [ do
+        ExFormation bs <- formation
+        return (ExFormation (withVoidRho bs)),
       do
         _ <- choice [symbol "$", symbol "ξ"]
         return ExThis,
@@ -304,8 +306,7 @@
     <?> "expression head"
 
 application :: Expression -> [Binding] -> Expression
-application expr [binding] = ExApplication expr binding
-application expr (bd : bds) = application (application expr [bd]) bds
+application = foldl ExApplication
 
 -- tail optional part of application
 -- 1. any head + dispatch
diff --git a/src/Printer.hs b/src/Printer.hs
--- a/src/Printer.hs
+++ b/src/Printer.hs
@@ -4,7 +4,7 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Printer (printExpression, printProgram, printSubstitutions) where
+module Printer (printExpression, printProgram, printSubstitutions, printCondition) where
 
 import Ast
 import qualified Data.Map.Strict as Map
@@ -12,6 +12,8 @@
 import Prettyprinter
 import Prettyprinter.Render.String (renderString)
 import Text.Printf (vFmt)
+import Yaml (Condition)
+import qualified Yaml as Y
 
 prettyMeta :: String -> Doc ann
 prettyMeta meta = pretty "!" <> pretty meta
@@ -89,6 +91,9 @@
         rparen
       ]
 
+instance Pretty Condition where
+  pretty (Y.NF expr) = pretty "NF(" <+> pretty expr <+> rparen
+
 instance {-# OVERLAPPING #-} Pretty [Subst] where
   pretty :: [Subst] -> Doc ann
   pretty [] = pretty "[]"
@@ -96,6 +101,9 @@
 
 prettyPrint :: (Pretty a) => a -> String
 prettyPrint printable = renderString (layoutPretty defaultLayoutOptions (pretty printable))
+
+printCondition :: Condition -> String
+printCondition = prettyPrint
 
 printSubstitutions :: [Subst] -> String
 printSubstitutions = prettyPrint
diff --git a/src/Replacer.hs b/src/Replacer.hs
--- a/src/Replacer.hs
+++ b/src/Replacer.hs
@@ -25,7 +25,7 @@
   let (ptn : ptnsRest) = ptns
   let (repl : replsRest) = repls
   if expr == ptn
-    then (repl, ptnsRest, replsRest)
+    then replaceExpression repl ptnsRest replsRest
     else case expr of
       ExDispatch inner attr -> do
         let (expr', ptns', repls') = replaceExpression inner ptns repls
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -6,21 +6,22 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Rewriter (rewrite, meets) where
+module Rewriter (rewrite) where
 
 import Ast
 import Builder
+import qualified Condition as C
 import Control.Exception
+import qualified Data.Map.Strict as M
+import Data.Maybe (catMaybes, isJust)
 import Data.Text (intercalate)
-import Matcher (Subst (Subst), matchProgram, MetaValue (MvAttribute))
+import Matcher (MetaValue (MvAttribute, MvBindings, MvExpression), Subst (Subst), combine, combineMany, matchProgram, substEmpty, substSingle)
 import Misc (ensuredFile)
 import Parser (parseProgram, parseProgramThrows)
 import Printer (printExpression, printProgram, printSubstitutions)
 import Replacer (replaceProgram)
-import System.Directory
 import Text.Printf
 import qualified Yaml as Y
-import qualified Data.Map.Strict as M
 
 data RewriteException
   = CouldNotBuild {expr :: Expression, substs :: [Subst]}
@@ -40,65 +41,6 @@
       (printExpression ptn)
       (printExpression res)
 
-attrInBinding :: Attribute -> Binding -> Bool
-attrInBinding attr (BiTau battr _) = attr == battr
-attrInBinding attr (BiVoid battr) = attr == battr
-attrInBinding AtLambda (BiLambda _) = True
-attrInBinding AtDelta (BiDelta _) = True
-attrInBinding _ _ = False
-
--- Check if given attribute is present in given binding
-attrInBindings :: Attribute -> [Binding] -> Bool
-attrInBindings attr (bd : bds) = attrInBinding attr bd || attrInBindings attr bds
-attrInBindings _ _ = False
-
--- For each substitution check if it meets to given condition
--- If substitution does not meet the condition - it's thrown out
--- and is not used in replacement
-meets :: Y.Condition -> [Subst] -> [Subst]
-meets _ [] = []
--- OR
-meets (Y.Or []) substs = substs
-meets (Y.Or (cond : rest)) [subst] = case meets cond [subst] of
-  [] -> meets (Y.Or rest) [subst]
-  substs -> substs
--- AND
-meets (Y.And []) substs = substs
-meets (Y.And (cond : rest)) [subst] = case meets cond [subst] of
-  [] -> []
-  _ -> meets (Y.And rest) [subst]
--- NOT
-meets (Y.Not cond) [subst] = case meets cond [subst] of
-  [] -> [subst]
-  _ -> []
--- IN
-meets (Y.In attr binding) [subst] =
-  case (buildAttribute attr subst, buildBinding binding subst) of
-    (Just attr, Just bds) -> [subst | attrInBindings attr bds] -- if attrInBindings attr bd then [subst] else []
-    (_, _) -> []
--- ALPHA
-meets (Y.Alpha (AtAlpha _)) substs = substs
-meets (Y.Alpha (AtMeta name)) [Subst mp] = case M.lookup name mp of
-  Just (MvAttribute (AtAlpha _)) -> [Subst mp]
-  _ -> []
-meets (Y.Alpha _) _ = []
--- EQ
-meets (Y.Eq (AtMeta left) (AtMeta right)) [subst] = [subst | left == right]
-meets (Y.Eq attr (AtMeta meta)) [Subst mp] = case M.lookup meta mp of
-  Just (MvAttribute found) -> [Subst mp | attr == found]
-  _ -> []
-meets (Y.Eq (AtMeta meta) attr) [Subst mp] = case M.lookup meta mp of
-  Just (MvAttribute found) -> [Subst mp | attr == found]
-  _ -> []
-meets (Y.Eq left right) [subst] = [subst | right == left]
--- Any condition with many substitutions
-meets cond (subst : rest) = do
-  let first = meets cond [subst]
-      next = meets cond rest
-  if null first
-    then next
-    else head first : next
-
 -- Build pattern and result expression and replace patterns to results in given program
 buildAndReplace :: Program -> Expression -> Expression -> [Subst] -> IO Program
 buildAndReplace program ptn res substs =
@@ -109,26 +51,32 @@
     (Nothing, _) -> throwIO (CouldNotBuild ptn substs)
     (_, Nothing) -> throwIO (CouldNotBuild res substs)
 
-applyRules :: Program -> [Y.Rule] -> IO Program
-applyRules program [] = pure program
-applyRules program [rule] = do
+-- Extend list of given substitutions with extra substitutions from 'where' yaml rule section
+extraSubstitutions :: Program -> Maybe [Y.Extra] -> [Subst] -> [Subst]
+extraSubstitutions prog extras substs = case extras of
+  Nothing -> substs
+  Just extras' -> do
+    catMaybes
+      [ case Y.meta extra of
+          ExMeta name -> do
+            let func = Y.function extra
+                args = Y.args extra
+            expr <- buildExpressionFromFunction func args subst prog
+            combine (substSingle name (MvExpression expr)) subst
+          _ -> Just subst
+        | subst <- substs,
+          extra <- extras'
+      ]
+
+rewrite :: Program -> [Y.Rule] -> IO Program
+rewrite program [] = pure program
+rewrite program (rule : rest) = do
   let ptn = Y.pattern rule
       res = Y.result rule
-  case matchProgram ptn program of
-    [] -> pure program
-    substs -> do
-      let replaced = buildAndReplace program ptn res
-      case Y.when rule of
-        Just cond -> case meets cond substs of
-          [] -> pure program
-          substs' -> replaced substs'
-        Nothing -> replaced substs
-applyRules program (rule : rest) = do
-  prog <- applyRules program [rule]
-  applyRules prog rest
-
-rewrite :: String -> [Y.Rule] -> IO String
-rewrite prog rules = do
-  program <- parseProgramThrows prog
-  rewritten <- applyRules program rules
-  pure (printProgram rewritten)
+      condition = Y.when rule
+      replaced = buildAndReplace program ptn res
+      extended = extraSubstitutions program (Y.where_ rule)
+  prog <- case C.matchProgramWithCondition ptn condition program of
+    Nothing -> pure program
+    Just matched -> replaced (extended matched)
+  rewrite prog rest
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -1,6 +1,7 @@
-{-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
@@ -10,14 +11,13 @@
 import Ast
 import Control.Applicative (asum)
 import Data.Aeson
-import Data.Aeson.KeyMap (keys)
-import Data.String (IsString (..))
+import qualified Data.ByteString as BS
+import Data.FileEmbed (embedDir)
 import Data.Text (unpack)
 import Data.Yaml (Parser)
 import qualified Data.Yaml as Yaml
-import Debug.Trace
-import GHC.Base
 import GHC.Generics
+import Misc (allPathsIn)
 import Parser
 
 parseJSON' :: String -> (String -> Either String a) -> Value -> Parser a
@@ -43,9 +43,36 @@
             Left err -> fail err
             Right attr -> pure attr
       )
+
 instance FromJSON Binding where
   parseJSON = parseJSON' "Binding" parseBinding
 
+instance FromJSON Number where
+  parseJSON v = case v of
+    Object o ->
+      asum
+        [ Ordinal <$> o .: "ordinal",
+          Length <$> o .: "length",
+          do
+            vals <- o .: "add"
+            case vals of
+              [first_, second_] -> do
+                first <- parseJSON first_
+                second <- parseJSON second_
+                pure (Add first second)
+              _ -> fail "'add' requires exactly two elements"
+        ]
+    Number num -> pure (Literal (round num))
+    _ ->
+      fail "Expected a numerable expression (object or number)"
+
+instance FromJSON Comparable where
+  parseJSON v =
+    asum
+      [ CmpAttr <$> parseJSON v,
+        CmpNum <$> parseJSON v
+      ]
+
 instance FromJSON Condition where
   parseJSON =
     withObject
@@ -56,13 +83,12 @@
               Or <$> v .: "or",
               Not <$> v .: "not",
               Alpha <$> v .: "alpha",
+              NF <$> v .: "nf",
+              FN <$> v .: "fn",
               do
                 vals <- v .: "eq"
                 case vals of
-                  [left_, right_] -> do
-                    left <- parseJSON left_
-                    right <- parseJSON right_
-                    pure (Eq left right)
+                  [left_, right_] -> Eq <$> parseJSON left_ <*> parseJSON right_
                   _ -> fail "'eq' must contain exactly two elements",
               do
                 vals <- v .: "in"
@@ -75,22 +101,66 @@
             ]
       )
 
+instance FromJSON Extra where
+  parseJSON = genericParseJSON defaultOptions
+
+instance FromJSON Rule where
+  parseJSON =
+    genericParseJSON
+      defaultOptions
+        { fieldLabelModifier = \case
+            "where_" -> "where"
+            other -> other
+        }
+
+data Number
+  = Ordinal Attribute
+  | Length Binding
+  | Add Number Number
+  | Literal Integer
+  deriving (Generic, Show)
+
+data Comparable
+  = CmpAttr Attribute
+  | CmpNum Number
+  deriving (Generic, Show)
+
 data Condition
   = And [Condition]
   | Or [Condition]
   | In Attribute Binding
   | Not Condition
   | Alpha Attribute
-  | Eq Attribute Attribute
+  | Eq Comparable Comparable
+  | NF Expression
+  | FN Expression
   deriving (Generic, Show)
 
+data Extra = Extra
+  { meta :: Expression,
+    function :: String,
+    args :: [Expression]
+  }
+  deriving (Generic, Show)
+
 data Rule = Rule
   { name :: Maybe String,
     pattern :: Expression,
     result :: Expression,
-    when :: Maybe Condition
+    when :: Maybe Condition,
+    where_ :: Maybe [Extra]
   }
-  deriving (Generic, FromJSON, Show)
+  deriving (Generic, Show)
+
+normalizationRules :: [Rule]
+{-# NOINLINE normalizationRules #-}
+normalizationRules = map decodeRule $(embedDir "resources")
+  where
+    decodeRule :: (FilePath, BS.ByteString) -> Rule
+    decodeRule (path, bs) =
+      case Yaml.decodeEither' bs of
+        Right r -> r
+        Left err -> error $ "YAML parse error in " ++ path ++ ": " ++ show err
 
 yamlRule :: FilePath -> IO Rule
 yamlRule = Yaml.decodeFileThrow
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -7,22 +7,24 @@
 module CLISpec (spec) where
 
 import CLI (runCLI)
-import System.IO.Silently (capture_)
-import System.Directory (removeFile)
-import Test.Hspec
-import System.IO
 import Control.Exception
+import Control.Monad (unless)
+import Data.List (isInfixOf)
+import Data.Version (showVersion)
 import GHC.IO.Handle
 import Paths_phino (version)
-import Data.Version (showVersion)
+import System.Directory (removeFile)
+import System.Exit (ExitCode (ExitFailure))
+import System.IO
+import System.IO.Silently (capture_)
+import Test.Hspec
 
-withRedirectedStdin :: String -> IO a -> IO a
-withRedirectedStdin input action = do
-  bracket (openTempFile "." "stdin.tmp") cleanup $ \(filePath, h) -> do
+withStdin :: String -> IO a -> IO a
+withStdin input action = do
+  bracket (openTempFile "." "stdinXXXXXX.tmp") cleanup $ \(filePath, h) -> do
     hSetEncoding h utf8
     hPutStr h input
     hFlush h
-    hSeek h AbsoluteSeek 0
     hClose h
     withFile filePath ReadMode $ \hIn -> do
       hSetEncoding hIn utf8
@@ -34,11 +36,50 @@
     restoreStdin orig = hDuplicateTo orig stdin >> hClose orig
     cleanup (fp, _) = removeFile fp
 
+withStdout :: IO a -> IO (String, a)
+withStdout action =
+  bracket
+    (openTempFile "." "stdoutXXXXXX.tmp")
+    cleanup
+    ( \(path, hTmp) -> do
+        hSetEncoding hTmp utf8
+        oldOut <- hDuplicate stdout
+        oldErr <- hDuplicate stderr
+        hDuplicateTo hTmp stdout
+        hDuplicateTo hTmp stderr
+
+        result <-
+          action `finally` do
+            hFlush stdout
+            hFlush stderr
+            hDuplicateTo oldOut stdout >> hClose oldOut
+            hDuplicateTo oldErr stderr >> hClose oldErr
+            hClose hTmp
+
+        captured <- readFile path
+        _ <- evaluate (length captured)
+        return (captured, result)
+    )
+  where
+    cleanup (fp, _) = removeFile fp
+
+testCLI :: [String] -> String -> Expectation
+testCLI args output = do
+  out <- capture_ (runCLI args)
+  unless (output `isInfixOf` out) $
+    expectationFailure
+      ("Expected that output contains:\n" ++ output ++ "\nbut got:\n" ++ out)
+
+testCLIFailed :: [String] -> String -> Expectation
+testCLIFailed args output = withStdin "" $ do
+  (out, result) <- withStdout (try (runCLI args) :: IO (Either ExitCode ()))
+  out `shouldContain` output
+  result `shouldBe` Left (ExitFailure 1)
+
 spec :: Spec
 spec = do
   it "prints version" $ do
-    output <- capture_ (runCLI ["--version"])
-    output `shouldContain` showVersion version
+    testCLI ["--version"] (showVersion version)
 
   it "prints help" $ do
     output <- capture_ (runCLI ["--help"])
@@ -46,19 +87,56 @@
     output `shouldContain` "Usage:"
 
   describe "rewrites" $ do
-    it "desugares with --nothing flag from file" $ do
-      let args = ["rewrite", "--nothing", "--phi-input=test-resources/cli/desugar.phi"]
-      output <- capture_ (runCLI args)
-      output `shouldContain` "Φ ↦ ⟦\n  foo ↦ Φ.org.eolang\n⟧"
+    it "desugares with --nothing flag from file" $
+      testCLI
+        ["rewrite", "--nothing", "--phi-input=test-resources/cli/desugar.phi"]
+        "Φ ↦ ⟦\n  foo ↦ Φ.org.eolang,\n  ρ ↦ ∅\n⟧"
 
-    it "desugares with --nothing flag from stdin" $ do
-      withRedirectedStdin "{[[foo ↦ QQ]]}" $ do
-        let args = ["rewrite", "--nothing"]
-        output <- capture_ (runCLI args)
-        output `shouldContain` "Φ ↦ ⟦\n  foo ↦ Φ.org.eolang\n⟧"
+    it "desugares with --nothing flag from stdin" $
+      withStdin "{[[foo ↦ QQ]]}" $
+        testCLI ["rewrite", "--nothing"] "Φ ↦ ⟦\n  foo ↦ Φ.org.eolang,\n  ρ ↦ ∅\n⟧"
 
-    it "rewrites with single rule" $ do
-      withRedirectedStdin "{T(x -> Q.y)}" $ do
-        let args = ["rewrite", "--rule=resources/dc.yaml"]
-        output <- capture_ (runCLI args)
-        output `shouldContain` "Φ ↦ ⊥"
+    it "rewrites with single rule" $
+      withStdin "{T(x -> Q.y)}" $
+        testCLI ["rewrite", "--rule=resources/dc.yaml"] "Φ ↦ ⊥"
+
+    it "normalizes with --normalize flag" $
+      testCLI
+        ["rewrite", "--normalize", "--phi-input=test-resources/cli/normalize.phi"]
+        ( unlines
+            [ "Φ ↦ ⟦",
+              "  x ↦ ⟦",
+              "    ρ ↦ ⟦",
+              "      y ↦ ⟦ ρ ↦ ∅ ⟧,",
+              "      ρ ↦ ∅",
+              "    ⟧",
+              "  ⟧,",
+              "  ρ ↦ ∅",
+              "⟧"
+            ]
+        )
+
+    it "fails with negative --max-depth" $
+      testCLIFailed
+        ["rewrite", "--max-depth=-1"]
+        "--max-depth must be non-negative"
+
+    it "fails with no rewriting options provided" $
+      testCLIFailed
+        ["rewrite"]
+        "no --rule, no --normalize, no --nothing are provided"
+
+    it "normalizes from stdin" $ do
+      withStdin "Φ ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ [[ ]]) ⟧" $
+        testCLI
+          ["rewrite", "--normalize"]
+          ( unlines
+              [ "Φ ↦ ⟦",
+                "  a ↦ ⟦",
+                "    b ↦ ⟦ ρ ↦ ∅ ⟧,",
+                "    ρ ↦ ∅",
+                "  ⟧,",
+                "  ρ ↦ ∅",
+                "⟧"
+              ]
+          )
diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/ConditionSpec.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveGeneric #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module ConditionSpec where
+
+import Ast (Expression, Program (Program))
+import Condition (meetCondition)
+import Control.Monad
+import Data.Aeson
+import Data.Yaml qualified as Y
+import GHC.Generics
+import Matcher (matchProgram)
+import Misc
+import Printer (printSubstitutions)
+import System.FilePath
+import Test.Hspec (Spec, describe, expectationFailure, it, runIO)
+import Yaml qualified as Y
+
+data ConditionPack = ConditionPack
+  { expression :: Expression,
+    pattern :: Expression,
+    condition :: Y.Condition
+  }
+  deriving (Generic, FromJSON, Show)
+
+spec :: Spec
+spec = do
+  describe "check conditions" $ do
+    let resources = "test-resources/condition-packs"
+    packs <- runIO (allPathsIn resources)
+    forM_
+      packs
+      ( \pth -> it (makeRelative resources pth) $ do
+          pack <- Y.decodeFileThrow pth :: IO ConditionPack
+          let matched = matchProgram (pattern pack) (Program (expression pack))
+          unless (matched /= []) (expectationFailure "List of matched substitutions is empty which is not expected")
+          let met = meetCondition (condition pack) matched
+          when
+            (null met)
+            ( expectationFailure $
+                "List of substitution after condition check must be not empty\nOriginal substitutions:\n"
+                  ++ printSubstitutions matched
+            )
+      )
diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs
--- a/test/MatcherSpec.hs
+++ b/test/MatcherSpec.hs
@@ -50,15 +50,19 @@
             ],
           [[("a", MvAttribute (AtLabel "x"))], [("a", MvAttribute (AtLabel "y"))]]
         ),
-        ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]])]",
+        ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]] ), (!e >> Q)]",
           ExMeta "e",
           ExFormation [BiTau (AtLabel "x") ExGlobal],
-          [[("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]))]]
+          [ [("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]))],
+            [("e", MvExpression ExGlobal)]
+          ]
         ),
-        ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang)]",
+        ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang), (!e >> Q, !a >> org)]",
           ExDispatch (ExMeta "e") (AtMeta "a"),
           ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"),
-          [[("e", MvExpression (ExDispatch ExGlobal (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]]
+          [ [("e", MvExpression (ExDispatch ExGlobal (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))],
+            [("e", MvExpression ExGlobal), ("a", MvAttribute (AtLabel "org"))]
+          ]
         ),
         ( "⟦!B1, !a ↦ ∅, !B2⟧.!a => ⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧) => [(!B1 >> ⟦x ↦ ξ.t⟧, !a >> t, !B2 >> ⟦⟧ )]",
           ExDispatch (ExFormation [BiMeta "B1", BiVoid (AtMeta "a"), BiMeta "B2"]) (AtMeta "a"),
diff --git a/test/MiscSpec.hs b/test/MiscSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/MiscSpec.hs
@@ -0,0 +1,50 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module MiscSpec where
+
+import Control.Monad (forM_)
+import Misc (withVoidRho)
+import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, shouldBe)
+import Ast
+
+testWithVoidRho :: [(String, [Binding], [Binding])] -> SpecWith (Arg Expectation)
+testWithVoidRho useCases =
+  forM_ useCases $ \(desc, before, after) ->
+    it desc $ withVoidRho before `shouldBe` after
+
+spec :: Spec
+spec = do
+  describe "with void rho binding" $ do
+    testWithVoidRho
+      [ ( "[[x -> ?]] => [[x -> ?, ^ -> ?]]",
+          [BiVoid (AtLabel "x")],
+          [BiVoid (AtLabel "x"), BiVoid AtRho]
+        ),
+        ( "[[^ -> ?, x -> ?]] => [[^ -> ?, x -> ?]]",
+          [BiVoid AtRho, BiVoid (AtLabel "x")],
+          [BiVoid AtRho, BiVoid (AtLabel "x")]
+        ),
+        ( "[[^ -> Q.x, x -> $.y]] => [[^ -> Q.x, x -> $.y]]",
+          [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))],
+          [BiTau AtRho (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
+        ),
+        ("[[!B]] => [[!B]]", [BiMeta "B"], [BiMeta "B"]),
+        ("[[x -> ?, !B]] => [[x -> ?, !B]]", [BiVoid (AtLabel "x"), BiMeta "B"], [BiVoid (AtLabel "x"), BiMeta "B"]),
+        ( "[[x -> ?, !B, y -> ?]] => [[x -> ?, !B, y -> ?]]",
+          [BiVoid (AtLabel "x"), BiMeta "B", BiVoid (AtLabel "y")],
+          [BiVoid (AtLabel "x"), BiMeta "B", BiVoid (AtLabel "y")]
+        ),
+        ( "[[^ -> ?, !B, y -> ?]] => [[^ -> ?, !B, y -> ?]]",
+          [BiVoid AtRho, BiMeta "B", BiVoid (AtLabel "y")],
+          [BiVoid AtRho, BiMeta "B", BiVoid (AtLabel "y")]
+        ),
+        ( "[[!a -> ?, x -> $.y]] => [[!a -> Q.x, x -> $.y]]",
+          [BiVoid (AtMeta "a"), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))],
+          [BiVoid (AtMeta "a"), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
+        ),
+        ( "[[!a -> Q.x, x -> $.y]] => [[!a -> Q.x, x -> $.y]]",
+          [BiTau (AtMeta "a") (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))],
+          [BiTau (AtMeta "a") (ExDispatch ExGlobal (AtLabel "x")), BiTau AtRho (ExDispatch ExTermination (AtLabel "y"))]
+        )
+      ]
diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs
--- a/test/ParserSpec.hs
+++ b/test/ParserSpec.hs
@@ -30,44 +30,44 @@
   describe "parse program" $
     test
       parseProgram
-      [ ("Q -> [[]]", Just (Program (ExFormation []))),
+      [ ("Q -> [[]]", Just (Program (ExFormation [BiVoid AtRho]))),
         ("Q -> T(x -> Q)", Just (Program (ExApplication ExTermination (BiTau (AtLabel "x") ExGlobal)))),
         ("Q -> Q.org.eolang", Just (Program (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")))),
-        ("Q -> [[x -> $, y -> ?]]", Just (Program (ExFormation [BiTau (AtLabel "x") ExThis, BiVoid (AtLabel "y")]))),
-        ("{[[foo ↦ QQ]]}", Just (Program (ExFormation [BiTau (AtLabel "foo") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"))])))
+        ("Q -> [[x -> $, y -> ?]]", Just (Program (ExFormation [BiTau (AtLabel "x") ExThis, BiVoid (AtLabel "y"), BiVoid AtRho]))),
+        ("{[[foo ↦ QQ]]}", Just (Program (ExFormation [BiTau (AtLabel "foo") (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")), BiVoid AtRho])))
       ]
 
   describe "parse expression" $
     test
       parseExpression
       [ ("Q.!a", Just (ExDispatch ExGlobal (AtMeta "a"))),
-        ("[[]](!a1 -> $)", Just (ExApplication (ExFormation []) (BiTau (AtMeta "a1") ExThis))),
+        ("[[]](!a1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtMeta "a1") ExThis))),
         ( "[[]](~0 -> $)(~11 -> Q)",
           Just
             ( ExApplication
                 ( ExApplication
-                    (ExFormation [])
+                    (ExFormation [BiVoid AtRho])
                     (BiTau (AtAlpha 0) ExThis)
                 )
                 (BiTau (AtAlpha 11) ExGlobal)
             )
         ),
-        ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExThis)) (BiTau (AtLabel "y") ExGlobal))),
+        ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtLabel "x") ExThis)) (BiTau (AtLabel "y") ExGlobal))),
         ("[[!B, !B1]]", Just (ExFormation [BiMeta "B", BiMeta "B1"])),
         ("[[!B2, !a2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "a2") ExThis])),
         ("!e0", Just (ExMeta "e0")),
-        ("[[x -> !e]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e")])),
+        ("[[x -> !e]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e"), BiVoid AtRho])),
         ("[[!a -> !e1]]", Just (ExFormation [BiTau (AtMeta "a") (ExMeta "e1")])),
         ("Q * !t", Just (ExMetaTail ExGlobal "t")),
-        ("[[]](x -> $) * !t1", Just (ExMetaTail (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExThis)) "t1")),
-        ("[[D> --]]", Just (ExFormation [BiDelta "--"])),
-        ("[[D> 1F-]]", Just (ExFormation [BiDelta "1F-"])),
-        ("[[\n  L> Func,\n  D> 00-\n]]", Just (ExFormation [BiLambda "Func", BiDelta "00-"])),
-        ("[[D> 1F-2A-00]]", Just (ExFormation [BiDelta "1F-2A-00"])),
-        ("[[D> !b0]]", Just (ExFormation [BiMetaDelta "b0"])),
-        ("[[L> Function]]", Just (ExFormation [BiLambda "Function"])),
-        ("[[L> !F3]]", Just (ExFormation [BiMetaLambda "F3"])),
-        ("[[x() -> [[]] ]]", Just (ExFormation [BiTau (AtLabel "x") (ExFormation [])])),
+        ("[[]](x -> $) * !t1", Just (ExMetaTail (ExApplication (ExFormation [BiVoid AtRho]) (BiTau (AtLabel "x") ExThis)) "t1")),
+        ("[[D> --]]", Just (ExFormation [BiDelta "--", BiVoid AtRho])),
+        ("[[D> 1F-]]", Just (ExFormation [BiDelta "1F-", BiVoid AtRho])),
+        ("[[\n  L> Func,\n  D> 00-\n]]", Just (ExFormation [BiLambda "Func", BiDelta "00-", BiVoid AtRho])),
+        ("[[D> 1F-2A-00]]", Just (ExFormation [BiDelta "1F-2A-00", BiVoid AtRho])),
+        ("[[D> !b0]]", Just (ExFormation [BiMetaDelta "b0", BiVoid AtRho])),
+        ("[[L> Function]]", Just (ExFormation [BiLambda "Function", BiVoid AtRho])),
+        ("[[L> !F3]]", Just (ExFormation [BiMetaLambda "F3", BiVoid AtRho])),
+        ("[[x() -> [[]] ]]", Just (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])),
         ( "[[y(^,@,z) -> [[q -> Q.a]] ]]",
           Just
             ( ExFormation
@@ -79,7 +79,8 @@
                           BiVoid (AtLabel "z"),
                           BiTau (AtLabel "q") (ExDispatch ExGlobal (AtLabel "a"))
                         ]
-                    )
+                    ),
+                  BiVoid AtRho
                 ]
             )
         ),
@@ -118,7 +119,8 @@
                     (ExDispatch ExThis (AtMeta "a")),
                   BiTau
                     (AtLabel "q")
-                    (ExMeta "e")
+                    (ExMeta "e"),
+                  BiVoid AtRho
                 ]
             )
         ),
@@ -133,7 +135,7 @@
                         )
                         (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "y")))
                     )
-                    (BiTau (AtAlpha 2) (ExDispatch (ExFormation []) (AtLabel "z")))
+                    (BiTau (AtAlpha 2) (ExDispatch (ExFormation [BiVoid AtRho]) (AtLabel "z")))
                 )
                 ( BiTau
                     (AtAlpha 3)
@@ -159,7 +161,7 @@
                                 (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
                                 ( BiTau
                                     (AtAlpha 0)
-                                    (ExFormation [BiDelta "40-14-00-00-00-00-00-00"])
+                                    (ExFormation [BiDelta "40-14-00-00-00-00-00-00", BiVoid AtRho])
                                 )
                             )
                         )
@@ -178,7 +180,7 @@
                                         (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
                                         ( BiTau
                                             (AtAlpha 0)
-                                            (ExFormation [BiDelta "40-14-00-00-00-00-00-00"])
+                                            (ExFormation [BiDelta "40-14-00-00-00-00-00-00", BiVoid AtRho])
                                         )
                                     )
                                 )
@@ -196,7 +198,7 @@
                                             (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
                                             ( BiTau
                                                 (AtAlpha 0)
-                                                (ExFormation [BiDelta "68-65-6C-6C-6F"])
+                                                (ExFormation [BiDelta "68-65-6C-6C-6F", BiVoid AtRho])
                                             )
                                         )
                                     )
diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs
--- a/test/PrinterSpec.hs
+++ b/test/PrinterSpec.hs
@@ -28,11 +28,11 @@
           )
           [ ("Q -> $", "Φ ↦ ξ"),
             ("Q -> Q.org.x", "Φ ↦ Φ.org.x"),
-            ("Q -> [[]]", "Φ ↦ ⟦⟧"),
-            ("Q -> [[@ -> ?]](~1 -> Q.x)", "Φ ↦ ⟦ φ ↦ ∅ ⟧(\n  α1 ↦ Φ.x\n)"),
+            ("Q -> [[]]", "Φ ↦ ⟦ ρ ↦ ∅ ⟧"),
+            ("Q -> [[@ -> ?]](~1 -> Q.x)", "Φ ↦ ⟦\n  φ ↦ ∅,\n  ρ ↦ ∅\n⟧(\n  α1 ↦ Φ.x\n)"),
             ("Q -> !e * !t", "Φ ↦ !e * !t"),
             ( "Q -> [[D> 00-,L> F,^ -> ?,!B,@ -> [[y -> ?]]]]",
-              "Φ ↦ ⟦\n  Δ ⤍ 00-,\n  λ ⤍ F,\n  ρ ↦ ∅,\n  !B,\n  φ ↦ ⟦ y ↦ ∅ ⟧\n⟧"
+              "Φ ↦ ⟦\n  Δ ⤍ 00-,\n  λ ⤍ F,\n  ρ ↦ ∅,\n  !B,\n  φ ↦ ⟦\n    y ↦ ∅,\n    ρ ↦ ∅\n  ⟧\n⟧"
             )
           ]
     test printProgram useCases
diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs
--- a/test/RewriterSpec.hs
+++ b/test/RewriterSpec.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE LambdaCase #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
@@ -7,16 +8,20 @@
 
 module RewriterSpec where
 
-import Control.Monad (forM_)
+import Control.Monad (forM_, unless)
 import Data.Aeson
+import Data.Char (isSpace)
+import Data.Foldable (foldlM)
 import Data.Yaml qualified as Yaml
 import GHC.Generics
 import Misc (allPathsIn, ensuredFile)
+import Parser (parseProgramThrows)
+import Printer (printProgram)
 import Rewriter (rewrite)
 import System.FilePath (makeRelative, replaceExtension, (</>))
-import Test.Hspec (Spec, describe, it, runIO, shouldBe)
+import Test.Hspec (Spec, describe, expectationFailure, it, pending, runIO)
+import Yaml (normalizationRules)
 import Yaml qualified as Y
-import Data.Char (isSpace)
 
 data Rules = Rules
   { basic :: Maybe [String],
@@ -27,10 +32,22 @@
 data YamlPack = YamlPack
   { input :: String,
     output :: String,
-    rules :: Maybe Rules
+    rules :: Maybe Rules,
+    skip :: Maybe Bool,
+    repeat_ :: Maybe Integer,
+    normalize :: Maybe Bool
   }
-  deriving (Generic, FromJSON, Show)
+  deriving (Generic, Show)
 
+instance FromJSON YamlPack where
+  parseJSON =
+    genericParseJSON
+      defaultOptions
+        { fieldLabelModifier = \case
+            "repeat_" -> "repeat"
+            other -> other
+        }
+
 yamlPack :: FilePath -> IO YamlPack
 yamlPack = Yaml.decodeFileThrow
 
@@ -44,24 +61,44 @@
     packs <- runIO (allPathsIn resources)
     forM_
       packs
-      ( \pth -> do
-          pack <- runIO $ yamlPack pth
-          let output' = output pack
-              input' = input pack
-          rules' <- case rules pack of
-            Just _rules -> case custom _rules of
-              Just custom' -> pure custom'
-              _ -> case basic _rules of
-                Just basic' ->
-                  runIO $
-                    mapM
-                      ( \name -> do
-                          yaml <- ensuredFile ("resources" </> replaceExtension name ".yaml")
-                          Y.yamlRule yaml
-                      )
-                      basic'
-                _ -> pure []
-            Nothing -> pure []
-          rewritten <- runIO $ rewrite input' rules'
-          it (makeRelative resources pth) (noSpaces rewritten `shouldBe` noSpaces output')
+      ( \pth -> it (makeRelative resources pth) $ do
+          pack <- yamlPack pth
+          let normalize' = case normalize pack of
+                Just _ -> True
+                _ -> False
+              repeat' =
+                if normalize'
+                  then 50
+                  else case repeat_ pack of
+                    Just num -> num
+                    _ -> 1
+          case skip pack of
+            Just True -> pending
+            _ -> do
+              program <- parseProgramThrows (input pack)
+              rules' <- case rules pack of
+                Just _rules -> case custom _rules of
+                  Just custom' -> pure custom'
+                  _ -> case basic _rules of
+                    Just basic' ->
+                      mapM
+                        ( \name -> do
+                            yaml <- ensuredFile ("resources" </> replaceExtension name ".yaml")
+                            Y.yamlRule yaml
+                        )
+                        basic'
+                    _ -> pure []
+                Nothing ->
+                  if normalize'
+                    then pure normalizationRules
+                    else pure []
+              rewritten <- foldlM (\prog _ -> rewrite prog rules') program [1 .. repeat']
+              result' <- parseProgramThrows (output pack)
+              unless (rewritten == result') $
+                expectationFailure
+                  ( "Wrong rewritten program. Expected:\n"
+                      ++ printProgram result'
+                      ++ "\nGot:\n"
+                      ++ printProgram rewritten
+                  )
       )
diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs
--- a/test/YamlSpec.hs
+++ b/test/YamlSpec.hs
@@ -1,30 +1,13 @@
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE DeriveGeneric #-}
-
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
 module YamlSpec where
 
-import Ast (Expression, Program (Program))
 import Control.Monad
-import Data.Aeson
-import Data.Yaml qualified as Y
-import GHC.Generics
-import Matcher (matchProgram)
 import Misc
-import Printer (printSubstitutions)
-import Rewriter (meets)
 import System.FilePath
-import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldReturn)
-import Yaml (Condition, yamlRule)
-
-data ConditionPack = ConditionPack
-  { expression :: Expression,
-    pattern :: Expression,
-    condition :: Condition
-  }
-  deriving (Generic, FromJSON, Show)
+import Test.Hspec (Spec, describe, it, runIO, shouldReturn)
+import Yaml (yamlRule)
 
 spec :: Spec
 spec = do
@@ -36,24 +19,4 @@
       ( \pth -> it (makeRelative resources pth) $ do
           _ <- yamlRule pth
           pure () `shouldReturn` ()
-      )
-
-  describe "check conditions" $ do
-    let resources = "test-resources/condition-packs"
-    packs <- runIO (allPathsIn resources)
-    forM_
-      packs
-      ( \pth -> it (makeRelative resources pth) $ do
-          pack <- Y.decodeFileThrow pth :: IO ConditionPack
-          let matched = matchProgram (pattern pack) (Program (expression pack))
-          unless (matched /= []) (expectationFailure "List of matched substitutions is empty which is not expected")
-          let met = meets (condition pack) matched
-          unless
-            (met == matched)
-            ( expectationFailure $
-                "Condition must not decrease the list of substitutions\nExpected:\n"
-                  ++ printSubstitutions matched
-                  ++ "\nGot:\n" 
-                  ++ printSubstitutions met
-            )
       )