parks-a-firing-whose-operand-has-a-void-phi.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# The 'dataize' operand of 'L_pair' is a formation whose φ is a void nothing
# filled, so the 'box' rule takes that φ and reaches the terminator ⊥ (#2168).
# Under '_partial' that parks the firing, and the protocol writes the box step
# and then the dead end as 'unanswered(⊥)' (#1401).
symbolic: |
  - λ: L_pair
    dataize:
      𝛿1: $.x
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
location: 'Q.y'
partial: true
input: '⟦ y ↦ ⟦ x ↦ ⟦ φ ↦ ∅ ⟧, λ ⤍ L_pair ⟧.z ⟧'
result: '⟦ x(φ) ↦ ⟦⟧, λ ⤍ L_pair ⟧.z'
protocol: |
  𝕄(Φ.y):
    𝔼(L_pair):
      𝔻(ξ.x):
        boxed 𝑛·1·1 := ∅:φ.φ
      unanswered ⊥  # 𝔻(⊥)
      stuck ⊥