stands-the-data-of-a-term-into-unknowns.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# A 'symbolize' line reduces nothing: it stands the data of a term another line
# of the entry has already bound into unknowns, so a normal form reached from a
# literal is written the way one reached from an unknown is written and the two
# of them compare as expressions. Here 𝑛1 came from a literal and 𝑛2 from a
# value nobody worked out: after the stage both of them carry ⟦ λ ⤍ 𝜎 ⟧ where
# they differ. What is known about each fresh symbol stands on a line of its
# own, since a 𝜎 is the name of a λ function and nothing binds bytes to it, and
# a term that carried no datum at all passes through as it was. The comments of
# the two pairs of lines are what tells them apart: a 'morph' operand is
# commented with the judgment that reduced it and the term it was reduced from,
# '𝕄(ξ.a)', where a 'symbolize' line names the meta it was told to stand and no
# judgment at all, since none ran (#1306).
symbolic: |
  - λ: L_join
    morph:
      𝑛1: $.a
      𝑛2: $.b
    symbolize:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    𝑛: ⟦ l ↦ 𝑛3 ⟧
location: 'Q.y'
input: '⟦ y ↦ ⟦ a ↦ ⟦ Δ ⤍ 01- ⟧, b ↦ ⟦ λ ⤍ 𝜎7 ⟧, λ ⤍ L_join ⟧.l ⟧'
result: '𝜎8:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_join):
      𝑛1·1 := 01-:Δ  # 𝕄(ξ.a)
      𝑛2·1 := 𝜎7:λ  # 𝕄(ξ.b)
      𝔻(𝜎8:λ) == 01-
      𝑛3·1 := 𝜎8:λ  # 𝑛1
      𝑛4·1 := 𝑛2·1  # 𝑛2
      𝑛·1·1 := 𝜎8:λ:l  # 𝑛
      𝑛·1·2 := 𝜎8:λ:l  # 𝕄(𝑛·1·1)