\[ \definecolor{leff}{RGB}{255,107,102} \definecolor{lcoeff}{RGB}{78,206,88} \definecolor{ltyp}{RGB}{255,202,79} \definecolor{lkvd}{RGB}{127,165,255} \definecolor{eff}{RGB}{177,35,43} \definecolor{coeff}{RGB}{35,177,53} \definecolor{typ}{RGB}{177,93,43} \definecolor{expr}{RGB}{0,0,0} \definecolor{kvd}{RGB}{0,45,177} \definecolor{num}{RGB}{43,177,93} \newcommand{\highlightType}[1]{{\color{typ} #1}} \newcommand{\highlight}[1]{\bbox[yellow]{#1}} \newcommand{\Int}{\mathsf{Int}} \newcommand{\Boolean}{\mathsf{Bool}} \newcommand{\Bool}{\mathsf{Bool}} \newcommand{\Unit}{\mathsf{Unit}} \newcommand{\Ref}[1]{\mathsf{Ref}~#1} \newcommand{\Refl}[2]{\mathsf{Ref}_{#1}~#2} \newcommand{\true}{\mathsf{true}} \newcommand{\false}{\mathsf{false}} \newcommand{\reff}{{\mathsf{ref}~}} \newcommand{\prot}[6]{{\mathsf{prot}^{{#5,#2,#3}}_{#6,#1} #4}} \newcommand{\ite}[3]{\mathsf{if} ~#1~ \mathsf{then} ~#2 ~\mathsf{else}~ #3} \newcommand{\TermT}[1]{{\color{kvd} \oblset{Term}_{#1}}} \newcommand{\oblset}[1]{\textsf{#1}} \newcommand{\ljoin}{\style{display: inline-block; margin-top:3px; transform:rotate(-0.25turn);}{\prec}} \newcommand{\lmeet}{\style{display: inline-block; transform:rotate(0.25turn);}{\prec}} \newcommand{\cjoin}{\widetilde{\ljoin}} \newcommand{\cmeet}{\widetilde{\lmeet}} \newcommand{\gsum}{\oplus} \newcommand{\evidence}[1]{\style{font-size:80%;opacity: 0.8}{\color{lcoeff} #1}~} \newcommand{\sub}{<:} \newcommand{\csub}{\widetilde{\sub}} \newcommand{\subl}{\preccurlyeq} \newcommand{\csubl}{\widetilde{\subl}} \newcommand{\vunit}{\mathsf{unit}} \]