fires-a-stalled-formation-again-after-what-its-own-firing-answered.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' stamps a stall with the count of answers
# the memo held when the firing began, not when it failed. 'L_pair' reduces
# 'x' and then 'y', and both spell the very same formation of 'L_outer'. The
# firing under 'x' brings 'first' down through 'L_inner', which answers, and
# then gets stuck on 'L_none'. Before #1507 the stall was stamped after that
# answer, so the firing under 'y' was told the stall bare, as if nothing was
# answered since. Now the answer made inside the first firing counts as one
# made after it began, so the firing under 'y' reduces its operands again.
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.first
      𝛿2: ξ.second
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_inner
    𝑛: ⟦ Δ ⤍ 01- ⟧
  - λ: L_pair
    morph:
      𝑛1: $.x
      𝑛2: $.y
    𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.p'
partial: true
acyclic: plausible
input: >
  ⟦ p ↦ ⟦
      x ↦ ⟦ first ↦ Φ.s, second ↦ ⟦ λ ⤍ L_none ⟧, λ ⤍ L_outer ⟧.φ,
      y ↦ ⟦ first ↦ Φ.s, second ↦ ⟦ λ ⤍ L_none ⟧, λ ⤍ L_outer ⟧.φ,
      λ ⤍ L_pair ⟧.φ,
    s ↦ ⟦ φ ↦ Φ.g ⟧,
    g ↦ ⟦ λ ⤍ L_inner ⟧ ⟧
protocol: |
  𝕄(Φ.p):
    𝔼(L_pair):
      𝕄(Φ.a🌵0):
        𝔼(L_outer):
          𝔻(Φ.a🌵1):
            𝔼(L_inner):
              𝑛·3·1 := 01-:Δ  # 𝑛
              𝑛·3·2 := 01-:Δ  # 𝕄(𝑛·3·1)
            𝛿·2·1 := 01-
          𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.first)
          𝔻(Φ.a🌵2):
            unanswered(L_none)  # 𝔻(L_none:λ)
          stuck(L_none)
      𝑛1·1 := ⟦ first ↦ Φ.s, second ↦ L_none:λ, λ ⤍ L_outer ⟧.φ  # 𝕄(ξ.x)
      𝕄(Φ.a🌵3):
        𝔼(L_outer):
          𝔻(Φ.a🌵4):
            𝔼(L_inner):
              𝑛·5·1 := 01-:Δ  # 𝑛
              𝑛·5·2 := 01-:Δ  # 𝕄(𝑛·5·1)
            𝛿·4·1 := 01-
          𝛿1·4 := 𝛿·4·1  # 𝔻(ξ.first)
          𝔻(Φ.a🌵5):
            unanswered(L_none)  # 𝔻(L_none:λ)
          stuck(L_none)
      𝑛2·1 := ⟦ first ↦ Φ.s, second ↦ L_none:λ, λ ⤍ L_outer ⟧.φ  # 𝕄(ξ.y)
      𝑛·1·1 := 𝜎1:λ:φ  # 𝑛
      𝑛·1·2 := 𝜎1:λ:φ  # 𝕄(𝑛·1·1)