answers-the-same-dataization-loop-under-partial.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# The program of 'answers-an-operand-that-dataizes-in-circles-with-a-symbol',
# run with '--partial' as well. The box step of 𝔻 answers the copy it would
# enter again with a fresh symbol (#2226), so nothing is left to park and the
# answer is the same, which is what "--acyclic needs no --partial" means for a
# loop 𝔻 catches (#1290).
symbolic: |
  - λ: L_outer
    dataize:
      𝛿1: ξ.arg
    𝑛: ⟦ bar ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.x'
acyclic: proven
partial: true
steps: 250
input: >
  ⟦ cyc ↦ ⟦ x ↦ ∅, φ ↦ Φ.cyc( ξ.x ) ⟧,
    x ↦ ⟦ arg ↦ Φ.cyc( ⟦⟧ ), λ ⤍ L_outer ⟧.bar ⟧
result: '𝜎2:λ'
protocol: |
  𝕄(Φ.x):
    𝔼(L_outer):
      𝔻(ξ.arg):
        𝕄(ξ.arg):
          𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )
          𝑛·1·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧
          morphed 𝑛·1·3 := 𝑛·1·2
        boxed 𝑛·1·4 := 𝑛·1·3.φ
        𝕄(𝑛·1·4):
          𝑛·1·5 := Φ.cyc( x ↦ ⟦⟧ )
          𝑛·1·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧
          morphed 𝑛·1·7 := 𝑛·1·6
        𝕄(𝑛·1·7.x):
          morphed 𝑛·1·8 := ⟦⟧
        looped 𝜎1 := Φ.cyc( x ↦ 𝑛·1·8 )  # 𝔻(𝑛·1·4), proven, repeats 𝑛·1·7
        𝛿·1·1 := 𝔻(𝜎1:λ)
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.arg)
      𝑛·1·9 := 𝜎2:λ:bar  # 𝑛
      𝕄(𝑛·1·9):
        morphed 𝑛·1·10 := 𝜎2:λ:bar
      𝑛·1·11 := 𝑛·1·10  # 𝕄(𝑛·1·9)
    morphed 𝑛·0·1 := 𝜎2:λ