🚀 go-pugleaf

$@>.NS(J@$@N6C+Bg3X$G$9!#(J

In article <SHINGO.92Dec5092048@ipc02.rtri.or.jp> shingo@ipc02.rtri.or.jp (Shingo MATSUMOTO) writes:

 |In article <SATOSHI.92Dec4174129@whale.math.ryukoku.ac.jp> satoshi@whale.math.ryukoku.ac.jp (Satoshi Kobayashi) writes:
 |>    |$@!tGSCfN'$h$j$b!"9=@.E*$H$$$&35G0$KD>@\7k$SIU$$$F$$$k$h$&$K;W$&!#(J
 |
 |>   $@!VGSCfN'$h$j$b!W(J$@7k$SIU$$$F$$$k$+$I$&$+$O$h$/$o$+$j$^$;$s$,!#;d$O!VGSCf(J
 |>   $@N'$r;H$o$J$$$3$H!W$OA4$/K\<AE*$J$3$H$@$H(J$@;W$$$^$9$N$G!#Hs9=@.E*$J86M}$H(J
 |>   $@$7$FIaDL$N?t3X<T$K$b$h$/CN$i$l$F$$$k$b$N$K$O!"Nc$($PA*Br8xM}$N$h(J$@$&$J8x(J
 |>   $@M}$,$"$j$^$9$,!"$=$s$J6/$$86M}$r;}$A=P$5$J$/$F$b!"GSCfN'$r;H$C$?$@$1$G(J
 |>   $@Hs9=@.E*$JB8(J$@:_DjM}$,4JC1$KF3$1$F$7$^$$$^$9$+$i!#(J
 |
 |  $@$J$k$[$I!#$=$l$O$=$&$G$9$M!#(J
 |  $@$?$@!"GSCfN'$,0l<!E*$H$$(J$@$&$h$j$O!"5"G<E*$H$+!"$=$A$i$N9M$($N$[$&$,0l<!E*(J
 |$@$G!"GSCfN'$O$=$&$$$&9M$(J}$+$iFs<!E*$K=P$F$/$k$N$G(J$@$O$J$$$+$H;W$C$?$b$N$G$9(J

$@$J$k$[$I!#$=$&$$$&$3$H$G$7$?$i!"5$;}$A$O$h$/$o$+$j$^$9!#$H$$$&$+!"$b$C(J
$@$H$b(J$@$@$H;W$$$^$9!#MW$9$k$K!"$"$k>r7o$rK~$?$9$b$N$NB8:_$,>ZL@$5$l$k$N$K!"(J
$@$=$l$r6qBNE*$K5a$a$kJ}K!(J($@Nc$($P!"(J$@<+A3?t$r5a$a$k$N$J$i!"$=$l$rCM$H$7$F(J
$@M?$($F$/$l$k$h$&$J5"G<E*4X?t$N$h$&$J$b$N(J)$@$,<($;$J$$!"$H$$$&$h$&$J(J$@>u67(J
$@$O5$$K$/$o$J$$!"$H$$$&$N$,9=@.E*?t3X$N=PH/E@$J$s$G$9$M!#$=$3$+$i!"$=$l(J
$@$G$O$=$&$$$&Hs9=@.E*$JB8:_(J$@>ZL@$r$7$J$$$h$&$K$9$k$K$O!"O@M}$r$I$N$h$&$K(J
$@JQ99$7$J$1$l$P$J$i$J$$$+!"$r9M$($?=j!"GSCfN'$N6X;_$H$$$&(J$@$3$H$,=P$F$-$?(J
$@$o$1$G$9!#$@$+$i!"(JP or not P $@$N7A$r$7$?O@M}<0$G$b!"9=@.E*$J4QE@$+$i8+(J
$@$F5v$5$l$k$h$&$J(J$@$b$N$O;H$($k$h$&$K$J$C$F$^$9$7$M!#Nc$($P!"(Jm,n $@$,<+A3?t(J
$@$N>l9g!"(Jm = n or not m = n $@$N$h$&$K!#(J

$@5U$K!"GS(J$@CfN'$5$(;H$o$J$1$l$P9=@.E*$H8@$($k$+!"$H$$$&$H!"$=$l$G$$$$$+$I(J
$@$&$+$O5DO@$NM>CO$,$"$k$H;W$$$^$9!#(J

 |$@$+$i!#(J $@7h$7$FGSCfN'$r$D$+$o$J$/$F$b!"9=@.E*$JM}O@$,$"$k$H$$$&0UL#$G$$$C$?(J
 |$@$N$G$O$"$j$^$;$s!#$4MF<O2<(J$@$5$$!#(J

$@$$$d!"JL$K$4MF<O$H$+$J$s$H$+8@$o$l$J$/$F$b!#JL$K;d$O$*$3$C$F$k$o$1$G$b(J
$@2?$G$b$J$$$G$9$+$i!#(J

 |>   $@!V=g=x?t$N9=@.!W$K$D$$$F$O!">>K\$5$s$,$I$&$$$&$3$H$r;X$7$F8@$C$F$*$i$l(J
 |>   $@$k$N$+!"$h$/$o$+$i(J$@$J$$$N$G!"2?$H$b8@$($^$;$s!#(JOrdinal diagram $@$_$?$$$J(J
 |>   $@$b$N$r8@$C$F$$$k$N$G$7$g$&$+!"$=$l$H$b9=@.(J$@E*=g=x?t$N$h$&$JOC$J$N$G$7$g(J
 |>   $@$&$+!#(J
 |
 |  $@$=$l$O!"<B$OITJY6/$G!"<ALd$7$h$&$+$J$H;W$C$F$$$?$N$G(J$@$9$,!#(J(^^;)
 |  Gentzen$@N.$N>ZL@O@$GMQ$$$k(JOrdinal diagram$@$G$$$&=g=x?t$O!"9=@.E*$J=g=x?t$H(J
 |$@$O8B$i$J$$(J$@$N$G$7$g$&$+!#(J($@$=$b$=$b!"!V9=@.E*!W$JJ}K!$G5v$5$l$kD68B5"G<K!$H(J
 |$@$$$&$N$O!"$$$o$f$k9=@.E*=g=x?t$ND68B(J$@5"G<K!$+$H!"C1=c$K9M$($F$$$?$b$N$G!#(J)

$@$&!<$s!"<B$OC]Fb@h@8$N(J Ordinal diagram $@$O;d$b$h$/M}2r$7$F$$$J$$(J$@$N$G!D!#(J
$@$:$C$H@N$KJY6/$7$h$&$H$7$F!"$/$8$1$F$7$^$$$^$7$?$+$i!#(J($@$=$N;v$r$"$k@h(J
$@@8$KOC$7$?$i!"!V$"$s$J(J$@$N$o$+$i$J$/$F$$$$$G$9!W$H8@$o$l$F$7$^$C$?!#(J)

$@$G$b!"0l1~!"C]Fb@h@8$H$7$F$O!"M-8B$NN)>l$K4p$E$$$F$"$"(J$@$$$&=g=x?t$N(J 
notation $@$r:n$i$l$?$D$b$j$J$N$@$+$i!"9=@.E*$JN)>l$G<u$1F~$l$i$l$kD68B(J
$@5"G<K!$r9M$($F$$$k(J$@$N$@!"$H$$$&$D$b$j$J$N$G$7$g$&$M$(!#(J

$@$7$+$7!"9=@.E*$G$"$m$&$,$J$+$m$&$,!"$H$K$+$/2?$i$+$NJ}K!$G!"E,Ev(J$@$KBg$-(J
$@$J=g=x?t$^$G$ND68B5"G<K!$r3NN)$7$F$7$^$$!"$=$l$rMQ$$$F!"(Jcut
elimination procedure $@$NDd;_@-$rO@(J$@$:$k$H$$$&$d$jJ}$N>ZL@O@$b$"$k$O$:$G(J
$@$9!#$J$K$b!"M-8B$NN)>l$K4p$E$/>ZL@O@$@$1$,>ZL@O@$G$O$J$$$N$G$9$+(J$@$i!#(J
($@$=$l$K!"M-8B$NN)>l$H$O0lBN2?$+!"$H$$$&$N$O!"$"$^$j$O$C$-$j$7$F$^$;$s!#(J)

$@!V9=@.E*!W$JJ}K!$G5v$5(J$@$l$kD68B5"G<K!$,$I$N$h$&$J$b$N$G$"$k$+$K$D$$$F$O!"(J
$@?M$K$h$C$F9M$(J}$,0c$C$F$/$k$G$7$g$&$7!"4JC1$KEz$((J$@$,=P$k$h$&$J$b$N$G$O(J
$@$J$$$G$7$g$&!#$3$&$$$&OC$O$H$F$bFq$7$$$N$G!"$G$-$l$P!"$3$3$GBG$A@Z$j$?(J
$@$$$G$9!#(J

$@;d$H$7$F$O!"=g=x?t$h$j$O!"(J($@$=$l$H?<$/4X78$7$F$$$^$9$,(J) inductive
definition $@$K6=L#$r;}$C$F$$$^$9!#(Jinductive $@$KDj5A$5$l$?=R8l$H$+!"=89g!"(J
$@7?$J$I$,$"$k$H!"$=$l$KIU?o$7$F$=$N>e$N(J($@D68B(J)$@5"G<K!$H$$$&$N$,F3F~(J$@$5$l$^(J
$@$9!#$3$l$O!"=g=x?t$K$D$$$F$ND68B5"G<K!$H$O0c$&(J($@$"$k0UL#$G$O0lHL2=(J)$@$N$G(J
$@$9$,!"=g=x?t$K$D$$$F$ND6(J$@8B5"G<K!$h$j$b!"9=@.E*?t3X$G$O=EMW$G$"$k$h$&$K(J
$@;W$$$^$9!#>/$J$/$H$b!"9=@.E*%W%m%0%i%_%s%0$G$OLr$KN)$D(J$@$_$?$$$G$9!#EvA3(J
$@$J$,$i!"7W;;$NDd;_@-$K?<$/4X78$7$F$^$9!#(J

 |$@!tCJ!9$H!"4pACO@9V:B$N$h$&$JOC$K$J$C$F$7(J$@$^$C$?!#(J(^^;)

$@$[$s$H(J :-)
--
			$@N6C+Bg3XM}9)3XIt?tM}>pJs3X2J(J    $@>.NS(J  $@Ao(J
			satoshi@whale.ryukoku.ac.jp
			0775-43-7523($@3X2J;vL3<<(J) 0775-43-7528($@8&5f<<(J)
			0775-43-7524(FAX)