\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔗��w���_\Romannumeral{7}  ���� 1}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2005 �N 10 �� 4 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item ���̃����_���̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB
  \begin{enumerate}
	\item $(\lambda zyx.zxy)(yx)x$ ,
	\item $(\lambda xy.x(zy))(\lambda z.zy)$ ,
	\item $(\lambda wz.(\lambda yx.y)zw)z$ .
  \end{enumerate}
% 2
\item $Z\equiv \lambda yx.x(yyx)$, $\mathsb{Y}\equiv ZZ$ �Ƃ���B���̂Ƃ�
	$\vdash_{\lambda\beta}\mathsb{Y}x \rhd x(\mathsb{Y}x)$ �������ؖ��}���������B
% 3
\item
 ����_���̑̌n LJ �̊�{�藝�𖽑�_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
% 4
\item �_���� \ $((((r\to s)\to p)\to p)\to q)\to q$
 \ �� �ÓT�_���̑̌n�ŏؖ��ł��Ȃ����Ƃ������B
%\vspace{5mm}
%\vspace{2mm}
%\vspace{5mm}
%\vspace{5mm}
\end{enumerate}
\newpage
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
%{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B

{\bf ���ώ�`����_�� NJ} �̐��_�K���͎��� 3 �ł��B
\[ \infer{MN:\beta}{M:\alpha \to \beta & N:\alpha},
\hspace{7mm} \infer{\lambda x.M:\alpha \to \beta}{\deduce{M:\beta}{\deduce{\Pi}{x:\alpha}}}
\]
\[
\infer{\mathsb{A}M:\alpha}{M:\bot}
\]

{\bf ���ώ�`�q��_�� LJ} �̌����^�͎��̂Q�ł�.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \alpha 
\end{array} \]

{\bf ���ώ�`�q��_�� LJ} �̐��_�K���͎��� 6 �ł��B
\begin{description}
\item[�\���Ɋւ��鐄�_�K��]\ 
\[
\infer[(w \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(c \rightarrow)]
	{\alpha, \Gamma \rightarrow \gamma}
	{\alpha, \alpha, \Gamma \rightarrow \gamma}
\]
\[
\infer[(e \rightarrow)]
	{\Delta, \beta, \alpha, \Gamma \rightarrow \gamma}
	{\Delta, \alpha, \beta, \Gamma \rightarrow \gamma}, \hspace{7mm}
\infer[(cut)]{\Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\alpha, \Delta \rightarrow \gamma}
\]
\item[�_���L���Ɋւ��鐄�_�K��]\ 
\[
\infer[(\to \rightarrow)]
	{\alpha \to \beta, \Gamma, \Delta \rightarrow \gamma}
	{\Gamma \rightarrow \alpha &
	\beta, \Delta \rightarrow \gamma}, \hspace{7mm}
\infer[(\rightarrow \to)]
	{\Gamma \rightarrow \alpha \to \beta}
	{\alpha, \Gamma \rightarrow \beta}
\]
\end{description}

{\bf �̌n $\lambda\beta$ �̌����^}�͎��� 2 �ł�:
\[
\begin{array}{lcccl}
(\beta) & (\lambda x.M)N & \rhd_{1} & [N/x]M, & \\
(\rho) & M & \rhd & N & (\mbox{ ������ } M\equiv_\alpha N).\\
\end{array}
\]

{\bf  �̌n $\lambda\beta$ �̐��_�K��}�� 7 �ł������Ŏg���\��������͎̂��� 4 �ł�:
\[
\infer[(\mu)]{MN \rhd_{1} MR}{N \rhd_{1} R},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\nu)]{MR \rhd_{1} NR}{M \rhd_{1} N},
\]
\[
\infer[(\kappa 1)\ \ (\mbox{ ������ } R\equiv_\alpha M)]{R \rhd_1 N}{M \rhd_{1} N}, \ \ \ \ \ \ \ \ \ 
\infer[(\tau)]{M \rhd R}{M \rhd_{1} N & N \rhd R},
\]
\end{document}
