\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}{\supset}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}
\title{��񐔊w\Romannumeral{1}  ���� 6}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2012 �N 7 �� 24 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item ���̏ȗ��`�̐��_�}�̐��K�`�����Ƃ߂�B�r���o�߂��������ƁB�܂�, �K�v�ŏ����� $\alpha$-�ϊ�
	�����邱�ƁB������ $A\equiv \alpha\to\beta\to\beta\to\gamma$ �ł���B
\[
\infer{(\delta\to\beta)\to(\alpha\to\beta\to\beta\to\gamma)\to\gamma}{
\infer[\lambda x]{(\beta\to A\to\gamma)\to(\delta\to\beta)\to A\to\gamma}{
\infer[\lambda y]{(\delta\to\beta)\to A\to\gamma}{
\infer{A\to\gamma}{x:\beta\to A\to\gamma &
	\infer{\beta}{y:\delta\to\beta & z:\delta}}}}
&
\infer[\lambda x]{\beta\to A\to\gamma}{\infer[\lambda z]
	{A\to\gamma}{\infer{\gamma}{\infer{\beta\to\gamma}{\infer{\beta\to\beta\to\gamma}{z:A & y:\alpha} & x:\beta} & x:\beta}}}}
\]
% 2
\item
���̘_�����ɂ���, �u$M: \mbox{�_����}$�v ���̌n NJ �ŏؖ��ł���悤�ȕ����_�� $M$ ������,
 �u$M: \mbox{�_����}$�v �� NJ �̏ؖ��}��`���B�ȗ��`�ŏؖ��}�������ꍇ��, �����_�� $M$ �𖾋L
 ���邱��.
\begin{enumerate}
  \item\label{1}
    $\neg\neg(((\alpha \to \beta) \to \alpha) \to \alpha)$
  \item\label{2}
    $(\neg\alpha\to\alpha)\to\neg(\alpha\to\neg\alpha)$
\end{enumerate}
% 3
\item
 ����_���̑̌n LJ �̊�{�藝�𖽑�_���̑̌n NJ �̐��K���藝���g���ďؖ�����B
% 4
\item ���������̌n $\lambda\beta$ �̐��_�}��`���B
\[
\lambda xy.x \rhd_1 \lambda x.x \vdash_{\lambda\beta} x = \lambda x.x
\]
%\vspace{5mm}
%\vspace{2mm}
%\vspace{5mm}
%\vspace{5mm}
\end{enumerate}
\newpage
%{\bf ����:} ����͎����I����ɉ�����܂��̂�, �������݂Ȃǂ͂��Ȃ��ŉ������B\\[2mm]
%
%{\bf ����:} �ȉ��ł�, �ׂ��ȏ���(�ϐ������Ȃ�)�͏ȗ�����Ă���B
% �܂�, LJ �̑̌n�͋��ȏ��Ƃ�
% �����قȂ��Ă���(�E�ӂ͋�Ƃ������Ƃ͂Ȃ�, ���傤�ǈ�̘_����)�B
\noindent
{\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 ���ώ�`����_�� LJ} �̌����^�͎��̂Q�ł�.
% {\bf ���ώ�`�q��_�� LJ} �̌����^�͎��̂Q�ł�.
\[ \begin{array}{cccc}
(I) & \alpha & \rightarrow & \alpha \\
(N) & \bot   & \rightarrow & \alpha 
\end{array} \]
%
{\bf ���ώ�`����_�� 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��}�͎��� 8 �ł�:
\[
\infer[(\mu)]{MN \rhd_{1} MR}{N \rhd_{1} R},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\nu)]{MR \rhd_{1} NR}{M \rhd_{1} N},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\xi)]{\lambda x.M \rhd_{1} \lambda x.N}{M \rhd_{1} N},
\]
\[
\infer[(\kappa 1)\ \ (\mbox{ ������ } R\equiv_\alpha N)]{M \rhd_1 R}{M \rhd_{1} N}, \ \ \ \ \ \ \ \ \ 
\infer[(\tau)]{M \rhd R}{M \rhd_{1} N & N \rhd R},
\]
\[
\infer[(\kappa)]{M = N}{M \rhd N}, \ \ \ \ \ \ \ \ \ 
\infer[(\sigma)]{N = M}{M = N}, \ \ \ \ \ \ \ \ \ 
\infer[(\tau=)]{M = R}{M = N & N = R}.
\]
\end{document}
