Example Trace

Raw file: Trace.tfdbi

;------------------------------;
// /* a staged power function */
// $powCode := [ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)
 ──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
// /* code generating 2^3 */
// $staged := ([%ω²]$powCode '2) 3
╭──([%ω²]$powCode '2) 3     ⊣ 
│ ╭──[%ω²]$powCode '2     ⊣ 
│ │ ╭──[%ω²]$powCode     ⊣ 
│ │ │%╭──$powCode     ⊣ 
│ │ │%│$ ──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│ │ │%╰──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│ │ │%╭──λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│ │ │%╰──ƛ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│ │ ╰──ƛ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│ │  ──'2     ⊣ 
│ │ ╭──λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│ │ ╰──ƛ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│ ╰──ƛ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│  ──3     ⊣ 
│ ╭──(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│ │?╭──v     ⊣ t()t()
│ │?╰──3     ⊣ t()t()
│ │?╭──`(,v1*,(f (v-1)))     ⊣ t()t()
│ │?│`╭╌╌,v1*,(f (v-1))     ⊣ _(())t()t()
│ │?│`┆*╭╌╌,v1     ⊣ _(())t()t()
│ │?│`┆*┆,╭──v1     ⊣ t()t()
│ │?│`┆*┆,│,╭──v     ⊣ t()
│ │?│`┆*┆,│,╰──'2     ⊣ t()
│ │?│`┆*┆,╰──'2     ⊣ t()t()
│ │?│`┆*╰╌╌2     ⊣ _(())t()t()
│ │?│`┆*╭╌╌,(f (v-1))     ⊣ _(())t()t()
│ │?│`┆*┆,╭──f (v-1)     ⊣ t()t()
│ │?│`┆*┆,│ ╭──f     ⊣ t()t()
│ │?│`┆*┆,│ ╰──ƛ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│ │?│`┆*┆,│ ╭──v-1     ⊣ t()t()
│ │?│`┆*┆,│ │-╭──v     ⊣ t()t()
│ │?│`┆*┆,│ │-╰──3     ⊣ t()t()
│ │?│`┆*┆,│ │- ──1     ⊣ t()t()
│ │?│`┆*┆,│ ╰──2     ⊣ t()t()
│ │?│`┆*┆,│ ╭──(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│ │?│`┆*┆,│ │?╭──v     ⊣ t()t()
│ │?│`┆*┆,│ │?╰──2     ⊣ t()t()
│ │?│`┆*┆,│ │?╭──`(,v1*,(f (v-1)))     ⊣ t()t()
│ │?│`┆*┆,│ │?│`╭╌╌,v1*,(f (v-1))     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*╭╌╌,v1     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,╭──v1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│,╭──v     ⊣ t()
│ │?│`┆*┆,│ │?│`┆*┆,│,╰──'2     ⊣ t()
│ │?│`┆*┆,│ │?│`┆*┆,╰──'2     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*╰╌╌2     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*╭╌╌,(f (v-1))     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,╭──f (v-1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ ╭──f     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ ╰──ƛ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ ╭──v-1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │-╭──v     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │-╰──2     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │- ──1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ ╰──1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ ╭──(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?╭──v     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?╰──1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?╭──`(,v1*,(f (v-1)))     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`╭╌╌,v1*,(f (v-1))     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*╭╌╌,v1     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,╭──v1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│,╭──v     ⊣ t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│,╰──'2     ⊣ t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,╰──'2     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*╰╌╌2     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*╭╌╌,(f (v-1))     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,╭──f (v-1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ ╭──f     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ ╰──ƛ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ ╭──v-1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ │-╭──v     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ │-╰──1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ │- ──1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ ╰──0     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ ╭──(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ │?╭──v     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ │?╰──0     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ │? ──'1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,│ ╰──'1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*┆,╰──'1     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`┆*╰╌╌1     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?│`╰╌╌2*1     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ │?╰──'(2*1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,│ ╰──'(2*1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*┆,╰──'(2*1)     ⊣ t()t()
│ │?│`┆*┆,│ │?│`┆*╰╌╌2*1     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?│`╰╌╌2*2*1     ⊣ _(())t()t()
│ │?│`┆*┆,│ │?╰──'(2*2*1)     ⊣ t()t()
│ │?│`┆*┆,│ ╰──'(2*2*1)     ⊣ t()t()
│ │?│`┆*┆,╰──'(2*2*1)     ⊣ t()t()
│ │?│`┆*╰╌╌2*2*1     ⊣ _(())t()t()
│ │?│`╰╌╌2*2*2*1     ⊣ _(())t()t()
│ │?╰──'(2*2*2*1)     ⊣ t()t()
│ ╰──'(2*2*2*1)     ⊣ t()t()
╰──'(2*2*2*1)     ⊣ 
// /* running 2^3 */
// %$staged
╭──%$staged     ⊣ 
│%╭──$staged     ⊣ 
│%│$ ──'(2*2*2*1)     ⊣ 
│%╰──'(2*2*2*1)     ⊣ 
│%╭──2*2*2*1     ⊣ 
│%│* ──2     ⊣ 
│%│*╭──2*2*1     ⊣ 
│%│*│* ──2     ⊣ 
│%│*│*╭──2*1     ⊣ 
│%│*│*│* ──2     ⊣ 
│%│*│*│* ──1     ⊣ 
│%│*│*╰──2     ⊣ 
│%│*╰──4     ⊣ 
│%╰──8     ⊣ 
╰──8     ⊣ 
// /* an unstaging function */
// $unstage := λ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))
╭──λ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ 
╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ 
// /* unstaging the power function */
// $unstagedPow := [%ω²]($unstage $powCode)
╭──[%ω²]($unstage $powCode)     ⊣ 
│%╭──$unstage $powCode     ⊣ 
│%│ ╭──$unstage     ⊣ 
│%│ │$ ──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ 
│%│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ 
│%│ ╭──$powCode     ⊣ 
│%│ │$ ──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│%│ ╰──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ 
│%│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│ ╭──v     ⊣ t()
│%│ │|│ ╰──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|╰──0     ⊣ t()
│%│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│ ╰──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|╰──0     ⊣ t()
│%│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│ ╰──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ ╰──[ω²]λ.λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ ╭──[`ω²]λ.[,ω²](f1 v)     ⊣ t()t()
│%│ │|│|│|│|│ │`╭╌╌λ.[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ╭╌╌[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,╭──f1 v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ ╭──f1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ ╰──[ω²]λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│ ╰──[ω²]λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╰──[ω²]λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╰──[ω²]λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╰──[ω²]λ.(v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╭──[`ω²]λ.[,ω²](f1 v)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`╭╌╌λ.[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ╭╌╌[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,╭──f1 v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ ╭──f1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ ╰──[ω²](v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│ ╰──[ω²](v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│ ╰──[ω²](v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│ ╰──[ω²](v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╰──[ω²](v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|╭──(λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ ╰──[ω²](v ? `(,v1*,(f (v-1))) : '1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ ╭──[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`╭╌╌([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?╭╌╌[,ω²](f3 v)     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,╭──f3 v     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──f3     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──v     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──[ω²]v     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|╭──(λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|╭──(λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|╭──λ.v v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╭──λ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╰──ƛ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|│ ╰──[ω²]v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|│|╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|│|╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|│|╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│|╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──[ω²]v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,╰──[ω²]v     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?╰╌╌v     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?╭╌╌[,ω²](f3 v1)     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,╭──f3 v1     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──f3     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──v1     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╭──v     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╰──[ω²]`(,v1*,(f (v-1)))     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──[ω²]`(,v1*,(f (v-1)))     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╰──[ω²]`(,v1*,(f (v-1)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╭──[`ω²][,ω²](f1 v)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`╭╌╌[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,╭──f1 v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ ╭──f1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ ╰──[ω²](,v1*,(f (v-1)))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│ ╰──[ω²](,v1*,(f (v-1)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│ ╰──[ω²](,v1*,(f (v-1)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│ ╰──[ω²](,v1*,(f (v-1)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│ ╰──[ω²](,v1*,(f (v-1)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|╭──(λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│ ╰──[ω²](,v1*,(f (v-1)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|╭──(λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²](,v1*,(f (v-1)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ ╭──[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`╭╌╌[,ω²](f2 v)*[,ω²](f2 v1)     ⊣ _(()())t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*╭╌╌[,ω²](f2 v)     ⊣ _(()())t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,╭──f2 v     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╭──f2     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╭──v     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╰──[ω²],v1     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╰──[ω²],v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╰──[ω²],v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╰──[ω²],v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╭──[`ω²][,ω²](f1 v)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`╭╌╌[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,╭──f1 v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╭──f1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╰──[ω²]v1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╭──(λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╭──(λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╭──λ.v v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──λ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──ƛ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²]v1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,╰──[ω²]v1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`╰╌╌v1     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╰──[ω²]v1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╰──[ω²]v1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,╰──[ω²]v1     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*╰╌╌v1     ⊣ _(()())t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*╭╌╌[,ω²](f2 v1)     ⊣ _(()())t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,╭──f2 v1     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╭──f2     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╭──v1     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │,╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │,╰──[ω²],(f (v-1))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╰──[ω²],(f (v-1))     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│ ╰──[ω²],(f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│ ╰──[ω²],(f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╰──[ω²],(f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╭──[`ω²][,ω²](f1 v)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`╭╌╌[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,╭──f1 v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╭──f1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╰──[ω²](f (v-1))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╭──(λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╭──(λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╭──λ.v v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──λ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──ƛ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²](f (v-1))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|│|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|│|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|│|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|│|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|│|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ │|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`┆,╰──[ω²](f (v-1))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ │`╰╌╌f (v-1)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|│ ╰──[ω²](f (v-1))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|│|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|│|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ │|╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,│ ╰──[ω²](f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*┆,╰──[ω²](f (v-1))     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`┆*╰╌╌f (v-1)     ⊣ _(()())t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ │`╰╌╌v1*f (v-1)     ⊣ _(()())t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²](v1*f (v-1))     ⊣ t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|│|╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|│|╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|│|╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|│|╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|│|╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ │|╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,│ ╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`┆,╰──[ω²](v1*f (v-1))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ │`╰╌╌v1*f (v-1)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╰──[ω²](v1*f (v-1))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──[ω²](v1*f (v-1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,╰──[ω²](v1*f (v-1))     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?╰╌╌v1*f (v-1)     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?╭╌╌[,ω²](f3 v2)     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,╭──f3 v2     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──f3     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──v2     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │,╰──[ω²]'1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──[ω²]'1     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│ ╰──[ω²]'1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╰──[ω²]'1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╭──[`ω²][,ω²](f1 v)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`╭╌╌[,ω²](f1 v)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,╭──f1 v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ ╭──f1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │,╭──f     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │,╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ ╰──ƛ.(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ ╰──[ω²]1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ ╭──(λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│ ╭──λ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│ ╰──ƛ[`ω²]`[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|╭──(λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│ ╭──λ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│ ╰──ƛ[`ω²]'[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|╭──(λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v || (λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│ ╭──λ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│ ╰──ƛ[`ω²],[,ω²]v~[`ω²][,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|╭──(λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v || (λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│ ╭──λ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│ ╰──ƛ[`ω²]λ.[,ω²]v~[`ω²]λ.[,ω²](f1 v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|╭──(λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v || (λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v ? [,ω²]v1 : [,ω²]v2)~[`ω²]([,ω²](f3 v) ? [,ω²](f3 v1) : [,ω²](f3 v2))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|╭──(λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v || λ.v v)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1)) v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──λ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──ƛ[`ω²]([,ω²]v*[,ω²]v1)~[`ω²]([,ω²](f2 v)*[,ω²](f2 v1))     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|╰──0     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|╭──λ.v v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──λ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──ƛ.v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╭──v     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|│ ╰──[ω²]1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|│|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|│|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|│|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|│|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|│|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ │|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`┆,╰──[ω²]1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ │`╰╌╌1     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|│ ╰──[ω²]1     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|│|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ │|╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,│ ╰──[ω²]1     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?┆,╰──[ω²]1     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`┆?╰╌╌1     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ │`╰╌╌(v ? v1*f (v-1) : 1)     ⊣ _(()())t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|│ ╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()t()t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│|╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|│|╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ │|╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,│ ╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ┆,╰──[ω²](v ? v1*f (v-1) : 1)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`┆λ╰╌╌(v ? v1*f (v-1) : 1)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ │`╰╌╌λ.(v ? v1*f (v-1) : 1)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|│ ╰──[ω²]λ.(v ? v1*f (v-1) : 1)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|│|╰──[ω²]λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|│|╰──[ω²]λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|│|╰──[ω²]λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ │|╰──[ω²]λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,│ ╰──[ω²]λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|│|│ │`┆λ┆,╰──[ω²]λ.(v ? v1*f (v-1) : 1)     ⊣ t()t()
│%│ │|│|│|│|│ │`┆λ╰╌╌λ.(v ? v1*f (v-1) : 1)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ │`╰╌╌λ.λ.(v ? v1*f (v-1) : 1)     ⊣ _(()())t()t()
│%│ │|│|│|│|│ ╰──[ω²]λ.λ.(v ? v1*f (v-1) : 1)     ⊣ t()t()
│%│ │|│|│|│|╰──[ω²]λ.λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|│|╰──[ω²]λ.λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|│|╰──[ω²]λ.λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ │|╰──[ω²]λ.λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%│ ╰──[ω²]λ.λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│%╰──[ω²]λ.λ.(v ? v1*f (v-1) : 1)     ⊣ 
│%╭──λ.λ.(v ? v1*f (v-1) : 1)     ⊣ 
│%╰──ƛ.λ.(v ? v1*f (v-1) : 1)     ⊣ 
╰──ƛ.λ.(v ? v1*f (v-1) : 1)     ⊣ 
// /* running the unstaged power function */
// ($unstagedPow 2) 3
╭──($unstagedPow 2) 3     ⊣ 
│ ╭──$unstagedPow 2     ⊣ 
│ │ ╭──$unstagedPow     ⊣ 
│ │ │$ ──ƛ.λ.(v ? v1*f (v-1) : 1)     ⊣ 
│ │ ╰──ƛ.λ.(v ? v1*f (v-1) : 1)     ⊣ 
│ │  ──2     ⊣ 
│ │ ╭──λ.(v ? v1*f (v-1) : 1)     ⊣ t()
│ │ ╰──ƛ.(v ? v1*f (v-1) : 1)     ⊣ t()
│ ╰──ƛ.(v ? v1*f (v-1) : 1)     ⊣ 
│  ──3     ⊣ 
│ ╭──(v ? v1*f (v-1) : 1)     ⊣ t()t()
│ │?╭──v     ⊣ t()t()
│ │?╰──3     ⊣ t()t()
│ │?╭──v1*f (v-1)     ⊣ t()t()
│ │?│*╭──v1     ⊣ t()t()
│ │?│*│,╭──v     ⊣ t()
│ │?│*│,╰──2     ⊣ t()
│ │?│*╰──2     ⊣ t()t()
│ │?│*╭──f (v-1)     ⊣ t()t()
│ │?│*│ ╭──f     ⊣ t()t()
│ │?│*│ ╰──ƛ.(v ? v1*f (v-1) : 1)     ⊣ t()t()
│ │?│*│ ╭──v-1     ⊣ t()t()
│ │?│*│ │-╭──v     ⊣ t()t()
│ │?│*│ │-╰──3     ⊣ t()t()
│ │?│*│ │- ──1     ⊣ t()t()
│ │?│*│ ╰──2     ⊣ t()t()
│ │?│*│ ╭──(v ? v1*f (v-1) : 1)     ⊣ t()t()
│ │?│*│ │?╭──v     ⊣ t()t()
│ │?│*│ │?╰──2     ⊣ t()t()
│ │?│*│ │?╭──v1*f (v-1)     ⊣ t()t()
│ │?│*│ │?│*╭──v1     ⊣ t()t()
│ │?│*│ │?│*│,╭──v     ⊣ t()
│ │?│*│ │?│*│,╰──2     ⊣ t()
│ │?│*│ │?│*╰──2     ⊣ t()t()
│ │?│*│ │?│*╭──f (v-1)     ⊣ t()t()
│ │?│*│ │?│*│ ╭──f     ⊣ t()t()
│ │?│*│ │?│*│ ╰──ƛ.(v ? v1*f (v-1) : 1)     ⊣ t()t()
│ │?│*│ │?│*│ ╭──v-1     ⊣ t()t()
│ │?│*│ │?│*│ │-╭──v     ⊣ t()t()
│ │?│*│ │?│*│ │-╰──2     ⊣ t()t()
│ │?│*│ │?│*│ │- ──1     ⊣ t()t()
│ │?│*│ │?│*│ ╰──1     ⊣ t()t()
│ │?│*│ │?│*│ ╭──(v ? v1*f (v-1) : 1)     ⊣ t()t()
│ │?│*│ │?│*│ │?╭──v     ⊣ t()t()
│ │?│*│ │?│*│ │?╰──1     ⊣ t()t()
│ │?│*│ │?│*│ │?╭──v1*f (v-1)     ⊣ t()t()
│ │?│*│ │?│*│ │?│*╭──v1     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│,╭──v     ⊣ t()
│ │?│*│ │?│*│ │?│*│,╰──2     ⊣ t()
│ │?│*│ │?│*│ │?│*╰──2     ⊣ t()t()
│ │?│*│ │?│*│ │?│*╭──f (v-1)     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ ╭──f     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ ╰──ƛ.(v ? v1*f (v-1) : 1)     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ ╭──v-1     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ │-╭──v     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ │-╰──1     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ │- ──1     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ ╰──0     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ ╭──(v ? v1*f (v-1) : 1)     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ │?╭──v     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ │?╰──0     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ │? ──1     ⊣ t()t()
│ │?│*│ │?│*│ │?│*│ ╰──1     ⊣ t()t()
│ │?│*│ │?│*│ │?│*╰──1     ⊣ t()t()
│ │?│*│ │?│*│ │?╰──2     ⊣ t()t()
│ │?│*│ │?│*│ ╰──2     ⊣ t()t()
│ │?│*│ │?│*╰──2     ⊣ t()t()
│ │?│*│ │?╰──4     ⊣ t()t()
│ │?│*│ ╰──4     ⊣ t()t()
│ │?│*╰──4     ⊣ t()t()
│ │?╰──8     ⊣ t()t()
│ ╰──8     ⊣ t()t()
╰──8     ⊣ 
;------------------------------;