diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@
 
 ```bash
 cabal update
-cabal install --overwrite-policy=always phino-0.0.0.62
+cabal install --overwrite-policy=always phino-0.0.0.63
 phino --version
 ```
 
@@ -195,23 +195,23 @@
 ```bash
 $ phino explain --normalize
 \begin{tabular}{rl}
-\trrule{ALPHA}
+\trrule{alpha}
   { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_2 -> e ) }
   { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }
-  { if $ \indexof{ \tau_2 } = |B_1| $ }
+  { if $ \indexof{ \tau_2 } = \vert B_1 \vert $ }
   { }
-\trrule{COPY}
+\trrule{copy}
   { [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e_1 ) }
   { [[ B_1, \tau -> e_3, B_2 ]] }
   { if $ \isnormal{ e_1 } $ }
   { where $ e_2 \coloneqq \scopeof{ e_1 } $ and $ e_3 \coloneqq \ctx{ e_1 }{ e_2 } $ }
-\trrule{DC}
+\trrule{dc}
   { T ( \tau -> e ) }
   { T }
   { }
   { }
 ...
-\trrule{STOP}
+\trrule{stop}
   { [[ B ]] . \tau }
   { T }
   { if $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.0.63
+version: 0.0.0.64
 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/resources/alpha.yaml b/resources/alpha.yaml
--- a/resources/alpha.yaml
+++ b/resources/alpha.yaml
@@ -1,7 +1,7 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: ALPHA
+name: alpha
 pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒)
 result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)
 when:
diff --git a/resources/copy.yaml b/resources/copy.yaml
--- a/resources/copy.yaml
+++ b/resources/copy.yaml
@@ -1,7 +1,7 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: COPY
+name: copy
 pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒1)
 result: ⟦ 𝐵1, 𝜏 ↦ 𝑒3, 𝐵2 ⟧
 when:
diff --git a/resources/dc.yaml b/resources/dc.yaml
--- a/resources/dc.yaml
+++ b/resources/dc.yaml
@@ -1,6 +1,6 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: DC
+name: dc
 pattern: ⊥(𝜏 ↦ 𝑒)
 result: ⊥
diff --git a/resources/dd.yaml b/resources/dd.yaml
--- a/resources/dd.yaml
+++ b/resources/dd.yaml
@@ -1,6 +1,6 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: DD
+name: dd
 pattern: ⊥.𝜏
 result: ⊥
diff --git a/resources/dot.yaml b/resources/dot.yaml
--- a/resources/dot.yaml
+++ b/resources/dot.yaml
@@ -1,7 +1,7 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: DOT
+name: dot
 pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧.𝜏
 result: 𝑒2(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧)
 when:
diff --git a/resources/miss.yaml b/resources/miss.yaml
--- a/resources/miss.yaml
+++ b/resources/miss.yaml
@@ -1,7 +1,7 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: MISS
+name: miss
 pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒)
 result: ⊥
 when:
diff --git a/resources/null.yaml b/resources/null.yaml
--- a/resources/null.yaml
+++ b/resources/null.yaml
@@ -1,6 +1,6 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: 'NULL'
+name: 'null'
 pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏
 result: ⊥
diff --git a/resources/over.yaml b/resources/over.yaml
--- a/resources/over.yaml
+++ b/resources/over.yaml
@@ -1,7 +1,7 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: OVER
+name: over
 pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2)
 result: ⊥
 when:
diff --git a/resources/phi.yaml b/resources/phi.yaml
--- a/resources/phi.yaml
+++ b/resources/phi.yaml
@@ -1,7 +1,7 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: PHI
+name: phi
 pattern: ⟦𝐵⟧.𝜏
 result: ⟦𝐵⟧.φ.𝜏
 when:
diff --git a/resources/stay.yaml b/resources/stay.yaml
--- a/resources/stay.yaml
+++ b/resources/stay.yaml
@@ -1,6 +1,6 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: STAY
+name: stay
 pattern: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧(ρ ↦ 𝑒2)
 result: ⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧
diff --git a/resources/stop.yaml b/resources/stop.yaml
--- a/resources/stop.yaml
+++ b/resources/stop.yaml
@@ -1,7 +1,7 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-name: STOP
+name: stop
 pattern: ⟦𝐵⟧.𝜏
 result: ⊥
 when:
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -13,7 +13,6 @@
 import AST
 import Builder
 import Control.Exception (Exception, throwIO)
-import Data.Char (toLower)
 import Data.Maybe (fromMaybe)
 import qualified Data.Set as Set
 import Deps
@@ -180,7 +179,7 @@
       where
         leadsTo :: Program -> [Rewritten]
         leadsTo _prog = case _rewrittens of
-          (program, _) : rest -> (_prog, Nothing) : (program, Just (map toLower (fromMaybe "unknown" (Y.name rule)))) : rest
+          (program, _) : rest -> (_prog, Nothing) : (program, Just (fromMaybe "unknown" (Y.name rule))) : rest
           [] -> [(_prog, Nothing)]
 
 -- Rewrite program by provided locator from RewriteContext
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -292,7 +292,7 @@
               logDebug "The 'when' condition wasn't met"
               pure []
             else do
-              logDebug (printf "Rule %s" (fromMaybe "unknown" (Y.name rule)))
+              logDebug (printf "Rule %s" name)
               extended <- extraSubstitutions when' (Y.where_ rule) ctx
               if null extended
                 then do
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -723,7 +723,7 @@
           ["rewrite", "--log-level=debug", "--log-lines=1", "--normalize"]
           [ intercalate
               "\n"
-              [ "[DEBUG]: Applied 'COPY' (44 nodes -> 39 nodes)"
+              [ "[DEBUG]: Applied 'copy' (44 nodes -> 39 nodes)"
               , "---| log is limited by --log-lines=1 option |---"
               ]
           ]
@@ -821,7 +821,7 @@
         ["explain", "--rule=resources/copy.yaml"]
         [ unlines
             [ "\\begin{tabular}{rl}"
-            , "\\trrule{COPY}"
+            , "\\trrule{copy}"
             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"
             , "  { [[ B_1, \\tau -> e_3, B_2 ]] }"
             , "  { if $ \\isnormal{ e_1 } $ }"
@@ -833,64 +833,64 @@
     it "explains multiple rules" $
       testCLISucceeded
         ["explain", "--rule=resources/copy.yaml", "--rule=resources/alpha.yaml"]
-        ["\\begin{tabular}{rl}", "\\trrule{COPY}", "\\trrule{ALPHA}"]
+        ["\\begin{tabular}{rl}", "\\trrule{copy}", "\\trrule{alpha}"]
 
     it "explains normalization rules" $
       testCLISucceeded
         ["explain", "--normalize"]
         [ unlines
             [ "\\begin{tabular}{rl}"
-            , "\\trrule{ALPHA}"
+            , "\\trrule{alpha}"
             , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_2 -> e ) }"
             , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e ) }"
             , "  { if $ \\indexof{ \\tau_2 } = \\vert B_1 \\vert $ }"
             , "  { }"
-            , "\\trrule{COPY}"
+            , "\\trrule{copy}"
             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e_1 ) }"
             , "  { [[ B_1, \\tau -> e_3, B_2 ]] }"
             , "  { if $ \\isnormal{ e_1 } $ }"
             , "  { where $ e_2 \\coloneqq \\scopeof{ e_1 } $ and $ e_3 \\coloneqq \\ctx{ e_1 }{ e_2 } $ }"
-            , "\\trrule{DC}"
+            , "\\trrule{dc}"
             , "  { T ( \\tau -> e ) }"
             , "  { T }"
             , "  { }"
             , "  { }"
-            , "\\trrule{DD}"
+            , "\\trrule{dd}"
             , "  { T . \\tau }"
             , "  { T }"
             , "  { }"
             , "  { }"
-            , "\\trrule{DOT}"
+            , "\\trrule{dot}"
             , "  { [[ B_1, \\tau -> e_1, B_2 ]] . \\tau }"
             , "  { e_2 ( ^ -> [[ B_1, \\tau -> e_1, B_2 ]] ) }"
             , "  { if $ \\isnormal{ e_1 } $ }"
             , "  { where $ e_2 \\coloneqq \\ctx{ e_1 }{ [[ B_1, \\tau -> e_1, B_2 ]] } $ }"
-            , "\\trrule{MISS}"
+            , "\\trrule{miss}"
             , "  { [[ B ]] ( \\tau -> e ) }"
             , "  { T }"
             , "  { if $ \\tau \\notin B \\;\\text{and}\\; \\tau \\notin [ ~0, ~1, \\dots ] $ }"
             , "  { }"
-            , "\\trrule{NULL}"
+            , "\\trrule{null}"
             , "  { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"
             , "  { T }"
             , "  { }"
             , "  { }"
-            , "\\trrule{OVER}"
+            , "\\trrule{over}"
             , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }"
             , "  { T }"
             , "  { if $ \\tau \\not= ^ $ }"
             , "  { }"
-            , "\\trrule{PHI}"
+            , "\\trrule{phi}"
             , "  { [[ B ]] . \\tau }"
             , "  { [[ B ]] . @ . \\tau }"
             , "  { if $ @ \\in B \\;\\text{and}\\; \\tau \\notin B $ }"
             , "  { }"
-            , "\\trrule{STAY}"
+            , "\\trrule{stay}"
             , "  { [[ B_1, ^ -> e_1, B_2 ]] ( ^ -> e_2 ) }"
             , "  { [[ B_1, ^ -> e_1, B_2 ]] }"
             , "  { }"
             , "  { }"
-            , "\\trrule{STOP}"
+            , "\\trrule{stop}"
             , "  { [[ B ]] . \\tau }"
             , "  { T }"
             , "  { if $ \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B $ }"