%\documentclass[dvips,12pt]{amsart}
\documentclass[pdftex,12pt]{amsart}
\usepackage{amsmath}
\usepackage[portuges]{babel}
\usepackage{enumerate}

\usepackage{hyperref}
\input{defport}
\input{defseqs}
\input{deflogic}
\def\shorttest#1{\ensuremath{\mathcal S_{#1}}}
\def\longtest#1{\ensuremath{\mathcal L_{#1}}}
\title{Teoria da Computa\c{c}ao \\
	Teste  \shorttest 0\\
	Helter Skelter}

\author{Raul H.C. Lopes}
\def\mergesort{\emph{Mergesort}}
\def\heapsort{\emph{HeapSort}}


%\setcounter{page}{0}
%\setcounter{section}{0}
%\setcounter{subsection}{0}

\def\lbop{\ensuremath{\downarrow}}
\def\ubop{\ensuremath{\uparrow}}
\def\lb#1{\ensuremath{\lbop\negthickspace #1}}
\def\gb#1{\ensuremath{\gbop\negthickspace #1}}

\def\xnil{\ensuremath{\lambda}}
\begin{document}

\maketitle

\section{Preliminares}
Ao longo do restante deste curso voc\^e far\'a dois tipos de avalia\c{c}\~oes:
\begin{itemize}
	\item testes curtos, identificados como \shorttest i,
		de uma hora de dura\c{c}\~ao, cuja nota final ser\'a dada
		pela nota m\'edia de todas as quest\~oes de todos os testes
		realizados.
	\item um teste de longa dura\c{c}\~ao.
\end{itemize}

Sua nota final ser\'a dada pela m\'edia das notas dos dois tipos de testes.

As seguintes restri\c{c}\~oes valem em rela\c{c}\~ao a este teste:

\begin{itemize}
	\item Ele \'e estritamente individual.
	\item Ele tem dura\c{c}\~ao prevista de uma hora.
	\item Voc\^e pode consultar seu pr\'oprio material, n\~ao sendo
		permitida qualquer troca de  objetos entre colegas.
	\item Todas as quest\~oes tratam de propriedades de seq\"u\^encias. 
		Em cada quest\~ao, a nota \'e atribu\'{\i}da exclusivamente 
		\`as provas de propriedades (ou refuta\c{c}\~oes) associadas.
\end{itemize}

\section{Seq\"u\^encias}

Uma \sqn\ de elementos de um tipo $A$  \ee\ uma \sqn\ vazia (denotada por
$\xnil$) ou o resultado de adicionar um elemento de $A$ a uma \sqn\ de 
elementos de $A$. Os axiomas a seguir definem \sqn s de elementos
de $A$, denotada \xsqntype A:
\begin{itemize}
	\item $\xnil \in \sqntype A$
	\item $(\xcons ax)\in\xsqntype A$ se $x\in\xsqntype A \land a\in A$
	\item{fecho universal.}
\end{itemize}

Pertin\^encia em uma \sqn\ \ee\ definida a seguir.
\begin{gather}
	a\not\in\xnil\\
	a\in (\xcons bx) =\lr. a=b\lor a\in x
\end{gather}

A seguir, a defini\cao\ de ordena\cao\ crescente n\ao\ estrita.
\begin{gather}
	\xincr{(\xnil)}\\
	\xincr{(\xcons a\xnil)}\\
	\xincr{(\xcons a(\xcons bx))} \llr.= a\le b\land \xincr{(\xcons bx)}
\end{gather}

Os axiomas a seguir definem o m\'{\i}nimo de uma seq\"u\^encia.
\begin{gather}
	a\le b\llr.\limp min(a,b) = a\\
	a>b\lr.\limp min(a,b) = b \\
	\lb\xnil = +\infty\\
	\lb{(\xcons ax)} \lr.= min(a,\lb x)
\end{gather}
\section{As quest\~oes}


\def\sameop{\ensuremath{\stackrel{=}{\land}}}
\def\bigo#1{\ensuremath{\mathcal{O}(#1)}}


\begin{qst}
	Defina um predicado $(\sameop)$ que determine em \bigo{n} se todos
	elementos de uma seq\"u\^encia de $n$ elementos s\~ao iguais. Prove que
	$$\bndA{x}{x\in\xsqntype A}
	          {\sameop x \ll.=\lr. \bndA{a,b}{a\in x\land b \in x}
		                       {a = b}}$$ 
\end{qst}

\def\nullpair{\ensuremath{\langle\rangle}}
\def\pair#1#2{\ensuremath{\langle#1,#2\rangle}}
\def\urlop{\ensuremath{\hookrightarrow}}
\def\del#1#2{\ensuremath{del(#1,#2)}}
\begin{qst}
	Considere os seguintes axiomas:
	\begin{gather}
		\del a\xnil = \xnil\\
		a = b \ll.\limp\lr. \del a{(\xcons bx)} = x \\
		a \neq b \ll.=\lr. \del a{(\xcons bx}) = \xcons b{(\del ax)} \\
		x = \xnil\ll.\limp\lr. delMin\ x = \nullpair \\
		x \neq\xnil\ll.\limp\lr. 
		delMin\ x = \pair{\lb x}{\del{\lb x}x}\\
		sort\ll.=\lr. \urlop delMin 
	\end{gather}

	Defina o operador $(\urlop)$ de modo que $(sort\ x)$ seja uma
	permuta\c{c}\~ao ordenada de $x$ e prove que
	$$\bndA{x}{x\in\xsqntype A}{\xincr{sort\ x.}}$$
\end{qst}

\section{When I get to the bottom \ldots}

\begin{quote}
When you get to the bottom \\
You go back to the top of the slide \\
And you stop and you turn \\
And you go for a ride \\
Then you get to the bottom \\
Then you see me again
\end{quote}
 

\end{document}

