diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,12 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v2.2.1 - 2024-11-27
+
+### Changes and fixes
+
+- Fix rules file not included into the released Haskell package ([#568](https://github.com/objectionary/eo-phi-normalizer/pull/568))
+
 ## v2.2.0 - 2024-11-26
 
 ### Breaking changes
@@ -14,11 +20,11 @@
 
 ### Changes and fixes
 
-- Pretty printing doesn't put enough eols ([#550](https://github.com/objectionary/eo-phi-normalizer/pull/550))
+- Fix pretty-printing ([#550](https://github.com/objectionary/eo-phi-normalizer/pull/550))
 
 ### Documentation and maintenance
 
-- Menu is broken on the site ([#551](https://github.com/objectionary/eo-phi-normalizer/pull/551))
+- Fix menu on the site ([#551](https://github.com/objectionary/eo-phi-normalizer/pull/551))
 
 ## v2.1.0 - 2024-11-22
 
diff --git a/eo-phi-normalizer.cabal b/eo-phi-normalizer.cabal
--- a/eo-phi-normalizer.cabal
+++ b/eo-phi-normalizer.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           eo-phi-normalizer
-version:        2.2.0
+version:        2.2.1
 synopsis:       Command line normalizer of 𝜑-calculus expressions.
 description:    Please see the README on GitHub at <https://github.com/objectionary/eo-phi-normalizer#readme>
 homepage:       https://github.com/objectionary/eo-phi-normalizer#readme
@@ -189,6 +189,9 @@
     data/0.41.2/org/eolang/txt/sscanf.phi
     data/0.41.2/org/eolang/txt/text.phi
     data/0.41.2/org/eolang/while.phi
+    test/eo/phi/rules/new.yaml
+    test/eo/phi/rules/streams.yaml
+    test/eo/phi/rules/yegor.yaml
 
 source-repository head
   type: git
diff --git a/test/eo/phi/rules/new.yaml b/test/eo/phi/rules/new.yaml
new file mode 100644
--- /dev/null
+++ b/test/eo/phi/rules/new.yaml
@@ -0,0 +1,244 @@
+# 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: "Rule set following Nov 2024 revision"
+rules:
+
+  - name: DOT
+    description: 'Accessing an α-binding'
+    pattern: |
+      ⟦ !τ ↦ !b, !B ⟧.!τ
+    result: |
+      ⌈ !b , ⟦ !τ ↦ !b, !B ⟧ ⌉(ρ ↦ ⟦ !τ ↦ !b, !B ⟧)
+    when:
+      - nf: '!b'
+      - nf: '⟦ !B ⟧' #TODO: change the condition, every object in !B should be in the nf
+    tests:
+      - name: 'Contextualization changes ξ'
+        input: ⟦ a ↦ ξ ⟧.a
+        output: ['⟦ a ↦ ξ ⟧ (ρ ↦ ⟦ a ↦ ξ ⟧)']
+      - name: 'Contextualization applies recursively'
+        input: ⟦ a ↦ ξ.b ⟧.a
+        output: ['⟦ a ↦ ξ.b ⟧.b (ρ ↦ ⟦ a ↦ ξ.b ⟧)']
+      - name: Phi Paper - Example E2
+        input: '⟦ x ↦ ξ.t, t ↦ ∅ ⟧.x'
+        output: ['⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)']
+      - name:  Phi Paper - Example E3 - first R_dot
+        input: '⟦ x ↦ ⟦t ↦ ⟦ρ ↦ ⟦⟧⟧⟧.t ⟧.x'
+        output: ['⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦t ↦ ⟦ρ ↦ ⟦⟧⟧⟧) ⟧.x']
+      - name:  Phi Paper - Example E3 - second R_dot
+        input: '⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧.x'
+        output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦x ↦ ⟦ρ ↦ ⟦⟧⟧⟧)']
+      - name: Phi Paper - Example E4 - first R_dot
+        input: '⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.y'
+        # output: ['⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.x(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)']
+        output: ['⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧.x(ρ ↦ ⟦ y ↦ ξ.x, x ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧)']
+      - name: Phi Paper - Example E4 - second R_dot
+        input: ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧.x(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)
+        output: ['⟦ρ ↦ ⟦⟧⟧(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)(ρ ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧)']
+
+  - name: COPY
+    description: 'Application of α-binding'
+    pattern: |
+      ⟦ !τ1 ↦ ⟦ !τ2 ↦ ∅, !B1 ⟧(!τ2 ↦ !b, !B2) * !t, !B3 ⟧
+    result: |
+      ⟦ !τ1 ↦ ⟦ !τ2 ↦ ⌈ !b , ⟦ !τ1 ↦ ⟦ !τ2 ↦ ∅, !B1 ⟧(!τ2 ↦ !b, !B2), !B3 ⟧ ⌉, !B1 ⟧(!B2) * !t, !B3 ⟧
+    when:
+      - nf: '!b'
+      - nf: '⟦ !B1 ⟧'
+      - nf: '⟦ !B3 ⟧'
+    tests:
+      - name: Should match
+        input: ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧ ⟧ () ⟧']
+      - name: 'Should match'
+        input: ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ).a ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ ξ) ⟧ ⟧ ().a ⟧']
+      - name: Phi Paper - Example E1
+        input: ⟦ k ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧(t ↦ ⟦ρ ↦ ⟦⟧⟧) ⟧
+        # output: ['⟦ k ↦ ⟦ x ↦ ξ.t, t ↦ ⟦ρ ↦ ⟦⟧⟧ ⟧() ⟧']
+        output: ['⟦ k ↦ ⟦ t ↦ ⟦ρ ↦ ⟦⟧⟧, x ↦ ξ.t ⟧() ⟧']
+      - name: Phi Paper - Example E4 - dispatch on y
+        input: ⟦ k ↦ ⟦ x ↦ ∅, y ↦ ξ.x ⟧(x ↦ ⟦ρ ↦ ⟦⟧⟧).y ⟧
+        output: ['⟦ k ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧().y ⟧']
+      - name: Phi Paper - Example E4 - remove dispatch on y
+        input: ⟦ k ↦ ⟦ x ↦ ∅, y ↦ ξ.x ⟧(x ↦ ⟦ρ ↦ ⟦⟧⟧) ⟧
+        output: ['⟦ k ↦ ⟦ x ↦ ⟦ρ ↦ ⟦⟧⟧, y ↦ ξ.x ⟧() ⟧']
+
+  - name: RHO
+    description: 'Application of a ρ-binding'
+    pattern: |
+      ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧
+    result: |
+      ⟦ !τ ↦ ⟦ !B1, ρ ↦ ⌈ !b , ⟦ !τ ↦ ⟦ !B1 ⟧(ρ ↦ !b, !B2) * !t, !B3 ⟧ ⌉ ⟧(!B2), !B3 ⟧
+    when:
+      - nf: '!b'
+      - absent_attrs:
+          attrs: ['ρ']
+          bindings: ['!B1']
+    tests: []
+
+  - name: phi
+    description: 'Accessing a decorated object'
+    pattern: |
+      ⟦!B ⟧.!τ
+    result: |
+      ⟦!B ⟧.φ.!τ
+    when:
+      - nf: '⟦ !B ⟧'
+      - present_attrs:
+          attrs: ['φ']
+          bindings: ['!B']
+      - absent_attrs:
+          attrs: ['!τ']
+          bindings: ['!B']
+    tests: []
+
+  # there's no B2 in the result
+  - name: STAY
+    description: 'Application of a ρ-binding when ρ already exists'
+    pattern: |
+      ⟦ ρ ↦ !b1, !B1 ⟧ (ρ ↦ !b, !B2)
+    result: |
+      ⟦ ρ ↦ !b1, !B1 ⟧ (!B2)
+    when: []
+    tests:
+      - name: Phi Paper - Example E3 - first R_stay
+        input: ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧)(ρ ↦ ⟦ x ↦ ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧) ⟧)
+        output: [⟦ ρ ↦ ⟦⟧ ⟧()(ρ ↦ ⟦ x ↦ ⟦ ρ ↦ ⟦⟧ ⟧(ρ ↦ ⟦ t ↦ ⟦ ρ ↦ ⟦⟧ ⟧ ⟧) ⟧)]
+      - name: 'Should match'
+        input: '⟦ ρ ↦ ⟦ c ↦ ∅ ⟧ ⟧ (ρ ↦ ⟦ ⟧, b ↦ ξ)'
+        output: ['⟦ ρ ↦ ⟦ c ↦ ∅ ⟧ ⟧ (b ↦ ξ)']
+
+  - name: OVER
+    description: 'Invalid application (attribute already attached)'
+    pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2)
+    result: ⊥
+    when:
+      - not_equal: ['!τ', 'ρ']
+    tests:
+      - name: ''
+        input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
+        output: ['⊥']
+
+  - name: STOP
+    description: 'Absent attribute access'
+    pattern: |
+      ⟦ !B ⟧.!τ
+    result: |
+      ⊥
+    when:
+      - absent_attrs:
+          attrs: ['!τ', 'φ', 'λ']
+          bindings: ['!B']
+      - nf: '⟦ !B ⟧'
+    tests:
+      - name: 'Accessing nonexistent attribute'
+        input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x'
+        output: ['⊥']
+
+  # Named VOID instead of NULL because NULL is a keyword in yaml
+  - name: VOID
+    description: 'Void attribute access'
+    pattern: |
+      ⟦ !τ ↦ ∅, !B ⟧.!τ
+    result: |
+      ⊥
+    when: []
+    tests:
+      - name: Phi Paper Example E2 second dispatch
+        input: '⟦ x ↦ ξ.t, t ↦ ∅ ⟧.t(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)'
+        output: ['⊥(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)']
+
+  - name: DUP
+    description: 'Empty application'
+    pattern: |
+      ⟦ !B ⟧()
+    result: |
+      ⟦ !B ⟧
+    when: []
+    tests:
+      - name: Should match
+        input: ⟦ a ↦ ⟦⟧ ⟧()
+        output: ['⟦ a ↦ ⟦⟧ ⟧']
+      - name: Should not match
+        input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧)
+        output: []
+      - name: Should match in subformation
+        input: ⟦ a ↦ ⟦ b ↦ ⟦⟧() ⟧ ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧']
+      - name: Should work with empty formation
+        input: ⟦⟧()
+        output: ['⟦⟧']
+
+  - name: MISS
+    description: 'Invalid application (absent attribute)'
+    pattern: ⟦ !B1 ⟧(!τ ↦ !b, !B2)
+    result: ⊥
+    when:
+      - absent_attrs:
+          attrs: ['!τ']
+          bindings: ['!B1']
+      - not_equal: ['!τ', 'ρ']
+    tests:
+      - name: ''
+        input: '⟦ t1 ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
+        output: ['⊥']
+      - name: Should not match if attr is present
+        input: ⟦ t ↦ ⟦⟧ ⟧(t ↦ ⟦ a ↦ ∅ ⟧)
+        output: []
+      - name: Should not match for rho
+        input: ⟦ ⟧(ρ ↦ ⟦ ⟧)
+        output: []
+      - name: Should apply in subformations
+        input: ⟦ a ↦ ⟦ b ↦ ⟦⟧(t ↦ ⟦⟧) ⟧ ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']
+
+  - name: DD
+    description: 'Accessing an attribute on bottom'
+    pattern: |
+      ⊥.!τ
+    result: |
+      ⊥
+    when: []
+    tests:
+      - name: 'Dispatch on bottom is bottom'
+        input: '⊥.a'
+        output: ['⊥']
+      - name: 'Dispatch on anything else is not touched'
+        input: '⟦ ⟧.a'
+        output: []
+
+  - name: DC
+    description: 'Application on bottom is bottom'
+    pattern: |
+      ⊥(!B)
+    result: |
+      ⊥
+    when: []
+    tests:
+      - name: Should apply in subformations
+        input: ⟦ a ↦ ⟦ b ↦ ⊥(t ↦ ⟦⟧, u ↦ ⟦⟧) ⟧ ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']
+      - name: Phi Paper Example E2 last application
+        input: '⊥(ρ ↦ ⟦ x ↦ ξ.t, t ↦ ∅ ⟧)'
+        output: ['⊥']
diff --git a/test/eo/phi/rules/streams.yaml b/test/eo/phi/rules/streams.yaml
new file mode 100644
--- /dev/null
+++ b/test/eo/phi/rules/streams.yaml
@@ -0,0 +1,87 @@
+# 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: "Rules for Java Streams"
+rules:
+  - name: "[java.util.Stream] map ↦ for-each"
+    description: |
+      Replacing Java Stream's map with a for-each loop.
+    context:
+    forall:
+      - '!τ1'
+      - '!b1'
+      - '!b2'
+      - '!t1'
+      - '!B1'
+    pattern: |
+       ⟦
+        !τ1 ↦ !b1.java_util_Stream$map(α0 ↦ !b2) * !t1,
+        !B1
+       ⟧
+    result: |
+      ⟦
+        !τ2 ↦ !b1,
+        !τ3 ↦ Φ.opeo.map-for-each(
+          α0 ↦ ξ.!τ2,
+          α1 ↦ !b2
+        ),
+        !τ1 ↦ ξ.!τ3 * !t1,
+        !B1
+      ⟧
+    fresh:
+      - name: '!τ2'
+        prefix: 'foreach_body'
+      - name: '!τ3'
+        prefix: 'java_util_Stream$map_result'
+    when: []
+    tests:
+      - name: Simple map to for-each example works
+        input: |
+          ⟦
+            list ↦ ∅,
+            result ↦ ξ.list.java_util_Stream$filter(
+              α0 ↦ ⟦
+                el ↦ ∅,
+                φ ↦ ξ.el.equals(
+                  α0 ↦ Φ.org.eolang.string(as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))
+                ).not
+              ⟧
+            ).java_util_Stream$map(
+              α0 ↦ ⟦
+                el ↦ ∅,
+                φ ↦ Φ.java_util_Integer.parseInt(
+                  α0 ↦ ξ.el
+                )
+              ⟧
+            ).java_util_Stream$toList
+          ⟧
+        output:
+          - |
+            ⟦
+              foreach_body$1 ↦ ξ.list.java_util_Stream$filter (α0 ↦ ⟦
+                el ↦ ∅, φ ↦ ξ.el.equals (α0 ↦ Φ.org.eolang.string (as-bytes ↦ Φ.org.eolang.bytes (Δ ⤍ 00-))).not
+              ⟧),
+              java_util_Stream$map_result$1 ↦ Φ.opeo.map-for-each (α0 ↦ ξ.foreach_body$1, α1 ↦ ⟦
+                el ↦ ∅, φ ↦ Φ.java_util_Integer.parseInt (α0 ↦ ξ.el)
+              ⟧),
+              result ↦ ξ.java_util_Stream$map_result$1.java_util_Stream$toList, list ↦ ∅
+            ⟧
diff --git a/test/eo/phi/rules/yegor.yaml b/test/eo/phi/rules/yegor.yaml
new file mode 100644
--- /dev/null
+++ b/test/eo/phi/rules/yegor.yaml
@@ -0,0 +1,288 @@
+# 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: "Rule set based on Yegor's draft"
+rules:
+
+  - name: Phi
+    description: 'Φ-dispatch'
+    context:
+      global_object: '!b'
+    pattern: |
+      Φ
+    result: |
+      !b
+    when:
+      - apply_in_subformations: false
+    tests: []
+
+  - name: xi
+    description: 'ξ-dispatch'
+    context:
+      current_object: '!b'
+    pattern: |
+      ξ
+    result: |
+      !b
+    when:
+      - apply_in_subformations: false
+    tests:
+      - name: Does not replace ξ inside a subformation
+        input: '⟦ a ↦ ⟦ ⟧, x ↦ ξ.a, ρ ↦ ⟦ ⟧ ⟧'
+        output: []
+      # How to test replacing without already having context?
+
+  - name: DOT
+    description: 'Accessing an α-binding'
+    pattern: |
+      ⟦ !τ ↦ !b, !B ⟧.!τ
+    result: |
+      !b[ ξ ↦ ⟦ !τ ↦ !b, !B ⟧ ]
+    when:
+      - apply_in_abstract_subformations: false
+      - nf_inside_formation: '!b'
+      - nf: '⟦ !B ⟧'
+      - not_equal: ['!τ', 'ρ']
+    tests:
+      - name: Should match
+        input: ⟦ hello ↦ ⟦⟧ ⟧.hello
+        output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧ ⟧ ⟧']
+      - name: Shouldn't match
+        input: ⟦ ⟧.hello
+        output: []
+      - name: Shouldn't match
+        input: ⟦ ρ ↦ ⟦⟧ ⟧.ρ
+        output: []
+      - name: Should apply in subformations
+        input: ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ⟦⟧ ⟧ ⟧.b ⟧
+        output: ['⟦ a ↦ ⟦ c ↦ ⟦⟧, ρ ↦ ⟦ b ↦ ⟦ c ↦ ⟦⟧ ⟧ ⟧ ⟧ ⟧']
+      - name: Should respect surrounding context
+        input: ⟦ hello ↦ ⟦⟧, goodbye ↦ ⟦ a ↦ ⟦⟧ ⟧ ⟧.hello
+        output: ['⟦ ρ ↦ ⟦ hello ↦ ⟦⟧, goodbye ↦ ⟦ a ↦ ⟦⟧ ⟧ ⟧ ⟧']
+
+  - name: DOTrho
+    description: 'Accessing ρ-binding'
+    pattern: |
+      ⟦ ρ ↦ !b, !B ⟧.ρ
+    result: |
+      !b
+    when:
+      - nf: '⟦ !B ⟧'
+    tests:
+      - name: Should match
+        input: ⟦ ρ ↦ ⟦ ⟧ ⟧.ρ
+        output: ['⟦ ⟧']
+
+  - name: phi
+    description: 'Accessing a decorated object'
+    pattern: |
+      ⟦!B ⟧.!τ
+    result: |
+      ⟦!B ⟧.φ.!τ
+    when:
+      - present_attrs:
+          attrs: ['φ']
+          bindings: ['!B']
+      - absent_attrs:
+          attrs: ['!τ']
+          bindings: ['!B']
+    tests:
+      - name: 'Attribute does not exist'
+        input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.b'
+        output: ['⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.φ.b']
+      - name: 'Attribute exists'
+        input: '⟦ φ ↦ ⟦ ⟧, a ↦ ⟦ ⟧ ⟧.a'
+        output: []
+      - name: 'Both attributes do not exist'
+        input: '⟦ b ↦ ⟦⟧ ⟧.a'
+        output: []
+
+  - name: COPY
+    description: 'Application of α-binding'
+    context:
+      current_object: "!b2"
+    pattern: |
+      ⟦ !τ ↦ ∅, !B1 ⟧(!τ ↦ !b1, !B2)
+    result: |
+      ⟦ !τ ↦ !b1[ ξ ↦ !b2 ], !B1 ⟧(!B2)
+    when:
+      - apply_in_subformations: false
+      - nf: '!b1'
+    tests:
+      - name: Should match
+        input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧)
+        output: ['⟦ a ↦ ⟦ ρ ↦ ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧) ⟧ ⟧()']
+      - name: Should not match in subformations
+        input: ⟦ a ↦ ⟦b ↦ ∅⟧(b ↦ ⟦⟧) ⟧
+        output: []
+
+  - name: COPY1
+    description: 'Application of α-binding'
+    # Warning: this is not correct for the chain variant because it only matches the first binding
+    # i.e., doesn't match an empty binding after an attached one.
+    # We should instead match the first empty binding.
+    context:
+      current_object: "!b2"
+    pattern: |
+      ⟦ !τ ↦ ∅, !B ⟧(α0 ↦ !b1)
+    result: |
+      ⟦ !τ ↦ !b1[ ξ ↦ !b2 ], !B ⟧
+    when:
+      - apply_in_subformations: false
+      - nf: '!b1'
+    tests:
+      - name: Should match first void attribute
+        input: ⟦ hello ↦ ⟦⟧, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧)
+        output: ['⟦ bye ↦ ⟦ ρ ↦ ⟦ hello ↦ ⟦⟧, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧) ⟧, hello ↦ ⟦⟧, hey ↦ ∅ ⟧']
+        options:
+          - take_one: true
+
+  - name: COPY2
+    description: 'Application of α-binding'
+    # Warning: this is not correct for the chain variant because it only matches the first two bindings
+    # i.e., doesn't match an empty binding after an attached one.
+    # We should instead match the first two empty bindings.
+    context:
+      current_object: "!b3"
+    pattern: |
+      ⟦ !τ1 ↦ ∅, !τ2 ↦ ∅, !B ⟧(α0 ↦ !b1, α1 ↦ !b2)
+    result: |
+      ⟦ !τ1 ↦ !b1[ ξ ↦ !b3 ], !τ2 ↦ !b2[ ξ ↦ !b3 ], !B ⟧
+    when:
+      - apply_in_subformations: false
+      - nf: '!b1'
+      - nf: '!b2'
+    tests:
+      - name: Should match positional arguments
+        input: ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧)
+        output: ['⟦ hello ↦ ⟦ ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, bye ↦ ⟦ a ↦ ⟦⟧, ρ ↦ ⟦ hello ↦ ∅, bye ↦ ∅, hey ↦ ∅ ⟧(α0 ↦ ⟦⟧, α1 ↦ ⟦ a ↦ ⟦⟧ ⟧) ⟧, hey ↦ ∅ ⟧']
+        options:
+          - take_one: true
+
+  - name: COPYdelta
+    description: 'Application of Δ-binding'
+    pattern: |
+      ⟦ Δ ⤍ ∅, !B ⟧(Δ ⤍ !y)
+    result: |
+      ⟦ Δ ⤍ !y, !B ⟧
+    when:
+      - apply_in_abstract_subformations: false
+    tests: []
+
+  - name: EMPTY
+    description: 'Empty application'
+    pattern: |
+      ⟦ !B1 ⟧()
+    result: |
+      ⟦ !B1 ⟧
+    when: []
+    tests:
+      - name: Should match
+        input: ⟦ a ↦ ⟦⟧ ⟧()
+        output: ['⟦ a ↦ ⟦⟧ ⟧']
+      - name: Should not match
+        input: ⟦ a ↦ ∅ ⟧(a ↦ ⟦⟧)
+        output: []
+      - name: Should match in subformation
+        input: ⟦ a ↦ ⟦ b ↦ ⟦⟧() ⟧ ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧']
+      - name: Should work with empty formation
+        input: ⟦⟧()
+        output: ['⟦⟧']
+
+  - name: OVER
+    description: 'Invalid application (attribute already attached)'
+    pattern: ⟦ !τ ↦ !b1, !B1 ⟧(!τ ↦ !b2, !B2)
+    result: ⊥
+    when: []
+    tests:
+      - name: ''
+        input: '⟦ t ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
+        output: ['⊥']
+
+  - name: STOP
+    description: 'Invalid attribute access'
+    pattern: |
+      ⟦ !B ⟧.!τ
+    result: |
+      ⊥
+    when:
+      - absent_attrs:
+          attrs: ['!τ', 'φ', 'λ']
+          bindings: ['!B']
+      - present_attrs:
+          attrs: ['ρ']
+          bindings: ['!B']
+      - nf: '⟦ !B ⟧'
+    tests:
+      - name: 'Accessing nonexistent attribute'
+        input: '⟦ ρ ↦ ⟦ ⟧ ⟧.x'
+        output: ['⊥']
+
+  - name: MISS
+    description: 'Invalid application (absent attribute)'
+    pattern: ⟦ !B1 ⟧(!τ ↦ !b, !B2)
+    result: ⊥
+    when:
+      - absent_attrs:
+          attrs: ['!τ', 'φ', 'λ']
+          bindings: ['!B1']
+    tests:
+      - name: ''
+        input: '⟦ t1 ↦ ⟦ a ↦ ∅ ⟧ ⟧(t ↦ ⟦ b ↦ ∅ ⟧)'
+        output: ['⊥']
+      - name: Should not match if attr is present
+        input: ⟦ t ↦ ⟦⟧ ⟧(t ↦ ⟦ a ↦ ∅ ⟧)
+        output: []
+      - name: Should not match if phi is present
+        input: ⟦ φ ↦ ⟦⟧, a ↦ ⟦⟧ ⟧(t ↦ ⟦ a ↦ ∅ ⟧)
+        output: []
+      - name: Should apply in subformations
+        input: ⟦ a ↦ ⟦ b ↦ ⟦⟧(t ↦ ⟦⟧) ⟧ ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']
+
+  - name: DD
+    description: 'Accessing an attribute on bottom'
+    pattern: |
+      ⊥.!τ
+    result: |
+      ⊥
+    when: []
+    tests:
+      - name: 'Dispatch on bottom is bottom'
+        input: '⊥.a'
+        output: ['⊥']
+      - name: 'Dispatch on anything else is not touched'
+        input: '⟦ ⟧.a'
+        output: []
+
+  - name: DC
+    description: 'Application on bottom is bottom'
+    pattern: |
+      ⊥(!B)
+    result: |
+      ⊥
+    when: []
+    tests:
+      - name: Should apply in subformations
+        input: ⟦ a ↦ ⟦ b ↦ ⊥(t ↦ ⟦⟧, u ↦ ⟦⟧) ⟧ ⟧
+        output: ['⟦ a ↦ ⟦ b ↦ ⊥ ⟧ ⟧']