cuts-a-loop-over-unknown-data-on-its-second-round.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A loop walking an index from zero up to a size that is a symbol, under
# '--acyclic=plausible'. The first round holds the number '0', the second holds
# the symbol 'plus' answered in its place, and a symbol stands for a term that
# holds no symbol of its own, so the fork of the second round is cut against
# the fork of the first one rather than a round later (#1491). The cut fork is
# the φ of a copy of 'rec', so the cut answers that copy with a fresh symbol,
# which the 'join' of the first fork pairs with the other branch (#1735).
symbolic: |
  - λ: L_id
    morph:
      𝑛1: $.x.φ
    𝑛: 𝑛1
  - λ: L_plus
    dataize:
      𝛿1: $.ρ
      𝛿2: $.b
    𝑛: Φ.num( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )
  - λ: L_eq
    dataize:
      𝛿1: $.ρ
      𝛿2: $.b
    𝑛: ⟦ φ ↦ Φ.bool( if ↦ ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧ ) ⟧
  - λ: L_fork
    dataize:
      𝛿1: $.φ
    morph:
      𝑛1: $.left
      𝑛2: $.right
    symbolize:
      𝑛3: 𝑛1
      𝑛4: 𝑛2
    join:
      𝑛5: [𝑛3, 𝑛4]
    𝑛: 𝑛5
location: 'Q.a'
deep: true
acyclic: plausible
partial: true
steps: 32
input: >
  ⟦ num ↦ ⟦ φ ↦ ∅, plus ↦ ⟦ ρ ↦ ∅, b ↦ ∅, λ ⤍ L_plus ⟧, eq ↦ ⟦ ρ ↦ ∅, b ↦ ∅, λ ⤍ L_eq ⟧ ⟧,
    bool ↦ ⟦ φ ↦ ∅, if ↦ ∅ ⟧,
    count ↦ ⟦ size ↦ ∅, φ ↦ ξ.rec( index ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 00- ⟧ ), accum ↦ Φ.num( φ ↦ ⟦ Δ ⤍ 00- ⟧ ) ), rec ↦ ⟦ ρ ↦ ∅, index ↦ ∅, accum ↦ ∅, φ ↦ ξ.index.eq( ξ.ρ.size ).if( ξ.accum, ξ.ρ.rec( index ↦ ξ.index.plus( Φ.num( φ ↦ ⟦ Δ ⤍ 01- ⟧ ) ), accum ↦ ξ.accum.plus( Φ.num( φ ↦ ⟦ Δ ⤍ 01- ⟧ ) ) ) ) ⟧ ⟧,
    a ↦ ⟦ λ ⤍ L_id, x ↦ Φ.count( size ↦ Φ.num( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ) ⟧ ⟧
protocol: |
  𝕄(Φ.a):
    𝕄(Φ.a.x):
      𝑛·0·1 := Φ.num( φ ↦ 𝜎1:λ )
      𝑛·0·2 := Φ.count( size ↦ 𝑛·0·1 )
    𝔼(L_id):
      𝕄(Φ.a🌵0):
        𝑛·1·1 := Φ.count( size ↦ 𝑛·0·1 )
        𝑛·1·2 := ⟦ index ↦ ∅, accum ↦ ∅, φ ↦ index.eq( ρ.size ).if( accum, ρ.rec( index ↦ index.plus( Φ.num( φ ↦ 01-:Δ ) ), accum ↦ accum.plus( Φ.num( φ ↦ 01-:Δ ) ) ) ) ⟧( index ↦ Φ.num( φ ↦ 00-:Δ ) )
        𝑛·1·3 := 𝑛·1·2( accum ↦ Φ.num( φ ↦ 00-:Δ ) )
        𝕄(Φ.a🌵0.index):
          𝑛·1·4 := Φ.num( φ ↦ 00-:Δ )
        𝕄(Φ.a🌵0.accum):
          𝑛·1·5 := Φ.num( φ ↦ 00-:Δ )
        𝕄(Φ.a🌵0.φ):
          𝑛·1·6 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·7 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·8 := Φ.num( φ ↦ 𝜎1:λ )
          𝑛·1·9 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·10 := 𝑛·1·9.eq( b ↦ 𝑛·1·8 )
          𝔼(L_eq):
            𝔻(Φ.a🌵1):
              𝕄(Φ.a🌵1):
                𝑛·2·1 := Φ.num( φ ↦ 00-:Δ )
              𝛿·2·1 := 00-
            𝛿1·2 := 𝛿·2·1  # 𝔻(ξ.ρ)
            𝔻(Φ.a🌵2):
              𝕄(Φ.a🌵2):
                𝑛·2·2 := Φ.num( φ ↦ 𝜎1:λ )
            𝛿2·2 := 𝔻(𝜎1:λ)  # 𝔻(ξ.b)
            𝑛·2·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ ):φ  # 𝑛
            𝑛·2·4 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ ):φ  # 𝕄(𝑛·2·3)
          𝑛·1·11 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ )
          𝑛·1·12 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·13 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ )
          𝑛·1·14 := ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝜎2:λ ⟧( left ↦ 𝑛·1·12 )
          𝑛·1·15 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·16 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·17 := Φ.num( φ ↦ 01-:Δ )
          𝑛·1·18 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·19 := 𝑛·1·18.plus( b ↦ 𝑛·1·17 )
          𝔼(L_plus):
            𝔻(Φ.a🌵3):
              𝕄(Φ.a🌵3):
                𝑛·3·1 := Φ.num( φ ↦ 00-:Δ )
              𝛿·3·1 := 00-
            𝛿1·3 := 𝛿·3·1  # 𝔻(ξ.ρ)
            𝔻(Φ.a🌵4):
              𝕄(Φ.a🌵4):
                𝑛·3·2 := Φ.num( φ ↦ 01-:Δ )
              𝛿·3·2 := 01-
            𝛿2·3 := 𝛿·3·2  # 𝔻(ξ.b)
            𝑛·3·3 := Φ.num( φ ↦ 𝜎3:λ )  # 𝑛
            𝕄(𝑛·3·3):
              𝑛·3·4 := Φ.num( φ ↦ 𝜎3:λ )
            𝑛·3·5 := 𝑛·3·4  # 𝕄(𝑛·3·3)
          𝑛·1·20 := ⟦ index ↦ ∅, accum ↦ ∅, φ ↦ index.eq( ρ.size ).if( accum, ρ.rec( index ↦ index.plus( 𝑛·3·2 ), accum ↦ accum.plus( 𝑛·3·2 ) ) ) ⟧( index ↦ 𝑛·3·4 )
          𝑛·1·21 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·22 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·23 := Φ.num( φ ↦ 01-:Δ )
          𝑛·1·24 := Φ.num( φ ↦ 00-:Δ )
          𝑛·1·25 := 𝑛·1·24.plus( b ↦ 𝑛·1·23 )
          𝔼(L_plus):
            𝑛·4·1 := 𝑛·3·4  # 𝑛
            𝑛·4·2 := 𝑛·3·5  # 𝕄(𝑛·4·1)
          𝑛·1·26 := ⟦ index ↦ ∅, accum ↦ ∅, φ ↦ index.eq( ρ.size ).if( accum, ρ.rec( index ↦ index.plus( 𝑛·1·23 ), accum ↦ accum.plus( 𝑛·1·23 ) ) ) ⟧( index ↦ 𝑛·3·4 )
          𝑛·1·27 := 𝑛·1·26( accum ↦ 𝑛·3·4 )
          𝑛·1·28 := ⟦ index ↦ ∅, accum ↦ ∅, φ ↦ index.eq( ρ.size ).if( accum, ρ.rec( index ↦ index.plus( 𝑛·1·23 ), accum ↦ accum.plus( 𝑛·1·23 ) ) ) ⟧( index ↦ 𝑛·3·4 )
          𝑛·1·29 := 𝑛·1·28( accum ↦ 𝑛·3·4 )
          𝑛·1·30 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ )
          𝑛·1·31 := ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝜎2:λ ⟧( left ↦ 𝑛·1·24 )
          𝑛·1·32 := 𝑛·1·31( right ↦ 𝑛·1·29 )
          𝔼(L_fork):
            𝛿1·5 := 𝔻(𝜎2:λ)  # 𝔻(ξ.φ)
            𝕄(Φ.a🌵6):
              𝑛·5·1 := Φ.num( φ ↦ 00-:Δ )
            𝑛1·5 := 𝑛·5·1  # 𝕄(ξ.left)
            𝕄(Φ.a🌵7):
              𝕄(Φ.a🌵7.φ):
                𝑛·5·2 := Φ.num( φ ↦ 𝜎1:λ )
                𝑛·5·3 := 𝑛·3·4.eq( b ↦ 𝑛·5·2 )
                𝔼(L_eq):
                  𝔻(Φ.a🌵8):
                    𝕄(Φ.a🌵8):
                      𝑛·6·1 := Φ.num( φ ↦ 𝜎3:λ )
                  𝛿1·6 := 𝔻(𝜎3:λ)  # 𝔻(ξ.ρ)
                  𝔻(Φ.a🌵9):
                    𝕄(Φ.a🌵9):
                      𝑛·6·2 := Φ.num( φ ↦ 𝜎1:λ )
                  𝛿2·6 := 𝔻(𝜎1:λ)  # 𝔻(ξ.b)
                  𝑛·6·3 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎4:λ ⟧ ):φ  # 𝑛
                  𝑛·6·4 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎4:λ ⟧ ):φ  # 𝕄(𝑛·6·3)
                𝑛·5·4 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎4:λ ⟧ )
                𝑛·5·5 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎4:λ ⟧ )
                𝑛·5·6 := ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝜎4:λ ⟧( left ↦ 𝑛·6·1 )
                𝑛·5·7 := Φ.num( φ ↦ 01-:Δ )
                𝑛·5·8 := 𝑛·6·1.plus( b ↦ 𝑛·5·7 )
                𝔼(L_plus):
                  𝔻(Φ.a🌵10):
                    𝕄(Φ.a🌵10):
                      𝑛·7·1 := Φ.num( φ ↦ 𝜎3:λ )
                  𝛿1·7 := 𝔻(𝜎3:λ)  # 𝔻(ξ.ρ)
                  𝔻(Φ.a🌵11):
                    𝕄(Φ.a🌵11):
                      𝑛·7·2 := Φ.num( φ ↦ 01-:Δ )
                    𝛿·7·1 := 01-
                  𝛿2·7 := 𝛿·7·1  # 𝔻(ξ.b)
                  𝑛·7·3 := Φ.num( φ ↦ 𝜎5:λ )  # 𝑛
                  𝕄(𝑛·7·3):
                    𝑛·7·4 := Φ.num( φ ↦ 𝜎5:λ )
                  𝑛·7·5 := 𝑛·7·4  # 𝕄(𝑛·7·3)
                𝑛·5·9 := ⟦ index ↦ ∅, accum ↦ ∅, φ ↦ index.eq( ρ.size ).if( accum, ρ.rec( index ↦ index.plus( 𝑛·7·2 ), accum ↦ accum.plus( 𝑛·7·2 ) ) ) ⟧( index ↦ 𝑛·7·4 )
                𝑛·5·10 := Φ.num( φ ↦ 01-:Δ )
                𝑛·5·11 := 𝑛·7·1.plus( b ↦ 𝑛·5·10 )
                𝔼(L_plus):
                  𝑛·8·1 := 𝑛·7·4  # 𝑛
                  𝑛·8·2 := 𝑛·7·5  # 𝕄(𝑛·8·1)
                𝑛·5·12 := ⟦ index ↦ ∅, accum ↦ ∅, φ ↦ index.eq( ρ.size ).if( accum, ρ.rec( index ↦ index.plus( 𝑛·5·10 ), accum ↦ accum.plus( 𝑛·5·10 ) ) ) ⟧( index ↦ 𝑛·7·4 )
                𝑛·5·13 := 𝑛·5·12( accum ↦ 𝑛·7·4 )
                𝑛·5·14 := ⟦ index ↦ ∅, accum ↦ ∅, φ ↦ index.eq( ρ.size ).if( accum, ρ.rec( index ↦ index.plus( 𝑛·5·10 ), accum ↦ accum.plus( 𝑛·5·10 ) ) ) ⟧( index ↦ 𝑛·7·4 )
                𝑛·5·15 := 𝑛·5·14( accum ↦ 𝑛·7·4 )
                𝑛·5·16 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎4:λ ⟧ )
                𝑛·5·17 := ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, φ ↦ 𝜎4:λ ⟧( left ↦ 𝑛·7·1 )
                𝑛·5·18 := 𝑛·5·17( right ↦ 𝑛·5·15 )
                looped(𝑛·1·32) := 𝜎6  # plausible
            𝑛2·5 := 𝜎6:λ  # 𝕄(ξ.right)
            𝔻(𝜎7:λ) == 00-
            𝑛3·5 := ⟦ φ ↦ 𝜎7:λ, plus(b) ↦ L_plus:λ, eq(b) ↦ L_eq:λ ⟧  # 𝑛1
            𝑛4·5 := 𝑛2·5  # 𝑛2
            𝔻(𝜎8:λ) ∈ { 𝔻(𝜎7:λ), 𝔻(𝜎6:λ) }
            𝑛5·5 := 𝜎8:λ  # [𝑛3, 𝑛4]
            𝑛·5·19 := 𝑛5·5  # 𝑛
            𝑛·5·20 := 𝑛5·5  # 𝕄(𝑛·5·19)
      𝑛1·1 := 𝑛·1·3  # 𝕄(ξ.x.φ)
      𝑛·1·33 := 𝑛1·1  # 𝑛
      𝑛·1·34 := 𝑛1·1  # 𝕄(𝑛·1·33)