leaves-an-abstract-formation-unwalked.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A method nobody applied is an abstract formation, one holding a void of its
# own: 'at' of the copy of 'text' the entry of 'L_entry' morphs waits for 'i'.
# The deep walk hands it back as it was written instead of entering it, since
# its body is parametric: the entry of 'L_dataized' inside it would dataize
# 'ξ.i', which stands for nothing, and the ⊥ it reaches would end the whole run
# even under '--partial' (#1393).
symbolic: |
  - λ: L_number_gt
    dataize:
      𝛿1: $.ρ
      𝛿2: $.b
    𝑛: Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧ )
  - λ: L_dataized
    dataize:
      𝛿1: $.target
    𝑛: Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
  - λ: L_entry
    dataize:
      𝛿1: $.n
    morph:
      𝑛1: $.v.φ
    𝑛: Φ.l🌵.root( 𝑛1 )
  - λ: L_root
    dataize:
      𝛿1: $.v
    𝑛: ⟦ ⟧
location: 'Q.l🌵'
deep: true
partial: true
acyclic: proven
steps: 32
input: |
  ⟦
    number ↦ ⟦ φ ↦ ∅, gt ↦ ⟦ ρ ↦ ∅, b ↦ ∅, λ ⤍ L_number_gt ⟧ ⟧,
    bytes ↦ ⟦ φ ↦ ∅ ⟧,
    bool ↦ ⟦ if ↦ ∅ ⟧,
    dataized ↦ ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧,
    text ↦ ⟦
      φ ↦ ∅,
      at ↦ ⟦
        i ↦ ∅,
        φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 00-00-00-00-00-00-00-00 ⟧ ) ).gt( b ↦ Φ.dataized( target ↦ ξ.i ) )
      ⟧
    ⟧,
    holder ↦ ⟦ buf ↦ ∅, φ ↦ ξ.buf ⟧,
    l🌵 ↦ ⟦
      mark ↦ ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧,
      root ↦ ⟦ v ↦ ∅, λ ⤍ L_root ⟧,
      e1 ↦ Φ.l🌵.mark(
        n ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 3F-F0-00-00-00-00-00-00 ⟧ ) )
      )( v ↦ Φ.holder( buf ↦ Φ.text( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ) ) )
    ⟧
  ⟧
protocol: |
  𝕄(Φ.l🌵):
    𝕄(Φ.l🌵.e1):
      𝑛·0·1 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
      𝑛·0·2 := Φ.number( φ ↦ 𝑛·0·1 )
      𝑛·0·3 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧( n ↦ 𝑛·0·2 )
      𝑛·0·4 := Φ.bytes( φ ↦ 𝜎1:λ )
      𝑛·0·5 := Φ.text( φ ↦ 𝑛·0·4 )
      𝑛·0·6 := Φ.holder( buf ↦ 𝑛·0·5 )
      𝑛·0·7 := ⟦ n ↦ ∅, v ↦ ∅, λ ⤍ L_entry ⟧( n ↦ 𝑛·0·2 )
      𝑛·0·8 := 𝑛·0·7( v ↦ 𝑛·0·6 )
      𝔼(L_entry):
        𝔻(Φ.a🌵0):
          𝕄(Φ.a🌵0):
            𝑛·1·1 := Φ.number( φ ↦ 𝑛·0·1 )
            𝑛·1·2 := Φ.bytes( φ ↦ 3F-F0-00-00-00-00-00-00:Δ )
          𝛿·1·1 := 3F-F0-00-00-00-00-00-00  # 1.0
        𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.n)
        𝕄(Φ.a🌵1):
          𝑛·1·3 := Φ.holder( buf ↦ 𝑛·0·5 )
          𝑛·1·4 := Φ.text( φ ↦ 𝑛·0·4 )
          𝑛·1·5 := Φ.text( φ ↦ 𝑛·0·4 )
          𝕄(Φ.a🌵1.φ):
            𝑛·1·6 := Φ.bytes( φ ↦ 𝜎1:λ )
        𝑛1·1 := 𝑛·1·5  # 𝕄(ξ.v.φ)
        𝑛·1·7 := Φ.l🌵.root( 𝑛·1·5 )  # 𝑛
        𝕄(𝑛·1·7):
          𝑛·1·8 := ⟦ v ↦ ∅, λ ⤍ L_root ⟧( v ↦ 𝑛·1·5 )
        𝑛·1·9 := 𝑛·1·8  # 𝕄(𝑛·1·7)
      𝔼(L_root):
        𝔻(Φ.a🌵2):
          𝕄(Φ.a🌵2):
            𝑛·2·1 := Φ.bytes( φ ↦ 𝜎1:λ )
        𝛿1·2 := 𝔻(𝜎1:λ)  # 𝔻(ξ.v)
        𝑛·2·2 := ⟦⟧  # 𝑛
        𝑛·2·3 := ⟦⟧  # 𝕄(𝑛·2·2)