\NeedsTeXFormat{LaTeX2e}%
\ProvidesPackage{vlralph}
\RequirePackage{virginialake}%

%~~~~~~Inference rule labels%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

%----Generic
\newcommand\rhoD {{\rho\!\!\downarrow}}%
\newcommand\rhoU {{\rho\!\!\uparrow}}%
\newcommand\arhoD {{\mathsf{a}\rho\!\downarrow}}%
\newcommand\arhoU {{\mathsf{a}\rho\!\uparrow}}%

%---- SKS
\newcommand\ai {{\mathsf{ai}}}%
\newcommand\aiD {{\mathsf{ai}}{\downarrow}}%
\newcommand\aiU {{\mathsf{ai}}{\uparrow}}%
\newcommand\ac {{\mathsf{ac}}}%
\newcommand\acD {{\mathsf{ac}}{\downarrow}}%
\newcommand\acU {{\mathsf{ac}}{\uparrow}}%
\newcommand\aw {{\mathsf{aw}}}%
\newcommand\awD {{\mathsf{aw}}{\downarrow}}%
\newcommand\awU {{\mathsf{aw}}{\uparrow}}%
\newcommand\swD {{\mathsf{s}}{\downarrow}}%
\newcommand\swU {{\mathsf{s}}{\uparrow}}%

%----SAKS
\newcommand\vlanass{{\vlan}{\mathsf{asso}}}%
\newcommand\vlorass{{\vlor}{\mathsf{asso}}}%
\newcommand\vlancom{{\vlan}{\mathsf{com}}}%
\newcommand\vlorcom{{\vlor}{\mathsf{com}}}%
\newcommand\vlorcD{{\vlor}{\mathsf{c}}{\downarrow}}%
\newcommand\vlancU{{\vlan}{\mathsf{c}}{\uparrow}}%

%----Merge contractions
\newcommand\gcU{{\mathsf{c}}{\uparrow}}%
\newcommand\gcD{{\mathsf{c}}{\downarrow}}%
\newcommand\hcU{{\mathsf{hc}}{\uparrow}}%
\newcommand\hcD{{\mathsf{hc}}{\downarrow}}%
\newcommand\mcU{{\mathsf{mc}}{\uparrow}}%
\newcommand\mcD{{\mathsf{mc}}{\downarrow}}%


%---- SKSae
\newcommand\aeD {{\text{\ae}\downarrow}}%
\newcommand\aeU {{\text{\ae}\uparrow}}%

%---- SKSq
\newcommand\qiD {{\mathsf{qi}}{\downarrow}}%
\newcommand\qiU {{\mathsf{qi}}{\uparrow}}%
\newcommand\qcD {{\mathsf{qc}}{\downarrow}}%
\newcommand\qcU {{\mathsf{qc}}{\uparrow}}%
\newcommand\qcmD {{\mathsf{qc_m}}{\downarrow}}%
\newcommand\qcmU {{\mathsf{qc_m}}{\uparrow}}%
\newcommand\roD {{\mathsf{r1}}{\downarrow}}%
\newcommand\roU {{\mathsf{r1}}{\uparrow}}%
\newcommand\rtD {{\mathsf{r2}}{\downarrow}}%
\newcommand\rtU {{\mathsf{r2}}{\uparrow}}%
\newcommand\rthD {{\mathsf{r3}}{\downarrow}}%
\newcommand\rthU {{\mathsf{r3}}{\uparrow}}%
\newcommand\rfD {{\mathsf{r4}}{\downarrow}}%
\newcommand\rfU {{\mathsf{r4}}{\uparrow}}%
\newcommand\nD {{\mathsf{n}}{\downarrow}}%
\newcommand\nU {{\mathsf{n}}{\uparrow}}%
\newcommand\rD {{\mathsf{r}}{\downarrow}}%
\newcommand\rU {{\mathsf{r}}{\uparrow}}%

%---- SKSr
\newcommand\moD {{\mathsf{m_1}}{\downarrow}}%
\newcommand\moU {{\mathsf{m_1}}{\uparrow}}%
\newcommand\mtD {{\mathsf{m_2}}{\downarrow}}%
\newcommand\mtU {{\mathsf{m_2}}{\uparrow}}%
\newcommand\grD {{\mathsf{gr}}{\downarrow}}%
\newcommand\grU {{\mathsf{gr}}{\uparrow}}%
\newcommand\uD {{\mathsf{u}}{\downarrow}}%
\newcommand\uU {{\mathsf{u}}{\uparrow}}%

%---SKSh
\newcommand\hD {{\mathsf{h}}{\downarrow}}%
\newcommand\hU {{\mathsf{h}}{\uparrow}}%

%---SKSex
\newcommand\nexD {{\mathsf{n_ex}}{\downarrow}}%
\newcommand\nexU {{\mathsf{n_ex}}{\uparrow}}%
\newcommand\exD {{\mathsf{ex}}{\downarrow}}%
\newcommand\exU {{\mathsf{ex}}{\uparrow}}%
\newcommand\snD {{\mathsf{sn}}{\downarrow}}%
\newcommand\snU {{\mathsf{sn}}{\uparrow}}%

%--- Misc
\newcommand\inU {{\forall\exists\uparrow}}%
\newcommand\geD {{\forall\exists\downarrow}}%
\newcommand\siD {{\mathsf{si}}{\downarrow}}%
\newcommand\siU {{\mathsf{si}}{\uparrow}}%
\newcommand\saiD {{\mathsf{sai}}{\downarrow}}%
\newcommand\saiU {{\mathsf{sai}}{\uparrow}}%
\newcommand\sqiD {{\mathsf{sqi}}{\downarrow}}%
\newcommand\sqiU {{\mathsf{sqi}}{\uparrow}}%
\newcommand\vqE {{\mathsf{vq}}{=}}%
\newcommand\vqeD {{\mathsf{vq\exists}}{\downarrow}}%
\newcommand\vqaD {{\mathsf{vq\forall}}{\downarrow}}%
\newcommand\vqeU {{\mathsf{vq\exists}}{\uparrow}}%
\newcommand\vqaU {{\mathsf{vq\forall}}{\uparrow}}%



%~~~Proof System Names~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

\newcommand\KSae {{\mathsf{KS\ae}}}%
\newcommand\SKSae {{\mathsf{SKS\ae}}}%
\newcommand\KSr {{\mathsf{KSr}}}%
\newcommand\SKSr {{\mathsf{SKSr}}}%
\newcommand\KSgr {{\mathsf{KSgr}}}%
\newcommand\SKSgr {{\mathsf{SKSgr}}}%
\newcommand\KSg {{\mathsf{KSg}}}%
\newcommand\SKSg {{\mathsf{SKSg}}}%
\newcommand\KSq {{\mathsf{KSq}}}%
\newcommand\SKSq {{\mathsf{SKSq}}}%
\newcommand\KSgq {{\mathsf{KSgq}}}%
\newcommand\SKSgq {{\mathsf{SKSgq}}}%
\newcommand\KSqc {{\mathsf{KSqc}}}%
\newcommand\SKSqc {{\mathsf{SKSqc}}}%
\newcommand\KSh {{\mathsf{KSh}}}%
\newcommand\SKSh {{\mathsf{SKSh}}}%
\newcommand\KSho {{\mathsf{KSh1}}}%
\newcommand\SKSho {{\mathsf{SKSh1}}}%
\newcommand\KSht {{\mathsf{KSh2}}}%
\newcommand\SKSht {{\mathsf{SKSh2}}}%
\newcommand\KShx {{\mathsf{KShx}}}%
\newcommand\SKShx {{\mathsf{SKShx}}}%
\newcommand\FKSq {{\mathsf{FKSq}}}%
\newcommand\FKSgq {{\mathsf{FKSgq}}}%
\newcommand\SKSex {{\mathsf{SKSex}}}%
\newcommand\SKSqx {{\mathsf{SKSqx}}}%
\newcommand\KSqx {{\mathsf{KSqx}}}%
\newcommand\SKSx {{\mathsf{SKSx}}}%
\newcommand\SAKS {{\mathsf{SAKS}}}%
\newcommand\AKS {{\mathsf{AKS}}}%
\newcommand\KSm {{\mathsf{KSm}}}%
\newcommand\SKSm {{\mathsf{SKSm}}}%

\newcommand\CD {{\mathsf{C_{\downarrow}}}}%

%~~~Other~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

%~~~~~Expansion Trees

\newcommand\Sh {{\mathit{Sh}}}%
\newcommand\Dp {{\mathit{Dp}}}%
\newcommand\Lab {{\mathit{Lab}}}%
\newcommand\Up {{\mathit{Up}}}%
\newcommand\Lo {{\mathit{Lo}}}%
\newcommand\EV {{\mathit{EV}}}%


%~~~~Rewriting Systems

\newcommand\reC{\mathrm{C}}
\newcommand\reH{\mathrm{H}}
\newcommand\reQ{\mathrm{Q}}
\newcommand\reW{\mathrm{W}}
\newcommand\reY{\mathrm{Y}}
\newcommand\Seq{\mathsf{Seq}}

%--- Binary relations

\newcommand\eq   {\mathrel=}
\renewcommand\neq  {\not\eq}
\newcommand\nideq{\not\ideq}

\newcommand\rels { \mathrel\alpha}
\newcommand\relt {\mathrel\beta}
\newcommand\relf {\mathrel\gamma}
\newcommand\relff {\mathrel\delta}
\newcommand\relsi {\mathrel\epsilon}
\newcommand\relse {\mathrel\zeta}
\newcommand\relei {\mathrel\theta}

\newcommand\relalp { \mathrel\alpha}
\newcommand\relbet {\mathrel\beta}
\newcommand\relgam {\mathrel\gamma}
\newcommand\reldel {\mathrel\delta}
\newcommand\releps {\mathrel\epsilon}
\newcommand\relzet {\mathrel\zeta}
\newcommand\relthe {\mathrel\theta}


%~~~~Miscellanea 

\newcommand\pr   {\mathop{\mathsf{pr}}}
\newcommand\cn   {\mathop{\mathsf{cn}}}
\newcommand\sects   {\mathop{\mathsf{sec}}}
\newcommand\ideq {\mathrel\equiv}
\newcommand\gap {\{\hspace{5px}\}}
\newcommand\Mv {M_{\vlor}}
\newcommand\Mvp {M_{\vlor}^{P}}
\newcommand\Mn {M_{\vlan}}
\newcommand\Mnp {M_{\vlan}^{P}}

%~~~~~Greek Characters~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

\DeclareMathVersion{mathchartertext}
\SetSymbolFont{letters}{mathchartertext}{OML}{mdbch}{m}{n}
\newcommand{\gchar}[1]{\mathversion{mathchartertext}$#1$\mathversion{normal}}
% The \gchar{\char} can be used in text to type
% Charter non-italic Greek characters.
% Usage example: \gchar{\phi}

%~~~~~Colours~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
\definecolor{darkgreen}{rgb}{0.0,0.4,0.0} 
\endinput