%%%%%%%%%
%Preamble sufficient for basic derivations in LaTeX
%%%%%%%%

%font setup
\renewcommand{\baselinestretch}{1.1}
\usepackage[mathscr]{euscript}
\usepackage{amssymb} \renewcommand{\mathcal}{\mathbf} \newcommand{\mathbold}{\mathbf} \newcommand{\altS}{S}

\newcommand{\mc}{\mathscr}
\newcommand{\ms}{\mathsf}
\newcommand{\mr}{\mathrm}
\newcommand{\mi}{\mathit}
\newcommand{\mf}{\mathfrak}
\newcommand{\mbb}[1]{\mathbb #1\!}
\newcommand{\mdb}[1]{\mi{\mbb #1}}
\newcommand{\prp}[1]{{\ms{\scriptstyle #1}}}
\newcommand{\ol}{\overline}
\newcommand{\os}{\overline\mathsf}


%turnstiles

\newcommand{\plust}{\mathbin{\hspace{.25em}\rotatebox[origin=c]{0}{\rule[-.04ex]{.5pt}{.6ex}}\hspace{-.16em}\rotatebox[origin=c]{90}{\rule[-.03ex]{.5pt}{.6ex}}    }}
\newcommand{\singleAD}[1][{{}}]{\vdash^#1_{\scriptscriptstyle \! \! \! A \! D}}
\newcommand{\singleADs}[1][{{}}]{\vdash^#1_{\scriptscriptstyle \! \! \! A \! D\! s}}
\newcommand{\singleADq}[1][{{}}]{\vdash^#1_{\scriptscriptstyle \! \! \! A \! D\! q}}
\newcommand{\singleND}[1][{{}}]{\vdash^#1_{\scriptscriptstyle \! \! \! N \!\! D}}
\newcommand{\singleNDs}[1][{{}}]{\vdash^#1_{\scriptscriptstyle \! \! \! N \!\! D \!s}}
\newcommand{\singleNDsp}[1][{{}}]{\vdash^#1_{\scriptscriptstyle \!\!\!{\mi{NDs}\!\plust}}}
\newcommand{\singleNDp}[1][{{}}]{\vdash^#1_{\scriptscriptstyle \! \! \! N \!\! D\!\!\plust}}
\newcommand{\doubleS}[1][{{}}]{\vDash^#1_{\scriptscriptstyle \! \! \! s}}
\usepackage{rotating}

%special characters
\newcommand{\pr}{^\prime}
\def\imp{\to}
\def\bimp{\leftrightarrow}
\newcommand{\til}{\mathord{\sim}}
\newcommand{\wdg}{\vee}
\newcommand{\crt}{\wedge}
\newcommand{\sstroke}{\mathbin{\uparrow}}
\newcommand{\zeros}{\emptyset}
\newcommand{\bottom}{\perp}
\newcommand{\Bottom}{\mbox{$\hspace{.05em}\rule{.668em}{.4pt}\hspace{-.668em}\rule[.28ex]{.668em}{.4pt}$}\hspace{-.355em}\rotatebox[origin=c]{90}{\rule[1.7ex]{.53em}{.5pt}} \hspace{-.4em} }

%\newcommand{\Bottom}{\mbox{$\bottom\hspace{-1.003em}\rule[-.28ex]{.668em}{.5pt}$}}
\newcommand{\smtriangleup}{{\scriptstyle \vartriangle}}
\newcommand{\smtriangledn}{{\scriptstyle \triangledown}}
\newcommand{\mcrt}{\mathbin{\smtriangleup}}
\newcommand{\mwdg}{\mathbin{\smtriangledn}}
\newcommand{\mimp}{\Rightarrow}
\newcommand{\mbimp}{\Leftrightarrow}


%for mathematical induction
\newenvironment{ind}{\begin{list}{}
{\setlength{\itemsep}{0ex}
 \setlength{\labelwidth}{2.5em}
  \setlength{\leftmargin}{2.8em}
  \setlength{\labelsep}{0.3em}}}{\end{list}} 
  
\newcommand{\Basis}{\item[\emph{Basis}:]}
\newcommand{\Assp}{\item[\emph{Assp}:]}
\newcommand{\Show}{\item[\emph{Show}:]}
\newcommand{\Indct}{\item[\emph{Indct}:]} 
\newcommand{\argline}{\vspace{-1.5ex} \item[\rule{1.2cm}{.5pt}] \rule{0cm}{1pt} \vspace{-.5ex}}
\newcommand{\Argline}{\vspace{-2ex} \item \rule{1.5cm}{.5pt} \rule{0cm}{1pt} \vspace{-1ex}}



%for derivations
\newlength{\xmpind}
\newlength{\xmpindb}
\newsavebox{\derboxa}
\newsavebox{\derboxb}

\newlength{\dergap}
\setlength{\dergap}{-2.5mm}
\newlength{\derstrut}
\setlength{\derstrut}{2ex}
\newlength{\derthin}
\setlength{\derthin}{-2mm}
\newlength{\dertthin}
\setlength{\dertthin}{-3mm}

\newcounter{dercount}
\newcounter{dernumber}
\newcommand{\li}[1]{\expandafter\ref*{#1:\arabic{dernumber}}}

\newenvironment{der}[2]
{\begin{footnotesize} \renewcommand{\arraystretch}{1.1}\stepcounter{dernumber} \setcounter{dercount}{0} \setlength{\tabcolsep}{.35em}   \begin{tabular}[#1]{#2} }
{\end{tabular} \end{footnotesize} }

\newenvironment{tder}[2]
{\begin{tiny} \renewcommand{\arraystretch}{1.1} \stepcounter{dernumber}\setcounter{dercount}{0} \setlength{\tabcolsep}{.35em}   \begin{tabular}[#1]{#2} }
{\end{tabular} \end{tiny} }


\newenvironment{sder}[2]
{\begin{scriptsize} \renewcommand{\arraystretch}{1.1} \stepcounter{dernumber}\setcounter{dercount}{0} \setlength{\tabcolsep}{.35em}   \begin{tabular}[#1]{#2} }
{\end{tabular} \end{scriptsize} }

\newcommand{\dsep}{{\rule[0mm]{0mm}{\derstrut}}}

\newcommand{\cttOne}{& \multicolumn{11}{l}{} \vspace{\dertthin} \\}
\newcommand{\clOne}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & \multicolumn{21}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clTwo}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & \multicolumn{20}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clThree}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & \multicolumn{19}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clFour}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & \multicolumn{18}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clFive}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & \multicolumn{17}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clSix}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & \multicolumn{16}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clSeven}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & \multicolumn{15}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clEight}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & \multicolumn{14}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clNine}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & \multicolumn{13}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clTen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & \multicolumn{12}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clEleven}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & \multicolumn{11}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clTwelve}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & \multicolumn{10}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clThirteen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & \multicolumn{9}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clFourteen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & &\multicolumn{8}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clFifteen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & & &\multicolumn{7}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clSixteen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & & & &\multicolumn{6}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clSeventeen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & & & & &\multicolumn{5}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clEighteen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & & & & & &\multicolumn{4}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clNineteen}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & & & & & & &\multicolumn{3}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\clTwenty}[4][.]{\refstepcounter{dercount} \expandafter\label{#2:\arabic{dernumber}} \arabic{dercount}#1 & & & & & & & & & & & & & & & & & & & &\multicolumn{2}{l}{$#3$} & \hspace{1em} #4 \\}

\newcommand{\caOne}[1]{\cline{2-2} & #1 \multicolumn{20}{l}{} \vspace{\dergap} \\}
\newcommand{\caTwo}[1]{\cline{3-3} & & #1 \multicolumn{19}{l}{} \vspace{\dergap} \\}
\newcommand{\caThree}[1]{\cline{4-4} & & & #1 \multicolumn{18}{l}{} \vspace{\dergap} \\}
\newcommand{\caFour}[1]{\cline{5-5} & & & & #1 \multicolumn{17}{l}{} \vspace{\dergap} \\}
\newcommand{\caFive}[1]{\cline{6-6} & & & & & #1 \multicolumn{16}{l}{} \vspace{\dergap} \\}
\newcommand{\caSix}[1]{\cline{7-7} & & & & & & #1 \multicolumn{15}{l}{} \vspace{\dergap} \\}
\newcommand{\caSeven}[1]{\cline{8-8} & & & & & & & #1 \multicolumn{14}{l}{} \vspace{\dergap} \\}
\newcommand{\caEight}[1]{\cline{9-9} & & & & & & & &  #1 \multicolumn{13}{l}{} \vspace{\dergap} \\}
\newcommand{\caNine}[1]{\cline{10-10} & & & & & & & & & #1 \multicolumn{12}{l}{} \vspace{\dergap} \\}
\newcommand{\caTen}[1]{\cline{11-11} & & & & & & & & & & #1 \multicolumn{11}{l}{} \vspace{\dergap} \\}
\newcommand{\caEleven}[1]{\cline{12-12} & & & & & & & & & & & #1 \multicolumn{10}{l}{} \vspace{\dergap} \\}
\newcommand{\caTwelve}[1]{\cline{13-13} & & & & & & & & & & & & #1 \multicolumn{9}{l}{}\vspace{\dergap} \\}
\newcommand{\caThirteen}[1]{\cline{14-14} & & & & & & & & & & & & & #1 \multicolumn{8}{l}{}\vspace{\dergap} \\}
\newcommand{\caFourteen}[1]{\cline{15-15} & & & & & & & & & & & & & & #1 \multicolumn{7}{l}{}\vspace{\dergap} \\}
\newcommand{\caFifteen}[1]{\cline{16-16} & & & & & & & & & & & & & & & #1 \multicolumn{6}{l}{}\vspace{\dergap} \\}
\newcommand{\caSixteen}[1]{\cline{17-17} & & & & & & & & & & & & & & & & #1 \multicolumn{5}{l}{}\vspace{\dergap} \\}
\newcommand{\caSeventeen}[1]{\cline{18-18} & & & & & & & & & & & & & & & & & #1 \multicolumn{4}{l}{}\vspace{\dergap} \\}
\newcommand{\caEighteen}[1]{\cline{19-19} & & & & & & & & & & & & & & & & & & #1 \multicolumn{3}{l}{}\vspace{\dergap} \\}
\newcommand{\caNineteen}[1]{\cline{20-20} & & & & & & & & & & & & & & & & & & & #1 \multicolumn{2}{l}{}\vspace{\dergap} \\}
\newcommand{\caTwenty}[1]{\cline{21-21} & & & & & & & & & & & & & & & & & & & & #1 \multicolumn{1}{l}{}\vspace{\dergap} \\}

\newcommand{\ctOne}{& \multicolumn{20}{l}{} \vspace{\derthin} \\}
\newcommand{\ctTwo}{& & \multicolumn{19}{l}{} \vspace{\derthin} \\}
\newcommand{\ctThree}{& & & \multicolumn{18}{l}{} \vspace{\derthin} \\}
\newcommand{\ctFour}{& & & & \multicolumn{17}{l}{} \vspace{\derthin} \\}
\newcommand{\ctFive}{& & & & & \multicolumn{16}{l}{} \vspace{\derthin} \\}
\newcommand{\ctSix}{& & & & & & \multicolumn{15}{l}{} \vspace{\derthin} \\}
\newcommand{\ctSeven}{& & & & & & & \multicolumn{14}{l}{} \vspace{\derthin} \\}
\newcommand{\ctEight}{& & & & & & & & \multicolumn{13}{l}{} \vspace{\derthin} \\}
\newcommand{\ctNine}{& & & & & & & & & \multicolumn{12}{l}{} \vspace{\derthin} \\}
\newcommand{\ctTen}{& & & & & & & & & & \multicolumn{11}{l}{} \vspace{\derthin} \\}
\newcommand{\ctEleven}{& & & & & & & & & & & \multicolumn{10}{l}{} \vspace{\derthin} \\}
\newcommand{\ctTwelve}{& & & & & & & & & & & & \multicolumn{9}{l}{} \vspace{\derthin} \\}
\newcommand{\ctThirteen}{& & & & & & & & & & & & & \multicolumn{8}{l}{}\vspace{\derthin} \\}
\newcommand{\ctFourteen}{& & & & & & & & & & & & & & \multicolumn{7}{l}{}\vspace{\derthin} \\}
\newcommand{\ctFifteen}{& & & & & & & & & & & & & & &\multicolumn{6}{l}{}\vspace{\derthin} \\}
\newcommand{\ctSixteen}{& & & & & & & & & & & & & & & &\multicolumn{5}{l}{}\vspace{\derthin} \\}
\newcommand{\ctSeventeen}{& & & & & & & & & & & & & & & & &\multicolumn{4}{l}{}\vspace{\derthin} \\}
\newcommand{\ctEighteen}{& & & & & & & & & & & & & & & & & &\multicolumn{3}{l}{}\vspace{\derthin} \\}
\newcommand{\ctNineteen}{& & & & & & & & & & & & & & & & & & &\multicolumn{2}{l}{}\vspace{\derthin} \\}

\newcommand{\nclOne}[4][.]{#2#1 & \multicolumn{21}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclTwo}[4][.]{#2#1 & & \multicolumn{20}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclThree}[4][.]{#2#1 & & & \multicolumn{19}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclFour}[4][.]{#2#1 & & & & \multicolumn{18}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclFive}[4][.]{#2#1 & & & & & \multicolumn{17}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclSix}[4][.]{#2#1 & & & & & & \multicolumn{16}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclSeven}[4][.]{#2#1 & & & & & & & \multicolumn{15}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclEight}[4][.]{#2#1 & & & & & & & & \multicolumn{14}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclNine}[4][.]{#2#1 & & & & & & & & & \multicolumn{13}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclTen}[4][.]{#2#1 & & & & & & & & & & \multicolumn{12}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclEleven}[4][.]{#2#1 & & & & & & & & & & & \multicolumn{11}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclTwelve}[4][.]{#2#1 & & & & & & & & & & & & \multicolumn{10}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclThirteen}[4][.]{#2#1 & & & & & & & & & & & & &\multicolumn{9}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclFourteen}[4][.]{#2#1 & & & & & & & & & & & & & &\multicolumn{8}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclFifteen}[4][.]{#2#1 & & & & & & & & & & & & & & & \multicolumn{7}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclSixteen}[4][.]{#2#1 & & & & & & & & & & & & & & & & \multicolumn{6}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclSeventeen}[4][.]{#2#1 & & & & & & & & & & & & & & & & & \multicolumn{5}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclEighteen}[4][.]{#2#1 & & & & & & & & & & & & & & & & & & \multicolumn{4}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclNineteen}[4][.]{#2#1 & & & & & & & & & & & & & & & & & & &\multicolumn{3}{l}{$#3$} & \hspace{1em} #4 \\}
\newcommand{\nclTwenty}[4][.]{#2#1 & & & & & & & & & & & & & & & & & & & &\multicolumn{2}{l}{$#3$} & \hspace{1em} #4 \\}


% for godel corner quotes (Sam Buss)
\newbox\gnBoxA
 \newdimen\gnCornerHgt
 \setbox\gnBoxA=\hbox{$\ulcorner$}
 \global\gnCornerHgt=\ht\gnBoxA
 \newdimen\gnArgHgt
 \def\Godelnum #1{%
 \setbox\gnBoxA=\hbox{$#1$}%
 \gnArgHgt=\ht\gnBoxA%
 \ifnum     \gnArgHgt<\gnCornerHgt \gnArgHgt=0pt%
 \else \advance \gnArgHgt by -\gnCornerHgt%
 \fi \raise\gnArgHgt\hbox{$\ulcorner$} \box\gnBoxA %
 \raise\gnArgHgt\hbox{$\urcorner$}}

\newbox\gnBoxAS
 \newdimen\gnCornerHgtS
 \setbox\gnBoxAS=\hbox{$\scriptstyle{\ulcorner}$}
 \global\gnCornerHgtS=\ht\gnBoxAS
 \newdimen\gnArgHgtS
 \def\SGodelnum #1{% this is the commend
 \setbox\gnBoxAS=\hbox{$\scriptstyle{#1}$}%
 \gnArgHgtS=\ht\gnBoxAS%
 \ifnum     \gnArgHgtS<\gnCornerHgtS \gnArgHgtS=0pt%
 \else \advance \gnArgHgtS by -\gnCornerHgtS%
 \fi \raise\gnArgHgtS\hbox{$\scriptstyle{\ulcorner}$} \box\gnBoxAS %
 \raise\gnArgHgtS\hbox{$\scriptstyle{\urcorner}$}}
 
\newcommand{\OGodelnum}[1]{\overline{\Godelnum{#1}}}
\newcommand{\OSGodelnum}[1]{\overline{\SGodelnum{#1}}}




% for cross-references and links
\usepackage{color}
\usepackage{hyperref}
\definecolor{lnkclr}{cmyk}{.5,.8,0,.2}
\hypersetup{colorlinks, linkcolor=lnkclr, citecolor=lnkclr, urlcolor=lnkclr}

