\begin{code}\>\<%
\\
%
\\
\>\AgdaSymbol{\{-\#} \AgdaKeyword{OPTIONS} --no-positivity-check \AgdaSymbol{\#-\}}\<%
\\
\>\AgdaKeyword{module} \AgdaModule{Bytecode} \AgdaKeyword{where}\<%
\\
%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Relation.Binary.PropositionalEquality} \AgdaKeyword{using} \AgdaSymbol{(}\_≡\_\AgdaSymbol{;} refl\AgdaSymbol{;} sym\AgdaSymbol{;} trans\AgdaSymbol{;} subst\AgdaSymbol{;} cong\AgdaSymbol{;} cong₂\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Data.Bool} \AgdaKeyword{using} \AgdaSymbol{(}true\AgdaSymbol{;} false\AgdaSymbol{)}\<%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Data.List} \AgdaKeyword{using} \AgdaSymbol{(}List\AgdaSymbol{;} []\AgdaSymbol{;} \_∷\_\AgdaSymbol{;} replicate\AgdaSymbol{;} \_++\_\AgdaSymbol{)}\<%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Data.Nat} \AgdaKeyword{using} \AgdaSymbol{(}ℕ\AgdaSymbol{;} \_+\_\AgdaSymbol{;} suc\AgdaSymbol{;} zero\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{Source}\<%
\\
%
\\
\>\AgdaKeyword{open} \AgdaKeyword{import} \AgdaModule{HFunctor}\<%
\\
%
\\
\>\AgdaFunction{\_	extasciitilde\_} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{α} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{a} \AgdaBound{b} \AgdaBound{c} \AgdaSymbol{:} \AgdaBound{α}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaBound{a} \AgdaDatatype{≡} \AgdaBound{b} \AgdaSymbol{→} \AgdaBound{b} \AgdaDatatype{≡} \AgdaBound{c} \AgdaSymbol{→} \AgdaBound{a} \AgdaDatatype{≡} \AgdaBound{c}\<%
\\
\>\AgdaFunction{\_	extasciitilde\_} \AgdaSymbol{=} \AgdaFunction{trans} \<[13]%
\>[13]\AgdaComment{-- just an easier-to-use notation for transitivity}\<%
\\
\>\AgdaKeyword{infixr} \AgdaNumber{5} \_	extasciitilde\_\<%
\\
%
\\
%
\\
\>\AgdaFunction{rep} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{n} \AgdaSymbol{:} \AgdaDatatype{ℕ}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaBound{A} \AgdaSymbol{→} \AgdaDatatype{List} \AgdaBound{A}\<%
\\
\>\AgdaFunction{rep} \AgdaSymbol{=} \AgdaFunction{replicate} \<[17]%
\>[17]\AgdaComment{-- just a shorter name, used a lot}\<%
\\
%
\\
%
\\
\>\AgdaFunction{coerce} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{F} \AgdaSymbol{:} \AgdaBound{A} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{\{}\AgdaBound{s₁} \AgdaBound{s₂} \AgdaSymbol{:} \AgdaBound{A}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaBound{s₁} \AgdaDatatype{≡} \AgdaBound{s₂} \AgdaSymbol{→} \AgdaBound{F} \AgdaBound{s₁} \AgdaSymbol{→} \AgdaBound{F} \AgdaBound{s₂}\<%
\\
\>\AgdaFunction{coerce} \AgdaSymbol{\_} \AgdaInductiveConstructor{refl} \AgdaBound{b} \AgdaSymbol{=} \AgdaBound{b}\<%
\\
%
\\
\>\AgdaFunction{lemmaConsAppend} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaBound{m} \AgdaBound{n} \AgdaSymbol{:} \AgdaDatatype{ℕ}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{a} \AgdaSymbol{:} \AgdaBound{A}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{s} \AgdaSymbol{:} \AgdaDatatype{List} \AgdaBound{A}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaSymbol{→} \AgdaBound{a} \AgdaInductiveConstructor{∷} \AgdaFunction{rep} \AgdaBound{m} \AgdaBound{a} \AgdaFunction{++} \AgdaBound{a} \AgdaInductiveConstructor{∷} \AgdaFunction{rep} \AgdaBound{n} \AgdaBound{a} \AgdaFunction{++} \AgdaBound{s} \AgdaDatatype{≡} \AgdaBound{a} \AgdaInductiveConstructor{∷} \AgdaSymbol{(}\AgdaFunction{rep} \AgdaBound{m} \AgdaBound{a} \AgdaFunction{++} \AgdaBound{a} \AgdaInductiveConstructor{∷} \AgdaFunction{rep} \AgdaBound{n} \AgdaBound{a}\AgdaSymbol{)} \AgdaFunction{++} \AgdaBound{s}\<%
\\
\>\AgdaFunction{lemmaConsAppend} \AgdaInductiveConstructor{zero} \<[24]%
\>[24]\AgdaBound{n} \AgdaBound{a} \AgdaBound{s} \AgdaSymbol{=} \AgdaInductiveConstructor{refl}\<%
\\
\>\AgdaFunction{lemmaConsAppend} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)} \AgdaBound{n} \AgdaBound{a} \AgdaBound{s} \AgdaSymbol{=} \AgdaFunction{cong} \AgdaSymbol{(}\AgdaInductiveConstructor{\_∷\_} \AgdaBound{a}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{lemmaConsAppend} \AgdaBound{m} \AgdaBound{n} \AgdaBound{a} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaFunction{lemmaPlusAppend} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaBound{m} \AgdaBound{n} \AgdaSymbol{:} \AgdaDatatype{ℕ}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{a} \AgdaSymbol{:} \AgdaBound{A}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaFunction{rep} \AgdaBound{m} \AgdaBound{a} \AgdaFunction{++} \AgdaFunction{rep} \AgdaBound{n} \AgdaBound{a} \AgdaDatatype{≡} \AgdaFunction{rep} \AgdaSymbol{(}\AgdaBound{m} \AgdaPrimitive{+} \AgdaBound{n}\AgdaSymbol{)} \AgdaBound{a}\<%
\\
\>\AgdaFunction{lemmaPlusAppend} \AgdaInductiveConstructor{zero} \<[24]%
\>[24]\AgdaBound{n} \AgdaBound{a} \AgdaSymbol{=} \AgdaInductiveConstructor{refl}\<%
\\
\>\AgdaFunction{lemmaPlusAppend} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)} \AgdaBound{n} \AgdaBound{a} \AgdaSymbol{=} \AgdaFunction{cong} \AgdaSymbol{(}\AgdaInductiveConstructor{\_∷\_} \AgdaBound{a}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{lemmaPlusAppend} \AgdaBound{m} \AgdaBound{n} \AgdaBound{a}\AgdaSymbol{)}\<%
\\
%
\\
%
\\
\>\AgdaComment{-- First, we define "typed stacks", which are stacks indexed by lists of TyExp.}\<%
\\
\>\AgdaComment{-- Each element of the stack has therefore a corresponding type.}\<%
\\
\>\<\end{code}

%<*stacktype>
\begin{code}\>\<%
\\
\>\AgdaFunction{StackType} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\<%
\\
\>\AgdaFunction{StackType} \AgdaSymbol{=} \AgdaDatatype{List} \AgdaDatatype{Tyₛ}\<%
\\
\>\<\end{code}
%</stacktype>

%<*stack>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{Stack} \AgdaSymbol{:} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{ε} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaDatatype{Stack} \AgdaInductiveConstructor{[]}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{\_▽\_} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{t} \AgdaBound{s'}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaFunction{⁅} \AgdaBound{t} \AgdaFunction{⁆} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s'} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaSymbol{(}\AgdaBound{t} \AgdaInductiveConstructor{∷} \AgdaBound{s'}\AgdaSymbol{)}\<%
\\
\>\<\end{code}
%</stack>
\begin{code}\>\<%
\\
%
\\
\>\AgdaKeyword{infixr} \AgdaNumber{7} \_▽\_\<%
\\
\>\<\end{code}


-- To complete the definition of the abstract machine,
-- we need to list the instructions of the bytecode operating on it, and give its semantics.

%<*bytecode>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{Bytecode} \AgdaSymbol{:} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{SKIP} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \<[20]%
\>[20]\AgdaSymbol{→} \AgdaDatatype{Bytecode} \AgdaBound{s} \AgdaBound{s}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{PUSH} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{t} \AgdaBound{s}\AgdaSymbol{\}} \<[20]%
\>[20]\AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{x} \AgdaSymbol{:} \AgdaFunction{⁅} \AgdaBound{t} \AgdaFunction{⁆}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Bytecode} \AgdaBound{s} \AgdaSymbol{(}\AgdaBound{t} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{ADD} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \<[20]%
\>[20]\AgdaSymbol{→} \AgdaDatatype{Bytecode} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\<\end{code}
%</bytecode>
\begin{code}\>\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{IF} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{t} \AgdaSymbol{:} \AgdaDatatype{Bytecode} \AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{e} \AgdaSymbol{:} \AgdaDatatype{Bytecode} \AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Bytecode} \AgdaSymbol{(}\AgdaInductiveConstructor{𝔹ₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaBound{s′}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{\_⟫\_} \<[9]%
\>[9]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s₀} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{c₁} \AgdaSymbol{:} \AgdaDatatype{Bytecode} \AgdaBound{s₀} \AgdaBound{s₁}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{c₂} \AgdaSymbol{:} \AgdaDatatype{Bytecode} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Bytecode} \AgdaBound{s₀} \AgdaBound{s₂}\<%
\\
%
\\
\>\AgdaKeyword{infixl} \AgdaNumber{4} \_⟫\_\<%
\\
\>\<\end{code}

%<*Tree>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{Tree} \AgdaSymbol{(}\AgdaBound{f} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{In} \AgdaSymbol{:} \AgdaBound{f} \AgdaSymbol{(}\AgdaDatatype{Tree} \AgdaBound{f}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{Tree} \AgdaBound{f}\<%
\\
\>\<\end{code}
%</Tree>

%<*HTree>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{HTree}\<%
\\
\>[4]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaBound{f} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaFunction{StackType} \AgdaSymbol{→} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \<[41]%
\>[41]\<%
\\
\>[6]\AgdaIndent{9}{}\<[9]%
\>[9]\AgdaSymbol{→} \AgdaSymbol{(}\AgdaFunction{StackType} \AgdaSymbol{→} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{)} \<[43]%
\>[43]\<%
\\
\>[0]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaBound{ixp} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{ixq} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{HTreeIn} \AgdaSymbol{:} \AgdaBound{f} \AgdaSymbol{(}\AgdaDatatype{HTree} \AgdaBound{f}\AgdaSymbol{)} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{→} \AgdaDatatype{HTree} \AgdaBound{f} \AgdaBound{ixp} \AgdaBound{ixq}\<%
\\
\>\<\end{code}
%</HTree>

\begin{code}\>\<%
\\
\>\AgdaKeyword{postulate} \AgdaPostulate{foldTree} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{F} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaFunction{StackType} \AgdaSymbol{->} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{->} \AgdaSymbol{(}\AgdaFunction{StackType} \AgdaSymbol{->} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{)\}} \AgdaSymbol{->} \AgdaSymbol{\{\{} \AgdaBound{functor} \AgdaSymbol{:} \AgdaRecord{HFunctor} \AgdaBound{F} \AgdaSymbol{\}\}} \AgdaSymbol{->} \AgdaSymbol{\{}\AgdaBound{r} \AgdaSymbol{:} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaSymbol{(} \AgdaSymbol{\{}\AgdaBound{ixp} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{ixq} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaBound{F} \AgdaBound{r} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{->} \AgdaBound{r} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)} \AgdaSymbol{->} \AgdaSymbol{(} \AgdaSymbol{\{}\AgdaBound{ixp} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{ixq} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HTree} \AgdaBound{F} \<[287]%
\>[287]\AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{->} \AgdaBound{r} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)}\<%
\\
\>\<\end{code}


%<*HGraph>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{HGraph'} \AgdaSymbol{\{}\AgdaBound{Ip} \AgdaBound{Iq} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaBound{F} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{Ip} \AgdaSymbol{→} \AgdaBound{Iq} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{Ip} \AgdaSymbol{→} \AgdaBound{Iq} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{v} \AgdaSymbol{:} \AgdaBound{Ip} \AgdaSymbol{→} \AgdaBound{Iq} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{ixp} \AgdaSymbol{:} \AgdaBound{Ip}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{ixq} \AgdaSymbol{:} \AgdaBound{Iq}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{HGraphIn} \<[14]%
\>[14]\AgdaSymbol{:} \AgdaBound{F} \AgdaSymbol{(}\AgdaDatatype{HGraph'} \AgdaBound{F} \AgdaBound{v}\AgdaSymbol{)} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{→} \AgdaDatatype{HGraph'} \AgdaBound{F} \AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{HGraphLet} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaDatatype{HGraph'} \AgdaBound{F} \AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{→} \AgdaDatatype{HGraph'} \AgdaBound{F} \AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{HGraph'} \AgdaBound{F} \AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{HGraphVar} \AgdaSymbol{:} \AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{→} \AgdaDatatype{HGraph'} \AgdaBound{F} \AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq}\<%
\\
\>\<\end{code}
%</HGraph>

\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{HGraph} \AgdaSymbol{\{}\AgdaBound{Ip} \AgdaBound{Iq} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaBound{F} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{Ip} \AgdaSymbol{->} \AgdaBound{Iq} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{->} \AgdaSymbol{(}\AgdaBound{Ip} \AgdaSymbol{->} \AgdaBound{Iq} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{ixp} \AgdaSymbol{:} \AgdaBound{Ip}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{ixq} \AgdaSymbol{:} \AgdaBound{Iq}\AgdaSymbol{)} \AgdaSymbol{:} \AgdaPrimitiveType{Set₁} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaInductiveConstructor{mkHGraph} \AgdaSymbol{:} \AgdaSymbol{(} \AgdaSymbol{\{}\AgdaBound{v} \AgdaSymbol{:} \AgdaBound{Ip} \AgdaSymbol{->} \AgdaBound{Iq} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaSymbol{(}\AgdaDatatype{HGraph'} \AgdaBound{F} \AgdaBound{v} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)} \AgdaSymbol{)} \AgdaSymbol{->} \AgdaDatatype{HGraph} \AgdaBound{F} \AgdaBound{ixp} \AgdaBound{ixq}\<%
\\
\>\<\end{code}

\begin{code}\>\<%
\\
%
\\
\>\AgdaKeyword{postulate} \AgdaPostulate{foldGraph} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{F} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaFunction{StackType} \AgdaSymbol{->} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{->} \AgdaSymbol{(}\AgdaFunction{StackType} \AgdaSymbol{->} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{)\}} \AgdaSymbol{->} \AgdaSymbol{\{\{} \AgdaBound{functor} \AgdaSymbol{:} \AgdaRecord{HFunctor} \AgdaBound{F} \AgdaSymbol{\}\}} \AgdaSymbol{->} \AgdaSymbol{\{}\AgdaBound{r} \AgdaSymbol{:} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaSymbol{(} \AgdaSymbol{\{}\AgdaBound{ixp} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{ixq} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaBound{F} \AgdaBound{r} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{->} \AgdaBound{r} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)->} \AgdaSymbol{(} \AgdaSymbol{\{}\AgdaBound{ixp} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{ixq} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HGraph} \AgdaBound{F} \<[288]%
\>[288]\AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{->} \AgdaBound{r} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)}\<%
\\
%
\\
\>\<\end{code}


%<*bytecodeF>
\begin{code}\>\<%
\\
\>\AgdaKeyword{data} \AgdaDatatype{BytecodeF} \AgdaSymbol{(}\AgdaBound{r} \AgdaSymbol{:} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{:}\<%
\\
\>[0]\AgdaIndent{19}{}\<[19]%
\>[19]\AgdaSymbol{(}\AgdaFunction{StackType} \AgdaSymbol{→} \AgdaFunction{StackType} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{SKIP'} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \<[21]%
\>[21]\AgdaSymbol{→} \AgdaDatatype{BytecodeF} \AgdaBound{r} \AgdaBound{s} \AgdaBound{s}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{PUSH'} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{a} \AgdaBound{s}\AgdaSymbol{\}} \<[21]%
\>[21]\AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{x} \AgdaSymbol{:} \AgdaFunction{⁅} \AgdaBound{a} \AgdaFunction{⁆}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{BytecodeF} \AgdaBound{r} \AgdaBound{s} \AgdaSymbol{(}\AgdaBound{a} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{ADD'} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \<[21]%
\>[21]\AgdaSymbol{→} \AgdaDatatype{BytecodeF} \AgdaBound{r} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\<\end{code}
%</bytecodeF>

\begin{code}\>\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{IF'} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{t} \AgdaSymbol{:} \AgdaBound{r} \AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{e} \AgdaSymbol{:} \AgdaBound{r} \AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{BytecodeF} \AgdaBound{r} \AgdaSymbol{(}\AgdaInductiveConstructor{𝔹ₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaBound{s′}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaInductiveConstructor{\_⟫'\_} \<[10]%
\>[10]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s₀} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{c₁} \AgdaSymbol{:} \AgdaBound{r} \AgdaBound{s₀} \AgdaBound{s₁}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaBound{c₂} \AgdaSymbol{:} \AgdaBound{r} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{BytecodeF} \AgdaBound{r} \AgdaBound{s₀} \AgdaBound{s₂}\<%
\\
\>\AgdaFunction{SKIP\_T} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaBound{s}\<%
\\
\>\AgdaFunction{SKIP\_T} \AgdaSymbol{=} \AgdaInductiveConstructor{HTreeIn} \AgdaInductiveConstructor{SKIP'}\<%
\\
%
\\
\>\AgdaFunction{PUSH\_T} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{α} \AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaSymbol{(}\AgdaBound{x} \AgdaSymbol{:} \AgdaFunction{⁅} \AgdaBound{α} \AgdaFunction{⁆}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaSymbol{(}\AgdaBound{α} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{PUSH\_T} \AgdaBound{x} \AgdaSymbol{=} \AgdaInductiveConstructor{HTreeIn} \AgdaSymbol{(}\AgdaInductiveConstructor{PUSH'} \AgdaBound{x}\AgdaSymbol{)} \<[29]%
\>[29]\<%
\\
%
\\
\>\AgdaFunction{ADD\_T} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{ADD\_T} \AgdaSymbol{=} \AgdaInductiveConstructor{HTreeIn} \AgdaInductiveConstructor{ADD'}\<%
\\
%
\\
\>\AgdaFunction{IF\_T} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s} \AgdaBound{s'}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaBound{s'} \AgdaSymbol{->} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaBound{s'} \AgdaSymbol{->} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaSymbol{(}\AgdaInductiveConstructor{𝔹ₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaBound{s'}\<%
\\
\>\AgdaFunction{IF\_T} \AgdaBound{t} \AgdaBound{f} \AgdaSymbol{=} \AgdaInductiveConstructor{HTreeIn} \AgdaSymbol{(}\AgdaInductiveConstructor{IF'} \AgdaBound{t} \AgdaBound{f}\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaFunction{\_⟫T\_} \<[6]%
\>[6]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s₀} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s₀} \AgdaBound{s₁}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s₀} \AgdaBound{s₂}\<%
\\
\>\AgdaFunction{\_⟫T\_} \AgdaBound{f} \AgdaBound{g} \AgdaSymbol{=} \AgdaInductiveConstructor{HTreeIn} \AgdaSymbol{(}\AgdaBound{f} \AgdaInductiveConstructor{⟫'} \AgdaBound{g}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{SKIP\_G} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{v} \AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s} \AgdaBound{s}\<%
\\
\>\AgdaFunction{SKIP\_G} \AgdaSymbol{=} \AgdaInductiveConstructor{HGraphIn} \AgdaInductiveConstructor{SKIP'}\<%
\\
%
\\
\>\AgdaFunction{PUSH\_G} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{v} \AgdaBound{α} \AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaSymbol{(}\AgdaBound{x} \AgdaSymbol{:} \AgdaFunction{⁅} \AgdaBound{α} \AgdaFunction{⁆}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s} \AgdaSymbol{(}\AgdaBound{α} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{PUSH\_G} \AgdaBound{x} \AgdaSymbol{=} \AgdaInductiveConstructor{HGraphIn} \AgdaSymbol{(}\AgdaInductiveConstructor{PUSH'} \AgdaBound{x}\AgdaSymbol{)} \<[30]%
\>[30]\<%
\\
%
\\
\>\AgdaFunction{ADD\_G} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{v} \AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaInductiveConstructor{ℕₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{ADD\_G} \AgdaSymbol{=} \AgdaInductiveConstructor{HGraphIn} \AgdaInductiveConstructor{ADD'}\<%
\\
%
\\
\>\AgdaFunction{IF\_G} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{v} \AgdaBound{s} \AgdaBound{s'}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s} \AgdaBound{s'} \AgdaSymbol{->} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s} \AgdaBound{s'} \AgdaSymbol{->} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaSymbol{(}\AgdaInductiveConstructor{𝔹ₛ} \AgdaInductiveConstructor{∷} \AgdaBound{s}\AgdaSymbol{)} \AgdaBound{s'}\<%
\\
\>\AgdaFunction{IF\_G} \AgdaBound{t} \AgdaBound{f} \AgdaSymbol{=} \AgdaInductiveConstructor{HGraphIn} \AgdaSymbol{(}\AgdaInductiveConstructor{IF'} \AgdaBound{t} \AgdaBound{f}\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaFunction{\_⟫G\_} \<[6]%
\>[6]\AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{v} \AgdaBound{s₀} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s₀} \AgdaBound{s₁}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaSymbol{(}\AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s₁} \AgdaBound{s₂}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s₀} \AgdaBound{s₂}\<%
\\
\>\AgdaFunction{\_⟫G\_} \AgdaBound{f} \AgdaBound{g} \AgdaSymbol{=} \AgdaInductiveConstructor{HGraphIn} \AgdaSymbol{(}\AgdaBound{f} \AgdaInductiveConstructor{⟫'} \AgdaBound{g}\AgdaSymbol{)}\<%
\\
%
\\
%
\\
%
\\
%
\\
\>\AgdaFunction{mapBytecodeF} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{a} \AgdaBound{b} \AgdaSymbol{:} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaFunction{StackType} \AgdaSymbol{->} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaSymbol{(} \AgdaSymbol{\{}\AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{->} \<[93]%
\>[93]\AgdaBound{a} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{->} \<[116]%
\>[116]\AgdaBound{b} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)} \<[127]%
\>[127]\<%
\\
\>[4]\AgdaIndent{53}{}\<[53]%
\>[53]\AgdaSymbol{->} \AgdaSymbol{(} \AgdaSymbol{\{}\AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{->} \AgdaDatatype{BytecodeF} \AgdaBound{a} \AgdaBound{ixp} \AgdaBound{ixq} \AgdaSymbol{->} \AgdaDatatype{BytecodeF} \AgdaBound{b} \AgdaBound{ixp} \AgdaBound{ixq}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{mapBytecodeF} \AgdaBound{f} \AgdaInductiveConstructor{SKIP'} \AgdaSymbol{=} \AgdaInductiveConstructor{SKIP'}\<%
\\
\>\AgdaFunction{mapBytecodeF} \AgdaBound{f} \AgdaSymbol{(}\AgdaInductiveConstructor{PUSH'} \AgdaBound{x}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaInductiveConstructor{PUSH'} \AgdaBound{x}\<%
\\
\>\AgdaFunction{mapBytecodeF} \AgdaBound{f} \AgdaInductiveConstructor{ADD'} \AgdaSymbol{=} \AgdaInductiveConstructor{ADD'}\<%
\\
\>\AgdaFunction{mapBytecodeF} \AgdaBound{f} \AgdaSymbol{(}\AgdaInductiveConstructor{IF'} \AgdaBound{t} \AgdaBound{e}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaInductiveConstructor{IF'} \AgdaSymbol{(}\AgdaBound{f} \AgdaBound{t}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaBound{f} \AgdaBound{e}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{mapBytecodeF} \AgdaBound{f} \AgdaSymbol{(}\AgdaInductiveConstructor{\_⟫'\_} \AgdaBound{c₁} \AgdaBound{c₂}\AgdaSymbol{)=} \AgdaBound{f} \AgdaBound{c₁} \AgdaInductiveConstructor{⟫'} \AgdaBound{f} \AgdaBound{c₂}\<%
\\
%
\\
%
\\
\>\AgdaFunction{BytecodeFunctor} \AgdaSymbol{:} \AgdaRecord{HFunctor} \AgdaDatatype{BytecodeF}\<%
\\
\>\AgdaFunction{BytecodeFunctor} \AgdaSymbol{=}\<%
\\
\>[47]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{record} \AgdaSymbol{\{}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaField{hmap} \AgdaSymbol{=} \AgdaFunction{mapBytecodeF}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaSymbol{\}}\<%
\\
%
\\
\>\AgdaComment{-- Now the operational semantics of the bytecode.}\<%
\\
\>\AgdaFunction{exec} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{Bytecode} \AgdaBound{s} \AgdaBound{s′} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s′}\<%
\\
\>\AgdaFunction{exec} \AgdaInductiveConstructor{SKIP} \<[17]%
\>[17]\AgdaBound{s} \<[29]%
\>[29]\AgdaSymbol{=} \AgdaBound{s}\<%
\\
\>\AgdaFunction{exec} \AgdaSymbol{(}\AgdaInductiveConstructor{PUSH} \AgdaBound{v}\AgdaSymbol{)} \<[17]%
\>[17]\AgdaBound{s} \<[29]%
\>[29]\AgdaSymbol{=} \AgdaBound{v} \AgdaInductiveConstructor{▽} \AgdaBound{s}\<%
\\
\>\AgdaFunction{exec} \AgdaInductiveConstructor{ADD} \<[17]%
\>[17]\AgdaSymbol{(}\AgdaBound{n} \AgdaInductiveConstructor{▽} \AgdaBound{m} \AgdaInductiveConstructor{▽} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaSymbol{(}\AgdaBound{n} \AgdaPrimitive{+} \AgdaBound{m}\AgdaSymbol{)} \AgdaInductiveConstructor{▽} \AgdaBound{s}\<%
\\
\>\AgdaFunction{exec} \AgdaSymbol{(}\AgdaInductiveConstructor{IF} \AgdaBound{t} \AgdaBound{e}\AgdaSymbol{)} \<[17]%
\>[17]\AgdaSymbol{(}\AgdaInductiveConstructor{true} \<[24]%
\>[24]\AgdaInductiveConstructor{▽} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaFunction{exec} \AgdaBound{t} \AgdaBound{s}\<%
\\
\>\AgdaFunction{exec} \AgdaSymbol{(}\AgdaInductiveConstructor{IF} \AgdaBound{t} \AgdaBound{e}\AgdaSymbol{)} \<[17]%
\>[17]\AgdaSymbol{(}\AgdaInductiveConstructor{false} \AgdaInductiveConstructor{▽} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaFunction{exec} \AgdaBound{e} \AgdaBound{s}\<%
\\
\>\AgdaFunction{exec} \AgdaSymbol{(}\AgdaBound{c₁} \AgdaInductiveConstructor{⟫} \AgdaBound{c₂}\AgdaSymbol{)} \<[17]%
\>[17]\AgdaBound{s} \<[29]%
\>[29]\AgdaSymbol{=} \AgdaFunction{exec} \AgdaBound{c₂} \AgdaSymbol{(}\AgdaFunction{exec} \AgdaBound{c₁} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
%
\\
\>\AgdaFunction{execAlg} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s} \AgdaBound{s′}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{BytecodeF} \AgdaSymbol{(λ} \AgdaBound{t} \AgdaBound{t'} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{t} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{t'}\AgdaSymbol{)} \AgdaBound{s} \AgdaBound{s′} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s′}\<%
\\
\>\AgdaFunction{execAlg} \AgdaInductiveConstructor{SKIP'} \<[21]%
\>[21]\AgdaBound{s} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaBound{s}\<%
\\
\>\AgdaFunction{execAlg} \AgdaSymbol{(}\AgdaInductiveConstructor{PUSH'} \AgdaBound{v}\AgdaSymbol{)} \<[21]%
\>[21]\AgdaBound{s} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaBound{v} \AgdaInductiveConstructor{▽} \AgdaBound{s}\<%
\\
\>\AgdaFunction{execAlg} \AgdaInductiveConstructor{ADD'} \<[21]%
\>[21]\AgdaSymbol{(}\AgdaBound{n} \AgdaInductiveConstructor{▽} \AgdaBound{m} \AgdaInductiveConstructor{▽} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaSymbol{(}\AgdaBound{n} \AgdaPrimitive{+} \AgdaBound{m}\AgdaSymbol{)} \AgdaInductiveConstructor{▽} \AgdaBound{s}\<%
\\
\>\AgdaFunction{execAlg} \AgdaSymbol{(}\AgdaInductiveConstructor{IF'} \AgdaBound{t} \AgdaBound{e}\AgdaSymbol{)} \<[21]%
\>[21]\AgdaSymbol{(}\AgdaInductiveConstructor{true} \<[28]%
\>[28]\AgdaInductiveConstructor{▽} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaBound{t} \AgdaBound{s}\<%
\\
\>\AgdaFunction{execAlg} \AgdaSymbol{(}\AgdaInductiveConstructor{IF'} \AgdaBound{t} \AgdaBound{e}\AgdaSymbol{)} \<[21]%
\>[21]\AgdaSymbol{(}\AgdaInductiveConstructor{false} \AgdaInductiveConstructor{▽} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaBound{e} \AgdaBound{s}\<%
\\
\>\AgdaFunction{execAlg} \AgdaSymbol{(}\AgdaBound{c₁} \AgdaInductiveConstructor{⟫'} \AgdaBound{c₂}\AgdaSymbol{)} \<[21]%
\>[21]\AgdaBound{s} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaBound{c₂} \AgdaSymbol{(}\AgdaBound{c₁} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\<\end{code}

%<*compile>
\begin{code}\>\<%
\\
\>\AgdaFunction{compile} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{t} \AgdaBound{z} \AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaBound{z} \AgdaSymbol{→} \AgdaDatatype{Bytecode} \AgdaBound{s} \AgdaSymbol{(}\AgdaFunction{replicate} \AgdaBound{z} \AgdaBound{t} \AgdaFunction{++} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{compile} \AgdaSymbol{(}\AgdaInductiveConstructor{vₛ} \AgdaBound{x}\AgdaSymbol{)} \<[32]%
\>[32]\AgdaSymbol{=} \AgdaInductiveConstructor{PUSH} \AgdaBound{x}\<%
\\
\>\AgdaFunction{compile} \AgdaSymbol{(}\AgdaBound{e₁} \AgdaInductiveConstructor{+ₛ} \AgdaBound{e₂}\AgdaSymbol{)} \<[32]%
\>[32]\AgdaSymbol{=} \AgdaFunction{compile} \AgdaBound{e₂} \AgdaInductiveConstructor{⟫} \AgdaFunction{compile} \AgdaBound{e₁} \AgdaInductiveConstructor{⟫} \AgdaInductiveConstructor{ADD}\<%
\\
\>\<\end{code}
%</compile>

\begin{code}\>\<%
\\
\>\AgdaFunction{compile} \AgdaSymbol{(}\AgdaInductiveConstructor{ifₛ} \AgdaBound{c} \AgdaInductiveConstructor{thenₛ} \AgdaBound{t} \AgdaInductiveConstructor{elseₛ} \AgdaBound{e}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaFunction{compile} \AgdaBound{c} \AgdaInductiveConstructor{⟫} \AgdaInductiveConstructor{IF} \AgdaSymbol{(}\AgdaFunction{compile} \AgdaBound{t}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{compile} \AgdaBound{e}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{compile} \AgdaSymbol{\{}\AgdaSymbol{.}\AgdaBound{σ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaSymbol{.(}\AgdaInductiveConstructor{suc} \AgdaBound{n} \AgdaPrimitive{+} \AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaInductiveConstructor{\_⟫ₛ\_} \AgdaSymbol{\{}\AgdaBound{σ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{m}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{n}\AgdaSymbol{\}} \AgdaBound{e₁} \AgdaBound{e₂}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaSymbol{=} \AgdaFunction{coerce} \AgdaSymbol{(}\AgdaDatatype{Bytecode} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>[2]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{lemmaConsAppend} \AgdaBound{n} \AgdaBound{m} \AgdaBound{σ} \AgdaBound{s}\<%
\\
\>[6]\AgdaIndent{7}{}\<[7]%
\>[7]\AgdaFunction{	extasciitilde} \AgdaFunction{cong} \AgdaSymbol{(λ} \AgdaBound{l} \AgdaSymbol{→} \AgdaBound{σ} \AgdaInductiveConstructor{∷} \AgdaBound{l} \AgdaFunction{++} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{lemmaPlusAppend} \AgdaBound{n} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)} \AgdaBound{σ}\AgdaSymbol{))}\<%
\\
\>[0]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{compile} \AgdaBound{e₁} \AgdaInductiveConstructor{⟫} \AgdaFunction{compile} \AgdaBound{e₂}\AgdaSymbol{)}\<%
\\
\>\<\end{code}

%<*compileT>
\begin{code}\>\<%
\\
\>\AgdaFunction{compileT} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{t} \AgdaBound{z} \AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaBound{z}\<%
\\
\>[0]\AgdaIndent{11}{}\<[11]%
\>[11]\AgdaSymbol{→} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaSymbol{(}\AgdaFunction{replicate} \AgdaBound{z} \AgdaBound{t} \AgdaFunction{++} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\<\end{code}
%</compileT>

\begin{code}\>\<%
\\
%
\\
\>\AgdaFunction{compileT} \AgdaSymbol{(}\AgdaInductiveConstructor{vₛ} \AgdaBound{x}\AgdaSymbol{)} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaFunction{PUSH\_T} \AgdaBound{x}\<%
\\
\>\AgdaFunction{compileT} \AgdaSymbol{(}\AgdaBound{e₁} \AgdaInductiveConstructor{+ₛ} \AgdaBound{e₂}\AgdaSymbol{)} \<[33]%
\>[33]\AgdaSymbol{=} \AgdaSymbol{(}\AgdaFunction{compileT} \AgdaBound{e₂} \AgdaFunction{⟫T} \AgdaFunction{compileT} \AgdaBound{e₁}\AgdaSymbol{)} \AgdaFunction{⟫T} \AgdaFunction{ADD\_T}\<%
\\
\>\AgdaFunction{compileT} \AgdaSymbol{(}\AgdaInductiveConstructor{ifₛ} \AgdaBound{c} \AgdaInductiveConstructor{thenₛ} \AgdaBound{t} \AgdaInductiveConstructor{elseₛ} \AgdaBound{e}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaFunction{compileT} \AgdaBound{c} \AgdaFunction{⟫T} \AgdaFunction{IF\_T} \AgdaSymbol{(}\AgdaFunction{compileT} \AgdaBound{t}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{compileT} \AgdaBound{e}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{compileT} \AgdaSymbol{\{}\AgdaSymbol{.}\AgdaBound{σ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaSymbol{.(}\AgdaInductiveConstructor{suc} \AgdaBound{n} \AgdaPrimitive{+} \AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaInductiveConstructor{\_⟫ₛ\_} \AgdaSymbol{\{}\AgdaBound{σ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{m}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{n}\AgdaSymbol{\}} \AgdaBound{e₁} \AgdaBound{e₂}\AgdaSymbol{)} \<[62]%
\>[62]\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaSymbol{=} \AgdaFunction{coerce} \AgdaSymbol{(}\AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{lemmaConsAppend} \AgdaBound{n} \AgdaBound{m} \AgdaBound{σ} \AgdaBound{s}\<%
\\
\>[6]\AgdaIndent{7}{}\<[7]%
\>[7]\AgdaFunction{	extasciitilde} \AgdaFunction{cong} \AgdaSymbol{(λ} \AgdaBound{l} \AgdaSymbol{→} \AgdaBound{σ} \AgdaInductiveConstructor{∷} \AgdaBound{l} \AgdaFunction{++} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{lemmaPlusAppend} \AgdaBound{n} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)} \AgdaBound{σ}\AgdaSymbol{))}\<%
\\
\>[0]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{compileT} \AgdaBound{e₁} \AgdaFunction{⟫T} \AgdaFunction{compileT} \AgdaBound{e₂}\AgdaSymbol{)}\<%
\\
\>\<\end{code}


\begin{code}\>\<%
\\
%
\\
%
\\
\>\AgdaFunction{compileG'} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{σ} \AgdaBound{z} \AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{σ} \AgdaBound{z} \AgdaSymbol{→} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{v}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s} \AgdaSymbol{(}\AgdaFunction{replicate} \AgdaBound{z} \AgdaBound{σ} \AgdaFunction{++} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{compileG'} \AgdaSymbol{(}\AgdaInductiveConstructor{vₛ} \AgdaBound{x}\AgdaSymbol{)} \<[34]%
\>[34]\AgdaSymbol{=} \AgdaFunction{PUSH\_G} \AgdaBound{x}\<%
\\
\>\AgdaFunction{compileG'} \AgdaSymbol{(}\AgdaBound{e₁} \AgdaInductiveConstructor{+ₛ} \AgdaBound{e₂}\AgdaSymbol{)} \<[34]%
\>[34]\AgdaSymbol{=} \AgdaSymbol{(}\AgdaFunction{compileG'} \AgdaBound{e₂} \AgdaFunction{⟫G} \AgdaFunction{compileG'} \AgdaBound{e₁}\AgdaSymbol{)} \AgdaFunction{⟫G} \AgdaFunction{ADD\_G}\<%
\\
\>\AgdaFunction{compileG'} \AgdaSymbol{(}\AgdaInductiveConstructor{ifₛ} \AgdaBound{c} \AgdaInductiveConstructor{thenₛ} \AgdaBound{t} \AgdaInductiveConstructor{elseₛ} \AgdaBound{e}\AgdaSymbol{)} \AgdaSymbol{=} \AgdaFunction{compileG'} \AgdaBound{c} \AgdaFunction{⟫G} \AgdaFunction{IF\_G} \AgdaSymbol{(}\AgdaFunction{compileG'} \AgdaBound{t}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{compileG'} \AgdaBound{e}\AgdaSymbol{)}\<%
\\
\>\AgdaFunction{compileG'} \AgdaSymbol{\{}\AgdaSymbol{.}\AgdaBound{σ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaSymbol{.(}\AgdaInductiveConstructor{suc} \AgdaBound{n} \AgdaPrimitive{+} \AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{s}\AgdaSymbol{\}} \AgdaSymbol{(}\AgdaInductiveConstructor{\_⟫ₛ\_} \AgdaSymbol{\{}\AgdaBound{σ}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{m}\AgdaSymbol{\}} \AgdaSymbol{\{}\AgdaBound{n}\AgdaSymbol{\}} \AgdaBound{e₁} \AgdaBound{e₂}\AgdaSymbol{)} \AgdaSymbol{\{}\AgdaBound{v}\AgdaSymbol{\}}\<%
\\
\>[0]\AgdaIndent{4}{}\<[4]%
\>[4]\AgdaSymbol{=} \AgdaFunction{coerce} \AgdaSymbol{(}\AgdaDatatype{HGraph'} \AgdaDatatype{BytecodeF} \AgdaBound{v} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>[4]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{lemmaConsAppend} \AgdaBound{n} \AgdaBound{m} \AgdaBound{σ} \AgdaBound{s}\<%
\\
\>[6]\AgdaIndent{7}{}\<[7]%
\>[7]\AgdaFunction{	extasciitilde} \AgdaFunction{cong} \AgdaSymbol{(λ} \AgdaBound{l} \AgdaSymbol{→} \AgdaBound{σ} \AgdaInductiveConstructor{∷} \AgdaBound{l} \AgdaFunction{++} \AgdaBound{s}\AgdaSymbol{)} \AgdaSymbol{(}\AgdaFunction{lemmaPlusAppend} \AgdaBound{n} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaBound{m}\AgdaSymbol{)} \AgdaBound{σ}\AgdaSymbol{))}\<%
\\
\>[0]\AgdaIndent{6}{}\<[6]%
\>[6]\AgdaSymbol{(}\AgdaFunction{compileG'} \AgdaBound{e₁} \AgdaFunction{⟫G} \AgdaFunction{compileG'} \AgdaBound{e₂}\AgdaSymbol{)}\<%
\\
\>\<\end{code}

%<*compileG>
\begin{code}\>\<%
\\
\>\AgdaFunction{compileG} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{s} \AgdaSymbol{:} \AgdaFunction{StackType}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{z} \AgdaBound{t}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{Src} \AgdaBound{t} \AgdaBound{z}\<%
\\
\>[0]\AgdaIndent{11}{}\<[11]%
\>[11]\AgdaSymbol{→} \AgdaDatatype{HGraph} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaSymbol{(}\AgdaFunction{replicate} \AgdaBound{z} \AgdaBound{t} \AgdaFunction{++} \AgdaBound{s}\AgdaSymbol{)}\<%
\\
\>\<\end{code}
%</compileG>

\begin{code}\>\<%
\\
\>\AgdaFunction{compileG} \AgdaBound{src} \AgdaSymbol{=} \AgdaInductiveConstructor{mkHGraph} \AgdaSymbol{(}\AgdaFunction{compileG'} \AgdaBound{src}\AgdaSymbol{)}\<%
\\
\>\<\end{code}

%<*execT>
\begin{code}\>\<%
\\
\>\AgdaFunction{execT} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s} \AgdaBound{s'}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{HTree} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaBound{s'}\<%
\\
\>[0]\AgdaIndent{8}{}\<[8]%
\>[8]\AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s'}\<%
\\
\>\<\end{code}
%</execT>

\begin{code}\>\<%
\\
\>\AgdaFunction{execT} \AgdaSymbol{=} \AgdaPostulate{foldTree} \AgdaFunction{execAlg}\<%
\\
\>\<\end{code}

%<*execG>
\begin{code}\>\<%
\\
\>\AgdaFunction{execG} \AgdaSymbol{:} \AgdaSymbol{∀} \AgdaSymbol{\{}\AgdaBound{s} \AgdaBound{s'}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaDatatype{HGraph} \AgdaDatatype{BytecodeF} \AgdaBound{s} \AgdaBound{s'}\<%
\\
\>[0]\AgdaIndent{8}{}\<[8]%
\>[8]\AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s} \AgdaSymbol{→} \AgdaDatatype{Stack} \AgdaBound{s'}\<%
\\
\>\<\end{code}
%</execG>

\begin{code}\>\<%
\\
\>\AgdaFunction{execG} \AgdaSymbol{=} \AgdaPostulate{foldGraph} \AgdaFunction{execAlg}\<%
\\
\>\<\end{code}
