\begin{aligned}& (λx. e (\begin{matrix}& (\begin{matrix}e′ & Q_{3,1} \\ : & \begin{aligned}& τ_{3} \\ → & a) \end{aligned} \end{matrix} \\ @ & Q_{3,2})) \end{matrix} \\ @ & \begin{aligned}& Q_{4} \\ ∩ & Q_{5} \end{aligned} \end{aligned}

\begin{aligned}& (λx. e (\begin{matrix}& (\begin{matrix}e′ & Q_{3,1} \\ : & \begin{aligned}& τ_{3} \\ → & a) \end{aligned} \end{matrix} \\ @ & Q_{3,2})) \end{matrix} \\ @ & \begin{aligned}& Q_{4} \\ ∩ & Q_{5} \end{aligned} \end{aligned}

\begin{aligned}& (λx. e (\begin{matrix}& (\begin{matrix}e′ & Q_{3,1} \\ : & \begin{aligned}& τ_{3} \\ → & a) \end{aligned} \end{matrix} \\ @ & Q_{3,2})) \end{matrix} \\ @ & Q_{4} ∩ Q_{5} \end{aligned}

\begin{aligned}& (λx. e (\begin{matrix}& (\begin{matrix}e′ & Q_{3,1} \\ : & \begin{aligned}& τ_{3} \\ → & a) \end{aligned} \end{matrix} \\ @ & Q_{3,2})) \end{matrix} \\ @ & Q_{4} ∩ Q_{5} \end{aligned}

\begin{aligned}& (λx. e (\begin{matrix}& (\begin{matrix}e′ & Q_{3,1} \\ : & τ_{3} → a) \end{matrix} \\ @ & Q_{3,2})) \end{matrix} \\ @ & Q_{4} ∩ Q_{5} \end{aligned}

\begin{aligned}& (λx. e (\begin{matrix}& (e′ Q_{3,1} : τ_{3} → a) \\ @ & Q_{3,2})) \end{matrix} \\ @ & Q_{4} ∩ Q_{5} \end{aligned}

\begin{aligned}& (λx. e ((e′ Q_{3,1} : τ_{3} → a) @ Q_{3,2})) \\ @ & Q_{4} ∩ Q_{5} \end{aligned}

(λx. e ((e′ Q_{3,1} : τ_{3} → a) @ Q_{3,2})) @ Q_{4} ∩ Q_{5} (λx. e ((e′ Q_{3,1} : τ_{3} → a) @ Q_{3,2})) @ Q_{4} ∩ Q_{5}

(\begin{matrix}e_{0} & (λx.e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (x :a_{0}) \\ : & \begin{matrix}e_{1} & a_{0} \\ → & a_{0}) \end{matrix} \end{matrix} \\ @ & e_{1} (x :a_{0}))) \end{matrix} \\ : & \begin{matrix}e_{1} & (e_{2} a_{0} → e_{2} a_{0}) \\ → & a_{0}) \end{matrix} \end{matrix}

@ e_{1} (λy.e_{2} (y :a_{0}))

(\begin{matrix}e_{0} & (λx.e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (x :a_{0}) \\ : & e_{1} a_{0} → a_{0}) \end{matrix} \\ @ & e_{1} (x :a_{0}))) \end{matrix} \\ : & e_{1} (e_{2} a_{0} → e_{2} a_{0}) → a_{0}) \end{matrix}

@ e_{1} (λy.e_{2} (y :a_{0}))

(\begin{matrix}e_{0} & (λx.e_{2} ((e_{0} (x :a_{0}) : e_{1} a_{0} → a_{0}) @ e_{1} (x :a_{0}))) \\ : & e_{1} (e_{2} a_{0} → e_{2} a_{0}) → a_{0}) \end{matrix}

@ e_{1} (λy.e_{2} (y :a_{0}))

(\begin{matrix}e_{0} & (λx.e_{2} ((e_{0} (x :a_{0}) : e_{1} a_{0} → a_{0}) @ e_{1} (x :a_{0}))) \\ : & e_{1} (e_{2} a_{0} → e_{2} a_{0}) → a_{0}) \end{matrix}

@ e_{1} (λy.e_{2} (y :a_{0}))

(e_{0} (λx.e_{2} ((e_{0} (x :a_{0}) : e_{1} a_{0} → a_{0}) @ e_{1} (x :a_{0}))) : e_{1} (e_{2} a_{0} → e_{2} a_{0}) → a_{0})

@ e_{1} (λy.e_{2} (y :a_{0}))

(\begin{matrix}e_{0} & (λx. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (\begin{matrix}& (\begin{matrix}e_{0} & (z : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (\begin{matrix}& (\begin{matrix}e_{0} & (x : a) \\ : & e_{1} (\begin{matrix}e_{2} & e_{2} e_{0} a \\ → & e_{2} (\begin{matrix}e_{2} & e_{1} a \\ → & e_{2} a)) \end{matrix} \end{matrix} → a) \end{matrix} \\ @ & e_{1} (λf. e_{2} (λu. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (f : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (u : a)))))) \end{matrix} \end{matrix} \end{matrix} \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (\begin{matrix}& (\begin{matrix}e_{0} & (x : a) \\ : & e_{1} (\begin{matrix}e_{2} & e_{2} e_{1} a \\ → & e_{2} (\begin{matrix}e_{2} & e_{0} a \\ → & e_{2} a)) \end{matrix} \end{matrix} → a) \end{matrix} \\ @ & e_{1} (λv. e_{2} (λg. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (g : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (v : a))))))) \end{matrix} \end{matrix} \end{matrix} \\ : & e_{1} ( e_{2} e_{0} e_{0} a ∩ (\begin{matrix}e_{2} & e_{0} e_{1} a \\ ∩ & e_{2} e_{1} a) \end{matrix} → e_{2} a) → a) \end{matrix}

@ e_{1} (λy. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (\begin{matrix}& (\begin{matrix}e_{0} & (y : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (y : a)) \end{matrix} \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (y : a))) \end{matrix}

(\begin{matrix}e_{0} & (λx. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (\begin{matrix}& (\begin{matrix}e_{0} & (z : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (\begin{matrix}& (\begin{matrix}e_{0} & (x : a) \\ : & e_{1} (\begin{matrix}e_{2} & e_{2} e_{0} a \\ → & e_{2} (\begin{matrix}e_{2} & e_{1} a \\ → & e_{2} a)) \end{matrix} \end{matrix} → a) \end{matrix} \\ @ & e_{1} (λf. e_{2} (λu. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (f : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (u : a)))))) \end{matrix} \end{matrix} \end{matrix} \\ : & e_{1} a → a) \end{matrix} \\ @ & e_{1} (\begin{matrix}& (\begin{matrix}e_{0} & (x : a) \\ : & e_{1} (\begin{matrix}e_{2} & e_{2} e_{1} a \\ → & e_{2} (\begin{matrix}e_{2} & e_{0} a \\ → & e_{2} a)) \end{matrix} \end{matrix} → a) \end{matrix} \\ @ & e_{1} (λv. e_{2} (λg. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (g : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (v : a))))))) \end{matrix} \end{matrix} \end{matrix} \\ : & e_{1} ( e_{2} e_{0} e_{0} a ∩ (\begin{matrix}e_{2} & e_{0} e_{1} a \\ ∩ & e_{2} e_{1} a) \end{matrix} → e_{2} a) → a) \end{matrix}

@ e_{1} (λy. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (\begin{matrix}& (\begin{matrix}e_{0} & (y : a) \\ : & \begin{aligned}& e_{1} a \\ → & a) \end{aligned} \end{matrix} \\ @ & e_{1} (y : a)) \end{matrix} \\ : & e_{1} a → a) \end{matrix} \\ @ & e_{1} (y : a))) \end{matrix}

(\begin{matrix}e_{0} & (λx. e_{2} (\begin{matrix}& (\begin{matrix}e_{0} & (\begin{matrix}& (e_{0} (z : a) : e_{1} a → a) \\ @ & e_{1} (\begin{matrix}& (\begin{matrix}e_{0} & (x : a) \\ : & e_{1} (e_{2} e_{2} e_{0} a → e_{2} (e_{2} e_{1} a → e_{2} a)) → a) \end{matrix} \\ @ & e_{1} (λf. e_{2} (λu. e_{2} (\begin{matrix}& (e_{0} (f : a) : e_{1} a → a) \\ @ & e_{1} (u : a)))))) \end{matrix} \end{matrix} \end{matrix} \\ : & e_{1} a → a) \end{matrix} \\ @ & e_{1} (\begin{matrix}& (e_{0} (x : a) : e_{1} (e_{2} e_{2} e_{1} a → e_{2} (e_{2} e_{0} a → e_{2} a)) → a) \\ @ & e_{1} (λv. e_{2} (λg. e_{2} (\begin{matrix}& (e_{0} (g : a) : e_{1} a → a) \\ @ & e_{1} (v : a))))))) \end{matrix} \end{matrix} \end{matrix} \\ : & e_{1} (e_{2} e_{0} e_{0} a ∩ (e_{2} e_{0} e_{1} a ∩ e_{2} e_{1} a) → e_{2} a) → a) \end{matrix}

@ e_{1} (λy. e_{2} ((e_{0} ((e_{0} (y : a) : e_{1} a → a) @ e_{1} (y : a)) : e_{1} a → a) @ e_{1} (y : a)))

[malloc {x(0), x′(0)}; y.0 := [z.0 := !x.0]; malloc {w(0)}; {x.0 := 5}; jmp !y.0]

[\begin{matrix}malloc & \begin{cases}x(0), \\ x′(0)\}; \end{cases} \\ y.0 := & [z.0 := !x.0 \\ malloc & \{w(0) \\ \{x.0 := 5 \\ jmp & !y.0 \end{matrix}

[\begin{matrix}malloc & \begin{cases}x(0), \\ x′(0)\}; \end{cases} \\ y.0 := & [z.0 := !x.0 \\ malloc & \{w(0)\}; \\ \{x.0 := 5\}; \\ jmp & !y.0 \end{matrix}

[\begin{matrix}malloc & \{x(0),x′(0)\}; \\ y.0 := [z.0 := !x.0]; & malloc \{w(0)\}; \\ \{x.0 := 5\}; & jmp !y.0 \end{matrix}

[\begin{matrix}malloc \{x(0),x′(0)\}; & y.0 := [z.0 := !x.0]; \\ malloc \{w(0)\}; & \{x.0 := 5\}; & jmp !y.0 \end{matrix}

[malloc {x(0),x′(0)}; y.0 := [z.0 := !x.0]; malloc {w(0)}; {x.0 := 5}; jmp !y.0] [malloc {x(0),x′(0)}; y.0 := [z.0 := !x.0]; malloc {w(0)}; {x.0 := 5}; jmp !y.0] [malloc {x(0),x′(0)}; y.0 := [z.0 := !x.0]; malloc {w(0)}; {x.0 := 5}; jmp !y.0] (let y = V in let x = V in if y = 0 then E_{0} else … if y = n then E_{n} else wrong) (\begin{matrix}let y = & V \\ in & let x = V in if \begin{aligned}& y \\ = & 0 \end{aligned} then E_{0} else … if \begin{aligned}& y \\ = & n \end{aligned} then E_{n} else wrong) \end{matrix}

(\begin{matrix}let y = & V \\ in & let x = V in if y = 0 then E_{0} else … if y = n then E_{n} else wrong) \end{matrix} (\begin{matrix}let y = & V \\ in & let x = V in if y = 0 then E_{0} else … if y = n then E_{n} else wrong) \end{matrix}

(\begin{matrix}let y = & V \\ in & let x = V in if y = 0 then E_{0} else …if y = n then E_{n} else wrong) \end{matrix}

(let y = V in let x = V in if y = 0 then E_{0} else …if y = n then E_{n} else wrong) (let y = V in let x = V in if y = 0 then E_{0} else …if y = n then E_{n} else wrong) (let y = V in let x = V in if y = 0 then E_{0} else …if y = n then E_{n} else wrong)