guards-a-side-holding-no-symbol-against-a-bottom.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The right side is ⊥ and the left side is a formation holding no symbol, so
# nothing could stand for ⊥ in a 'joined' line. A fork one branch of which
# raises is the other branch under the condition, so the join answers the left
# side as it is and writes a 'guarded' line saying the right side is ⊥ (#2370).
symbolic: |
  - λ: L_fork
    dataize:
      𝛿1: $.on🌵
    morph:
      𝑛1: $.left🌵
      𝑛2: $.right🌵
    join:
      on: 𝛿1
      left: 𝑛1
      right: 𝑛2
      otherwise: L_fork
location: 'Q.e1'
input: '⟦ k ↦ ⟦ q ↦ ⟦⟧ ⟧, e1 ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ Δ ⤍ 00- ⟧, left🌵 ↦ ⟦ φ ↦ Φ.k ⟧, right🌵 ↦ ⊥ ⟧.φ ⟧'
result: '⟦ q ↦ ⟦⟧ ⟧'
protocol: |
  𝕄(Φ.e1):
    𝔼(L_fork):
      𝔻(ξ.on🌵):
        𝛿·1·1 := 00-
      𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.on🌵)
      𝕄(ξ.left🌵):
        morphed 𝑛·1·1 := Φ.k:φ
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.left🌵)
      𝕄(ξ.right🌵):
        morphed 𝑛·1·2 := ⊥
      𝑛2·1 := ⊥  # 𝕄(ξ.right🌵)
      guarded 𝛿1·1 ? 𝑛1·1 : 𝑛2·1  # where 𝑛2·1 is ⊥
      𝑛·1·3 := 𝑛·1·1
    normalized 𝑛·0·1 := Φ.k  # 𝑛·1·3.φ
    normalized 𝑛·0·2 := ⟦⟧:q  # Φ.k
    morphed 𝑛·0·3 := 𝑛·0·2