keeps-a-cut-met-inside-a-firing-for-the-next-firing.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps a cut the way it keeps an answer.
# 'L_pair' reduces 'x' and then 'y', and both spell the very same formation
# of 'L_outer'. The firing under 'x' brings its operand down through 𝔻,
# which goes round 'cyc' until the mode cuts it, so the firing never
# answers. Before #1480 the firing under 'y' went all the way down to the
# same cut again, since only an answer was kept. Now the second firing takes
# the cut the first one met: it is written at its own site with the
# formation the cut carried, and nothing under it is reduced.
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_pair
    morph:
      𝑛1: $.x
      𝑛2: $.y
    𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.p'
acyclic: plausible
input: >
  ⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧,
    p ↦ ⟦
      x ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.φ,
      y ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.φ,
      λ ⤍ L_pair ⟧.φ ⟧
protocol: |
  𝕄(Φ.p):
    𝔼(L_pair):
      𝕄(Φ.a🌵0):
        𝔼(L_outer):
          𝔻(Φ.a🌵1):
            𝕄(Φ.a🌵1):
              𝑛·2·1 := Φ.cyc( x ↦ ⟦⟧ )
              𝑛·2·2 := Φ.cyc( x ↦ ⟦⟧ )
            looped(𝑛·2·2)  # plausible
      𝑛1·1 := ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.φ  # 𝕄(ξ.x)
      𝕄(Φ.a🌵2):
        𝔼(L_outer):
          looped(𝑛·2·2)  # 𝕄(Φ.a🌵2), plausible
      𝑛2·1 := ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.φ  # 𝕄(ξ.y)
      𝑛·1·1 := 𝜎1:λ:φ  # 𝑛
      𝑛·1·2 := 𝜎1:λ:φ  # 𝕄(𝑛·1·1)