cuts-a-recursion-that-differs-by-symbols-only.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A recursion over a symbolic argument, under '--acyclic=proven'. 'L_down'
# answers a call of 'down' over a fresh symbol, and 'ml' dispatches 'φ' off
# that answer, which fires 'down' again: the first round fires it with x ↦ 𝜎1,
# the second with x ↦ 𝜎2, and no two rounds are ever the same term. They are
# the same formation up to a renaming of symbols, which is what the guard
# compares by (#1420), and 'ml' enters the formation it fires, so the second
# firing is cut before it opens and writes a 'looped' line where its block
# would have stood, carrying the term of the round that was kept (#1434). The
# budget is generous here, so what ends the run is the cut and not the limit.
symbolic: |
  - λ: L_down
    dataize:
      𝛿1: $.x
    𝑛: Φ.down( x ↦ ⟦ λ ⤍ 𝜎 ⟧ )
location: 'Q.y'
acyclic: proven
steps: 250
input: '⟦ down ↦ ⟦ x ↦ ∅, λ ⤍ L_down ⟧, y ↦ Φ.down( x ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).φ ⟧'
result: '⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧.φ'
protocol: |
  𝕄(Φ.y):
    𝑛·0·1 := Φ.down( x ↦ 𝜎1:λ )
    𝔼(L_down):
      𝔻(ξ.x):
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.x)
      𝑛·1·1 := Φ.down( x ↦ 𝜎2:λ )  # 𝑛
      𝕄(𝑛·1·1):
        𝑛·1·2 := Φ.down( x ↦ 𝜎2:λ )
        morphed 𝑛·1·3 := 𝑛·1·2
      𝑛·1·4 := 𝑛·1·2  # 𝕄(𝑛·1·1)
    looped 𝑛·0·1  # proven