\newcommand{\header}[1]
	{
	\documentclass{article}
	\usepackage{amsmath,amssymb}
	\title{Proof obligations for #1}
	\author{(automatically generated)}
	\begin{document}
	\maketitle
	}
\newcommand{\footer}
	{
	\end{document}
	}

\newcommand{\code}{\section{Annotated code}}
\newenvironment{definitions}{\section{Definitions} }{ }
\newenvironment{obligations}{\section{Proof obligations} }{ }

\newcommand{\definition}[3]
	{
	\paragraph{Definition: } (used in proof rule #3)  
	\begin{displaymath} #1 \equiv #2 \end{displaymath}
	}

\newcommand{\obligation}[2]
	{
	\paragraph{Note #1: }
	\begin{displaymath}
	#2
	\end{displaymath}
	}
\newcommand{\unary}[2]
	{
		( #1 #2 )
	}
\newcommand{\binary}[3]
	{
		( #2 #1 #3 )
	}
\newcommand{\literal}[1]
	{
		#1
	}
\newcommand{\substitution}[3]
	{
		[#1 \leftarrow #2]#3
	}
\newcommand{\welldefined}[1]
	{
		(\text{def}.#1 )
	}
\newcommand{\opand}{\wedge}
\newcommand{\opnot}{\neg}
\newcommand{\opgte}{\geq}
\newcommand{\opgt}{>}
\newcommand{\opsub}{-}
\newcommand{\opor}{\vee}
\newcommand{\opequal}{=}
\newcommand{\oplt}{<}
\newcommand{\oplte}{\leq}
\newcommand{\opunequal}{\neq}
\newcommand{\opmul}{\cdot}
\newcommand{\opadd}{+}
\newcommand{\opimplies}{\Rightarrow}
\newcommand{\opneg}{-} % unary negation



