cuts-an-entry-that-answers-with-a-firing-of-itself.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# The same entry answering with a firing of itself, under '_acyclic': morphing
# comes back to the very dispatch it is already reducing, so it stops there
# instead of going round until the budget is gone, and answers the dispatch
# with a fresh symbol (#2307). The budget is generous here, so what ends the
# run is the cut and not the limit.
symbolic: |
  - λ: L_loop
    𝑛: ⟦ λ ⤍ L_loop ⟧
location: 'Q.x'
acyclic: proven
steps: 250
input: '⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo ⟧'
result: '𝜎1:λ'
protocol: |
  𝕄(Φ.x):
    𝔼(L_loop):
      𝑛·1·1 := L_loop:λ  # 𝑛
      𝕄(𝑛·1·1):
        morphed 𝑛·1·2 := L_loop:λ
      𝑛·1·3 := L_loop:λ  # 𝕄(𝑛·1·1)
    looped 𝜎1  # proven, repeats L_loop:λ
    morphed 𝑛·0·1 := 𝜎1:λ