diff --git a/eo-phi-normalizer/eo-phi-normalizer.cabal b/eo-phi-normalizer/eo-phi-normalizer.cabal
index b47fe0c17..b2cbd8b4a 100644
--- a/eo-phi-normalizer/eo-phi-normalizer.cabal
+++ b/eo-phi-normalizer/eo-phi-normalizer.cabal
@@ -390,6 +390,11 @@ extra-source-files:
     data/0.50.0/org/eolang/tuple.phi
     data/0.50.0/org/eolang/txt/sprintf.phi
     data/0.50.0/org/eolang/while.phi
+    test/eo/phi/confluence.yaml
+    test/eo/phi/dataization.yaml
+    test/eo/phi/from-eo/as-phi.yaml
+    test/eo/phi/metrics.yaml
+    test/eo/phi/rewriting.yaml
     test/eo/phi/rules/new.yaml
     test/eo/phi/rules/streams.yaml
     test/eo/phi/rules/yegor.yaml
@@ -430,7 +435,6 @@ library
       Language.EO.Phi.Report.Html
       Language.EO.Phi.Rules.Common
       Language.EO.Phi.Rules.Fast
-      Language.EO.Phi.Rules.PhiPaper
       Language.EO.Phi.Rules.RunYegor
       Language.EO.Phi.Rules.Yaml
       Language.EO.Phi.Syntax
@@ -561,7 +565,6 @@ test-suite doctests
       Language.EO.Phi.Report.Html
       Language.EO.Phi.Rules.Common
       Language.EO.Phi.Rules.Fast
-      Language.EO.Phi.Rules.PhiPaper
       Language.EO.Phi.Rules.RunYegor
       Language.EO.Phi.Rules.Yaml
       Language.EO.Phi.Syntax
@@ -625,6 +628,7 @@ test-suite spec
   main-is: Main.hs
   other-modules:
       Language.EO.Phi.DataizeSpec
+      Language.EO.Phi.RewriteSpec
       Language.EO.PhiSpec
       Language.EO.Rules.PhiPaperSpec
       Language.EO.YamlSpec
diff --git a/eo-phi-normalizer/package.yaml b/eo-phi-normalizer/package.yaml
index c906ba9fe..6a97c2b8c 100644
--- a/eo-phi-normalizer/package.yaml
+++ b/eo-phi-normalizer/package.yaml
@@ -35,7 +35,7 @@ extra-source-files:
   - grammar/EO/Phi/Syntax.cf
   - report/**/*
   - data/**/*
-  - test/eo/phi/rules/**
+  - test/eo/phi/**/*
 
 verbatim:
   cabal-version: 1.24
diff --git a/eo-phi-normalizer/src/Language/EO/Phi.hs b/eo-phi-normalizer/src/Language/EO/Phi.hs
index 3822bbff8..ad2cae64c 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi.hs
@@ -22,21 +22,18 @@
 -- SOFTWARE.
 {- FOURMOLU_ENABLE -}
 module Language.EO.Phi (
-  defaultMain,
   normalize,
   parseProgram,
   unsafeParseObject,
   unsafeParseProgram,
+  unsafeParseProgramFromFile,
   module Language.EO.Phi.Syntax,
 ) where
 
-import System.Exit (exitFailure)
-
-import Language.EO.Phi.Syntax.Abs qualified as Phi
-import Language.EO.Phi.Syntax.Par qualified as Phi
-
 import Language.EO.Phi.Normalize
 import Language.EO.Phi.Syntax
+import Language.EO.Phi.Syntax.Abs qualified as Phi
+import Language.EO.Phi.Syntax.Par qualified as Phi
 
 -- | Parse a 'Program' or return a parsing error.
 parseProgram :: String -> Either String Phi.Program
@@ -59,16 +56,9 @@ unsafeParseProgram input =
 unsafeParseObject :: String -> Phi.Object
 unsafeParseObject = either error id . parseObject
 
--- | Default entry point.
--- Parses a 𝜑-program from standard input, normalizes,
--- then pretty-prints the result to standard output.
-defaultMain :: IO ()
-defaultMain = do
-  input <- getContents -- read entire standard input
-  let tokens = Phi.myLexer input
-  case Phi.pProgram tokens of
-    Left parseError -> do
-      putStrLn parseError
-      exitFailure
-    Right program -> do
-      putStrLn (printTree (normalize program))
+unsafeParseProgramFromFile :: FilePath -> IO Phi.Program
+unsafeParseProgramFromFile inputFile = do
+  src <- readFile inputFile
+  case parseProgram src of
+    Left err -> error ("Error parsing program from '" ++ inputFile ++ "':\n" ++ err)
+    Right program -> pure program
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs b/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs
deleted file mode 100644
index 238ad6522..000000000
--- a/eo-phi-normalizer/src/Language/EO/Phi/Rules/PhiPaper.hs
+++ /dev/null
@@ -1,42 +0,0 @@
-{- FOURMOLU_DISABLE -}
--- The MIT License (MIT)
-
--- Copyright (c) 2016-2024 Objectionary.com
-
--- Permission is hereby granted, free of charge, to any person obtaining a copy
--- of this software and associated documentation files (the "Software"), to deal
--- in the Software without restriction, including without limitation the rights
--- to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
--- copies of the Software, and to permit persons to whom the Software is
--- furnished to do so, subject to the following conditions:
-
--- The above copyright notice and this permission notice shall be included
--- in all copies or substantial portions of the Software.
-
--- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
--- IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
--- FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
--- AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
--- LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
--- OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
--- SOFTWARE.
-{- FOURMOLU_ENABLE -}
-module Language.EO.Phi.Rules.PhiPaper where
-
-import Control.Monad (guard)
-import Language.EO.Phi
-import Language.EO.Phi.Rules.Common
-
--- * Yegor's Rules
-
--- | Rule 6.
-rule6 :: Rule
-rule6 ctx (ObjectDispatch (Formation bindings) a)
-  | Just obj <- lookupBinding a bindings = do
-      guard (isNF ctx obj)
-      return (Application obj [AlphaBinding Rho (Formation bindings')])
- where
-  bindings' = filter (not . isDispatched) bindings
-  isDispatched (AlphaBinding a' _) = a == a'
-  isDispatched _ = False
-rule6 _ _ = []
diff --git a/eo-phi-normalizer/src/Language/EO/Phi/TH.hs b/eo-phi-normalizer/src/Language/EO/Phi/TH.hs
index 78ff19b1a..f5c524510 100644
--- a/eo-phi-normalizer/src/Language/EO/Phi/TH.hs
+++ b/eo-phi-normalizer/src/Language/EO/Phi/TH.hs
@@ -24,7 +24,7 @@
 module Language.EO.Phi.TH where
 
 import Data.Aeson (Options (..), SumEncoding (..), camelTo2)
-import Data.Aeson.TH as TH (deriveJSON)
+import Data.Aeson.TH as TH (deriveFromJSON, deriveJSON)
 import Data.Aeson.Types (defaultOptions)
 import Language.Haskell.TH (Dec, Name, Q)
 
@@ -38,3 +38,6 @@ defaultOptions' =
 
 deriveJSON :: Name -> Q [Dec]
 deriveJSON = TH.deriveJSON defaultOptions'
+
+deriveFromJSON :: Name -> Q [Dec]
+deriveFromJSON = TH.deriveFromJSON defaultOptions'
diff --git a/eo-phi-normalizer/test/Language/EO/Phi/DataizeSpec.hs b/eo-phi-normalizer/test/Language/EO/Phi/DataizeSpec.hs
index b31909648..27a45d34f 100644
--- a/eo-phi-normalizer/test/Language/EO/Phi/DataizeSpec.hs
+++ b/eo-phi-normalizer/test/Language/EO/Phi/DataizeSpec.hs
@@ -38,7 +38,7 @@ import Language.EO.Phi.Dataize.Context (defaultContext)
 import Language.EO.Phi.Dependencies (deepMergePrograms)
 import Language.EO.Phi.Rules.Common (equalObject)
 import Language.EO.Phi.Rules.Yaml (convertRuleNamed, parseRuleSetFromFile, rules)
-import Test.EO.Phi (DataizationResult (Bytes, Object), DataizeTest (..), DataizeTestGroup (..), dataizationTests)
+import Test.EO.Phi (DataizationResult (Bytes, Object), DataizeTest (..), DataizeTestGroup (..), dataizationTests, progToObj)
 
 newtype ObjectOrBytes = ObjectOrBytes (Either Phi.Object Phi.Bytes)
 
@@ -53,13 +53,6 @@ instance Eq ObjectOrBytes where
     x == y
   _ == _ = False
 
-getProgram :: FilePath -> IO Phi.Program
-getProgram inputFile = do
-  src <- readFile inputFile
-  case Phi.parseProgram src of
-    Left err -> error ("Error parsing program from '" ++ inputFile ++ "': " ++ err)
-    Right program -> pure program
-
 spec :: Spec
 spec = do
   DataizeTestGroup{..} <- runIO (dataizationTests "test/eo/phi/dataization.yaml")
@@ -75,7 +68,7 @@ spec = do
         describe rulesTitle do
           forM_ tests $
             \test -> do
-              deps <- runIO $ mapM getProgram test.dependencies
+              deps <- runIO $ mapM Phi.unsafeParseProgramFromFile test.dependencies
               let mergedProgs = case deepMergePrograms (test.input : deps) of
                     Left err -> error ("Error merging programs: " ++ err)
                     Right prog -> prog
@@ -87,6 +80,3 @@ spec = do
               it test.name $ do
                 let dataizedResult = dataizeRecursively ctx inputObj
                 ObjectOrBytes dataizedResult `shouldBe` ObjectOrBytes expectedResult
-
-progToObj :: Phi.Program -> Phi.Object
-progToObj (Phi.Program bindings) = Phi.Formation bindings
diff --git a/eo-phi-normalizer/test/Language/EO/Phi/RewriteSpec.hs b/eo-phi-normalizer/test/Language/EO/Phi/RewriteSpec.hs
new file mode 100644
index 000000000..3ca52c0e1
--- /dev/null
+++ b/eo-phi-normalizer/test/Language/EO/Phi/RewriteSpec.hs
@@ -0,0 +1,81 @@
+{- FOURMOLU_DISABLE -}
+-- The MIT License (MIT)
+
+-- Copyright (c) 2016-2024 Objectionary.com
+
+-- Permission is hereby granted, free of charge, to any person obtaining a copy
+-- of this software and associated documentation files (the "Software"), to deal
+-- in the Software without restriction, including without limitation the rights
+-- to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+-- copies of the Software, and to permit persons to whom the Software is
+-- furnished to do so, subject to the following conditions:
+
+-- The above copyright notice and this permission notice shall be included
+-- in all copies or substantial portions of the Software.
+
+-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+-- IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+-- FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
+-- AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+-- LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+-- OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+-- SOFTWARE.
+{- FOURMOLU_ENABLE -}
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Language.EO.Phi.RewriteSpec where
+
+import Control.Monad (forM_)
+import Data.Yaml qualified as Yaml
+import GHC.Generics (Generic)
+import Language.EO.Phi (Program (..))
+import Language.EO.Phi.Dataize.Context (defaultContext)
+import Language.EO.Phi.Rules.Common (applyRules)
+import Language.EO.Phi.Rules.Yaml (convertRuleNamed, parseRuleSetFromFile, rules)
+import Language.EO.Phi.Syntax (printTree)
+import Language.EO.Phi.TH
+import Test.EO.Phi (progToObj)
+import Test.Hspec
+
+data Test = Test
+  { name :: String
+  , input :: Program
+  , output :: Program
+  }
+  deriving stock (Generic, Show)
+
+$(deriveFromJSON ''Test)
+
+data RewriteTests = RewriteTests
+  { title :: String
+  , tests :: [Test]
+  }
+  deriving stock (Generic, Show)
+
+$(deriveFromJSON ''RewriteTests)
+
+spec :: Spec
+spec = do
+  rewriteTests <- runIO (Yaml.decodeFileThrow @_ @RewriteTests "test/eo/phi/rewriting.yaml")
+  describe rewriteTests.title do
+    forM_
+      [ ("New Yegor's rules", "test/eo/phi/rules/new.yaml")
+      ]
+      $ \(rulesTitle, rulesFile) -> do
+        ruleset <- runIO $ parseRuleSetFromFile rulesFile
+        let rules' = convertRuleNamed <$> ruleset.rules
+        describe rulesTitle do
+          forM_ rewriteTests.tests $
+            \test -> it test.name do
+              let
+                inputObj = progToObj test.input
+                expectedOutputObj = progToObj test.output
+                ctx = defaultContext rules' inputObj
+                outputObj = head $ applyRules ctx inputObj
+              printTree outputObj `shouldBe` printTree expectedOutputObj
diff --git a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
index 49fc71ed3..da38fa7ef 100644
--- a/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
+++ b/eo-phi-normalizer/test/Language/EO/PhiSpec.hs
@@ -25,10 +25,8 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedRecordDot #-}
-{-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE ViewPatterns #-}
 
 module Language.EO.PhiSpec where
 
@@ -37,15 +35,12 @@ import Data.Char (isSpace)
 import Data.List (dropWhileEnd)
 import Data.String (IsString (..))
 import Data.Yaml (decodeFileThrow)
-import Language.EO.Phi
-import Language.EO.Phi.Dataize.Context (defaultContext)
+import Language.EO.Phi (Binding (..), Object, Program (..), normalize, printTree)
 import Language.EO.Phi.Metrics.Collect (getProgramMetrics)
 import Language.EO.Phi.Metrics.Data (BindingsByPathMetrics (..), ProgramMetrics (..))
-import Language.EO.Phi.Rules.Common (Rule, equalProgram)
-import Language.EO.Phi.Rules.PhiPaper (rule6)
-import PyF (fmt)
-import Test.EO.Phi
-import Test.Hspec
+import Language.EO.Phi.Rules.Common (equalProgram)
+import Test.EO.Phi (PhiTest (..), PhiTestGroup (..), allPhiTests)
+import Test.Hspec (Spec, describe, it, runIO, shouldBe, shouldSatisfy)
 import Test.Metrics.Phi (MetricsTest (..), MetricsTestSet (..))
 
 applyRule :: (Object -> [Object]) -> Program -> [Program]
@@ -57,15 +52,6 @@ applyRule rule = \case
 
 spec :: Spec
 spec = do
-  describe "Pre-defined rules" $
-    forM_ ([(6, rule6)] :: [(Int, Rule)]) $
-      \(idx, rule) -> do
-        PhiTestGroup{..} <- runIO (fileTests [fmt|test/eo/phi/rule-{idx}.yaml|])
-        describe title $
-          forM_ tests $
-            \PhiTest{..} ->
-              it name $
-                applyRule (rule (defaultContext [] (progToObj input))) input `shouldBe` [normalized]
   describe "Programs translated from EO" $ do
     phiTests <- runIO (allPhiTests "test/eo/phi/from-eo/")
     forM_ phiTests $ \PhiTestGroup{..} ->
@@ -86,6 +72,3 @@ spec = do
 
 trim :: String -> String
 trim = dropWhileEnd isSpace
-
-progToObj :: Program -> Object
-progToObj (Program bindings) = Formation bindings
diff --git a/eo-phi-normalizer/test/Test/EO/Phi.hs b/eo-phi-normalizer/test/Test/EO/Phi.hs
index 4f487c507..64a914c7a 100644
--- a/eo-phi-normalizer/test/Test/EO/Phi.hs
+++ b/eo-phi-normalizer/test/Test/EO/Phi.hs
@@ -71,10 +71,12 @@ data DataizeTest = DataizeTest
   , dependencies :: [FilePath]
   }
   deriving (Generic, FromJSON)
+
 data DataizationResult
   = Bytes {bytes :: Phi.Bytes}
   | Object {object :: Phi.Object}
   deriving (Generic, Show)
+
 instance FromJSON DataizationResult where
   parseJSON = genericParseJSON defaultOptions{sumEncoding = UntaggedValue}
 
@@ -101,3 +103,6 @@ instance FromJSON Phi.Object where
   parseJSON = fmap unsafeParseObject . parseJSON
 
 deriving newtype instance FromJSON Phi.Bytes
+
+progToObj :: Phi.Program -> Phi.Object
+progToObj (Phi.Program bindings) = Phi.Formation bindings
diff --git a/eo-phi-normalizer/test/eo/phi/rewriting.yaml b/eo-phi-normalizer/test/eo/phi/rewriting.yaml
new file mode 100644
index 000000000..d681076a7
--- /dev/null
+++ b/eo-phi-normalizer/test/eo/phi/rewriting.yaml
@@ -0,0 +1,120 @@
+# The MIT License (MIT)
+
+# Copyright (c) 2016-2024 Objectionary.com
+
+# Permission is hereby granted, free of charge, to any person obtaining a copy
+# of this software and associated documentation files (the "Software"), to deal
+# in the Software without restriction, including without limitation the rights
+# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+# copies of the Software, and to permit persons to whom the Software is
+# furnished to do so, subject to the following conditions:
+
+# The above copyright notice and this permission notice shall be included
+# in all copies or substantial portions of the Software.
+
+# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+# FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
+# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+# SOFTWARE.
+
+title: "Rewriting tests (integration tests)"
+tests:
+# TODO #655:10m Enable
+# - name: e-alph
+#   input: |
+#     {⟦ k ↦ ⟦ x ↦ ∅ ⟧ ( α0 ↦ ⟦ Δ ⤍ 42- ⟧ ).x ⟧}
+#   output: |
+#     {⟦ k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧}
+# - name: e-fnk
+#   input: |
+#     {⟦ m ↦ ⟦ x ↦ ⟦ t ↦ ∅ ⟧ (t ↦ ξ.k), k ↦ ⟦ λ ⤍ Fn ⟧ ⟧.x.t.p ⟧}
+#   output: |
+#     {⟦ m ↦ ⟦ λ ⤍ Fn, ρ ↦ ⟦ x ↦ ⟦ t ↦ ∅ ⟧ (t ↦ ξ.k), k ↦ ⟦ λ ⤍ Fn ⟧ ⟧ ⟧.p ⟧}
+- name: e-ald
+  input: |
+    {⟦ k ↦ ⟦ x ↦ ∅ ⟧ ( α1 ↦ ⟦ Δ ⤍ 42- ⟧ ).x ⟧}
+  output: |
+    {⟦ k ↦ ⊥ ⟧}
+- name: e-app
+  input: |
+    {⟦ k ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧ (t ↦ ⟦ Δ ⤍ 42- ⟧) ⟧}
+  output: |
+    {⟦ k ↦ ⟦ t ↦ ⟦ Δ ⤍ 42- ⟧, x ↦ ξ.t ⟧ ⟧}
+- name: e-cpy
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ∅, y ↦ ξ.x ⟧ (x ↦ ⟦ Δ ⤍ 42- ⟧).y ⟧}
+  output: |
+    { ⟦ m ↦ ⟦ ρ ↦ ⟦ x ↦ ⟦ Δ ⤍ 42- ⟧, y ↦ ξ.x ⟧, Δ ⤍ 42- ⟧ ⟧}
+- name: e-int
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ⟦ t ↦ ⟦ Δ ⤍ 42- ⟧ ⟧.t ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⟦ ρ ↦ ⟦ t ↦ ⟦ Δ ⤍ 42- ⟧ ⟧, Δ ⤍ 42- ⟧ ⟧}
+- name: e-lam
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ⟦ λ ⤍ Fn ⟧.ρ.k, k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⟦ λ ⤍ Fn ⟧.ρ.k(ρ ↦ ⟦ x ↦ ⟦ λ ⤍ Fn ⟧.ρ.k, k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧ ) ⟧}
+- name: e-nf
+  input: |
+    {⟦ x ↦ ⟦ t ↦ Φ.x ⟧ ⟧}
+  output: |
+    {⟦ x ↦ ⟦ t ↦ Φ.x ⟧ ⟧}
+- name: e-nk
+  input: |
+    {⟦ x ↦ ξ.k, k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧}
+  output: |
+    {⟦ x ↦ ξ.k, k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧}
+- name: e-np
+  input: |
+    {⟦ x ↦ ξ.t, λ ⤍ Fn ⟧}
+  output: |
+    {⟦ x ↦ ξ.t, λ ⤍ Fn ⟧}
+- name: e-nr
+  input: |
+    {⟦ x ↦ ξ.k, t ↦ ⟦ Δ ⤍ 42- ⟧ ⟧}
+  output: |
+    {⟦ x ↦ ξ.k, t ↦ ⟦ Δ ⤍ 42- ⟧ ⟧}
+- name: e-nt
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ⟦ Δ ⤍ 42- ⟧, λ ⤍ Fn ⟧.y ⟧}
+  output: |
+    {⟦ m ↦ ⟦ x ↦ ⟦ Δ ⤍ 42- ⟧, λ ⤍ Fn ⟧.y ⟧}
+- name: e-phi
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ξ.t, φ ↦ ⟦ t ↦ ⟦⟧ ⟧ ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⟦ ρ ↦ ⟦ t ↦ ⟦ ⟧, ρ ↦ ⟦ φ ↦ ⟦ t ↦ ⟦ ⟧ ⟧, x ↦ ξ.t ⟧ ⟧ ⟧ ⟧}
+- name: e-rep
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ξ.t (k ↦ ξ.f).k, t ↦ ⟦ k ↦ ∅ ⟧, f ↦ ⟦⟧ ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⟦ ρ ↦ ⟦f ↦ ⟦⟧, x ↦ ξ.t (k ↦ ξ.f).k, t ↦ ⟦k ↦ ∅⟧ ⟧ ⟧ ⟧}
+- name: e-rha
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ⟦ ρ ↦ ∅ ⟧.ρ.k, k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⊥ ⟧}
+- name: e-rhi
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ⟦ t ↦ ⟦ p ↦ ξ.ρ.ρ.k ⟧.p ⟧.t, k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⊥ ⟧}
+- name: e-rho
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ξ.ρ.ρ.t ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⊥ ⟧}
+- name: e-twi
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ⟦ t ↦ ξ.ρ.k.ρ.t ⟧, k ↦ ⟦⟧, t ↦ ⟦⟧ ⟧.x.t ⟧}
+  output: |
+    { ⟦ m ↦ ⟦ ρ ↦ ⟦ t ↦ ⟦ ⟧, ρ ↦ ⟦ ρ ↦ ⟦ x ↦ ⟦ t ↦ ξ.ρ.k.ρ.t ⟧, k ↦ ⟦ ⟧, t ↦ ⟦ ⟧ ⟧, t ↦ ξ.ρ.k.ρ.t ⟧, k ↦ ⟦ ⟧, x ↦ ⟦ t ↦ ξ.ρ.k.ρ.t ⟧ ⟧ ⟧ ⟧}
+- name: e-xxi
+  input: |
+    {⟦ m ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧.x ⟧}
+  output: |
+    {⟦ m ↦ ⊥ ⟧}
diff --git a/eo-phi-normalizer/test/eo/phi/rule-6.yaml b/eo-phi-normalizer/test/eo/phi/rule-6.yaml
deleted file mode 100644
index d323d0440..000000000
--- a/eo-phi-normalizer/test/eo/phi/rule-6.yaml
+++ /dev/null
@@ -1,60 +0,0 @@
-# The MIT License (MIT)
-
-# Copyright (c) 2016-2024 Objectionary.com
-
-# Permission is hereby granted, free of charge, to any person obtaining a copy
-# of this software and associated documentation files (the "Software"), to deal
-# in the Software without restriction, including without limitation the rights
-# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-# copies of the Software, and to permit persons to whom the Software is
-# furnished to do so, subject to the following conditions:
-
-# The above copyright notice and this permission notice shall be included
-# in all copies or substantial portions of the Software.
-
-# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-# FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE
-# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-# SOFTWARE.
-
-title: Tests for Rule 6
-tests:
-  - name: "Case (1)"
-    input: |
-      { ⟦ a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b ⟧ }
-    normalized: |
-      { ⟦ a ↦ ⟦ Δ ⤍ 00- ⟧(ρ ↦ ⟦ c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧) ⟧ }
-    prettified: |
-      { ⟦ a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b ⟧ }
-  - name: "Case (2)"
-    input: |
-      { ⟦
-        a ↦
-          ⟦
-            b ↦
-              ⟦
-                c ↦ ∅,
-                d ↦ ⟦ φ ↦ ξ.ρ.c ⟧
-              ⟧,
-            e ↦ ξ.b(c ↦ ⟦⟧).d
-          ⟧.e
-        ⟧
-      }
-    normalized: |
-      { ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ }
-    prettified: |
-      { ⟦
-        a ↦
-          ⟦
-            b ↦
-              ⟦
-                c ↦ ∅,
-                d ↦ ⟦ φ ↦ ξ.ρ.c ⟧
-              ⟧,
-            e ↦ ξ.b(c ↦ ⟦⟧).d
-          ⟧.e
-        ⟧
-      }