phino-0.0.152: test-resources/evaluate-packs/tells-a-budget-stall-to-a-firing-no-shallower.yaml
# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# The memo of '--acyclic=plausible' keeps a stall the step budget made beside
# the steps its firing had spent, and tells it to a firing of the same
# formation that has spent at least as many. The operand of 'x.arg' runs out
# of steps two firings down, so the stall is kept. Before #1521 it was dropped,
# and 'x' walked the nest again inside its own firing, while 'y.arg' and 'y'
# fired it all over. Now the firing inside 'x' is told the stall, and so are
# 'y.arg' and 'y', which stand as deep as 'x.arg' and 'x' did.
symbolic: |
- λ: L_outer
dataize:
𝛿1: ξ.arg
𝑛: ⟦ λ ⤍ 𝜎 ⟧
deep: true
partial: true
acyclic: plausible
steps: 4
input: >
⟦ x ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_none ⟧ ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧,
y ↦ ⟦ λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ λ ⤍ L_none ⟧ ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧ ⟧
protocol: |
𝕄(Φ):
𝑛·0·1 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 )
𝑛·0·2 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 )
𝑛·0·3 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 )
𝑛·0·4 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 ) ⟧( v ↦ 1 ) ⟧( v ↦ 1 )
𝑛·0·5 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 ) ⟧( v ↦ 1 )
𝑛·0·6 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·7 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·2 ⟧( v ↦ 1 )
𝑛·0·8 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·3 ⟧( v ↦ 1 )
𝑛·0·9 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·4 ⟧( v ↦ 1 )
𝑛·0·10 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·5 ⟧( v ↦ 1 )
𝑛·0·11 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·6 ⟧( v ↦ 1 )
𝑛·0·12 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·13 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·9 ⟧( v ↦ 1 )
𝑛·0·14 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·10 ⟧( v ↦ 1 )
𝑛·0·15 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·11 ⟧( v ↦ 1 )
𝑛·0·16 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·12 ⟧( v ↦ 1 )
𝑛·0·17 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·18 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·14 ⟧( v ↦ 1 )
𝑛·0·19 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·15 ⟧( v ↦ 1 )
𝑛·0·20 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·16 ⟧( v ↦ 1 )
𝑛·0·21 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·17 ⟧( v ↦ 1 )
𝑛·0·22 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·23 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·20 ⟧( v ↦ 1 )
𝑛·0·24 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·21 ⟧( v ↦ 1 )
𝑛·0·25 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·22 ⟧( v ↦ 1 )
𝑛·0·26 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·27 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·24 ⟧( v ↦ 1 )
𝑛·0·28 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·25 ⟧( v ↦ 1 )
𝑛·0·29 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·26 ⟧( v ↦ 1 )
𝑛·0·30 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·31 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·29 ⟧( v ↦ 1 )
𝑛·0·32 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·30 ⟧( v ↦ 1 )
𝑛·0·33 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·34 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·32 ⟧( v ↦ 1 )
𝑛·0·35 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·33 ⟧( v ↦ 1 )
𝑛·0·36 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·37 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·36 ⟧( v ↦ 1 )
𝑛·0·38 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·39 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·38 ⟧( v ↦ 1 )
𝑛·0·40 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·41 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·42 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝕄(Φ.x):
𝕄(Φ.x.arg):
𝑛·0·43 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·27 ⟧( v ↦ 1 )
𝑛·0·44 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·34 ⟧( v ↦ 1 )
𝑛·0·45 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·39 ⟧( v ↦ 1 )
𝑛·0·46 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·42 ⟧( v ↦ 1 )
𝑛·0·47 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·48 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·45 ⟧( v ↦ 1 )
𝑛·0·49 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·46 ⟧( v ↦ 1 )
𝑛·0·50 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·47 ⟧( v ↦ 1 )
𝑛·0·51 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·52 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·50 ⟧( v ↦ 1 )
𝑛·0·53 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·51 ⟧( v ↦ 1 )
𝑛·0·54 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·55 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·54 ⟧( v ↦ 1 )
𝑛·0·56 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·57 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
starved(4)
starved(4)
starved(4)
starved(4)
𝑛·0·58 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·43 ⟧( v ↦ 1 )
𝑛·0·59 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·48 ⟧( v ↦ 1 )
𝑛·0·60 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·52 ⟧( v ↦ 1 )
𝑛·0·61 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·55 ⟧( v ↦ 1 )
𝑛·0·62 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·57 ⟧( v ↦ 1 )
𝑛·0·63 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·64 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·60 ⟧( v ↦ 1 )
𝑛·0·65 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·61 ⟧( v ↦ 1 )
𝑛·0·66 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·62 ⟧( v ↦ 1 )
𝑛·0·67 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·63 ⟧( v ↦ 1 )
𝑛·0·68 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·69 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·66 ⟧( v ↦ 1 )
𝑛·0·70 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·67 ⟧( v ↦ 1 )
𝑛·0·71 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·68 ⟧( v ↦ 1 )
𝑛·0·72 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·73 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·71 ⟧( v ↦ 1 )
𝑛·0·74 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·72 ⟧( v ↦ 1 )
𝑛·0·75 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·76 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·75 ⟧( v ↦ 1 )
𝑛·0·77 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·78 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝔼(L_outer):
𝔻(Φ.a🌵0):
𝔼(L_outer):
𝔻(Φ.a🌵1):
𝔼(L_outer):
starved(4) # 𝔻(Φ.a🌵2)
stuck(L_outer)
stuck(L_outer)
𝑛·0·79 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·64 ⟧( v ↦ 1 )
𝑛·0·80 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·69 ⟧( v ↦ 1 )
𝑛·0·81 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·73 ⟧( v ↦ 1 )
𝑛·0·82 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·76 ⟧( v ↦ 1 )
𝑛·0·83 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·78 ⟧( v ↦ 1 )
𝑛·0·84 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·85 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·81 ⟧( v ↦ 1 )
𝑛·0·86 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·82 ⟧( v ↦ 1 )
𝑛·0·87 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·83 ⟧( v ↦ 1 )
𝑛·0·88 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·84 ⟧( v ↦ 1 )
𝑛·0·89 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·90 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·87 ⟧( v ↦ 1 )
𝑛·0·91 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·88 ⟧( v ↦ 1 )
𝑛·0·92 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·89 ⟧( v ↦ 1 )
𝑛·0·93 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·94 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·92 ⟧( v ↦ 1 )
𝑛·0·95 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·93 ⟧( v ↦ 1 )
𝑛·0·96 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·97 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·96 ⟧( v ↦ 1 )
𝑛·0·98 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·99 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝔼(L_outer):
𝔻(Φ.a🌵3):
𝔼(L_outer):
stall(L_outer)
stuck(L_outer)
𝕄(Φ.y):
𝕄(Φ.y.arg):
𝑛·0·100 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·90 ⟧( v ↦ 1 )
𝑛·0·101 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·94 ⟧( v ↦ 1 )
𝑛·0·102 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·97 ⟧( v ↦ 1 )
𝑛·0·103 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·99 ⟧( v ↦ 1 )
𝑛·0·104 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·105 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·102 ⟧( v ↦ 1 )
𝑛·0·106 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·103 ⟧( v ↦ 1 )
𝑛·0·107 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·104 ⟧( v ↦ 1 )
𝑛·0·108 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·109 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·107 ⟧( v ↦ 1 )
𝑛·0·110 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·108 ⟧( v ↦ 1 )
𝑛·0·111 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·112 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·111 ⟧( v ↦ 1 )
𝑛·0·113 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·114 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
starved(4)
starved(4)
starved(4)
starved(4)
𝑛·0·115 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·100 ⟧( v ↦ 1 )
𝑛·0·116 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·105 ⟧( v ↦ 1 )
𝑛·0·117 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·109 ⟧( v ↦ 1 )
𝑛·0·118 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·112 ⟧( v ↦ 1 )
𝑛·0·119 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·114 ⟧( v ↦ 1 )
𝑛·0·120 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·121 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·117 ⟧( v ↦ 1 )
𝑛·0·122 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·118 ⟧( v ↦ 1 )
𝑛·0·123 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·119 ⟧( v ↦ 1 )
𝑛·0·124 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·120 ⟧( v ↦ 1 )
𝑛·0·125 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·126 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·123 ⟧( v ↦ 1 )
𝑛·0·127 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·124 ⟧( v ↦ 1 )
𝑛·0·128 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·125 ⟧( v ↦ 1 )
𝑛·0·129 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·130 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·128 ⟧( v ↦ 1 )
𝑛·0·131 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·129 ⟧( v ↦ 1 )
𝑛·0·132 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·133 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·132 ⟧( v ↦ 1 )
𝑛·0·134 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·135 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝔼(L_outer):
stall(L_outer)
𝑛·0·136 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·121 ⟧( v ↦ 1 )
𝑛·0·137 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·126 ⟧( v ↦ 1 )
𝑛·0·138 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·130 ⟧( v ↦ 1 )
𝑛·0·139 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·133 ⟧( v ↦ 1 )
𝑛·0·140 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·135 ⟧( v ↦ 1 )
𝑛·0·141 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·142 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·138 ⟧( v ↦ 1 )
𝑛·0·143 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·139 ⟧( v ↦ 1 )
𝑛·0·144 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·140 ⟧( v ↦ 1 )
𝑛·0·145 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·141 ⟧( v ↦ 1 )
𝑛·0·146 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·147 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·144 ⟧( v ↦ 1 )
𝑛·0·148 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·145 ⟧( v ↦ 1 )
𝑛·0·149 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·146 ⟧( v ↦ 1 )
𝑛·0·150 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·151 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·149 ⟧( v ↦ 1 )
𝑛·0·152 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·150 ⟧( v ↦ 1 )
𝑛·0·153 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·154 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·153 ⟧( v ↦ 1 )
𝑛·0·155 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·156 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝔼(L_outer):
stall(L_outer)
𝑛·0·157 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·142 ⟧( v ↦ 1 )
𝑛·0·158 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·147 ⟧( v ↦ 1 )
𝑛·0·159 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·151 ⟧( v ↦ 1 )
𝑛·0·160 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·154 ⟧( v ↦ 1 )
𝑛·0·161 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·156 ⟧( v ↦ 1 )
𝑛·0·162 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·163 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·158 ⟧( v ↦ 1 )
𝑛·0·164 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·159 ⟧( v ↦ 1 )
𝑛·0·165 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·160 ⟧( v ↦ 1 )
𝑛·0·166 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·161 ⟧( v ↦ 1 )
𝑛·0·167 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·162 ⟧( v ↦ 1 )
𝑛·0·168 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·169 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·165 ⟧( v ↦ 1 )
𝑛·0·170 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·166 ⟧( v ↦ 1 )
𝑛·0·171 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·167 ⟧( v ↦ 1 )
𝑛·0·172 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·168 ⟧( v ↦ 1 )
𝑛·0·173 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·174 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·170 ⟧( v ↦ 1 )
𝑛·0·175 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·171 ⟧( v ↦ 1 )
𝑛·0·176 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·172 ⟧( v ↦ 1 )
𝑛·0·177 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·173 ⟧( v ↦ 1 )
𝑛·0·178 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·179 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·176 ⟧( v ↦ 1 )
𝑛·0·180 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·177 ⟧( v ↦ 1 )
𝑛·0·181 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·178 ⟧( v ↦ 1 )
𝑛·0·182 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·183 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·180 ⟧( v ↦ 1 )
𝑛·0·184 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·181 ⟧( v ↦ 1 )
𝑛·0·185 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·182 ⟧( v ↦ 1 )
𝑛·0·186 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·187 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·185 ⟧( v ↦ 1 )
𝑛·0·188 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·186 ⟧( v ↦ 1 )
𝑛·0·189 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·190 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·188 ⟧( v ↦ 1 )
𝑛·0·191 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·189 ⟧( v ↦ 1 )
𝑛·0·192 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·193 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·192 ⟧( v ↦ 1 )
𝑛·0·194 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·195 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ 𝑛·0·194 ⟧( v ↦ 1 )
𝑛·0·196 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·197 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )
𝑛·0·198 := ⟦ v ↦ ∅, λ ⤍ L_outer, arg ↦ L_none:λ ⟧( v ↦ 1 )