\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\renewcommand{\to}{\rightarrow}
\newtheorem{definition}{��`}[section]
\newtheorem{theorem}[definition]{�藝}
%\newtheorem{problem}[definition]{���}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{���_���w\Romannumeral{2}  ���� 3}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2003 �N 1 �� 31 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item CL �� \ \ $\lambda^* xy.xyy$ \ \ �����߂�($S$, $K$ �ŕ\��)�B
%\vspace{5mm}
% 2
\item CL �� \ \ $(\lambda^* xy.xyy)xy$ \ \ �� weak reduction ����B
% 3
\item CL �� \ \ $\lambda^* xy.xyy$ \ \ �����^ $\delta$ ������,
	\ \ $\lambda^* xy.xyy\in \delta$ \ \ �Ɏ��� TA$_C$ �̏ؖ��}�������B
%\vspace{5mm}
% 4
\item �����_�� \ \ $\lambda xy.(\lambda uz.y(xz))(\lambda y.yz)$ \ \ �����^ $\delta$ ������,\\
	\ \ $\lambda xy.(\lambda uz.y(xz))(\lambda y.yz)\in\delta$ \ \ �Ɏ��� TA$_\lambda$ �̏ؖ��}
	�������B
%\vspace{5mm}
% 5
%\vspace{2mm}
\item �����_�� \ \ $\lambda xy.(\lambda uz.y(xz))(\lambda y.yz)$ \ \ �� $\beta$ ���K�`($\beta$-nf)
	$M$ ������,  4 �ŋ��߂� $\delta$ �ɑ΂��� \ \ $M\in\delta$ \ \ �Ɏ��� TA$_\lambda$ �̏ؖ��}
	�������B
\end{enumerate}
\newpage
%\vspace{2cm}
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
\begin{definition}[Weak reduction]\em
Any CL-term $KXY$ or $SXYZ$ is called a (weak) redex. Contracting an occurence of a redex in a term
$U$ means replacing one occurence of
\[\begin{array}{lll}
KXY & by & X, \\
SXYZ & by & XZ(YZ).\\
\end{array}\]
If this changes $U$ to $U'$, we say that $U$ (weakly) contracts to $U'$ , or
\[U\rhd_{1w} U'.\]
We say that $U$ (weakly) reduces to $V$, or
\[U\rhd_w V\]
iff $V$ is obtained from $U$ by a finite (perhaps empty) series of weak contractions.
\end{definition}

\begin{definition}[Abstraction]\label{def-abstraction}\em
For each CL-term $M$ and each variable $x$, a CL-term $\lambda^* x.M$ is defined by induction on $M$, thus:
\[\begin{array}{lllll}
(a) & \lambda^* x.M & \equiv & KM & \mbox{if\ } x\notin FV(M);\\
(b) & \lambda^* x.x & \equiv & SKK & ;\\
(c) & \lambda^* x.Ux  & \equiv & U   & \mbox{if\ } x\notin FV(U);\\
(d) & \lambda^* x.UV  & \equiv & S(\lambda^* x.U)(\lambda^* x.V) & \mbox{if neither (a) nor (c) applies.}
\end{array}\]
\end{definition}

\begin{definition}[The type-assignment system TA$_C$]\em
It has two axiom-schemes; they are
\[
\begin{array}{ll}
(\to K) & K\in \alpha \to \beta \to \alpha, \\
(\to S) & S\in (\alpha \to \beta \to \gamma) \to (\alpha\to \beta) \to \alpha \to \gamma. \\
\end{array}
\]
Its only rule is called the $\to$-elimination rule or ($\to$e);
$$ 
\infer[(\to\mbox{e})]{XY\in\beta}{X\in\alpha \to \beta & Y\in\alpha}.
$$
\end{definition}

\begin{definition}[The type-assignment system TA$_\lambda$]\em
It has no axiom-schemes and two rules the $\to$-elimination rule ($\to$e) and
the $\to$-introduction rule ($\to$i);
$$ 
\infer[(\to\mbox{e})]{XY\in\beta}{X\in\alpha \to \beta & Y\in\alpha},
$$
$$ 
\infer[(\to\mbox{i})]{\lambda x.M \in \alpha\to\beta}{\deduce{M\in\beta}{[x\in\alpha]}}.
$$
\end{definition}

\end{document}
