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
# cut answers the whole dispatch of 'φ' with a fresh symbol, named after the
# call the facts trace with 'φ' on top (#2307). 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: '𝜎3:λ'
protocol: |
  𝕄(Φ.y):
    remembered 𝑛·0·1 ≡ Φ.down  # ⟦ x ↦ ∅, λ ⤍ L_down ⟧
    𝑛·0·2 := Φ.down( x ↦ 𝜎1:λ )
    𝑛·0·3 := ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧
    remembered 𝑛·0·3 ≡ 𝑛·0·1( 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:λ )
        𝑛·1·3 := ⟦ x ↦ 𝜎2:λ, λ ⤍ L_down ⟧
        remembered 𝑛·1·3 ≡ 𝑛·0·1( x ↦ 𝜎2:λ )
        morphed 𝑛·1·4 := 𝑛·1·3
      𝑛·1·5 := 𝑛·1·3  # 𝕄(𝑛·1·1)
      remembered 𝑛·1·3 ≡ 𝑛·0·3
    recalled 𝑛·1·3 ⇒ 𝑛·0·3
    recalled 𝑛·0·3 ⇒ 𝑛·0·1( x ↦ 𝜎1:λ )
    recalled 𝑛·0·1 ⇒ Φ.down
    looped 𝜎3 := 𝑛·0·2.φ  # proven, repeats 𝑛·0·3
    morphed 𝑛·0·4 := 𝜎3:λ