%format ph = "\rho{}"
%format (sub (x) (y)) = "{" x "}_{" y "}"
%format (sup (x) (y)) = "{" x "}^{" y "}"
%format (ann (x) (y) (z)) = "{" x "}_{" y "}^{" z "}"
%format pc = "\phi{}"
%format pc1
%format ~< = "\preceq{}"
%format >~ = "\succeq{}"
%format tau = "\tau{}"
%format (many (m)) = "\overline{" m "}"
%format (over (a) (s)) = "\overset{" a "}{" s "}"
%format q1
%format Phi = "\Phi"
%format Upsilon = "\Upsilon"
%format <+> = "\cup"
%format ~> = "\leadsto"
%format :-> = "\mapsto"
%format :- = "\vdash"
%format . = "."
%format \/ = "\cup"
%format \+/ = "\uplus"
%format emptyset = "\emptyset{}"
%format (semb(x)(y)) = "\llbracket{}{" x "}\rrbracket{}_{" y "}"
%format `bar` = "|"
%format `pre` = "\prec"
%format `notpre` = "\not\prec"
%format Gamma = "\Gamma{}"
%format `compose` = "\circ"
%format initial = "\mathsf{initial}"
%format ^ = " "
%format ^^ = "\;"
%format ^^^ = "\hspace{1em}"
%format Heap = H
%format unit = "\imath{}"
%format ---> = "\longrightarrow{}"
%format Ktx = "\mathcal{K}"
%format vinkje = "\!\!\!{\surd{}}"
%format `subseteq` = "\subseteq"
%format `notsubseteq` = "\not\subseteq"
%format `notelem` = "\not\in"
%format atom = "\nu{}"
%format (opt (x)) = "{" x "}^{\mbox{?}}"
%format `comm` = "\diamond{}"
%format ell = "\ell{}"
%format Psi = "\Psi{}"
%format Sigma = "\Sigma{}"
%format delta = "\delta{}"
%format eta = "\eta{}"
%format dopen = "\circ{}"
%format dclosed = "\bullet{}"
%format `sep` = "\,;\,"
%format `dmap` = "\mapsto_\delta{}"
%format `omap` = "\mapsto_\circ{}"
%format `cmap` = "\mapsto_\bullet{}"
%format (plook (p) (k)) = p "(" k ")"
%format (hlook (h) (k)) = h "(" k ")"
%format (ready (l) (r)) = l " \;\surd\; " r
%format (readydep (l) (r)) = l " \;\surd_{\mbox{\scriptsize dep}}\; " r
%format (load (l) (o) (v)) = l " \vdash " o " \uparrow " v
%format (store (h) (v) (o) (r)) = h "\vdash" v " \downarrow " o " \leadsto " r
%format (listsize (x)) = "{\mid" x "\mid}"
%format phaseOf = "\Varid{phase}"
%format `div` = "\backslash"
%format `greater` = ">"
%format trdwn = "\triangleleft"
%format trup = "\triangleright"
%format trnew = "\times"
%format trval = "\bullet"
%format trref = "\circ"
%format zdown = z "^\triangleleft"
%format zup   = z "^\triangleright"
%format (occval (d)) = d "^" trval
%format (prevctx (c)) = c "^{-1}"
%format wr1 = "\mathsf{wr}"
%format rd1 = "\mathsf{rd}"
%format ref1 = "\mathsf{ref}"
%format -< = "\prec{}"
% %format @ = "\mathop{\mathsmaller{@}}\!\!"
% %format @@ = "\mathsmaller{@}\!"
%format atsymbol = "@"
%format $= = "\mathbin{\$\!\!\!=}"
%format ~ = "\mathrel{\sim}"
%format :=: = "\mathrel{:=:}"

%format return = "\mathbf{return}"
%format expl = "\mathbf{expl}"
%format inh = "\mathbf{inh}"
%format syn = "\mathbf{syn}"
%format chn = "\mathbf{chn}"
%format thr = "\mathbf{thr}"
%format ioc = "\mathbf{ioc}"
%format loc = "\mathbf{loc}"
%format lhs = "\mathbf{lhs}"
%format inst = "\mathbf{inst}"
%format use = "\mathbf{use}"
%format phase = "\mathbf{phase}"
%format sem = "\mathbf{sem}"
%format child = "\mathbf{child}"
%format order = "\mathbf{order}"
%format attr = "\mathbf{attr}"
%format rule = "\mathbf{rule}"
%format begin = "\mathbf{begin}"
%format end = "\mathbf{end}"
%format con = "\mathbf{con}"
%format prod = "\mathbf{prod}"
%format conf = "\mathbf{conf}"
%format sim = "\mathbf{sim}"
%format invoke = "\mathbf{invoke}"
%format ainvoke = "\Varid{invoke}"
%format attach = "\mathbf{attach}"
%format detach = "\mathbf{detach}"
%format visit = "\mathbf{visit}"
%format ainh = "\Varid{inh}"
%format asyn = "\Varid{syn}"
%format athr = "\Varid{thr}"
%format abar = "\Varid{bar}"
%format barrier = "\mathbf{barrier}"
%format achild = "\Varid{child}"
%format abegin = "\Varid{begin}"
%format aend = "\Varid{end}"
%format ctx = "\mathcal{C}"
%format <-+ = <- "^+"
%format +-> = -> "^+"
%format <-* = <- "^\ast"
%format *-> = -> "^\ast"
%format dead = "\mathbf{dead}"
%format epsilon = "\epsilon"
%format <% = "\mathbin{\langle}"
%format %> = "\mathbin{\rangle}"
%format `elem1` = "\in_1"
%format exists = "\exists"
%format forall = "\forall"

%format alpha = "\alpha{}"
%format beta = "\beta{}"
%format ctx1
%format ctx2
%format ctx3
%format ctx4
%format v4
%format v5
%format v6
%format v7
%format v8
%format v9
%format d1
%format d2
%format o1
%format o2
%format o3
%format o4
%format y0
%format y1
%format y2
%format y3
%format z0
%format z1
%format z2
%format z3
%format z4
%format z5
%format s0
%format s1
%format s2
%format s3
%format c0
%format c1
%format c2
%format c3
%format c4
%format c5
%format c6
%format c7
%format ck = c "_k"
%format Heap0
%format Heap1
%format Heap2
%format Heap3
%format H0
%format H1
%format H2
%format H3
%format Gamma0
%format Gamma1
%format Gamma2
%format r0
%format f1
%format f2
%format f3
%format f4
%format f5
%format r1
%format r2
%format r3
%format r4
%format r5
%format r6
%format r7
%format r8
%format r9
%format l1
%format l2
%format l3
%format v0
%format v1
%format v2
%format v3
%format g0
%format g1
%format g2
%format g3
%format g4
%format ph0
%format ph1
%format ph2
%format ph3
%format ph4
%format ph'
%format p1
%format p2
%format p3
%format p4
%format p5
%format p6
%format x0
%format x1
%format x2
%format x3
%format x4
%format x5
%format k0
%format k1
%format k2
%format k3
%format s0
%format s1
%format s2
%format s3
%format s4
%format s5
%format a0
%format a1
%format a2
%format p0
%format p1
%format p2
%format m0
%format m1
%format m2
%format m3
%format m4
%format Psi'
%format Psi0
%format Psi1
%format Psi2
%format Psi3
%format ell0
%format ell1
%format ell2
%format ell3
%format Sigma0
%format Sigma1
%format Sigma2
%format Sigma3
%format sigma = "\sigma"
%format sigma0
%format sigma1
%format sigma2
%format phi = "\phi"
%format phi0
%format phi1
%format phi2
%format delta0
%format delta1
%format delta2
%format delta3
%format eta0
%format eta1
%format eta2
%format eta3
%format all2
%format all3
%format ainh1
%format asyn1

%format oper1
%format oper2

% Make our identifiers with underscores a bit nicer
%format _ = "\!{\scriptscriptstyle\_}"
%format top_lmin = top _ lmin
%format top_gmin = top _ gmin
%format top_repl = top _ repl
%format lhs_repl = "\Varid{lhs}" _ repl
%format lhs_lmin = "\Varid{lhs}" _ lmin
%format lhs_gmin = "\Varid{lhs}" _ gmin
%format l_lmin = l _ lmin
%format r_lmin = r _ lmin
%format l_repl = l _ repl
%format r_repl = r _ repl