

%\newtheorem{theorem}{Theorem}    %% Patrick: added for 'article' class version
%\newtheorem{maintheorem}[theorem]{Main Theorem}
%\newtheorem{observation}[theorem]{Observation}
%\newtheorem{corollary}[theorem]{Corollary}
%\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{plain}
\newtheorem{proposition}[theorem]{Proposition}
%\newtheorem{conjecture}[theorem]{Conjecture}
%
%\theoremstyle{definition}
%\newtheorem{definition}[theorem]{Definition}
%\newtheorem{example}[theorem]{Example}
%\newtheorem{notation}[theorem]{Notation}
%\newtheorem{convention}[theorem]{Convention}
%\newtheorem{remark}[theorem]{Remark}
%\newtheorem{discussion}[theorem]{Discussion}

\newcommand{\todo}[1]{{\color{red}{\textbf{Todo:} #1}}}
\newcommand{\anupam}[1]{{\color{orange}{\textbf{Anupam:} #1}}}
\newcommand{\patrick}[1]{{\color{blue}{\textbf{Patrick:} #1}}}

\newcommand{\IH}{\mathit{IH}}

\newcommand{\defined}{:=}
	
	\newcommand{\LL}{\it{LL}}
	\vllineartrue
	
	
	\newcommand{\FV}{\mathit{FV}}
	
	
	%specification
	
	\newcommand{\eqspec}{\mathcal E}
	\newcommand{\closure}[1]{\overline{#1}}
	
	\newcommand{\conv}{\mathit{Conv}}
	
	% theories
	\newcommand{\theory}{\mathcal T}
	\newcommand{\system}{\mathcal S}

	
	%terms
	\newcommand{\pred}{p}
	\newcommand{\cond}{C}
	\renewcommand{\succ}{\mathsf{s}}
	\renewcommand{\epsilon}{\varepsilon}
	
	% linear connectives
	
	\newcommand{\limp}{\multimap}
	\renewcommand{\land}{\otimes}
	\newcommand{\laand}{\&}
	\newcommand{\laor}{\oplus}
	\renewcommand{\lor}{\vlpa}
	\renewcommand{\lnot}[1]{{#1^{\perp}}}
	\newcommand{\lnotnot}[1]{#1^{\perp \perp}}
	
	% classical connectives
	
	\newcommand{\cimp}{\rightarrow}
	\newcommand{\cand}{\wedge}
	\newcommand{\cor}{\vee}
	\newcommand{\cnot}{\neg}
	
	
	\newcommand{\Ax}{\mathit{(Ax)}}
	\newcommand{\Rl}{\mathit{(Rl)}}
	
	\newcommand{\MELL}{\mathit{MELL}}
	\newcommand{\MEAL}{\mathit{MELLW}}
	\newcommand{\MELLW}{\mathit{MELL(W)}}
	
	\newcommand{\Aonetwo}{\mathcal{A}^1_2}
	\newcommand{\logic}{\mathit{L}_{\mathcal A} }
	
	% predicates
	\newcommand{\nat}{N}
	\newcommand{\word}{W}
	
	\newcommand{\Nat}{\mathbb{N}}
	\newcommand{\Word}{\mathbb{W}}
	
	%axioms
	\newcommand{\wk}{\mathit{wk}}
	\newcommand{\impl}{\cimp\text{-}\mathit{l}}
	\newcommand{\impcomm}{\mathit{com}}
	\newcommand{\conint}{\cand\text{-}\mathit{i}}
	\newcommand{\conel}{\cand\text{-}\mathit{e}}
	\newcommand{\negclass}{\cnot}
	
	%equality
	\newcommand{\refl}{\mathit{ref}}
	\newcommand{\symm}{\mathit{sym}}
	\newcommand{\trans}{\mathit{trans}}
	\newcommand{\subst}{\mathit{sub}}
	
	%rules
	\newcommand{\inv}[1]{#1\text{-inv}}
	
	\renewcommand{\mp}{\mathit{mp}}
	\newcommand{\gen}{\mathit{gen}}
	\newcommand{\inst}{\mathit{ins}}
	\newcommand{\id}{\it{id}}
	\newcommand{\cut}{\it{cut}}
	\newcommand{\multicut}{\it{mcut}}
	\newcommand{\indr}{\mathit{PIND}}
	\newcommand{\nec}{\mathit{nec}}
	\newcommand{\tax}{\mathit{T}}
	\newcommand{\four}{\mathit{4}}
	\newcommand{\kax}{\mathit{K}}
	\newcommand{\cntr}{\mathit{cntr}}
	
	\newcommand{\lefrul}[1]{#1\text{-}\mathit{l}}
	\newcommand{\rigrul}[1]{#1\text{-}\mathit{r}}
	
	%consequence relations
	\newcommand{\admits}{\vDash}
	\newcommand{\seqar}{\vdash}
	\newcommand{\proves}{\vdash_e}
	
	%induction
	\newcommand{\ind}{\mathit{PIND}}
	\newcommand{\pind}{\mathit{PIND}}
	\newcommand{\cax}[2]{#1\text{-}#2}

	\newcommand{\sigone}{\Sigma^{\word^+}_1 }
	\newcommand{\sigzer}{\Sigma^{\word^+}_0}
	\newcommand{\bharith}{\mathcal A^1_2}
	\newcommand{\arith}{I\sigone}
	
	

          % sizes
          \newcommand{\height}[1]{\mathit{h}(#1)}
