phino-0.0.156: test-resources/evaluate-packs/remints-a-call-as-the-symbol-its-firing-answers.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# Morphing is lazy, so the tail of the pair below is still the call of 'L_inc'
# as the code spells it. A 'remint' step works such a term out the way an
# argument of a deferred copy is worked out since #1916: it morphs the term,
# fires what it comes to and writes every step, and the answer of 'L_inc' is
# a copy of 'Φ.num' whose φ is the fresh symbol '𝜎2', so the tail is '𝜎2'
# (#1923).
symbolic: |
  - λ: L_shrink
    morph:
      𝑛1: $.x
    rewrite:
      𝑛2:
        of: 𝑛1
        rules:
          - name: small-pair
            pattern: ⟦ !B1, head ↦ 𝑒1, tail ↦ 𝑒2, !B2 ⟧
            result: ⟦ !B1, head ↦ 𝑒3, tail ↦ 𝑒4, !B2 ⟧
            where:
              - meta: 𝑒3
                function: remint
                args: [𝑒1]
              - meta: 𝑒4
                function: remint
                args: [𝑒2]
    𝑛: 𝑛2
  - λ: L_inc
    dataize:
      𝛿1: $.x
    𝑛: Φ.num( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
location: 'Q.y'
input: '⟦ num(φ) ↦ ⟦⟧, inc(x) ↦ ⟦ λ ⤍ L_inc ⟧, y ↦ ⟦ x ↦ ⟦ head ↦ ⟦ λ ⤍ 𝜎1 ⟧, tail ↦ Φ.inc( ⟦ Δ ⤍ 2A- ⟧ ) ⟧, λ ⤍ L_shrink ⟧.tail ⟧'
result: '𝜎2:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_shrink):
      𝑛1·1 := ⟦ head ↦ 𝜎1:λ, tail ↦ Φ.inc( 2A-:Δ ) ⟧  # 𝕄(ξ.x)
      𝕄(Φ.inc( 2A-:Δ )):
        𝑛·1·1 := Φ.inc( x ↦ 2A-:Δ )
      𝔼(L_inc):  # 𝔼(Φ.inc( 2A-:Δ ))
        𝔻(Φ.a🌵1):
          𝛿·2·1 := 2A-
        𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.x)
        𝑛·2·1 := Φ.num( φ ↦ 𝜎2:λ )  # 𝑛
        𝕄(𝑛·2·1):
          𝑛·2·2 := Φ.num( φ ↦ 𝜎2:λ )
        𝑛·2·3 := 𝑛·2·2  # 𝕄(𝑛·2·1)
      𝑛2·1 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝑛1
      𝑛·1·2 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝑛
      𝑛·1·3 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝕄(𝑛·1·2)