\documentclass[12pt]{article}
\usepackage{fullpage}
\usepackage{times}
\usepackage{amsmath,amsfonts,amssymb,amsthm}
\usepackage{enumerate}
\usepackage{fitch}
\usepackage{qtree}
\usepackage{bussproofs}
\usepackage{algorithmic}
\usepackage{algorithm}

\newcommand{\ignore}[1]{}
\newcommand{\hoare}[1]{(\! | #1 |\!)}
\newcommand{\Inv}{\mathcal{I}}


\begin{document}

\par\noindent{\bf CS81 HW\#6 Spring 2012} {\em Out: 02/22/2012. Due: 02/29/2012 (before class)} 
\paragraph{\bf Policy on homeworks}
\begin{enumerate}
\item {\em Collaboration}: 
	You may discuss a question with any other student currently taking CS81 provided:
	(i) both of you contribute equally; 
	(ii) you come away from any discussion with an understanding in your mind (and no archived solution of any form is retained); 
	(iii) your submission is your own work prepared by yourself on a separate occassion.

\item {\em Reference materials}: 
	You should only refer to materials from this semester of CS81 
	(class notes, handouts, textbooks, grutors, instructor, etc).

\item {\em Submission}:
	Your submission should be legible or is prepared using TeX.
\end{enumerate}

\paragraph{Of Tableaux, Sequents and Triples}
\begin{enumerate}
\item (Peirce's Law) Prove the following assertion using the Analytic Tableaux {\em and} 
Sequent Calculus methods.
\[
\vdash (((a \to b) \to a) \to a).
\]

\item (Prove or Disprove) Consider the following assertion:
\[
(\forall x)(\exists y)[A(x) \to B(y)] \vdash (\exists y)(\forall x)[A(x) \to B(y)]
\]
If {\bf prove}, provide the proof in the three methods we have studied
(Natural Deduction, Analytic Tableaux, and Sequent Calculus).
If {\bf disprove}, exhibit a single {\em model} contradicting the assertion.

\item (Correct or Not Even Wrong) Consider the following program called {\sc exp}
whose inputs are integers:
\begin{algorithmic}[1]
\STATE $y = 1$
\WHILE {$(b > 0)$}
	\IF {$(b \mbox{ is even})$}
		\STATE $a = a*a$
		\STATE $b = b/2$
	\ELSE
		\STATE $y = y * a$ 
		\STATE $b = b - 1$
	\ENDIF
\ENDWHILE
\end{algorithmic}

Prove that the following Hoare triple holds:
\begin{equation} \label{eqn:exp-triple}
\hoare{(a = m) \wedge (b = n) \wedge (m > 0) \wedge (n \ge 0)} 
\ \
\mbox{\sc exp}
\ \
\hoare{y = m^{n}}
\end{equation}
State your invariant $\Inv$ explicitly and use Hoare's logic rules to show (\ref{eqn:exp-triple}).

\end{enumerate}


\end{document}



