🚀 go-pugleaf

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

In article <RYU.92Nov9094836@sysipk.sys.titech.ac.jp> ryu@sys.titech.ac.jp (ryu) writes:

 | | |Ea = 1 $@$H$J$i$J$$$b$N$b4^$a$F9M$($k(J$@!"$F$3$H$OD>4Q<g5A$H$O4X78$J$$$s$G(J
 | | |$@$9$+!)(J
 | |
 | |$@4X78$"$j$^$;$s!#%V!<%kBe?tCM$N=89gO@$G$b!"(JEa = 1 $@$G$J$$$b$N(J
 | |$@$r4^$a$F9M$($k$3$H$K$J$j$^$9!#$b$C$H$b!"(JE $@=R8l$O8EE5O@M}$K4p(J
 | |$@$E$/=89gO@$G$O$"(J$@$^$j;H$o$l$J$$$N$G$9$,!#(J
 |
 |$@%V!<%kBe?tCM$N=89gO@$G$O&8$X$N<LA|$rItJ,=89g$H$7$F$H$i$($F$?$+$i!V(JEa =
 |1$@!W$H$J$i$J$$$b$N$O4X78$J$$$s$@$J!"$H;W$C$F$$$?$s$G$9$,!"(JV^$@&8$G$b$=$&(J
 |$@$J$s$G$7$g$&$+!)(J
 |$@$=$l$H$b(J$@!"$=$b$=$b$NA0Ds$,4*0c$$!)(J

$@$*$C$7$c$C$F$$$k$3$H$N0UL#$,$"$^$j$h$/$o$+$i$J$$$N$G$9$,!"MW$9$k$K;d$N(J
$@8@(J$@$$$?$$$3$H$O!"(JEa $@$,(J 0 $@$H$b(J 1 $@$H$b0[$J$k$b$N$r9M$($k$H$$$&$3$H<+BN$O!"(J
$@%Y!<%9$H$J$kO@M}$,8EE5O@M}$G$"$k(J$@$+!"D>4Q<g5AO@M}$G$"$k$+!"$H$$$&$3$H$H(J
$@$O4X78$J$$!"$H$$$&$3$H$G$9!#$=$b$=$b!"(JE $@$H$$$&$b$N<+BN!"JX59>e(J$@F3F~$5$l(J
$@$?$@$1$N$b$N$G!"$J$/$C$?$C$F$h$$$N$G$9!#$D$^$j!"(JV^(\Omega) $@$r;H$o$J$/(J
$@$?$C$F!"K\$N(J29$@%Z!<%8$G(J$@Dj5A$5$l$F$$$k(J U^(\Omega) $@$r;H$C$?$C$F$h$$$N$G$9!#(J
$@$^$?!"5U$K!"%V!<%kBe?tCM$N=89gO@$N$[$&$G$b!"(JE $@$rF3(J$@F~$7$F$b9=$o$J$$$G$9(J
$@$7!#C]Fb@h@8$NK\$G(J E $@$rF3F~$7$F$$$kM}M3$O!"AX$NM}O@$H$NBP1~4X78$r8+$d(J
$@$9$/$9$k$?(J$@$a$G$7$g$&!#(J

 | |$@$=$b$=$b!"(JIZF $@$NCf$G$O!"G;EY$K$D$$$F$N5DO@$O!"(JZFC $@$NCf$G$N$h(J
 | |$@$&$K4JC1$K9T$+$J$$(J$@$N$G!"8D?t$N35G0<+BN$,(JV^(\Omega)$@%b%G%k$NCf(J
 | |$@$G$OAjEv0c$C$?$b$N$K$J$C$F$$$k$H9M$($?$[$&$,$h$$$G$7$g(J$@$&!#(J
 |
 |$@G;EY$K$D$$$F$N5DO@$G$O!V0lHL$N%b%G%k!W$G$b$=$&$G$9$,!"$3$3$G;d$N$$$C$F(J
 |$@$$$k$N$O!VCM#1$r$H(J$@$i$J$$%U%)!<%_%e%i!W$O!"$d$C$Q$jL5;k$C$F$3$H$J$s$G$7$g(J
 |$@$&$+!"$H$$$&$3$H$G$9!#(J

$@!VL5;k!W$H$$$&8@MU$r(J$@$I$&$$$&0UL#$G;H$o$l$F$$$k$N$+$h$/$o$+$j$^$;$s$,!"(J
$@!VCM(J1$@$r$H$i$J$$(J formula $@!W$O!"@5$7$$(J formula $@$H$O9M(J$@$($^$;$s!#(J

 | | |$@@P86$5$s$N8@$&!V%U%!%8!<$J!W$C$F$$$&$N$K$&$^$$6q9g$KA46u4V$H$J$i$J$$%*!<(J
 | | |$@%W%s(J$@%;%C%H$,BP1~$7$F$?$iLLGr$+$C$?$N$K$J!"$C$F$$$&0UL#$G$9!#(J
 | |
 | |[a \in {x \in {0,1} | x = 0 and \phi}] $@$,A46u4V$K$b6u$K$b$J(J
 | |$@$i$J$$$3$H$,$"$k!"$H$$$&0UL#$G$OBP1~$7$^$9$h!#(J
 |
 |$@$@$+$i$=$l$O(J V^$@&8(J $@$N(J$@2?$KBP1~$7$F$$$k$N$G$7$g$&!)(J

$@C1$K!"Nc$($P(J [0 \in {x \in {0,1} | x = 0 and \phi}] $@$,(J(\phi $@$N$H$jJ}$K(J
$@$h$C$F$O(J)$@A46u4V$K$b6u$K$b$J$i$J$$$3$H$,$"$k!"$H8@$$$?$+$C$?$@$1$G$9!#(J

$@3^$5$s$N8@$$$?$+$C$?$3$H$O!"$R(J$@$g$C$H$7$F!"(J0 < [E{x \in {0,1} | x = 0
and \phi}] < 1 $@$H$J$C$F$$$?$iLLGr$+$C$?$N$K$J!"$H$$$&0UL#$J$N$G(J$@$7$g$&(J
$@$+(J? $@$7$+$7!"$=$&$$$&0UL#$@$H$7$?$i!"@P86$5$s$N$$$&!V%U%!%8!<$J!W$H$$$&(J
$@35G0$H$OD>@\4X78$"$j$^$;(J$@$s!#<B:]!"@P86$5$s$N$"$2$?(J($@%U%'%k%^!<M=A[$r(J
\phi $@$H$*$/(J)$@Nc$G$O!"(J[E{x \in {0,1} | x = 0 and \phi}] = 1 $@$G$9!#(J

 | | |$@;d$O!V2?$8$c%3%j%c!W$H;W$C$?$s$G$9$h!#(J
 | | |$@$@$C$F@5B'$JO@M}<0(JA$@$KBP$7$F!"0z?t$,!"!V@5(J$@$7$$!W=89g$@$C$?$i!"(J
 | | |[not A or A] = 1
 | | |$@$K$J$C$F$$$^$9$b$N!#(J
 | |
 | |$@$3$NJ8Cf$N!"!V@5B'$JO@(J$@M}<0!W!"!V0z?t!W!"!V!V@5$7$$!W=89g!W$H(J
 | |$@$$$&8@MU$,2?$r;X$7$F$$$k$N$+$o$+$j$^$;$s!#6H3&MQ8l$H$7$F$O(J$@J9(J
 | |$@$$$?$3$H$,$J$$I=8=$G$9!#!V@5B'!W$O(J wff, $@!V0z?t!W(J $@$O(J 
 | |parameter $@$N$3$H$+$7$i!#(J
 |
 |$@<:Ni$7$^(J$@$7$?!#(J
 |$@#4#3%Z!<%8$N2<$N$[$&$NOC$7$G$9!#(J
 |$@!V@5B'!W$O!V@55,!W$N4V0c$$$G!V0z?t!W$O%U%)!<%_%e%i$K8=$l$k(J$@!J@)8B$5$l$?!K(J
 |$@JQ?t$G!"!V@5$7$$=89g!W$OIaDL$N=89gO@$N1'Ch$+$i$NKd$a9~$_$G$9!#(J
 |$@!t$3$H$P$E$+$$$,%a%C(J$@%A%c$/$A$c!#(J

$@$J$k$[$I!#3N$+$K$=$&$$$&0UL#$G$7$?$i!"$*$C$7$c$kDL$j(J[not A or A] = 1$@$K(J
$@$J$j$^$9!#$H$$$&(J$@$N$O!"MW$9$k$K$=$&$$$&>l9g$K$O!"K\<AE*$K(J A $@$NCf$G$O!"(J
$@IaDL$N=89g$rKd$a9~$s$GF@$i$l$k=89g$K$7$+8@5Z$7$F(J$@$J$$$+$i$G!"=>$C$F!"Ia(J
$@DL$N(J V $@$NCf$G(J A $@$N0UL#$r9M$($k$N$HF1$8$K$J$C$F$7$^$&$+$i$G$9!#(J

 | | |$@$=$l$KHf(J$@$Y$?$i(J
 | | |$@!VG$0U$N(J A $@$K$D$$$F(J not(A) or not(not(A))$@!W(J
 | | |$@$J$s$F%I%*%C$F$3$H$J$$!"$H;W$$$^$;$s$+(J$@!)(J
 | |
 | |$@%I%*%C$F$3$H$"$j$^$9(J :-)$@!#(J $@$^$:$$(J principle $@$J$N$G$9$+$i!#(J
 |
 |$@$G$b#6%Z!<%8$N>ZL@$rFI$`8B(J$@$j!"$=$s$J$i$=$&$$$&Cf4VO@M}$r8&5f$7$?J}$,$^(J
 |$@$7$d$s!"$H;W$C$?$N$G$9!#(J

$@$=$&$$$&Cf4VO@M}$r8&5f$7$F$b(J$@$b$A$m$s$$$$$G$9$1$I$M!#$?$@!"$3$NK\$N<g;](J
$@$K$O9g$o$J$/$J$C$F$7$^$&$o$1$G$9!#(J

$@$G$b!"<B:]8@$C$F!"(J{0,1} $@$,0lHL$K40HwB+$K$J$i$J$$$H$$$&$N$O!"Bg$7$?LdBj(J
$@$G$O$J$$$G$9$1$I$M!#(J(V^({\Omega}))^({0,1}) $@$r:n$m$&$H(J$@$9$k$H%3%1$k!"$H(J
$@$$$&$"$?$j$GLdBj$K$J$k$@$1$N$3$H$G$9$M!#$3$NK\$N<g;]$+$i$9$l$P!"(J{0,1} 
$@$r??M}CM$N6u4V(J$@$K$H$C$F$bFC$KLLGr$$$3$H$O$J$$$N$G!"(J(V^({\Omega}))^({0,1})
$@$,:n$l$J$/$F$b$I$&$C$F$3$H$O$J$$$7!#(J

 | | |$@$@$+$i!VD>4Q<g5AE*=89gO@!W$O<B$O!VGSCfN)$NFHN)@-!W$J$N$+$bCN$l$J$$!"$J(J
 | | |$@$s$F;W$C$F$$$k$s$G$9$,(J$@!"E*30$l$G$7$g$&$+!)(J
 | |
 | |$@$3$3$G8@$o$l$F$$$k!VD>4Q<g5AE*=89gO@!W$H$$$&$N$O!"Nc$NK\$N$3(J
 | |$@$H$J$N(J$@$G$9$+(J?  $@$=$l$H$b!"(JV^(\omega) $@%b%G%k$N$3$H$G$9$+(J? 
 |
 |$@$b$A$m$s(J V^$@&8(J $@$N$3$H$G$9!#(J
 |$@$D$^$j$G$9$M!"(JV^$@&8(J $@$O$"$^$j(J ZF + LJ $@$NNI$$%b%G%k$G$O$J$$$J$"!"$H;W$C$?(J
 |$@$o$1$G$9!#(J

$@$(!<$H!"2f!9$N6H3&$G$O(J ZF $@$H=q$/(J$@$H!"$9$G$K$=$3$KGSCfN'$,F~$C$F$$$^$9$N(J
$@$G!"(JZF + LJ $@$H$$$&8@$$J}$OJQ$G$9!#$G!"$b$A$m$s!"(JV^(\Omega) $@$O(J ZF $@$N%b(J
$@%G%k$K$O0lHL$K$O$J$i$J$/$F!"(JIZF $@$N%b%G%k$G$9!#(J

 |$@!t2?$r$b$C$F!V8@$$!W$H$$$&$+$OFq$7$$$G$9$,!#(J

$@$^$"!"$=$&$G$9$M!#$G$b!"$=$N%b%G%k$r;H$C$F?'!9$JLLGr$$;v$,>ZL@$G$-$k$N(J
$@$J$i!"$^$"!"NI$$%b%G%k$H8@$((J$@$k$+$bCN$l$^$;$s!#(J

 |$@$=$l$G!"$I$&$;%U%)!<%7%s%0;H$&$N$J$i!VFHN)@-$N>ZL@!W$NJ}$,LLGr$$$s$H$A$c(J
 |$@$&$+(J$@$J!"$C$F$$$&;W$$$D$-$G$9!#(J

$@FHN)@-$N>ZL@$K$J$C$F$$$k$3$H$O3N$+$G$9!#$G$b!"GSCfN'$O!"$$$+$K$bFHN)$H(J
$@$$(J$@$&8xM}$J$N$G!"$=$l$,FHN)$@$H8@$($F$bFC$KLLGr$/$O$J$$$G$9!#$3$NK\$N<g(J
$@Bj$O!"$=$l$h$j$b!"(JHeyting-valued analysis (Boolean-valued analysis $@$N(J 
cHa version) $@$K$"$k$N$@$H;W$$$^$9!#FC$K!"(JCauchy-real $@$H(J Dedekind real 
$@$,0[$J$k$h$&$J%b%G%k$K6=L#$,$"$k$N$@$H;W$$$^$9!#(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)