\documentclass[a4j]{jarticle}
\usepackage{latexsym,amssymb,amsmath,amsthm,proof}
\pagestyle{plain}

\newtheorem{df}{��`}[section]
\newtheorem{thm}[df]{�藝}
\newtheorem{cor}[df]{�n}
\newtheorem{lemma}[df]{���}
\newtheorem{ex}[df]{��}

\def\betaeq{=_\beta}
\def\equivdef{\equiv_{def}}
\def\circed#1{#1^{\circ}}
\def\sharped#1{#1^{\sharp}}
\def\varsets#1#2#3{#1_{#2}, \dots, #1_{#3}}
\def\lra{\leftrightarrow}
\def\defeq{\stackrel{\mathrm{def}}{=}}
\def\num#1{\widetilde{#1}}
\def\nnum#1{{\num{#1}}^*}
\def\q{\hspace*{1em}}

\newcommand{\mathsb}[1]{\mathbf{\mathsf{#1}}}


\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% �\��
\thispagestyle{empty}
\vspace*{1cm}
\begin{center}
{\Large ��t��w��w�@�@���R�Ȋw�����ȁ@\\[3mm]�C�m�_��}
\end{center}

\vspace*{1cm}
\begin{center}
{\huge\bf �����_����$\beta$���K�`�������q��p���ċ��߂���@}
\end{center}

\vspace*{1cm}
\begin{center}
{\Large ����18�N3��}
\end{center}

\vspace*{5.7cm}
\begin{center}
{\Large ���w�E��񐔗��w ��U \\[2mm]��񐔗��w �u��}
\end{center}

\vspace*{5mm}
\begin{center}
{\Large �������G}
\end{center}

\setcounter{page}{0}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% �ڎ�
\tableofcontents

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{�͂��߂�}

�^����ꂽ�����_�� $M$ �ɑ΂��āA���̐��K�` $M^*$ ���蓮�ŋ��߂�Ƃ����̂͌��\�ʓ|�Ȃ��Ƃł���B�v�Z�@���g���ċ��߂�ۂɂ�������s������$\alpha$�ϊ��ȂǂɎ��Ԃ�v���邽�߂Ɍ������グ�邱�Ƃ�����B\\
�����Ŗ{�_���ł́A$\beta$���K�`�𑁂����߂邱�Ƃ�ڕW�Ɉȉ��̕��@�ɂ��Ă̌��؂��s���Ă݂��B
\begin{enumerate}
\item �����_������x�����q��p���ă����_�������������ɕϊ�����B
\item ����ɂ���ɂ��ĕϊ��K����p���Ă���ȏ�ό`�ł��Ȃ��`�ɂ���B
\item ������Ăу����_���ɕϊ����Ă���$\beta$���_�N�V�������s���A$\beta$���K�`�����߂�B
\end{enumerate}
���̕��@�͌����q�̕ϊ��K����p���邱�Ƃɂ���āA$\beta$ ���_�N�V�����̉񐔂����炷���Ƃɂ�葬�x�𑁂߂鎖��ړI�Ƃ��Ă���B \\
�܂����̕��@��p���ċ��܂������̂� $M^*$ �� $=_{\alpha}$ �ɂȂ��Ă��邱�Ƃ̏ؖ����s���Ă݂��B

�Ȃ����̘_����\cite{kleene}���Q�l�ɌÐX�Y��搶���ڍׂȕ��j��^�����A�����̌����E���؂�������s�����B


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{CLt-��}

CLt-���Ƃ������̂��ȉ��̂悤�ɋA�[�I�ɒ�`����B
�萔�L���ɂ� $\mathsb{I, K', B', C', S'}$ ���܂܂�Ă�����̂Ƃ���B

\begin{df}[CLt-��]\em \ 
	\begin{enumerate}
		\item �ϐ��ƒ萔�L���� CLt-�� �ł���(���̌`�� CLt-����{\bf ���q} �Ƃ���).
		\item $M$ �� $N$ �� CLt-�� �Ȃ��, $(MN)$ ��	CLt-�� �ł���(���̌`�� CLt-����
		{\bf �K�p} �Ƃ���).
	\end{enumerate}
\end{df}

\bigskip

��`�ʂ�ɏ����Ɗ��ʂ������Ȃ��ēǂ݂Â炭�Ȃ��Ă��܂��̂œK���ɏȗ����鎖�Ƃ���B�����āA����Ȃ����ʂ͍�����₤���Ƃɂ���B
�Ⴆ�� $\mathsb{S'}xy\mathsb{C'}\mathsb{K'}$ �� $((((\mathsb{S'}x)y)\mathsb{C'})\mathsb{K'})$ ��\���Ă���B

�����ł� $\mathsb{I, K', B', C', S'}$ ����{�I�Ȍ����q�Ƃ�CLt-���̕ϊ��K�����ȉ��̂悤�ɒ�`����B

\begin{df}[�ϊ��K��]\em \
\[(\mathsb{I})\ \ \mathsb{I}M \rhd_{1wt} M, \ \ \ \ (\mathsb{K'})\ \ \mathsb{K'}MNRU \rhd_{1wt} MNR, \ \ \ \ 
	(\mathsb{B'})\ \ \mathsb{B'}MNRU \rhd_{1wt} MN(RU),\]
\[(\mathsb{C'})\ \ \mathsb{C'}MNRU \rhd_{1wt} M(NU)R,
	\ \ \ \ (\mathsb{S'})\ \ \mathsb{S'}MNRU \rhd_{1wt} M(NU)(RU) \ . \]
\end{df}

\bigskip

CLt-�� $M$ �ɑ΂��ď�̕ϊ��K����p���ėL����̕ό`���s���A����ȏ�ό`�ł��Ȃ��Ȃ������̍ŏI���ʂ� $M$ �̐��K�`�ƌĂ� $\overline{M}$ �ƕ\�����ƂƂ���B

\bigskip


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{�����_��}

�����_�����ȉ��̂悤�ɍċA�I�ɒ�`����B

\begin{df}[�����_��]\em \ 
	\begin{enumerate}
		\item �ϐ��� �����_�� �ł���(���̌`�� �����_����{\bf ���q} �Ƃ���).
		\item $M$ �� $N$ �� �����_�� �Ȃ��, $(MN)$ ��	�����_�� �ł���(���̌`�� �����_����
		{\bf �K�p} �Ƃ���).
\item $x$ ���ϐ� $M$ �������_���̎� ($\lambda x . M$)�̓����_���ł���(���̌`�̃����_����{\bf ����}�Ƃ���).
	\end{enumerate}
\end{df}

\bigskip

CLt-���̎��Ɠ��l�Ɋ��ʂ��ȗ����A����Ȃ����ʂ͍�����₤���ƂƂ���B
���������ۂɂ��Ă͈�ԊO���̊��ʂƂȂ��Ă���Ƃ������ȗ�����B
���Ȃ킿 $(\lambda x .M)$ �� $\lambda x .M$ �Əȗ����邪,$((\lambda x .M)N)$ �� $\lambda x. MN$ �Ƃ͂��Ȃ� $\lambda x. MN$ �� $(\lambda x. (MN))$ �̏ȗ��`�ł���.�܂� $(\lambda x .(\lambda y .(\lambda z .M)))$ �Ȃǂ� $\lambda xyz.M$ �Əȗ�����.

\bigskip

�����_�� $M$ �Ɋ܂܂�鎩�R�ϐ��̏W���� $FV(M)$ �Ƃ���B
 
\begin{df}[{\bf ���(substitution)}]\label{sub}\em \ 
$M, N$ �������_��, $x$ ��ϐ��Ƃ���. $M$ �̒���(���R�Ɍ����) $x$ �� $N$ ������������
$[N/x]M$ �����̂悤�ɋA�[�I�ɒ�`����.
	\begin{enumerate}
		\item\label{sub1} $[N/x]x \equiv N$ ,
		\item\label{sub2} $[N/x]M \equiv M$ \ \ ($x \notin FV(M)$ �̂Ƃ�),
		\item\label{sub3} $[N/x](QR) \equiv ([N/x]Q\ [N/x]R)$ \ \ ($x \in FV(QR)$ �̂Ƃ�),
		\item\label{sub4} $[N/x](\lambda y.Q) \equiv \lambda y.[N/x]Q$ \ \ ($x \in FV(Q)$ ���� $y\notin FV(N)$ ��
		�Ƃ�),
		\item\label{sub5} $[N/x](\lambda y.Q) \equiv \lambda z.[N/x][z/y]Q$ \ \ ($x \in FV(Q)$ ���� $y\in FV(N)$
		�̂Ƃ�).
	\end{enumerate}
	������ $y\not\equiv x$ �͉��肳��Ă���. �܂�, $z$ �� ���܂łɌ���Ă��Ȃ��ϐ��ł���

\end{df}

\bigskip

\begin{df}[$\beta$ �ϊ�]\em \

�����_���� $\beta$ �ϊ� $\rhd_{1\beta}$ ���ȉ��̂悤�ɍċA�I�ɒ�`����B

\begin{enumerate}
   \item $(\lambda x .M)N \rhd_{1\beta} [N/x]M$
   \item $M \rhd_{1\beta}$ $N$�Ȃ�΁A$\lambda x . M \rhd_{1\beta} \lambda x .N$,
     \hspace*{5mm} $MP \rhd_{1\beta} NP$,  \hspace*{5mm} $PM \rhd_{1\beta} PN$.
\end{enumerate}

$\beta$ �ϊ��̊�ɂȂ� $(\lambda x .M)N$ �̌`�̃����_���� $\beta$ -redex �Ƃ��.
\end{df}

\bigskip

$\beta$ �ϊ���L����J��Ԃ����s���� $P$ ���� $Q$ ��������Ƃ�\\
$P \rhd_{\beta} Q$ �Ƃ���.�܂� $\beta$ �ϊ��\�ȃ����_�����m�𓯈ꎋ���邱�Ƃɂ���ē����郉���_���Ԃ̓����֌W�� $\betaeq$ �ŕ\��.���Ȃ킿�����_�� $P,Q$ �ɑ΂���
\begin{center}
$P \equiv P_1 \lra_{\beta} P_2 \lra_{\beta} \cdots \lra_{\beta} P_{n} \equiv Q$\\
(������ $M \lra_{\beta} N  \Longleftrightarrow_{def} (M \rhd_{1\beta} N \mbox{�܂���} N \rhd_{1\beta} M)$)\\
�𖞂��� $n \geq 1$ �� $P_1,P_2,\cdots, P_n$ �����鎞�A$P \betaeq Q$ �Ƃ���
\end{center}

\bigskip

�����_�� $M$ �� $\beta$-redex ���܂܂Ȃ��Ƃ� $M$ �� $\beta$ ���K�`�ł���Ƃ���.
�܂� $M \rhd_{\beta} N$ �𖞂��� $\beta$ ���K�` $N$ �����鎞 $M$ �� $\beta$ ���K�` $N$ �����A���邢�� $N$ �� $M$ �� $\beta$ ���K�`�ł���Ƃ���.

\bigskip

\begin{thm}[Church-Rosser �̒藝] 
$M \rhd_{\beta} N$ ���� $M \rhd_{\beta} R$ �Ȃ�Ύ��̂悤�ȍ� $T$ �����݂���.\\
$N \rhd_{\beta} T$ ���� $R \rhd_{\beta} T$.
\end{thm}

\bigskip


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{�����_������CLt-���ւ̕ϊ�}

\begin{df}[�ϊ� $\circed{}$]\em \
$M$ �������_���Ƃ���B���̂Ƃ�CLt-���ւ̕ϊ� $\circed{M}$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B

\begin{enumerate}
  \item $\circed{x} \equiv x$
  \item $\circed{(MN)} \equiv \circed{M}\circed{N}$
  \item $\circed{(\lambda x . M)} \equiv \lambda x^t . \circed{M}$
\end{enumerate}

\end{df}

\bigskip

�܂� $\lambda x^t . M$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B

\begin{df}[�ϊ�$t$] \em \
$M$ �� CLt-��, $x$ ��ϐ��Ƃ���. �ϐ� $x$ ���܂܂Ȃ��� $(\lambda^t x.M)$ ���ȉ��̂悤��
�A�[�I�ɒ�`����.
	\begin{enumerate}
		\item $(\lambda^t x.x) \equiv \mathsb{I}$,
		\item $(\lambda^t x. MUV) \equiv \mathsb{K'}MUV$ \ \ ($M$ �������� $x\notin FV(UV)$ �̂Ƃ�),
		\item $(\lambda^t x. MUV) \equiv \mathsb{B'}MU(\lambda^t x.V)$ \ \ ($M$ �������� $x\notin FV(U)$ �̂Ƃ�),
		\item $(\lambda^t. MUV) \equiv \mathsb{C'}M(\lambda^t x.U)V)$ \ \ ($M$ �������� $x\notin FV(V)$ �̂Ƃ�),
		\item $(\lambda^t x. MUV) \equiv \mathsb{S'}M(\lambda^t x.U)(\lambda^t x.V)$ \ \ ($M_1$��������$x \in FV(U) \mbox{����} x \in FV(V)$) �̎�
),
		\item $(\lambda^t x. MN) \equiv (\lambda^t x.IMN)$,
		\item $(\lambda^t x.M) \equiv (\lambda^t x.IIM)$ \ .
	\end{enumerate}
\end{df}

\bigskip

���̕ϊ� $t$ ��David Turner �ɂ���Ĕ������ꂽ�ϊ��������ύX�������̂ł���i\cite{komori}�Q�Ɓj\\
�ق��̕ϊ����@�ł�
$\lambda \varsets{x}{1}{n} . M$ ��ϊ������Ƃ��̕ϊ���̍��̑傫�����ň��̏ꍇ$n^2$�ɔ�Ⴕ���傫���ɂȂ��Ă��܂��̂ɑ΂��A���̕ϊ��͍ň��̏ꍇ�ł� $n$ �ɔ�Ⴕ���傫���ŗ}���邱�Ƃ��ł���B

\begin{ex}[�ϊ���]
���ۂ�$\lambda xyz.xz(yz)$��CL-t���ɕϊ����Ă݂�B

$
\begin{array}{rcl}
& & \\

\lambda^t z.xz(yz) & \equiv & \lambda^t z.\mathsb{I}(xz)(yz) \\
     & \equiv  & \mathsb{S'I}(\lambda^t z . xz)(\lambda^t z . yz) \\
     & \equiv & \mathsb{S'I}(\lambda^t z . \mathsb{I}xz)(\lambda^t z . \mathsb
{I}yz) \\
     & \equiv & \mathsb{S'I}(\mathsb{B'I}x (\lambda^t z . z))(\mathsb{B'I} y (\lambda^t  z . z)) \\
     & \equiv & \mathsb{S'I}(\mathsb{B'I}x \mathsb{I})(\mathsb{B'I}y \mathsb{I
}) \\

& & \\

\lambda^t yz.xz(yz) & \equiv & \lambda^t y. \mathsb{S'I}(\mathsb{B'I}x \mathsb
{I})(\mathsb{B'I}y \mathsb{I}) \\
     & \equiv & \mathsb{B'}(\mathsb{S'I})(\mathsb{B'I}x \mathsb{I})(\lambda^t 
y. \mathsb{B'I}y \mathsb{I}) \\
     & \equiv & \mathsb{B'}(\mathsb{S'I})(\mathsb{B'I}x \mathsb{I})(\mathsb{C'
}(\mathsb{B'I})\mathsb{II}) \\

&& \\

\lambda^t xyz.xz(yz) & \equiv & \lambda^t x. \mathsb{B'}(\mathsb{S'I})(\mathsb{
B'I}x \mathsb{I})(\mathsb{C'}(\mathsb{B'I})\mathsb{II}) \\
     & \equiv & \mathsb{C'}(\mathsb{B'}(\mathsb{S'I}))(\lambda^t x . \mathsb{B
'I}x \mathsb{I}) (\mathsb{C'}(\mathsb{B'I})\mathsb{II}) \\
     & \equiv & \mathsb{C'}(\mathsb{B'}(\mathsb{S'I}))(\mathsb{C'}(\mathsb{B'I
})(\mathsb{C'}(\mathsb{B'I}))) \\

& & \\
\end{array}
$

����� 
$ \circed{(\lambda xyz. xz(yz))} \equiv \mathsb{C'}(\mathsb{B'}(\mathsb{S'I}))
(\mathsb{C'}(\mathsb{B'I})(\mathsb{C'}(\mathsb{B'I}))) $ 
�ƂȂ�B

\end{ex}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{CLt-�����烉���_���ւ̕ϊ�}

\begin{df}[CLt-�����烉���_���ւ̕ϊ�]
CLt-�����烉���_���ւ̕ϊ�$\sharped{}$ ���ȉ��̂悤�ɋA�[�I�ɒ�`����B

\item $\sharped{x} \equiv x$
\item $\sharped{\mathsb{I}} \equiv \lambda x . x$
\item $\sharped{\mathsb{K'}} \equiv \lambda xyzu.xyz$
\item $\sharped{\mathsb{B'}} \equiv \lambda xyzu.xy(zu)$
\item $\sharped{\mathsb{C'}} \equiv \lambda xyzu.x(yu)z$
\item $\sharped{\mathsb{S'}} \equiv \lambda xyzu.x(yu)(zu)$
\item $\sharped{(MN)} \equiv \sharped{M}\sharped{N}$

\end{df}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{$=_{\alpha}$ �ł��邱�Ƃ̏ؖ�}

�����ł̓����_�� $M$ �ɑ΂��A���̕��@��p���ċ��܂������̂��A���̐��K�` $M^*$ �� $\beta$ ���l�ł��邱�Ƃ̏ؖ����s���B�܂��͏����Ƃ��Ĉȉ��̕��������B\\
���ӂƂ��āA����ȍ~�̏ؖ��ł�$\mathsb{S'}$���̊�{�����q�������_���ɕϊ������ۂɌ����ϐ��i�Ⴆ��$\mathsb{S'}$��ϊ�����$\lambda xyzu.x(yu)(zu)$��$xyzu$�j�͂��ׂč��܂łɌ���ĂȂ��ϐ�(new-variable)�ł���Ƃ���B

\begin{lemma}[]\label{hodai1}
�C�ӂ�CLt-�� $M$ �ɑ΂�
\[
\begin{array}{rcl}
 \sharped{(\lambda^t x . M)} x \betaeq \sharped{M} \\
\end{array}
\]
�����藧�B
\end{lemma}

\begin{proof}
$M$ �Ɋւ���A�[�@�Ŏ����B

�� $M \equiv x$ �̎�
\[
\begin{array}{rcl}

\sharped{(\lambda^t x . x)} x & \equiv & \sharped{\mathsb{I}} x \\
    & \equiv & (\lambda x . x) x \\
    & \rhd_{1\beta} & x \\
\end{array}
\]

\bigskip

�� $M \equiv M_1M_2M_3$ ($M_1$��������$x \notin FV(M_2M_3)$) �̎�\\

\[
\begin{array}{rcl}

\sharped{(\lambda^t x . M_1M_2M_3)} x & \equiv & \sharped{(\mathsb{K'}M_1M_2M_3)} x \\
    & \equiv & (\lambda xyzu . xyz) \sharped{M_1}\sharped{M_2}\sharped{M_3}x \\
    & \rhd_{1\beta} &   \sharped{M_1}\sharped{M_2}\sharped{M_3}\\
    & \equiv & \sharped{(M_1M_2M_3)} \\
\end{array}
\]

\bigskip

�� $M \equiv M_1M_2M_3$ ($M_1$��������$x \notin FV(M_2)$) �̎�

\[
\begin{array}{rcl}

\sharped{(\lambda^t x . M_1M_2M_3)} x & \equiv & \sharped{(\mathsb{B'}M_1M_2(\lambda^t x .M_3))} x \\
    & \equiv & (\lambda xyzu . xy(zu)) \sharped{M_1}\sharped{M_2}\sharped{(\lambda^t x . M_3)}x \\
    & \rhd_{1\beta} &   \sharped{M_1}\sharped{M_2}(\sharped{(\lambda^t x .M_3)} x)\\
\end{array}
\]

�A�[�@�̉��肩��
$\sharped{(\lambda^t x . M_3)} x  \betaeq  \sharped{M_3} $ �A�����
\[
\begin{array}{rcl}

    & \betaeq &  \sharped{M_1}\sharped{M_2}\sharped{M_3} \\
     & \equiv & \sharped{(M_1M_2M_3)} \\

\end{array}
\]

\bigskip

�� $M \equiv M_1M_2M_3$ ($M_1$��������$x \notin FV(M_3)$) �̎�\\
��Ɠ��l��
\[
\begin{array}{rcl}

\sharped{(\lambda^t x . M_1M_2M_3)} x & \equiv & \sharped{(\mathsb{C'}M_1(\lambda^t x .M_2)M_3)} x \\
    & \equiv & (\lambda xyzu . x(yu)z) \sharped{M_1}\sharped{(\lambda^t x . M_2)M_2}\sharped{M_3}x \\
    & \rhd_{1\beta} &   \sharped{M_1}(\sharped{(\lambda^t x .M_2)} x) \sharped{M_3}\\
    & \betaeq & \sharped{M_1}\sharped{M_2}\sharped{M_3} \\
    & \equiv & \sharped{(M_1M_2M_3)} \\

\end{array}
\]

\bigskip

�� $M \equiv M_1M_2M_3$ ($M_1$��������$x \in FV(M_2) \mbox{����} x \in FV(M_3)$) �̎�\\
��Ɠ��l��
\[
\begin{array}{rcl}

\sharped{(\lambda^t x . M_1M_2M_3)} x & \equiv & \sharped{(\mathsb{S'}M_1(\lambda^t x .M_2)(\lambda^t x .M_3))} x \\
    & \equiv & (\lambda xyzu . x(yu)(zu)) \sharped{M_1}\sharped{(\lambda^t x . M_2)}\sharped{(\lambda^t x . M_3)}x \\
    & \rhd_{1\beta} &   \sharped{M_1}(\sharped{(\lambda^t x .M_2)} x) (\sharped{(\lambda^t x .M_3)}x)\\
    & \betaeq & \sharped{M_1}\sharped{M_2}\sharped{M_3} \\
    & \equiv & \sharped{(M_1M_2M_3)} \\

\end{array}
\]

\bigskip

�� $M \equiv M_1M_2$ �̎�

\[
\begin{array}{rcl}
\sharped{(\lambda^t x . M_1M_2)} x & \equiv & \sharped{(\lambda^t x . \mathsb{I}M_1M_2)} x \\

\end{array}
\]
\\
$\mathsb{I}$ �͕��Ȃ̂ŁA��̂����ꂩ�Ɠ����c�_������΂悢�B

\bigskip

�� $M \equiv M_1$ �̎�

\[
\begin{array}{rcl}
\sharped{(\lambda^t x . M_1)} x & \equiv & \sharped{(\lambda^t x . \mathsb{II}M_1)} x \\

\end{array}
\]
\\
$\mathsb{I}$ �͕��Ȃ̂ŁA��̂����ꂩ�Ɠ����c�_������΂悢�B


\end{proof}


\bigskip

\begin{thm}[]\label{teiri1}

�C�ӂ̃����_�� $M$ �ɑ΂�
\[
\begin{array}{rcl}
\sharped{(\circed{M})} \betaeq M \\
\end{array}
\]

�����藧�B

\end{thm}

\begin{proof}

$M$ �Ɋւ���A�[�@�Ŏ����B

��  $M \equiv x$ �̎�

\[
\begin{array}{rcl}
\sharped{(\circed{x})} & \equiv & \sharped{x} \\
                & \equiv & x \\
\end{array}
\]

\bigskip

�� $M \equiv M_1M_2 �̎� $ \\
�A�[�@�̉��肩��

\[
\begin{array}{rcl}
\sharped{(\circed{M_1})} & \equiv & M_1 \\
\sharped{(\circed{M_2})} & \equiv & M_2 \\
\end{array}
\]
�����
\[
\begin{array}{rcl}
\sharped{(\circed{(M_1M_2)})} & \equiv & \sharped{(\circed{M_1}\circed{M_2})} \\
        &  \equiv & \sharped{(\circed{M_1})}\sharped{(\circed{M_2})} \\
        & \equiv  & M_1M_2 \\

\end{array}
\]

\bigskip

�� $M \equiv \lambda x.N$ �̎�

\[
\begin{array}{rcl}
\circed{M} & \equiv & \circed{(\lambda x . N)} \\
    & \equiv & \lambda^t x .\circed{N} \\
\end{array}
\]


�� $\circed{N} \equiv x$ �̎�
\[
\begin{array}{rcl}

\sharped{(\lambda^t x . x)} & \equiv & \sharped{\mathsb{I}} \\
      & \equiv & \lambda x.x\\

\end{array}
\]

\bigskip

�� $\circed{N} \equiv N_1N_2N_3$ ($N_1$ �������� $x \notin FV(M_2M_3)$) �̎�

\[
\begin{array}{rcl}

\sharped{(\lambda^t x . N_1N_2N_3)} & \equiv & \sharped{(\mathsb{K'}N_1N_2N_3)} \\
  & \equiv & (\lambda xyzu. xyz)\sharped{N_1}\sharped{N_2}\sharped{N_3} \\
  & \rhd_{1\beta} & \lambda u .\sharped{N_1}\sharped{N_2}\sharped{N_3} \\
  & =_{\alpha} & \lambda x . \sharped{N_1}\sharped{N_2}\sharped{N_3} \hspace*{5mm}(\mbox{u ��new-variable �Ȃ̂� $N_1$,$N_2$,$N_3$ �ɂ͏o�����Ȃ�}) \\
  &\equiv &  \lambda x . \sharped{(N_1N_2N_3)} \\
  & \equiv & \lambda x . \sharped{(\circed{N})} \\
  & \betaeq & \lambda x . N \hspace*{5mm}(\mbox{�A�[�@�̉�����})\\

\end{array}
\]

\bigskip

�� $\circed{N} \equiv N_1N_2N_3$ ($N_1$ �������� $x \notin FV(N_2)$) �̎�

\[
\begin{array}{rcl}

\sharped{(\lambda^t x . N_1N_2N_3)} & \equiv & \sharped{(\mathsb{B'}N_1N_2(\lambda^t x .N_3))} \\
  & \equiv & (\lambda xyzu. xy(zu))\sharped{N_1}\sharped{N_2}\sharped{(\lambda^t x .N_3)} \\
  & \rhd_{1\beta} & \lambda u .\sharped{N_1}\sharped{N_2}(\sharped{(\lambda^t x . N_3)}u) \\
  & =_{\alpha} &  \lambda x .\sharped{N_1}\sharped{N_2}(\sharped{(\lambda^t x .N_3)}x) \\ 
  & \betaeq & \lambda x .\sharped{N_1}\sharped{N_2}\sharped{N_3} \hspace*{5mm}(\mbox{���\ref{hodai1}���}) \\
  & \equiv & \lambda x . \sharped{(N_1N_2N_3)} \\
  & \equiv & \lambda x . \sharped{(\circed{N})} \\
  & \betaeq & \lambda x . N \hspace*{5mm}(\mbox{�A�[�@�̉�����})\\

\end{array}
\]

\bigskip

�� $\circed{N} \equiv N_1N_2N_3$ ($N_1$ �������� $x \notin FV(N_3)$) �̎�\\
��Ɠ��l��

\[
\begin{array}{rcl}

\sharped{(\lambda^t x . N_1N_2N_3)} & \equiv & \sharped{(\mathsb{C'}N_1(\lambda^t x .N_2)N_3)} \\
  & \equiv & (\lambda xyzu. x(yu)z)\sharped{N_1}\sharped{(\lambda^t x .N_2)}\sharped{N_3} \\
  & \rhd_{1\beta} & \lambda u .\sharped{N_1}(\sharped{(\lambda^t x . N_2)}u)\sharped{N_3} \\
  & =_{\alpha} &  \lambda x .\sharped{N_1}(\sharped{(\lambda^t x . N_2)}x)\sharped{N_3} \\
  & \betaeq & \lambda x .\sharped{N_1}\sharped{N_2}\sharped{N_3} \\
  & \equiv & \lambda x . \sharped{(N_1N_2N_3)} \\
  & \equiv & \lambda x . \sharped{(\circed{N})} \\
  & \betaeq & \lambda x . N \\

\end{array}
\]

\bigskip

�� $\circed{N} \equiv N_1N_2N_3$ ($M_1$��������$x \in FV(N_2) \mbox{����} x \in FV(N_3)$) �̎�\\
��Ɠ��l��

\[
\begin{array}{rcl}

\sharped{(\lambda^t x . N_1N_2N_3)} & \equiv & \sharped{(\mathsb{S'}N_1(\lambda^t x .N_2)(\lambda^t x .N_3)} \\
  & \equiv & (\lambda xyzu. x(yu)(zu))\sharped{N_1}\sharped{(\lambda^t x .N_2)}\sharped{(\lambda^t x .N_3)} \\
  & \rhd_{1\beta} & \lambda u .\sharped{N_1}(\sharped{(\lambda^t x . N_2)}u)(\sharped{(\lambda^t x .N_3)}u) \\
  & =_{\alpha} &  \lambda x .\sharped{N_1}(\sharped{(\lambda^t x . N_2)}x)(\sharped{(\lambda^t x.N_3)}x) \\
  & \betaeq & \lambda x .\sharped{N_1}\sharped{N_2}\sharped{N_3} \\
  & \equiv & \lambda x . \sharped{(N_1N_2N_3)} \\
  & \equiv & \lambda x . \sharped{(\circed{N})} \\
  & \betaeq & \lambda x . N \\

\end{array}
\]

\bigskip

�� $\circed{N} \equiv N_1N_2$  �̎�\\

\[
\begin{array}{rcl}

\sharped{(\lambda^t x .N_1N_2)} & \equiv & \sharped{(\lambda^t x . \mathsb{I}N_1N_2)} \\

\end{array}
\]

$\mathsb{I}$ �͕��Ȃ̂ŏ�̂����ꂩ�Ɠ����c�_������΂悢�B

\bigskip

�� $\circed{N} \equiv N_1$  �̎�\\

\[
\begin{array}{rcl}

\sharped{(\lambda^t x .N_1)} & \equiv & \sharped{(\lambda^t x . \mathsb{II}N_1)} \\

\end{array}
\]

$\mathsb{I}$ �͕��Ȃ̂ŏ�̂����ꂩ�Ɠ����c�_������΂悢�B

\bigskip

\end{proof}


\bigskip

\begin{thm}[]\label{teiri2}
CLt-�� $M$,$N$ �ɑ΂� $M$ $\rhd_{1wt}$ $N$ $\Rightarrow$
$\sharped{M} \rhd_{\beta} \sharped{N}$

\end{thm}

\begin{proof} (����)

 $M \rhd_{1wt} N$ �ɂ���
�g��ꂽ�K���� $(\mathsb{S'})$ �̎����l����.
���̂Ƃ� $M$ �� $\mathsb{S'}M_1M_2M_3M_4$ ���܂�ł���. �܂�
\[
\begin{array}{rcl}
  M &\equiv & \cdots (\cdots (\mathsb{S'}M_1M_2M_3M_4\cdots)\cdots)\cdots \\
\end{array}
\]

�Ƃ���킹��.����� $N$ �͂����ϊ��������́A�܂�
\[
\begin{array}{rcl}
  N &\equiv &\cdots (\cdots (M_1(M_2M_4)(M_3M_4)\cdots)\cdots)\cdots \\
\end{array}
\]
�Ƃ���킹��.
�����
\[
\begin{array}{rcl}
  \sharped{M} & \equiv & \cdots\sharped{} (\cdots \sharped{}(\sharped{(\mathsb{S'})}\sharped{M_1}\sharped{M_2}\sharped{M_3}\sharped{M_4}\cdots\sharped{})\cdots\sharped{})\cdots\sharped{} \\
  & \equiv & \cdots\sharped{} (\cdots \sharped{}((\lambda xyzu.x(yu)(zu))\sharped{M_1}\sharped{M_2}\sharped{M_3}\sharped{M_4}\cdots\sharped{})\cdots\sharped{})\cdots\sharped{} \\
  & \rhd_{\beta} & \cdots\sharped{} (\cdots \sharped{}(\sharped{M_1}(\sharped{M_2}\sharped{M_4})(\sharped{M_3}\sharped{M_4})\cdots\sharped{})\cdots\sharped{})\cdots\sharped{} \\
  & \equiv & \sharped{N} \\
\end{array}
\]

�g��ꂽ�ϊ��K�����ق��̏ꍇ�����l�ł���.

\end{proof}


\bigskip

�藝\ref{teiri1},�藝\ref{teiri2}�ƃ����_���̃`���[�`$\cdot$���b�T�[������ȉ��̂��Ƃ����藧�B
\bigskip

\begin{thm}[]
�����_�� $M$ �ɑ΂� 

\[
\begin{array}{rcl}
 M^* =_{\alpha} (\sharped{(\overline{\circed{M}})})^*
\end{array}
\]

�����藧�B

\end{thm}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{$\beta$ ���K�`�̋��܂鑬�x}


��L�̕��@��p���� $\beta$ ���K�`�����߂�Ƃ��A���ۂɕ��ʂɋ��߂�̂Ɣ�r���Ăǂꂭ�炢��������̂��A��L�̕��@���s�� C �v���O�������쐬���Č��؂��Ă݂�.
���̃v���O�����y�у}�j���A���͈ȉ��̃y�[�W�ɂ̂��Ă����\��ł���.

http://www.math.s.chiba-u.ac.jp/$\tilde{\,\,\,}$04um0304/

���̃v���O�����ł̓����_���y��CLt-���� tree �^�̃O���t�Ƃ��Ĉ����Ă���.�܂�CLT-���ɕϊ����ċ��߂�ꍇ�̍Ō�� $\beta$-���_�N�V�����ɂ��ẮA���ڋ��߂�ꍇ�Ɠ����֐���p���Čv�Z���Ă���.�܂�����̎��͕K�� $\alpha$ �ϊ����s���悤�ɍ���Ă���A�������񂵂ɂ����肹���ɍŌ�܂ōs���Ă��玟�ɐi�ނ悤�ɂ��Ă���.

\begin{ex}[���s��1]

$ (\lambda x y z . x z(y z))(\lambda x y . y)(u u)$
�� $\beta$ ���K�`�����߂Ă݂�

�ȉ��v���O�����̓��o�͂ł���.


$>$ (lambda x y z . x z (y z))(lambda x y . y)(u u);\\
-------------------kekka----------------------\\
(lambda x . u u x)\\
0 SEC\\
chokusetu:(lambda x . u u x)\\
0 SEC\\
----------------------------------------------\\

---kekka--- �ȍ~���v���O�����̏o�͂ł���B�܂� SEC �� $\beta$ ���K�`�����߂�܂łɂ����������Ԃł���ACLt-���ɂȂ����ċ��߂���@��CLt���ɕϊ����s���Ƃ��납�� $\beta$ ���K�`�����߂�܂łɂ����������Ԃł���.
�܂������_�ȉ��͐؂�̂ĂĂ���.�m���ɒ��ڋ��߂���@�� $=_{\alpha}$ �ƂȂ��Ă��邱�Ƃ��킩��.\\
�܂����̃����_���ɂ� $\eta$ -redex ���܂܂�Ă��邪 $\eta$ ���_�N�V�����͍s���Ă��Ȃ����Ƃ��킩��. \\
�Ȃ�$\eta$ ���_�N�V�����Ƃ͈ȉ��̂悤�Ȃ��̂ł���]���Ȓ��ۂ���������Ӗ�������
\[
\begin{array}{rcl}
(\lambda x . Mx) & \rhd_{\eta} & M (x \notin FV(M)) \\
\end{array}
\]

\end{ex}

\bigskip

\begin{ex}[�����_���ɂ�����Q�i�v�Z�̑����Z] 
���̌��؂Ɏg�p������̂�$2004$�N�x�̏C�m�_���u�����_�v�Z�ɂ�����Q�i�v�Z�v(\cite{ooie}�Q��)���A���Z���s�������_�����A���̃����_�������������͂ɑ΂��������������ǂ����Ƃ����m�F�����߂āA�g�p�����Ă��������܂���.�ȉ��ɊȒP�ɂ��̒�`���Љ�܂�\\
\end{ex}

��{�I�ȃ����_����
���� $n$ �̂Q�i�\�L�������_���ŕ\�������͈̂ȉ��̂悤�ɒ�`����.

\begin{df}[�^�U�l] \em \
�����_�� $T, F$ �����̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcll}
T & \equiv & \lambda x y . x \\
F & \equiv & \lambda x y . y \\
\end{array}
\end{equation*}

$T, F$ �����̂悤�ɒ�߂邱�ƂŁA�����_�� $LMN$ �ɑ΂��āA$L$ �� $T$ �̏ꍇ�� $M$�A$L$ ��$F$ �̏ꍇ�� $N$ �Ƃ��邱�Ƃ��ł���B

\end{df}

\begin{df}[1���̐�] \em \
���� $1, 0, -1$ �ɑΉ����郉���_��
$\nnum{1}, \nnum{0}, \nnum{-1}$ �����̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcll}
\nnum{1} & \equiv & \lambda x y z . x \\
\nnum{0} & \equiv & \lambda x y z . y \\
\nnum{-1} & \equiv & \lambda x y z . z \\
\end{array}
\end{equation*}

\end{df}

\bigskip

\begin{df}[���̕\��] \em \
���� n �����̂悤�ɕ\����Ƃ���B

\begin{center}
$n$ = $2^i * x_i$ + $2^{i-1} * x_{i-1}$ + $2^{i-2} * x_{i-2}$ + \dots + $2^0 * x_0$ \quad $i \ge 0$ \\
$x_j$ ($0 \le j \le i$) �� 1 �܂��� 0 �܂��� $-1$
\end{center}

���̐��� n �ɑΉ����郉���_�� $\num{n}$ �����̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcll}
\num{n} & \equiv & <\dots<<<\num{0}, \num{x_i}>, \num{x_{i-1}}>, \num{x_{i-2}}>, \dots >, \num{x_0}>
\end{array}
\end{equation*}

�������A$x_k$ ($0 \le k \le i$) ���� $x_i$ �ɂ͘A������ $\num{0}$ ������Ȃ����ƁA�܂�
$x_k$ �ɂ� $\num{1}$ �� $\num{-1}$ �������ɂ͌���Ȃ����ƂƂ���B
�܂� $<M,N>$ �͑΂�\���Ă���ȉ��̂��̂̏ȗ��\���Ƃ��ėp���Ă���.

\begin{equation*}
Pair \defeq \lambda x . x M N \quad M, N �̓����_��
\end{equation*}

\end{df}

\bigskip

\begin{df}
$\nnum{1}, \nnum{0}, \nnum{-1}$ �̏ꍇ�� $\nnum{0}$�A
$\num{n} = <M, N>$ �̏ꍇ�� $M$ ��Ԃ��悤�ȃ����_�� $Hdr$ �����̂悤�ɒ�߂�B
\begin{equation*}
\begin{array}{rcll}
Hdr & \defeq & \lambda x . (Isn \, x) \quad \nnum{0} \quad (x K)
\end{array}
\end{equation*}
�܂��A$\nnum{1}, \nnum{0}, \nnum{-1}$ �̏ꍇ�͂��̂܂܁A$\num{n} = <M, N>$ �̏ꍇ�� $N$ ��Ԃ��悤�ȃ����_�� $Ftr$ ��
���̂悤�ɒ�߂�B
\begin{equation*}
\begin{array}{rcll}
Ftr & \defeq & \lambda x . (Isn \, x) \quad x \quad (x(K I))
\end{array}
\end{equation*}
\end{df}

\bigskip

\begin{thm}
$\nnum{1}, \nnum{0}, \nnum{-1}$ �̏ꍇ�ɂ� $T$�A
�΂̏ꍇ�ɂ� $F$ ��Ԃ��悤�ȃ����_�� $Isn$ ��
���̂悤�ɒ�߂���B
\begin{equation*}
\begin{array}{l}
Isn = \lambda x . x K^3_3 K K I F T \\
 x �ɂ͔C�ӂ̃����_������́B
\end{array}
\end{equation*}

������ $K^3_3 \equiv \lambda xyz.z$ �ł���.
\end{thm}

\bigskip

\begin{df}[]
1���̐����m�����Z�������ʁA�J��オ��̒l��Ԃ������_�� $Add_1$ �ƁA
�J��オ���؂�̂Ă��l��Ԃ������_�� $Add_2$ ���ȉ��̂悤�ɒ�߂�B

\begin{equation*}
\begin{array}{rcrccc}
Add_1 & \defeq & \lambda x y z. x \, (y & (z \, \nnum{1} \, \nnum{1} \, \nnum{0}) & (z \, \nnum{1} \, \nnum{0} \, \nnum{0})  & \nnum{0}                              )   \\
      &        &                     (y & (z \, \nnum{1} \, \nnum{0} \, \nnum{0}) & \nnum{0}                               & (z \, \nnum{0} \, \nnum{0} \, \nnum{-1} ))  \\
      &        &                     (y & \nnum{0}                              & (z \, \nnum{0} \, \nnum{0} \, \nnum{-1}) & (z \, \nnum{0} \, \nnum{-1} \, \nnum{-1})) \\
\\
Add_2 & \defeq & \lambda x y z. x \, (y & (z \, \nnum{1} \, \nnum{0} \, \nnum{1}) & (z \, \nnum{0} \, \nnum{1} \, \nnum{0})  & z                                    )   \\
      &        &                     (y & (z \, \nnum{0} \, \nnum{1} \, \nnum{0}) & z                                     & (z \, \nnum{0} \, \nnum{-1} \, \nnum{0} ))  \\
      &        &                     (y & z                                    & (z \, \nnum{0} \, \nnum{-1} \, \nnum{0}) & (z \, \nnum{-1} \, \nnum{0} \, \nnum{-1})) \\
\end{array}
\end{equation*}

�Ȃ���ɂ����āA $x$ �͌J��オ��A$y, z$ �͉��Z���鐔������킵�A
���ꂼ�� $\nnum{1}, \nnum{0}, \nnum{-1}$ ����́B

\end{df}

�����̒�`��p���āA�����_�� $\num{n_1}, \num{n_2}$ �����Z���郉���_�����ċA�I�ɒ�`����B

\begin{df}[]
�J��オ�肨���2�̃����_�� $\num{n_1}, \num{n_2}$ �����Z�������ʂ�Ԃ������_�� $Add^*$ �����̂悤�ɒ�߂�B

\begin{quote}
$Add^* = \lambda x y z .$ \\
\q ($Isn$ $y$) \\
\q\q (($Isn$ $z$) \\
\q\q\q ($Pair$ ($Add_1$ $x$ $y$ $z$) ($Add_2$ $x$ $y$ $z$)) \\
\q\q\q ($Pair$ ($Add^*$ ($Add_1$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)) ($Hdr$ $y$) ($Hdr$ $z$)) \\
\q\q\q\q ($Add_2$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)))) \\
\q\q ($Pair$ ($Add^*$ ($Add_1$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)) ($Hdr$ $y$) ($Hdr$ $z$)) \\
\q\q\q ($Add_2$ $x$ ($Ftr$ $y$) ($Ftr$ $z$)))

$x$ �͌J��オ���\�������_�� $\nnum{1}, \nnum{0}, \nnum{-1}$ �ŁA$y, z$ ��
�����_�� $\num{n_1}, \num{n_2}$�B

\end{quote}
\end{df}

\bigskip

\begin{df}
2�̃����_�� $\num{n_1}, \num{n_2}$ �����Z���郉���_�� $Add$ �����̂悤�ɒ�߂�B

\begin{equation*}
Add \defeq Add^* \, \nnum{0}
\end{equation*}

\end{df}

\bigskip

\begin{ex}[]
�ȏ�̃����_����p����
\begin{enumerate}
\item\label{e1} $ \nnum{1} + \nnum{1}$, 
\item\label{e2} $ <\nnum{1}, \nnum{1}> + <<\nnum{1}, \nnum{0}>, \nnum{0}> $, 
\item\label{e3} $ <<<<<<<\nnum{1},\nnum{0}>,\nnum{-1}>,\nnum{1}>,\nnum{0}>,\nnum{0}>,\nnum{-1}>,\nnum{1}>$ \\ 
$+$\\ 
$ <<<<<<<<<<\nnum{1},\nnum{-1}>,\nnum{0}>,\nnum{-1}>,\nnum{1}>,\nnum{1}>,\nnum{1}>,\nnum{0}>,\nnum{-1}>,\nnum{-1}>,\nnum{0}>$

\end{enumerate}
�̌v�Z���s���Ă݂�.������\ref{e3}�Ɋւ��Ă͒��ڋ��߂���@�ł͌v�Z�ɂ��Ȃ�̎��Ԃ�������Ǝv����̂ōs���Ă��Ȃ�.
�ȉ������̏o�͂ł���.
���������͂ɂ����� $N1,N0,Nm1$ �͂��ꂼ��  $\nnum{1}, \nnum{0}, \nnum{-1}$������킷

\begin{enumerate}

\item

$>$ Add N1 N1; $\cdots$����\\
-------------------kekka----------------------\\
(lambda x . x (lambda x y z . x) (lambda x y z . y))\\
0 SEC\\
chokusetu:(lambda x . x (lambda x y z . x) (lambda x y z . y))\\
27 SEC\\
----------------------------------------------\\
$>$ \\


\item
$>$ Add (lambda x . x N1 N1)(lambda x . x (lambda x . x N1 N0)N0); $\cdots$����\\
-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . x))\\
0 SEC\\
chokusetu:(lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . x))\\
536 SEC\\
----------------------------------------------\\
$>$ \\

\item
$>$ Add\\
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x N1 N0)Nm1)N1)N0)N0)Nm1)N1)\\
(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x(lambda x.x N1 Nm1)N0)Nm1)N1)N1)N1)N0)Nm1)Nm1)N0); \\
$\cdots$����\\
-------------------kekka----------------------\\
(lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x . x (lambda x y z . y) (lambda x y z . x)) (lambda x y z . z)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x)) (lambda x y z . x)) (lambda x y z . y)) (lambda x y z . z)) (lambda x y z . y)) (lambda x y z . y)) (lambda x y z . x))\\
3 SEC\\
----------------------------------------------\\
$>$ \\


\end{enumerate}

�v�Z���̂͐������s���Ă���̂ő����Z�Ɋւ��Ă͐�������`����Ă���悤�ł���.
�܂�\ref{e1},\ref{e2} ����킩��悤�ɒ��ڋ��߂�������炩�ɑ������܂��Ă��邱�Ƃ��킩��.���̂悤�ɍċA���g���Ă����肷�郉���_���Ɋւ��Ă�,���ڋ��߂�������Ȃ葁�����߂邱�Ƃ��ł������ł���.

\end{ex}


\section{�I����}

����̌��ʂɂ��ẮA���K�`�����߂鑬�x�ɂ��Ă��Ȃ�̍����łĂ��܂��Ă��邪�A�Ȃ������܂ō����ł邩�����_�I�ɉ𖾂��鎖���܂��ł��Ă��Ȃ��A����č���̉ۑ�Ƃ��ẮA���̍������܂�邱�Ƃ𗝘_�I�ɉ𖾂��鎖����������B\\

�܂��A�����_�v�Z�ɂ����čċA���`���邽�߂ɕK�v�ȃ����_���Ƃ��� $Y$ �R���r�l�[�^�Ƃ������̂�����.���ۂɍ��񌟏؂ɗ��p�����Q�i���̑����Z���s�������_�����ċA������̂�,���� $Y$ �R���r�l�[�^���g���Ă���.���̘_���ł� $Y$ �R���r�l�[�^�Ɋւ���ϊ��K�����`���Ă��Ȃ��̂���, $Y$ �R���r�l�[�^�Ɋւ���K���� CLt���̕ϊ��K���ɉ����Ă��΂���Ɍ����悭���߂邱�Ƃ��ł������ł���.\\

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newpage

\section{�ӎ�}

�{�_���쐬�ɂ�����A�w�������̌ÐX�Y��搶�A�Ȃ�тɌÐX�������̊F�l��
����Ȃ����͂𒸂��܂������Ƃ�S���犴�ӂ������܂��B

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{9}
\bibitem{kleene} S.C.Kleene,�uProof by Cases in Formal Logic�v ,\\ The Annals of Mathematics, 2nd Ser., Vol.35,No3(Jul,1934)529-544, P537�̒藝6V
\bibitem{komori} ��t��w���w��2005�N�x�@�O����񐔊w1 �z�z���� �ÐX�Y�꒘
\bibitem{ooie}  ��t��w���R�Ȋw������2004�N�x�C�m�_��, \\��ƍK�q,
�u�����_�v�Z�ɂ�����Q�i�v�Z�v\\
http://www.math.s.chiba-u.ac.jp/$\tilde{\,\,\,}$komori/masters\_thesis/2004
\bibitem{kyoukasho} �������q, �u�v�Z�_ -�v�Z�\���ƃ����_�v�Z-�v�ߑ�Ȋw�� 1991
 
\end{thebibliography}

\end{document}
