\documentstyle[11pt,fullpage]{article}
\input{macros}
\newcommand{\la}{\mbox{$-\!\circ$}}     % Linear Arrow
\newcommand{\bla}{\mbox{$\circ\!-$}}    % Backwards Linear Arrow
%\newcommand{\Par}{\,{\parfont P}\,}    % Par (font)
\newcommand{\Par}{{\mbox{\raisebox{.4ex}{$\wp$}}}} % Par (gross)
\newcommand{\with}{\mbox{\,{\&}\,}}     % With (Additive And) (&)
\newcommand{\lplus}{\mbox{$\oplus$}}    % oplus
\newcommand{\tensor}{\mbox{$\otimes$}}  % Tensor (Multiplicative And)
\newcommand{\one}{\mbox{$1$}}           % 1
\newcommand{\zero}{\mbox{$0$}}          % 0
\renewcommand{\bottom}{\mbox{$\bot$}}     % bottom
\newcommand{\ltop}{\mbox{$\top$}}       % top

\begin{document}
\begin{center}
{\large
Exercises }\\
April 24 Lecture\\
CS 358, Spring 1995
\end{center}
\vskip 2ex

\begin{enumerate}
\item Show permutability for $\Par$. More specifically, show that
if there is a cut-free proof of a sequent $\ts \Gamma, A \Par B$
(in the standard one-sided system), then there is a cut-free
proof of this sequent whose last rule is
\[
{\displaystyle\strut \ts \Gamma, A, B} 
\over {\displaystyle\strut \ts \Gamma, A\Par B} 
\]

\item Show that permutability (as in the previous exercise) fails
for tensor ($\otimes$).

\item Consider the fragment of linear logic with
$1, \bottom, \tensor, \Par$ only.
Define the weight $H(A)$ of any formula inductively by
\[\begin{array}{rcl}
H(1) &=& 1\\
H(\bottom) &=& 0\\
H(A \Par B) &=& H(A) + H(B)\\
H(A \tensor B) &=& H(A) + H(B) -1
\end{array}
\]
Show that if $A$ is provable, then $H(A) = 1$.


\item Find a linear formula $A$ over
$1, \bottom, \tensor, \Par$
that is not provable but  has
weight  $H(A) = 1$.
\end{enumerate}
\end{document}