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.
# The firing under 'x' brings its operand down through 𝔻, which goes round
# 'cyc' until the mode cuts it, so the firing never answers; 'y' spells the
# very same formation, and before #1480 its firing walked 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
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
deep: true
acyclic: plausible
steps: 64
input: >
  ⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧,
    x ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧,
    y ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧ ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.x):
      𝕄(Φ.x.arg):
        𝑛·0·1 := Φ.cyc( x ↦ ⟦⟧ )
      𝔼(L_outer):
        𝔻(Φ.a🌵0):
          𝕄(Φ.a🌵0):
            𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )
            𝑛·1·2 := Φ.cyc( x ↦ ⟦⟧ )
          looped(𝑛·1·2)  # plausible
    𝕄(Φ.y):
      𝔼(L_outer):
        looped(𝑛·1·2)  # 𝕄(Φ.y), plausible