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.2
+version:            0.0.0.3
 license:            MIT
 synopsis:           Command-Line Manipulator of 𝜑-Calculus Expressions
 description:        Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/src/Ast.hs b/src/Ast.hs
--- a/src/Ast.hs
+++ b/src/Ast.hs
@@ -16,7 +16,7 @@
   | ExGlobal                              -- Q
   | ExTermination                         -- T
   | ExMeta String                         -- !e
-  | ExApplication Expression [Binding]    -- expr(attr -> expr)
+  | ExApplication Expression Binding      -- expr(attr -> expr)
   | ExDispatch Expression Attribute       -- expr.attr
   | ExMetaTail Expression String          -- expr * !t
   deriving (Eq, Show, Generic)
diff --git a/src/Builder.hs b/src/Builder.hs
--- a/src/Builder.hs
+++ b/src/Builder.hs
@@ -8,7 +8,7 @@
   ( buildExpressions,
     buildExpression,
     buildAttribute,
-    buildBindings,
+    buildBinding
   )
 where
 
@@ -65,10 +65,11 @@
   dispatched <- buildExpression expr subst
   attr <- buildAttribute attr subst
   return (ExDispatch dispatched attr)
-buildExpression (ExApplication expr taus) subst = do
+buildExpression (ExApplication expr (BiTau battr bexpr)) subst = do
   applied <- buildExpression expr subst
-  bindings <- buildBindings taus subst
-  Just (ExApplication applied bindings)
+  [binding] <- buildBinding (BiTau battr bexpr) subst
+  Just (ExApplication applied binding)
+buildExpression (ExApplication _ _) _ = Nothing
 buildExpression (ExFormation bds) subst = buildBindings bds subst >>= (Just . ExFormation)
 buildExpression (ExMeta meta) (Subst mp) = case Map.lookup meta mp of
   Just (MvExpression expr) -> Just expr
diff --git a/src/Matcher.hs b/src/Matcher.hs
--- a/src/Matcher.hs
+++ b/src/Matcher.hs
@@ -6,12 +6,9 @@
 module Matcher where
 
 import Ast
-import Data.List (findIndex, partition)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
-import Data.Maybe (fromMaybe, isJust, maybeToList)
-import Data.Sequence (foldlWithIndex)
-import Misc
+import Data.Maybe (catMaybes)
 
 -- Meta value
 -- The right part of substitution
@@ -27,7 +24,7 @@
 -- Tail operation after expression
 -- Dispatch or application
 data Tail
-  = TaApplication [Binding] -- BiTau only
+  = TaApplication Binding -- BiTau only
   | TaDispatch Attribute
   deriving (Eq, Show)
 
@@ -57,134 +54,92 @@
         | otherwise -> Nothing
       Nothing -> combine' rest (Map.insert key value acc)
 
-matchAttribute :: Attribute -> Attribute -> Maybe Subst
-matchAttribute (AtMeta meta) tgt = Just (substSingle meta (MvAttribute tgt))
+combineMany :: [Subst] -> [Subst] -> [Subst]
+combineMany xs xy = catMaybes [combine x y | x <- xs, y <- xy]
+
+matchAttribute :: Attribute -> Attribute -> [Subst]
+matchAttribute (AtMeta meta) tgt = [substSingle meta (MvAttribute tgt)]
 matchAttribute ptn tgt
-  | ptn == tgt = Just substEmpty
-  | otherwise = Nothing
+  | ptn == tgt = [substEmpty]
+  | otherwise = []
 
-matchBinding :: Binding -> Binding -> Maybe Subst
+matchBinding :: Binding -> Binding -> [Subst]
 matchBinding (BiVoid pattr) (BiVoid tattr) = matchAttribute pattr tattr
 matchBinding (BiDelta pbts) (BiDelta tbts)
-  | pbts == tbts = Just substEmpty
-  | otherwise = Nothing
-matchBinding (BiMetaDelta meta) (BiDelta tBts) = Just (substSingle meta (MvBytes tBts))
+  | pbts == tbts = [substEmpty]
+  | otherwise = []
+matchBinding (BiMetaDelta meta) (BiDelta tBts) = [substSingle meta (MvBytes tBts)]
 matchBinding (BiLambda pFunc) (BiLambda tFunc)
-  | pFunc == tFunc = Just substEmpty
-  | otherwise = Nothing
-matchBinding (BiMetaLambda meta) (BiLambda tFunc) = Just (substSingle meta (MvFunction tFunc))
-matchBinding (BiTau pattr pexp) (BiTau tattr texp) = do
-  mattr <- matchAttribute pattr tattr
-  mexp <- matchExpression pexp texp
-  combine mattr mexp
-matchBinding _ _ = Nothing
+  | pFunc == tFunc = [substEmpty]
+  | otherwise = []
+matchBinding (BiMetaLambda meta) (BiLambda tFunc) = [substSingle meta (MvFunction tFunc)]
+matchBinding (BiTau pattr pexp) (BiTau tattr texp) = combineMany (matchAttribute pattr tattr) (matchExpression pexp texp)
+matchBinding _ _ = []
 
 -- Match bindings with ordering
--- Function returns tuple (X, Y), where
--- - X - "before bindings" - list of bindings before each exact binding. It's used to join with
---   meta binding which goes before exact binding, if such is exist. If there's no one,
---   it'll be []
--- - Y - Substitution for bindings
--- 
--- How it works:
--- We start process pattern bindings. 
--- 1. If we meet meta binding (!B), we skip for now
---    and go the next recursive cycle with next pattern and wait for the result.
---    Result will contain list of "before bindings". This list will be
---    matched to current meta binding
--- 2. If we meet exact binding in pattern, like void, tau, delta, lambda, etc... we try to match it
---    with current target binding. If it matches, we go further and try to match next patterns with next targets.
---    If it does not match, there may be two options:
---    a) we came here from step 1. It means that we should skip this target binding and go the next
---       cycle. When we get the result, we join skipped target binding with returned list of "before" bindings
---       and return to the step one
---    b) we came from somewhere else. Then we just returns Nothing as substitution and don't go further
-matchBindingsInOrder :: [Binding] -> [Binding] -> Bool -> ([Binding], Maybe Subst)
-matchBindingsInOrder [] [] _ = ([], Just substEmpty)
-matchBindingsInOrder [] tbs True = (tbs, Just substEmpty)
-matchBindingsInOrder [] tbs False = ([], Nothing)
-matchBindingsInOrder [BiMeta name] tbs _ = ([], Just (substSingle name (MvBindings tbs)))
-matchBindingsInOrder ((BiMeta name) : pbs) tbs meta = case matchBindingsInOrder pbs tbs True of
-  (_, Nothing) -> ([], Nothing)
-  (before, Just subst) -> ([], combine (substSingle name  (MvBindings before)) subst)
-matchBindingsInOrder (pb : pbs) (tb : tbs) meta = case matchBinding pb tb of
-  Nothing -> if meta 
-    then case matchBindingsInOrder (pb : pbs) tbs meta of
-      (_, Nothing) -> ([], Nothing)
-      (before, Just subst) -> (tb : before, Just subst)
-    else ([], Nothing)
-  Just subst -> case matchBindingsInOrder pbs tbs False of
-    (_, Nothing) -> ([], Nothing)
-    (before, Just subst') -> (before, combine subst subst')
-
--- Match pattern bindings to target bindings
--- !! Pattern bindings list may contain only one BiMeta binding
--- !! Pattern and target bindings may be placed in random order
---
--- If pattern bindings contains only BiMeta binding - all the target bindings are matched
-matchBindings :: [Binding] -> [Binding] -> Maybe Subst
-matchBindings [] [] = Just substEmpty
-matchBindings pbs tbs = do
-  let (_, subst) = matchBindingsInOrder pbs tbs False
-  subst
+matchBindings :: [Binding] -> [Binding] -> [Subst]
+matchBindings [] [] = [substEmpty]
+matchBindings [] _ = []
+matchBindings ((BiMeta name) : pbs) tbs = do
+  let splits = [splitAt idx tbs | idx <- [0 .. length tbs]]
+  catMaybes
+    [ combine (substSingle name (MvBindings before)) subst
+      | (before, after) <- splits,
+        subst <- matchBindings pbs after
+    ]
+matchBindings (pb : pbs) (tb : tbs) = combineMany (matchBinding pb tb) (matchBindings pbs tbs)
+matchBindings _ _ = []
 
 -- Recursively go through given target expression and try to find
 -- the head expression which matches to given pattern.
 -- If there's one - build the list of all the tail operations after head expression.
 -- The tail operations may be only dispatches or applications
-tailExpressions :: Expression -> Expression -> Maybe (Subst, [Tail])
+tailExpressions :: Expression -> Expression -> ([Subst], [Tail])
 tailExpressions ptn tgt = do
-  (subst, tails) <- tailExpressionsReversed ptn tgt
-  return (subst, reverse tails)
+  let (substs, tails) = tailExpressionsReversed ptn tgt
+  (substs, reverse tails)
   where
-    tailExpressionsReversed :: Expression -> Expression -> Maybe (Subst, [Tail])
+    tailExpressionsReversed :: Expression -> Expression -> ([Subst], [Tail])
     tailExpressionsReversed ptn' tgt' = case matchExpression ptn' tgt' of
-      Just subst -> Just (subst, [])
-      Nothing -> case tgt' of
+      [] -> case tgt' of
         ExDispatch expr attr -> do
-          (subst, tails) <- tailExpressionsReversed ptn' expr
-          return (subst, TaDispatch attr : tails)
-        ExApplication expr bds -> do
-          (subst, tails) <- tailExpressionsReversed ptn' expr
-          return (subst, TaApplication bds : tails)
-        _ -> Nothing
+          let (substs, tails) = tailExpressionsReversed ptn' expr
+          (substs, TaDispatch attr : tails)
+        ExApplication expr tau -> do
+          let (substs, tails) = tailExpressionsReversed ptn' expr
+          (substs, TaApplication tau : tails)
+        _ -> ([], [])
+      substs -> (substs, [])
 
-matchExpression :: Expression -> Expression -> Maybe Subst
-matchExpression (ExMeta meta) tgt = Just (substSingle meta (MvExpression tgt))
-matchExpression ExThis ExThis = Just substEmpty
-matchExpression ExGlobal ExGlobal = Just substEmpty
-matchExpression ExTermination ExTermination = Just substEmpty
+matchExpression :: Expression -> Expression -> [Subst]
+matchExpression (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)]
+matchExpression ExThis ExThis = [substEmpty]
+matchExpression ExGlobal ExGlobal = [substEmpty]
+matchExpression ExTermination ExTermination = [substEmpty]
 matchExpression (ExFormation pbs) (ExFormation tbs) = matchBindings pbs tbs
-matchExpression (ExDispatch pexp pattr) (ExDispatch texp tattr) = do
-  mexp <- matchExpression pexp texp
-  mattr <- matchAttribute pattr tattr
-  combine mexp mattr
-matchExpression (ExApplication pexp pbs) (ExApplication texp tbs) = do
-  mexp <- matchExpression pexp texp
-  mbs <- matchBindings pbs tbs
-  combine mexp mbs
-matchExpression (ExMetaTail exp meta) tgt = do
-  (subst, tails) <- tailExpressions exp tgt
-  combine subst (substSingle meta (MvTail tails))
-matchExpression _ _ = Nothing
+matchExpression (ExDispatch pexp pattr) (ExDispatch texp tattr) = combineMany (matchAttribute pattr tattr) (matchExpression pexp texp)
+matchExpression (ExApplication pexp pbd) (ExApplication texp tbd) = combineMany (matchExpression pexp texp) (matchBinding pbd tbd)
+matchExpression (ExMetaTail exp meta) tgt = case tailExpressions exp tgt of
+  ([], _) -> []
+  (substs, tails) -> combineMany substs [substSingle meta (MvTail tails)]
+matchExpression _ _ = []
 
+-- Deep match pattern to expression inside binding
+matchBindingExpression :: Binding -> Expression -> [Subst]
+matchBindingExpression (BiTau _ texp) ptn = matchExpressionDeep ptn texp
+matchBindingExpression _ _ = []
+
 -- Match expression with deep nested expression(s) matching
 matchExpressionDeep :: Expression -> Expression -> [Subst]
 matchExpressionDeep ptn tgt = do
-  let here = maybeToList (matchExpression ptn tgt)
-      deep = case tgt of
-        ExFormation bds -> concatMap matchBindingExpression bds
-        ExDispatch dexp _ -> matchExpressionDeep ptn dexp
-        ExApplication aexp taus -> matchExpressionDeep ptn aexp ++ concatMap matchBindingExpression taus
-        _ -> []
-        where
-          -- Deep match pattern to expression inside binding
-          matchBindingExpression :: Binding -> [Subst]
-          matchBindingExpression (BiTau _ texp) = matchExpressionDeep ptn texp
-          matchBindingExpression _ = []
-  case here of
-    [] -> deep
-    found : _ -> found : deep
+  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
 
 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
@@ -13,7 +13,7 @@
 import System.Directory (doesDirectoryExist, doesFileExist, listDirectory)
 import System.FilePath ((</>))
 import Text.Printf (printf)
-import Data.Binary.IEEE754  
+import Data.Binary.IEEE754
 import Data.ByteString.Builder (word64BE, toLazyByteString)
 import Data.List (intercalate)
 import Data.ByteString.Lazy (unpack)
@@ -28,15 +28,6 @@
 instance Show FsException where
   show FileDoesNotExist {..} = printf "File '%s' does not exist" file
   show DirectoryDoesNotExist {..} = printf "Directory '%s' does not exist" dir
-
--- List without element by given index
-withoutAt :: Int -> [a] -> [a]
-withoutAt i xs = take i xs ++ drop (i + 1) xs
-
--- Returns True if given binding is BiMeta (!B)
-isMetaBinding :: Binding -> Bool
-isMetaBinding (BiMeta _) = True
-isMetaBinding _ = False
 
 ensuredFile :: FilePath -> IO FilePath
 ensuredFile pth = do
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -11,14 +11,14 @@
     parseExpression,
     parseExpressionThrows,
     parseAttribute,
-    parseBinding
+    parseBinding,
   )
 where
 
 import Ast
 import Control.Exception (Exception, throwIO)
 import Control.Monad (guard)
-import Data.Char (isDigit, isLower)
+import Data.Char (isAsciiLower, isDigit, isLower)
 import Data.Scientific (toRealFloat)
 import Data.Sequence (mapWithIndex)
 import Data.Text.Internal.Fusion.Size (lowerBound)
@@ -44,16 +44,16 @@
 dataExpression obj bts =
   ExApplication
     (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel obj))
-    [ BiTau
+    ( BiTau
         (AtAlpha 0)
         ( ExApplication
             (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
-            [ BiTau
+            ( BiTau
                 (AtAlpha 0)
                 (ExFormation [BiDelta bts])
-            ]
+            )
         )
-    ]
+    )
 
 -- White space consumer
 whiteSpace :: Parser ()
@@ -69,17 +69,17 @@
 
 label' :: Parser String
 label' = lexeme $ do
-  first <- lowerChar
+  first <- oneOf ['a' .. 'z']
   rest <- many (satisfy (`notElem` " \r\n\t,.|':;!?][}{)(⟧⟦") <?> "allowed character")
   return (first : rest)
 
 function :: Parser String
 function = lexeme $ do
-  first <- upperChar
+  first <- oneOf ['A' .. 'Z']
   rest <-
     many
       ( satisfy
-          (\ch -> isDigit ch || isLower ch || ch == '_' || ch == 'φ')
+          (\ch -> isDigit ch || isAsciiLower ch || ch == '_' || ch == 'φ')
           <?> "allowed character in function name"
       )
   return (first : rest)
@@ -114,6 +114,16 @@
   ds <- lexeme (many digitChar)
   return (c : ds)
 
+meta' :: Char -> String -> Parser String
+meta' ch uni =
+  choice
+    [ meta ch,
+      do
+        _ <- symbol uni
+        ds <- lexeme (many digitChar)
+        return (ch : ds)
+    ]
+
 byte :: Parser String
 byte = do
   f <- hexDigitChar >>= upperHex
@@ -163,7 +173,7 @@
     ]
 
 metaBinding :: Parser Binding
-metaBinding = BiMeta <$> meta 'B'
+metaBinding = BiMeta <$> meta' 'B' "𝐵"
 
 -- binding
 -- 1. tau
@@ -223,7 +233,7 @@
 attribute =
   choice
     [ void',
-      AtMeta <$> meta 'a'
+      AtMeta <$> meta' 'a' "𝜏"
     ]
     <?> "attribute"
 
@@ -288,11 +298,15 @@
         _ <- char '"'
         str <- manyTill L.charLiteral (char '"')
         return (dataExpression "string" (strToHex str)),
-      try (ExMeta <$> meta 'e'),
+      try (ExMeta <$> meta' 'e' "𝑒"),
       ExDispatch ExThis <$> fullAttribute
     ]
     <?> "expression head"
 
+application :: Expression -> [Binding] -> Expression
+application expr [binding] = ExApplication expr binding
+application expr (bd : bds) = application (application expr [bd]) bds
+
 -- tail optional part of application
 -- 1. any head + dispatch
 -- 2. any head except $ and Q + application
@@ -316,18 +330,13 @@
                 _ <- symbol "("
                 bds <-
                   choice
-                    [ try $
-                        choice
-                          [ try (tauBinding fullAttribute),
-                            metaBinding
-                          ]
-                          `sepBy1` symbol ",",
+                    [ try $ tauBinding fullAttribute `sepBy1` symbol ",",
                       do
                         exprs <- expression `sepBy1` symbol ","
                         return (zipWith (BiTau . AtAlpha) [0 ..] exprs) -- \idx expr -> BiTau (AtAlpha idx) expr
                     ]
                 _ <- symbol ")"
-                return (ExApplication expr bds),
+                return (application expr bds),
               do
                 guard
                   ( case expr of
diff --git a/src/Printer.hs b/src/Printer.hs
--- a/src/Printer.hs
+++ b/src/Printer.hs
@@ -51,8 +51,7 @@
   pretty ExGlobal = pretty "Φ"
   pretty ExTermination = pretty "⊥"
   pretty (ExMeta meta) = prettyMeta meta
-  pretty (ExApplication expr []) = pretty expr <> pretty "()"
-  pretty (ExApplication expr taus) = pretty expr <> vsep [lparen, indent 2 (pretty taus), rparen]
+  pretty (ExApplication expr tau) = pretty expr <> vsep [lparen, indent 2 (pretty tau), rparen]
   pretty (ExDispatch expr attr) = pretty expr <> pretty "." <> pretty attr
   pretty (ExMetaTail expr meta) = pretty expr <+> pretty "*" <+> prettyMeta meta
 
@@ -60,13 +59,13 @@
   pretty (Program expr) = pretty "Φ" <+> prettyArrow <+> pretty expr
 
 instance Pretty Tail where
-  pretty (TaApplication []) = pretty "()"
-  pretty (TaApplication taus) = vsep [lparen, indent 2 (pretty taus), rparen]
+  pretty (TaApplication tau) = vsep [lparen, indent 2 (pretty tau), rparen]
   pretty (TaDispatch attr) = pretty "." <> pretty attr
 
 instance Pretty MetaValue where
   pretty (MvAttribute attr) = pretty attr
   pretty (MvBytes bytes) = pretty bytes
+  pretty (MvBindings []) = pretty "[]"
   pretty (MvBindings bindings) = vsep [pretty "[", indent 2 (pretty bindings), pretty "]"]
   pretty (MvFunction func) = pretty func
   pretty (MvExpression expr) = pretty expr
diff --git a/src/Replacer.hs b/src/Replacer.hs
--- a/src/Replacer.hs
+++ b/src/Replacer.hs
@@ -30,10 +30,10 @@
       ExDispatch inner attr -> do
         let (expr', ptns', repls') = replaceExpression inner ptns repls
         (ExDispatch expr' attr, ptns', repls')
-      ExApplication inner taus -> do
+      ExApplication inner tau -> do
         let (expr', ptns', repls') = replaceExpression inner ptns repls
-        let (taus', ptns'', repls'') = replaceBindings taus ptns' repls'
-        (ExApplication expr' taus', ptns'', repls'')
+        let ([tau'], ptns'', repls'') = replaceBindings [tau] ptns' repls'
+        (ExApplication expr' tau', ptns'', repls'')
       ExFormation bds -> do
         let (bds', ptns', repls') = replaceBindings bds ptns repls
         (ExFormation bds', ptns', repls')
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -6,34 +6,28 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Rewriter (rewrite) where
+module Rewriter (rewrite, meets) where
 
 import Ast
 import Builder
 import Control.Exception
 import Data.Text (intercalate)
-import Matcher (Subst, matchProgram)
+import Matcher (Subst (Subst), matchProgram, MetaValue (MvAttribute))
 import Misc (ensuredFile)
 import Parser (parseProgram, parseProgramThrows)
 import Printer (printExpression, printProgram, printSubstitutions)
 import Replacer (replaceProgram)
 import System.Directory
 import Text.Printf
-import Yaml
 import qualified Yaml as Y
+import qualified Data.Map.Strict as M
 
 data RewriteException
-  = CouldNotMatch {pattern :: Expression, program :: Program}
-  | CouldNotBuild {expr :: Expression, substs :: [Subst]}
+  = CouldNotBuild {expr :: Expression, substs :: [Subst]}
   | CouldNotReplace {prog :: Program, ptn :: Expression, res :: Expression}
   deriving (Exception)
 
 instance Show RewriteException where
-  show CouldNotMatch {..} =
-    printf
-      "Couldn't find given pattern in provided program\n--Pattern: %s\n--Program: %s"
-      (printExpression pattern)
-      (printProgram program)
   show CouldNotBuild {..} =
     printf
       "Couldn't build given expression with provided substitutions\n--Expression: %s\n--Substitutions: %s"
@@ -46,7 +40,6 @@
       (printExpression ptn)
       (printExpression res)
 
--- Check if given attribute is present in given binding
 attrInBinding :: Attribute -> Binding -> Bool
 attrInBinding attr (BiTau battr _) = attr == battr
 attrInBinding attr (BiVoid battr) = attr == battr
@@ -54,41 +47,50 @@
 attrInBinding AtDelta (BiDelta _) = True
 attrInBinding _ _ = False
 
--- Check if all given attributes are present in given bindings
-attrsInBindings :: [Attribute] -> [Binding] -> Bool
-attrsInBindings [] _ = True
-attrsInBindings attrs [] = False
-attrsInBindings [attr] (bd : rest) = attrInBinding attr bd || attrsInBindings [attr] rest
-attrsInBindings (attr : rest) bds = attrsInBindings [attr] bds && attrsInBindings rest bds
+-- 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 :: Condition -> [Subst] -> [Subst]
+meets :: Y.Condition -> [Subst] -> [Subst]
 meets _ [] = []
 -- OR
-meets (Or []) substs = substs
-meets (Or (cond : rest)) [subst] = case meets cond [subst] of
-  [] -> meets (Or rest) [subst]
+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 (And []) substs = substs
-meets (And (cond : rest)) [subst] = case meets cond [subst] of
+meets (Y.And []) substs = substs
+meets (Y.And (cond : rest)) [subst] = case meets cond [subst] of
   [] -> []
-  _ -> meets (And rest) [subst]
+  _ -> meets (Y.And rest) [subst]
 -- NOT
-meets (Not cond) [subst] = case meets cond [subst] of
+meets (Y.Not cond) [subst] = case meets cond [subst] of
   [] -> [subst]
   _ -> []
 -- IN
-meets (In attrs bindings) [subst] =
-  case (traverse (`buildAttribute` subst) attrs, buildBindings bindings subst) of
-    (Just attrs', Just bds) -> [subst | attrsInBindings attrs' bds] -- if attrsInBindings attrs' bds then [subst] else []
+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 []
     (_, _) -> []
-meets (In attrs bindings) (subst : rest) = do
-  let cond = In attrs bindings
-      substs = meets cond [subst]
-  head substs : meets cond rest
+-- 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]
@@ -99,7 +101,7 @@
 
 -- 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 = 
+buildAndReplace program ptn res substs =
   case (buildExpressions ptn substs, buildExpressions res substs) of
     (Just ptns, Just repls) -> case replaceProgram program ptns repls of
       Just prog -> pure prog
@@ -113,7 +115,7 @@
   let ptn = Y.pattern rule
       res = Y.result rule
   case matchProgram ptn program of
-    [] -> throwIO (CouldNotMatch ptn program)
+    [] -> pure program
     substs -> do
       let replaced = buildAndReplace program ptn res
       case Y.when rule of
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -55,13 +55,22 @@
             [ And <$> v .: "and",
               Or <$> v .: "or",
               Not <$> v .: "not",
+              Alpha <$> v .: "alpha",
               do
+                vals <- v .: "eq"
+                case vals of
+                  [left_, right_] -> do
+                    left <- parseJSON left_
+                    right <- parseJSON right_
+                    pure (Eq left right)
+                  _ -> fail "'eq' must contain exactly two elements",
+              do
                 vals <- v .: "in"
                 case vals of
-                  [attrs_, bindings_] -> do
-                    attrs' <- parseJSON attrs_
-                    bds <- parseJSON bindings_
-                    pure (In attrs' bds)
+                  [attr_, binding_] -> do
+                    attr <- parseJSON attr_
+                    bd <- parseJSON binding_
+                    pure (In attr bd)
                   _ -> fail "'in' must contain exactly two elements"
             ]
       )
@@ -69,8 +78,10 @@
 data Condition
   = And [Condition]
   | Or [Condition]
-  | In [Attribute] [Binding]
+  | In Attribute Binding
   | Not Condition
+  | Alpha Attribute
+  | Eq Attribute Attribute
   deriving (Generic, Show)
 
 data Rule = Rule
diff --git a/test/BuilderSpec.hs b/test/BuilderSpec.hs
--- a/test/BuilderSpec.hs
+++ b/test/BuilderSpec.hs
@@ -26,9 +26,9 @@
           Just (ExDispatch ExGlobal (AtLabel "x"))
         ),
         ( "Q.c(!a -> !e) => (!a >> x, !e >> $.y.z) => Q.c(x -> $.y.z)",
-          ExApplication (ExDispatch ExGlobal (AtLabel "c")) [BiTau (AtMeta "a") (ExMeta "e")],
+          ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtMeta "a") (ExMeta "e")),
           [("a", MvAttribute (AtLabel "x")), ("e", MvExpression (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z")))],
-          Just (ExApplication (ExDispatch ExGlobal (AtLabel "c")) [BiTau (AtLabel "x") (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))])
+          Just (ExApplication (ExDispatch ExGlobal (AtLabel "c")) (BiTau (AtLabel "x") (ExDispatch (ExDispatch ExThis (AtLabel "y")) (AtLabel "z"))))
         ),
         ( "[[!a -> $.x, !B]] => (!a >> y, !B >> [[b -> ?, L> Func]]) => [[y -> $.x, b -> ?, L> Func]]",
           ExFormation [BiTau (AtMeta "a") (ExDispatch ExThis (AtLabel "x")), BiMeta "B"],
@@ -43,8 +43,8 @@
         ),
         ( "Q * !t => (!t >> [.a, .b, (~1 -> $.x)]) => Q.a.b(~1 -> $.x)",
           ExMetaTail ExGlobal "t",
-          [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication [BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x"))]])],
-          Just (ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) [BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x"))])
+          [("t", MvTail [TaDispatch (AtLabel "a"), TaDispatch (AtLabel "b"), TaApplication (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x")))])],
+          Just (ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "a")) (AtLabel "b")) (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "x"))))
         ),
         ( "Q.!a => () => X",
           ExDispatch ExGlobal (AtMeta "a"),
@@ -52,14 +52,14 @@
           Nothing
         ),
         ( "!e0(!a1 -> !e1, !a2 => !e2) => (!e0 >> [[]], !a1 >> x, !e1 >> Q, !a2 >> y, !e2 >> $) => [[]](x -> Q, y -> $)",
-          ExApplication (ExMeta "e0") [BiTau (AtMeta "a1") (ExMeta "e1"), BiTau (AtMeta "a2") (ExMeta "e2")],
+          ExApplication (ExApplication (ExMeta "e0") (BiTau (AtMeta "a1") (ExMeta "e1"))) (BiTau (AtMeta "a2") (ExMeta "e2")),
           [ ("e0", MvExpression (ExFormation [])),
             ("a1", MvAttribute (AtLabel "x")),
             ("e1", MvExpression ExGlobal),
             ("a2", MvAttribute (AtLabel "y")),
             ("e2", MvExpression ExThis)
           ],
-          Just (ExApplication (ExFormation []) [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])
+          Just (ExApplication (ExApplication (ExFormation []) (BiTau (AtLabel "x") ExGlobal)) (BiTau (AtLabel "y") ExThis))
         ),
         ( "⟦!a ↦ ∅, !B⟧.!a => (!a >> t, !B >> ⟦ x ↦ ξ.t ⟧ ) => ⟦ t ↦ ∅, x ↦ ξ.t ⟧.t",
           ExDispatch (ExFormation [BiVoid (AtMeta "a"), BiMeta "B"]) (AtMeta "a"),
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -56,7 +56,7 @@
         let args = ["rewrite", "--nothing"]
         output <- capture_ (runCLI args)
         output `shouldContain` "Φ ↦ ⟦\n  foo ↦ Φ.org.eolang\n⟧"
-    
+
     it "rewrites with single rule" $ do
       withRedirectedStdin "{T(x -> Q.y)}" $ do
         let args = ["rewrite", "--rule=resources/dc.yaml"]
diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs
--- a/test/MatcherSpec.hs
+++ b/test/MatcherSpec.hs
@@ -18,14 +18,6 @@
   type ExpectedResult e
   toExpected :: e -> ExpectedResult e
 
-instance Expected (Maybe [(String, MetaValue)]) where
-  type ExpectedResult (Maybe [(String, MetaValue)]) = Maybe Subst
-  toExpected = fmap (Subst . Map.fromList)
-
-instance Expected ([Binding], [(String, MetaValue)]) where
-  type ExpectedResult ([Binding], [(String, MetaValue)]) = ([Binding], Maybe Subst)
-  toExpected (rest, pairs) = (rest, Just (Subst (Map.fromList pairs)))
-
 instance Expected [[(String, MetaValue)]] where
   type ExpectedResult [[(String, MetaValue)]] = [Subst]
   toExpected = map (Subst . Map.fromList)
@@ -58,17 +50,15 @@
             ],
           [[("a", MvAttribute (AtLabel "x"))], [("a", MvAttribute (AtLabel "y"))]]
         ),
-        ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]]), (!e >> Q)]",
+        ( "!e => [[x -> Q]] => [(!e >> [[x -> Q]])]",
           ExMeta "e",
           ExFormation [BiTau (AtLabel "x") ExGlobal],
-          [[("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]))], [("e", MvExpression ExGlobal)]]
+          [[("e", MvExpression (ExFormation [BiTau (AtLabel "x") ExGlobal]))]]
         ),
-        ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang), (!e >> Q, !a >> org)]",
+        ( "!e.!a => Q.org.eolang => [(!e >> Q.org, !a >> eolang)]",
           ExDispatch (ExMeta "e") (AtMeta "a"),
           ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang"),
-          [ [("e", MvExpression (ExDispatch ExGlobal (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))],
-            [("e", MvExpression ExGlobal), ("a", MvAttribute (AtLabel "org"))]
-          ]
+          [[("e", MvExpression (ExDispatch ExGlobal (AtLabel "org"))), ("a", MvAttribute (AtLabel "eolang"))]]
         ),
         ( "⟦!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"),
@@ -81,14 +71,14 @@
                 )
                 (AtLabel "t")
             )
-            [ BiTau
+            ( BiTau
                 AtRho
                 ( ExFormation
                     [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t")),
                       BiVoid (AtLabel "t")
                     ]
                 )
-            ],
+            ),
           [ [ ("B1", MvBindings [BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t"))]),
               ("a", MvAttribute (AtLabel "t")),
               ("B2", MvBindings [])
@@ -100,10 +90,10 @@
   describe "matchAttribute: attribute => attribute => substitution" $
     test
       matchAttribute
-      [ ("~1 => ~1 => ()", AtAlpha 1, AtAlpha 1, Just []),
-        ("!a => ^ => (!a >> ^)", AtMeta "a", AtRho, Just [("a", MvAttribute AtRho)]),
-        ("!a => @ => (!a >> @)", AtMeta "a", AtPhi, Just [("a", MvAttribute AtPhi)]),
-        ("~0 => x => X", AtAlpha 0, AtLabel "x", Nothing)
+      [ ("~1 => ~1 => [()]", AtAlpha 1, AtAlpha 1, [[]]),
+        ("!a => ^ => [(!a >> ^)]", AtMeta "a", AtRho, [[("a", MvAttribute AtRho)]]),
+        ("!a => @ => [(!a >> @)]", AtMeta "a", AtPhi, [[("a", MvAttribute AtPhi)]]),
+        ("~0 => [] => [()]", AtAlpha 0, AtLabel "x", [])
       ]
 
   describe "matchBindings: [binding] => [binding] => substitution" $
@@ -112,91 +102,183 @@
       [ ( "[[]] => [[]] => ()",
           [],
           [],
-          Just []
+          [[]]
         ),
         ( "[[!B]] => T:[[x -> ?, D> 01-, L> Func]] => (!B >> T)",
           [BiMeta "B"],
           [BiVoid (AtLabel "x"), BiDelta "01-", BiLambda "Func"],
-          Just [("B", MvBindings [BiVoid (AtLabel "x"), BiDelta "01-", BiLambda "Func"])]
+          [[("B", MvBindings [BiVoid (AtLabel "x"), BiDelta "01-", BiLambda "Func"])]]
         ),
-        ( "[[D> 00-]] => [[D> 00-, L> Func]] => X",
+        ( "[[D> 00-]] => [[D> 00-, L> Func]] => []",
           [BiDelta "00-"],
           [BiDelta "00-", BiLambda "Func"],
-          Nothing
+          []
         ),
         ( "[[y -> ?, !a -> ?]] => [[y -> ?, x -> ?]] => (!a >> x)",
           [BiVoid (AtLabel "y"), BiVoid (AtMeta "a")],
           [BiVoid (AtLabel "y"), BiVoid (AtLabel "x")],
-          Just [("a", MvAttribute (AtLabel "x"))]
+          [[("a", MvAttribute (AtLabel "x"))]]
         ),
         ( "[[!B, x -> ?]] => [[x -> ?]] => (!B >> [[]])",
           [BiMeta "B", BiVoid (AtLabel "x")],
           [BiVoid (AtLabel "x")],
-          Just [("B", MvBindings [])]
+          [[("B", MvBindings [])]]
         ),
         ( "[[!B1, x -> ?, !B2]] => [[x -> ?, y -> ?]] => (!B1 >> [[]], !B2 >> [[y -> ?]])",
           [BiMeta "B1", BiVoid (AtLabel "x"), BiMeta "B2"],
           [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")],
-          Just [("B1", MvBindings []), ("B2", MvBindings [BiVoid (AtLabel "y")])]
+          [[("B1", MvBindings []), ("B2", MvBindings [BiVoid (AtLabel "y")])]]
         ),
         ( "[[!B1, !x -> ?, !B2]] => [[y -> ?, D> -> 00-, L> Func]] => (!x >> y, !B1 >> [[]], !B2 >> [[D> -> 00-, L> Func]])",
           [BiMeta "B1", BiVoid (AtMeta "x"), BiMeta "B2"],
           [BiVoid (AtLabel "y"), BiDelta "00-", BiLambda "Func"],
-          Just [("B1", MvBindings []), ("B2", MvBindings [BiDelta "00-", BiLambda "Func"]), ("x", MvAttribute (AtLabel "y"))]
+          [[("B1", MvBindings []), ("B2", MvBindings [BiDelta "00-", BiLambda "Func"]), ("x", MvAttribute (AtLabel "y"))]]
         ),
         ( "[[!x -> ?, !y -> ?]] => [[a -> ?, b -> ?]] => (!x >> a, !y >> b)",
           [BiVoid (AtMeta "x"), BiVoid (AtMeta "y")],
           [BiVoid (AtLabel "a"), BiVoid (AtLabel "b")],
-          Just [("x", MvAttribute (AtLabel "a")), ("y", MvAttribute (AtLabel "b"))]
+          [[("x", MvAttribute (AtLabel "a")), ("y", MvAttribute (AtLabel "b"))]]
         ),
         ( "[[t -> ?, !B]] => [[t -> ?, x -> Q, y -> $]] => (!B >> [[x -> Q, y -> $]])",
           [BiVoid (AtLabel "t"), BiMeta "B"],
           [BiVoid (AtLabel "t"), BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis],
-          Just [("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]
+          [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]
         ),
         ( "[[!B, z -> Q]] => [[x -> Q, y -> $, z -> Q]] => (!B >> [[x -> Q, y -> $]])",
           [BiMeta "B", BiTau (AtLabel "z") ExGlobal],
           [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis, BiTau (AtLabel "z") ExGlobal],
-          Just [("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]
+          [[("B", MvBindings [BiTau (AtLabel "x") ExGlobal, BiTau (AtLabel "y") ExThis])]]
         ),
-        ( "[[L> Func, D> 00-]] => [[D> 00-, L> Func]] => X",
+        ( "[[L> Func, D> 00-]] => [[D> 00-, L> Func]] => []",
           [BiLambda "Func", BiDelta "00-"],
           [BiDelta "00-", BiLambda "Func"],
-          Nothing
+          []
         ),
-        ( "[[t -> ?, !B]] => [[x -> ?, t -> ?]] => X",
+        ( "[[t -> ?, !B]] => [[x -> ?, t -> ?]] => []",
           [BiVoid (AtLabel "t"), BiMeta "B"],
           [BiVoid (AtLabel "x"), BiVoid (AtLabel "t")],
-          Nothing
+          []
+        ),
+        ( "[[!B, !a -> ?]] => [[x -> ?, y -> ?]] => (!a >> y, !B >> [[ x -> ? ]] )",
+          [BiMeta "B", BiVoid (AtMeta "a")],
+          [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")],
+          [[("a", MvAttribute (AtLabel "y")), ("B", MvBindings [BiVoid (AtLabel "x")])]]
+        ),
+        ( "[[!B1, !a -> ?, !B2]] => [[ x -> ?, y -> ?, z -> ? ]] => [(), (), ()]",
+          [BiMeta "B1", BiVoid (AtMeta "a"), BiMeta "B2"],
+          [BiVoid (AtLabel "x"), BiVoid (AtLabel "y"), BiVoid (AtLabel "z")],
+          [ [ ("B1", MvBindings []),
+              ("a", MvAttribute (AtLabel "x")),
+              ("B2", MvBindings [BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "x")]),
+              ("a", MvAttribute (AtLabel "y")),
+              ("B2", MvBindings [BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")]),
+              ("a", MvAttribute (AtLabel "z")),
+              ("B2", MvBindings [])
+            ]
+          ]
+        ),
+        ( "[[!B1, !a1 -> ?, !B2, !a2 -> ?, !B3]] => [[ a -> ?, b -> ?, x -> ?, y -> ?, z -> ? ]] => [10 substs]",
+          [BiMeta "B1", BiVoid (AtMeta "a1"), BiMeta "B2", BiVoid (AtMeta "a2"), BiMeta "B3"],
+          [ BiVoid (AtLabel "a"),
+            BiVoid (AtLabel "b"),
+            BiVoid (AtLabel "x"),
+            BiVoid (AtLabel "y"),
+            BiVoid (AtLabel "z")
+          ],
+          [ [ ("B1", MvBindings []),
+              ("a1", MvAttribute (AtLabel "a")),
+              ("B2", MvBindings []),
+              ("a2", MvAttribute (AtLabel "b")),
+              ("B3", MvBindings [BiVoid (AtLabel "x"), BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings []),
+              ("a1", MvAttribute (AtLabel "a")),
+              ("B2", MvBindings [BiVoid (AtLabel "b")]),
+              ("a2", MvAttribute (AtLabel "x")),
+              ("B3", MvBindings [BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings []),
+              ("a1", MvAttribute (AtLabel "a")),
+              ("B2", MvBindings [BiVoid (AtLabel "b"), BiVoid (AtLabel "x")]),
+              ("a2", MvAttribute (AtLabel "y")),
+              ("B3", MvBindings [BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings []),
+              ("a1", MvAttribute (AtLabel "a")),
+              ("B2", MvBindings [BiVoid (AtLabel "b"), BiVoid (AtLabel "x"), BiVoid (AtLabel "y")]),
+              ("a2", MvAttribute (AtLabel "z")),
+              ("B3", MvBindings [])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "a")]),
+              ("a1", MvAttribute (AtLabel "b")),
+              ("B2", MvBindings []),
+              ("a2", MvAttribute (AtLabel "x")),
+              ("B3", MvBindings [BiVoid (AtLabel "y"), BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "a")]),
+              ("a1", MvAttribute (AtLabel "b")),
+              ("B2", MvBindings [BiVoid (AtLabel "x")]),
+              ("a2", MvAttribute (AtLabel "y")),
+              ("B3", MvBindings [BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "a")]),
+              ("a1", MvAttribute (AtLabel "b")),
+              ("B2", MvBindings [BiVoid (AtLabel "x"), BiVoid (AtLabel "y")]),
+              ("a2", MvAttribute (AtLabel "z")),
+              ("B3", MvBindings [])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "a"), BiVoid (AtLabel "b")]),
+              ("a1", MvAttribute (AtLabel "x")),
+              ("B2", MvBindings []),
+              ("a2", MvAttribute (AtLabel "y")),
+              ("B3", MvBindings [BiVoid (AtLabel "z")])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "a"), BiVoid (AtLabel "b")]),
+              ("a1", MvAttribute (AtLabel "x")),
+              ("B2", MvBindings [BiVoid (AtLabel "y")]),
+              ("a2", MvAttribute (AtLabel "z")),
+              ("B3", MvBindings [])
+            ],
+            [ ("B1", MvBindings [BiVoid (AtLabel "a"), BiVoid (AtLabel "b"), BiVoid (AtLabel "x")]),
+              ("a1", MvAttribute (AtLabel "y")),
+              ("B2", MvBindings []),
+              ("a2", MvAttribute (AtLabel "z")),
+              ("B3", MvBindings [])
+            ]
+          ]
         )
       ]
 
   describe "matchExpression: expression => pattern => substitution" $
     test
       matchExpression
-      [ ("$ => $ => ()", ExThis, ExThis, Just []),
-        ("Q => Q => ()", ExGlobal, ExGlobal, Just []),
-        ( "!e => Q => (!e >> Q)",
+      [ ("$ => $ => [()]", ExThis, ExThis, [[]]),
+        ("Q => Q => [()]", ExGlobal, ExGlobal, [[]]),
+        ( "!e => Q => [(!e >> Q)]",
           ExMeta "e",
           ExGlobal,
-          Just [("e", MvExpression ExGlobal)]
+          [[("e", MvExpression ExGlobal)]]
         ),
-        ( "!e => Q.org(x -> $) => (!e >> Q.org(x -> $))",
+        ( "!e => Q.org(x -> $) => [(!e >> Q.org(x -> $))]",
           ExMeta "e",
-          ExApplication (ExDispatch ExGlobal (AtLabel "org")) [BiTau (AtLabel "x") ExThis],
-          Just [("e", MvExpression (ExApplication (ExDispatch ExGlobal (AtLabel "org")) [BiTau (AtLabel "x") ExThis]))]
+          ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis),
+          [[("e", MvExpression (ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") ExThis)))]]
         ),
-        ( "!e1.x => Q.org.x => (!e1 >> Q.org)",
+        ( "!e1.x => Q.org.x => [(!e1 >> Q.org)]",
           ExDispatch (ExMeta "e1") (AtLabel "x"),
           ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "x"),
-          Just [("e1", MvExpression (ExDispatch ExGlobal (AtLabel "org")))]
+          [[("e1", MvExpression (ExDispatch ExGlobal (AtLabel "org")))]]
         ),
-        ( "!e.org.!a => $.org.x => (!e >> $, !a >> x)",
+        ( "!e.org.!a => $.org.x => [(!e >> $, !a >> x)]",
           ExDispatch (ExDispatch (ExMeta "e") (AtLabel "org")) (AtMeta "a"),
           ExDispatch (ExDispatch ExThis (AtLabel "org")) (AtLabel "x"),
-          Just [("e", MvExpression ExThis), ("a", MvAttribute (AtLabel "x"))]
+          [[("e", MvExpression ExThis), ("a", MvAttribute (AtLabel "x"))]]
         ),
-        ( "[[!a -> !e, !B]].!a => [[x -> Q, y -> $]].x => (!a >> x, !e >> Q, !B >> [y -> $])",
+        ( "[[!a -> !e, !B]].!a => [[x -> Q, y -> $]].x => [(!a >> x, !e >> Q, !B >> [y -> $])]",
           ExDispatch (ExFormation [BiTau (AtMeta "a") (ExMeta "e"), BiMeta "B"]) (AtMeta "a"),
           ExDispatch
             ( ExFormation
@@ -205,31 +287,49 @@
                 ]
             )
             (AtLabel "x"),
-          Just
-            [ ("a", MvAttribute (AtLabel "x")),
+          [ [ ("a", MvAttribute (AtLabel "x")),
               ("e", MvExpression ExGlobal),
               ("B", MvBindings [BiTau (AtLabel "y") ExThis])
             ]
+          ]
         ),
-        ( "Q * !t => Q.org => (!t >> [.org])",
+        ( "Q * !t => Q.org => [(!t >> [.org])]",
           ExMetaTail ExGlobal "t",
           ExDispatch ExGlobal (AtLabel "x"),
-          Just [("t", MvTail [TaDispatch (AtLabel "x")])]
+          [[("t", MvTail [TaDispatch (AtLabel "x")])]]
         ),
-        ( "Q * !t => Q.org(x -> [[]]) => (!t >> [.org, (x -> [[]])])",
+        ( "Q * !t => Q.org(x -> [[]]) => [(!t >> [.org, (x -> [[]])])]",
           ExMetaTail ExGlobal "t",
-          ExApplication (ExDispatch ExGlobal (AtLabel "org")) [BiTau (AtLabel "x") (ExFormation [])],
-          Just [("t", MvTail [TaDispatch (AtLabel "org"), TaApplication [BiTau (AtLabel "x") (ExFormation [])]])]
+          ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") (ExFormation [])),
+          [[("t", MvTail [TaDispatch (AtLabel "org"), TaApplication (BiTau (AtLabel "x") (ExFormation []))])]]
         ),
-        ( "Q.!a * !t => Q.org(x -> [[]]) => (!a >> org, !t >> [(x -> [[]])])",
+        ( "Q.!a * !t => Q.org(x -> [[]]) => [(!a >> org, !t >> [(x -> [[]])])]",
           ExMetaTail (ExDispatch ExGlobal (AtMeta "a")) "t",
-          ExApplication (ExDispatch ExGlobal (AtLabel "org")) [BiTau (AtLabel "x") (ExFormation [])],
-          Just [("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaApplication [BiTau (AtLabel "x") (ExFormation [])]])]
+          ExApplication (ExDispatch ExGlobal (AtLabel "org")) (BiTau (AtLabel "x") (ExFormation [])),
+          [[("a", MvAttribute (AtLabel "org")), ("t", MvTail [TaApplication (BiTau (AtLabel "x") (ExFormation []))])]]
         ),
-        ( "Q.x(y -> $ * !t1) * !t2 => Q.x(y -> $.q).p => (!t1 >> [.q], !t2 >> [.p])",
-          ExMetaTail (ExApplication (ExDispatch ExGlobal (AtLabel "x")) [BiTau (AtLabel "y") (ExMetaTail ExThis "t1")]) "t2",
-          ExDispatch (ExApplication (ExDispatch ExGlobal (AtLabel "x")) [BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "q"))]) (AtLabel "p"),
-          Just [("t1", MvTail [TaDispatch (AtLabel "q")]), ("t2", MvTail [TaDispatch (AtLabel "p")])]
+        ( "Q.x(y -> $ * !t1) * !t2 => Q.x(y -> $.q).p => [(!t1 >> [.q], !t2 >> [.p])]",
+          ExMetaTail (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExMetaTail ExThis "t1"))) "t2",
+          ExDispatch (ExApplication (ExDispatch ExGlobal (AtLabel "x")) (BiTau (AtLabel "y") (ExDispatch ExThis (AtLabel "q")))) (AtLabel "p"),
+          [[("t1", MvTail [TaDispatch (AtLabel "q")]), ("t2", MvTail [TaDispatch (AtLabel "p")])]]
+        ),
+        ( "[[!B1, !a ↦ !e1, !B2]](!a ↦ !e2) => ⟦ t ↦ ξ.k, x ↦ ξ.t, k ↦ ∅ ⟧(x ↦ ξ) => []",
+          ExApplication (ExFormation [BiMeta "B1", BiTau (AtMeta "a") (ExMeta "e1"), BiMeta "B2"]) (BiTau (AtMeta "a") (ExMeta "e2")),
+          ExApplication
+            ( ExFormation
+                [ BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k")),
+                  BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t")),
+                  BiVoid (AtLabel "k")
+                ]
+            )
+            (BiTau (AtLabel "x") ExThis),
+          [ [ ("B1", MvBindings [BiTau (AtLabel "t") (ExDispatch ExThis (AtLabel "k"))]),
+              ("a", MvAttribute (AtLabel "x")),
+              ("B2", MvBindings [BiVoid (AtLabel "k")]),
+              ("e1", MvExpression (ExDispatch ExThis (AtLabel "t"))),
+              ("e2", MvExpression ExThis)
+            ]
+          ]
         )
       ]
 
diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs
--- a/test/ParserSpec.hs
+++ b/test/ParserSpec.hs
@@ -31,7 +31,7 @@
     test
       parseProgram
       [ ("Q -> [[]]", Just (Program (ExFormation []))),
-        ("Q -> T(x -> Q)", Just (Program (ExApplication ExTermination [BiTau (AtLabel "x") ExGlobal]))),
+        ("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"))])))
@@ -41,25 +41,25 @@
     test
       parseExpression
       [ ("Q.!a", Just (ExDispatch ExGlobal (AtMeta "a"))),
-        ("[[]](!a1 -> $)", Just (ExApplication (ExFormation []) [BiTau (AtMeta "a1") ExThis])),
+        ("[[]](!a1 -> $)", Just (ExApplication (ExFormation []) (BiTau (AtMeta "a1") ExThis))),
         ( "[[]](~0 -> $)(~11 -> Q)",
           Just
             ( ExApplication
                 ( ExApplication
                     (ExFormation [])
-                    [BiTau (AtAlpha 0) ExThis]
+                    (BiTau (AtAlpha 0) ExThis)
                 )
-                [BiTau (AtAlpha 11) ExGlobal]
+                (BiTau (AtAlpha 11) ExGlobal)
             )
         ),
-        ("[[]](x -> $, y -> Q)", Just (ExApplication (ExFormation []) [BiTau (AtLabel "x") ExThis, BiTau (AtLabel "y") ExGlobal])),
+        ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation []) (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")])),
         ("[[!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")),
+        ("[[]](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-"])),
@@ -87,7 +87,7 @@
           Just
             ( ExApplication
                 (ExMeta "e")
-                [ BiTau
+                ( BiTau
                     (AtLabel "x")
                     ( ExFormation
                         [ BiVoid AtRho,
@@ -95,7 +95,7 @@
                           BiTau (AtLabel "w") (ExMeta "e1")
                         ]
                     )
-                ]
+                )
             )
         ),
         ( "[[x -> y.z, a -> ~1, w -> ^, u -> @, p -> !a, q -> !e]]",
@@ -125,19 +125,26 @@
         ( "Q.x(~1, y, [[]].z, Q.y(^,@))",
           Just
             ( ExApplication
-                (ExDispatch ExGlobal (AtLabel "x"))
-                [ BiTau (AtAlpha 0) (ExDispatch ExThis (AtAlpha 1)),
-                  BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "y")),
-                  BiTau (AtAlpha 2) (ExDispatch (ExFormation []) (AtLabel "z")),
-                  BiTau
+                ( ExApplication
+                    ( ExApplication
+                        ( ExApplication
+                            (ExDispatch ExGlobal (AtLabel "x"))
+                            (BiTau (AtAlpha 0) (ExDispatch ExThis (AtAlpha 1)))
+                        )
+                        (BiTau (AtAlpha 1) (ExDispatch ExThis (AtLabel "y")))
+                    )
+                    (BiTau (AtAlpha 2) (ExDispatch (ExFormation []) (AtLabel "z")))
+                )
+                ( BiTau
                     (AtAlpha 3)
                     ( ExApplication
-                        (ExDispatch ExGlobal (AtLabel "y"))
-                        [ BiTau (AtAlpha 0) (ExDispatch ExThis AtRho),
-                          BiTau (AtAlpha 1) (ExDispatch ExThis AtPhi)
-                        ]
+                        ( ExApplication
+                            (ExDispatch ExGlobal (AtLabel "y"))
+                            (BiTau (AtAlpha 0) (ExDispatch ExThis AtRho))
+                        )
+                        (BiTau (AtAlpha 1) (ExDispatch ExThis AtPhi))
                     )
-                ]
+                )
             )
         ),
         ( "5.plus(5.q(\"hello\".length))",
@@ -146,62 +153,70 @@
                 ( ExDispatch
                     ( ExApplication
                         (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number"))
-                        [ BiTau
+                        ( BiTau
                             (AtAlpha 0)
                             ( ExApplication
                                 (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
-                                [ BiTau
+                                ( BiTau
                                     (AtAlpha 0)
                                     (ExFormation [BiDelta "40-14-00-00-00-00-00-00"])
-                                ]
+                                )
                             )
-                        ]
+                        )
                     )
                     (AtLabel "plus")
                 )
-                [ BiTau
+                ( BiTau
                     (AtAlpha 0)
                     ( ExApplication
                         ( ExDispatch
                             ( ExApplication
                                 (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number"))
-                                [ BiTau
+                                ( BiTau
                                     (AtAlpha 0)
                                     ( ExApplication
                                         (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
-                                        [ BiTau
+                                        ( BiTau
                                             (AtAlpha 0)
                                             (ExFormation [BiDelta "40-14-00-00-00-00-00-00"])
-                                        ]
+                                        )
                                     )
-                                ]
+                                )
                             )
                             (AtLabel "q")
                         )
-                        [ BiTau
+                        ( BiTau
                             (AtAlpha 0)
                             ( ExDispatch
                                 ( ExApplication
                                     (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "string"))
-                                    [ BiTau
+                                    ( BiTau
                                         (AtAlpha 0)
                                         ( ExApplication
                                             (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "bytes"))
-                                            [ BiTau
+                                            ( BiTau
                                                 (AtAlpha 0)
                                                 (ExFormation [BiDelta "68-65-6C-6C-6F"])
-                                            ]
+                                            )
                                         )
-                                    ]
+                                    )
                                 )
                                 (AtLabel "length")
                             )
-                        ]
+                        )
                     )
-                ]
+                )
             )
         ),
-        ("Q.x(!B)", Just (ExApplication (ExDispatch ExGlobal (AtLabel "x")) [BiMeta "B"]))
+        ( "[[𝐵1, 𝜏0 -> $, x -> 𝑒]]",
+          Just
+            ( ExFormation
+                [ BiMeta "B1",
+                  BiTau (AtMeta "a0") ExThis,
+                  BiTau (AtLabel "x") (ExMeta "e")
+                ]
+            )
+        )
       ]
 
   describe "just parses" $
@@ -223,9 +238,7 @@
         "[[\n  x -> \"Hi\",\n  y -> 42\n]]",
         "[[x -> -42, y -> +34]]",
         "⟦x ↦ Φ.org.eolang(z ↦ ξ.f, x ↦ α0, φ ↦ ρ, t ↦ φ, first ↦ ⟦ λ ⤍ Function_name, Δ ⤍ 42- ⟧)⟧",
-        "[[x -> 1.00e+3, y -> 2.32e-4]]",
-        "Q.x(!B)",
-        "Q.x(~1 -> Q.y, x -> 5, !B1)"
+        "[[x -> 1.00e+3, y -> 2.32e-4]]"
       ]
       (\expr -> it expr (parseExpression expr `shouldSatisfy` isRight))
 
@@ -249,7 +262,9 @@
             "[[y(!e) -> [[]] ]]",
             "[[z(w) -> Q.x]]",
             "Q.x(y(~1) -> [[]])",
-            "Q.x(1, 2, !B)"
+            "Q.x(1, 2, !B)",
+            "Q.x(~1 -> Q.y, x -> 5, !B1)",
+            "Q.x(𝐵1, 𝜏0 -> $, x -> 𝑒)"
           ]
       )
 
diff --git a/test/ReplacerSpec.hs b/test/ReplacerSpec.hs
--- a/test/ReplacerSpec.hs
+++ b/test/ReplacerSpec.hs
@@ -21,11 +21,11 @@
   describe "replaceProgram: program => ([expression], [expression]) => program" $ do
     test
       replaceProgram
-      [ ( "Q -> Q.y.x() => ([Q.y], [$]) => Q -> $.x()",
-          Program (ExApplication (ExDispatch (ExDispatch ExGlobal (AtLabel "y")) (AtLabel "x")) []),
+      [ ( "Q -> Q.y.x => ([Q.y], [$]) => Q -> $.x",
+          Program (ExDispatch (ExDispatch ExGlobal (AtLabel "y")) (AtLabel "x")),
           [ExDispatch ExGlobal (AtLabel "y")],
           [ExThis],
-          Just (Program (ExApplication (ExDispatch ExThis (AtLabel "x")) []))
+          Just (Program (ExDispatch ExThis (AtLabel "x")))
         ),
         ( "Q -> [[x -> [[y -> $]], z -> [[w -> $]] ]] => ([[y -> $], [w -> $]], [Q.y, Q.w]) => Q -> [[x -> Q.y, z -> Q.w]]",
           Program
@@ -58,7 +58,7 @@
           [ExThis, ExThis],
           Just (Program ExThis)
         ),
-        ( "",
+        ( "Q -> [[ x -> $.t, t -> ? ]].t(^ -> [[ x -> $.t, t -> ? ]]) => ([ [[ x -> $.t, t -> ? ]].t ], [T]) => T(^ -> [[ x -> $.t, t -> ? ]])",
           Program
             ( ExApplication
                 ( ExDispatch
@@ -69,14 +69,14 @@
                     )
                     (AtLabel "t")
                 )
-                [ BiTau
+                ( BiTau
                     AtRho
                     ( ExFormation
                         [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t")),
                           BiVoid (AtLabel "t")
                         ]
                     )
-                ]
+                )
             ),
           [ ExDispatch
               ( ExFormation
@@ -91,14 +91,14 @@
             ( Program
                 ( ExApplication
                     ExTermination
-                    [ BiTau
+                    ( BiTau
                         AtRho
                         ( ExFormation
                             [ BiTau (AtLabel "x") (ExDispatch ExThis (AtLabel "t")),
                               BiVoid (AtLabel "t")
                             ]
                         )
-                    ]
+                    )
                 )
             )
         )
diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs
--- a/test/RewriterSpec.hs
+++ b/test/RewriterSpec.hs
@@ -16,6 +16,7 @@
 import System.FilePath (makeRelative, replaceExtension, (</>))
 import Test.Hspec (Spec, describe, it, runIO, shouldBe)
 import Yaml qualified as Y
+import Data.Char (isSpace)
 
 data Rules = Rules
   { basic :: Maybe [String],
@@ -33,6 +34,9 @@
 yamlPack :: FilePath -> IO YamlPack
 yamlPack = Yaml.decodeFileThrow
 
+noSpaces :: String -> String
+noSpaces = filter (not . isSpace)
+
 spec :: Spec
 spec = do
   describe "rewrite packs" $ do
@@ -59,5 +63,5 @@
                 _ -> pure []
             Nothing -> pure []
           rewritten <- runIO $ rewrite input' rules'
-          it (makeRelative resources pth) (rewritten `shouldBe` output')
+          it (makeRelative resources pth) (noSpaces rewritten `shouldBe` noSpaces output')
       )
diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs
--- a/test/YamlSpec.hs
+++ b/test/YamlSpec.hs
@@ -1,14 +1,31 @@
+{-# 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, it, runIO, shouldReturn)
-import Yaml (yamlRule)
+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)
+
 spec :: Spec
 spec = do
   describe "parses yaml rule" $ do
@@ -19,4 +36,24 @@
       ( \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
+            )
       )