\def\ra{\rightarrow}
\renewcommand{\to}{\supset}
\documentclass[11pt]{jarticle}
\usepackage{latexsym}
\usepackage{proof2}
\setlength{\oddsidemargin}{40pt}
   \setlength{\evensidemargin}{40pt}
\setlength{\marginparwidth}{10pt}
\addtolength{\textwidth}{50pt}
\addtolength{\textheight}{20pt}
% \pagestyle{empty}
\newcommand{\Romannumeral}[1]{\uppercase\expandafter{\romannumeral#1}}
\title{��񐔊w\Romannumeral{1}  ���� 1}
\author{} % ��t��w ���w�� ���w�E��񐔗��w�� �ÐX �Y��}
\date{2002 �N 4 �� 23 �� (��)}
\begin{document}
\maketitle
\begin{enumerate}
% 1
\item\label{c-p1.1} $C(CKK)xy \rhd yx$ ���̌n CLw �ŏؖ��\�ł��邱�Ƃ�����($C(CKK)xy \rhd yx$ ��
	���� CLw �̏ؖ��}������).
%\vspace{7mm}
% 2
\item $B(BW)(BBC)xyz \rhd xz(yz)$ ���̌n CLw �ŏؖ��\�ł��邱�Ƃ�����(�K�������ؖ��}��`���Ȃ��Ă��悢).
\vspace{7mm}
% 3
\item �C�ӂ̍� $\alpha$ �ɑ΂���, ���̎����ؖ��ł���ϐ� $x$ ���܂܂Ȃ��� $\beta$
	�����݂��邱�Ƃ�����: \[ \beta x \rhd \alpha \ . \]
\vspace{7mm}
% 4
\item ��������(������, $I$ �� $Ix \rhd x$ �� CLw �ŏؖ��\�ȕ��Ƃ���).
\[x \rhd Kxy, K \rhd KI \vdash_{CLw} x \rhd y\]
\end{enumerate}
\newpage
�̌n CLw �̌����^�͎��� 4�ł�.
\[
\begin{array}{ll}
(B) & B\alpha\beta\gamma \rhd \alpha(\beta\gamma) \\
(C) & C\alpha\beta\gamma \rhd \alpha\gamma\beta \\
(K) & K\alpha\beta \rhd \alpha \\
(W) & W\alpha\beta \rhd \alpha\beta\beta \\
\end{array}
\]

�ؖ��}�͌�����t�Ƃ���؏�̐}�`�ł�. �ؖ��}����邽�߂̋K����
{\bf ���_�K��\index{������񂫂���@���_�K��}(rule of inference)}�Ƃ����܂�. 
 �̌n CLw �̐��_�K���͎��� 3 �ł�:
\[
\infer[(\mu)]{\alpha\beta \rhd \alpha\gamma}{\beta \rhd \gamma},
	\ \ \ \ \ \ \ \ \ \ 
\infer[(\nu)]{\alpha\gamma \rhd \beta\gamma}{\alpha \rhd \beta},
\]
\[
\infer[(\tau)]{\alpha \rhd \gamma}{\alpha \rhd \beta & \beta \rhd \gamma}.
\]
\\[1cm]

�̌n CLw �̏ؖ��}�͌����ł��鎮����[�Ƃ���؏�̐}�`�ł���.
������, ��[�ɂ��鎮�Ƃ��Č����ȊO�̂��̂�F��
�����̂�{\bf ���_�}\index{�������@���_�}}(deduction)} �Ƃ������Ƃɂ��܂�.
���_�}�̏�[�ɂ��鎮�Ō����łȂ����̂�, ���̐��_�}��
{\bf ����\index{���Ă�@����}(assumption)}�Ƃ����܂�. $\Gamma$ �����̗�Ƃ��܂�.
 $\Gamma$ �Ɋ܂܂�鎮������Ƃ�,
 $\alpha \rhd \beta$ �Ɏ��� CLw �̐��_�}������Ƃ�, $\Gamma
 \vdash_{CLw} \alpha \rhd \beta$ �Ə���, CLw �ŉ��� $\Gamma$ ����
 $\alpha \rhd \beta$ ���ł�Ƃ����܂�. ���_�}�̉���͑S�� $\Gamma$ �ɓ�����
���Ȃ���΂����܂���, ���ۂɏ�[�ɂȂ����� $\Gamma$ �ɓ����Ă��Ă����܂�
�܂���.
\end{document}
