fires-a-stalled-formation-again-once-something-was-answered.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps a stall only while nothing new was
# answered. The firing of 'f' under 'x' brings 'big' down inside the box of
# 's', and 's' is within 'big', so the mode cuts the operand and the firing
# gets stuck. Then 'g' answers, and 'f' is fired again at its own site, where
# nothing cuts it. Before #1495 that firing took the stall the first one met
# and reduced nothing; now it brings 'big' down and answers.
symbolic: |
  - λ: L_f
    dataize:
      𝛿1: $.arg
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
  - λ: L_g
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
deep: true
partial: true
acyclic: plausible
steps: 32
input: >
  ⟦ x ↦ ⟦ λ ⤍ L_f, arg ↦ Φ.s ⟧,
    g ↦ ⟦ λ ⤍ L_g ⟧,
    f ↦ ⟦ λ ⤍ L_f, arg ↦ Φ.big ⟧,
    s ↦ ⟦ φ ↦ Φ.f ⟧,
    big ↦ ⟦ φ ↦ Φ.k( x ↦ Φ.f ) ⟧,
    k ↦ ⟦ x ↦ ∅, φ ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧
protocol: |
  𝕄(Φ):
    𝕄(Φ.x):
      𝔼(L_f):
        𝔻(Φ.a🌵0):
          𝔼(L_f):
            𝔻(Φ.a🌵1):
              looped(Φ.f:φ)  # plausible
            stuck(L_f)
        stuck(L_f)
    𝕄(Φ.g):
      𝔼(L_g):
        𝑛·3·1 := 𝜎1:λ  # 𝑛
        𝑛·3·2 := 𝜎1:λ  # 𝕄(𝑛·3·1)
    𝕄(Φ.f):
      𝔼(L_f):
        𝔻(Φ.a🌵2):
          𝕄(Φ.a🌵2):
            𝑛·4·1 := Φ.k( x ↦ Φ.f )
          𝛿·4·1 := 01-
        𝛿1·4 := 𝛿·4·1  # 𝔻(ξ.arg)
        𝑛·4·2 := 𝜎2:λ  # 𝑛
        𝑛·4·3 := 𝜎2:λ  # 𝕄(𝑛·4·2)
    𝕄(Φ.big):
      𝕄(Φ.big.φ):
        𝑛·0·1 := Φ.k( x ↦ Φ.f )