🚀 go-pugleaf

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

In article <TANABE.93Mar9132043@Polaris.ai.cs.Fujitsu.Co.JP> tanabe@ai.cs.Fujitsu.Co.JP (Yoshinori TANABE) writes:

 |$@EDJU(J> $@$3$N(Jd$@$O(JAFA$@$NMW7o$r$_(J$@$?$9$h$&$K;W$$$^$9!%(J
 |
 |$@$^$G$O$$$$$H$7$F!$(J

$@$3$3$^$G$O$$$$$G$9$M!#$7$+$7!"(J

 >$@$J!<$k$[$I!%$8$c$"!$=8(J$@9gB2(JF={a_r|r$@$O<B?t(J}$@$G!$(J
 >	a_r \in a_s   iff  r > s
 >(\in$@$O!VB0$9$k!W$N5-9f$N$D$b$j$G$9!%$D$$$G$K$$$&(J$@$H!V(J_$@!W$O$=(J
 >$@$N<!$NJ8;z$rE:;z$@$H;W$C$F$/$l$H$$$&$D$b$j$G$9!%(J) $@$rK~$?$9!%(J
 >$@$J$s$F$N$b$"$j$J$s$@!%$H(J$@0l=V;W$C$?$s$G$9$,!$$A$g$C$H<ALd$5$;(J

$@$N(J iff $@$H$$$&$N$,@.$jN)$C$F$/$l$J$/$F!"(J
	a_r \in a_s   if  r > s
                      ^^
$@$7$+@.$jN)$?$J$$$s$G$9$M!#$=$l$r(J iff $@$,8@$($k$h$&$K$9$k$?$a$K$O!"3{$5(J
$@$s$,(J$@$d$C$?$_$?$$$J$d$d$3$7$$$3$H$r$7$J$$$H$$$1$J$$$o$1$G$9!#(J

 |$@EDJU(J> $@$9$k$H!$(Jd$@$N0l0U@-$+(J
 |$@EDJU(J> $@$i!$(JAFA$@$O$`$7$m(JF$@$N$h$&$J$b$N$NHsB8:_$r<gD%$7$F$$$k!%(J
 |
 |$@$H$$$&$N$,8m$j$G$3$3$GHsB8:_$,$o$+$k$N$O(J
 |	  $@=89g(J$@B2(J{b_r|r$@$O<B?t(J}$@$G!$(Jb_r={b_s|s$@$O(Jr$@$h$jBg$-$J<B?t(J}
 |	  $@$H$J$k$b$N(J
 |$@$G$7$?!%!J:#EY$O9g$C$F$$$FM_$7$$$J$"(J$@!%!K(J

$@$$$$$(!"$3$&$$$&$N$bB8:_$7$^$9!#<B:]!"A0$K=q$+$l$F$$$?$h$&$K!"<B?t$N=8(J
$@9g$H$=$N>e$NBg>.4X78$rAH(J$@$K$7$?$b$N$r%0%i%U$H$7$F$H$C$F(J AFA $@$rE,MQ$9$l(J
$@$P$9$0:n$l$k$o$1$G$9!#(Jd$@$N0l0U@-$,LdBj$K$J$k$H;W$o$l$?$h(J$@$&$G$9$,!"(Jd $@$N(J
$@0l0U@-$H$$$&$N$O!"%0%i%U$r0l$D8GDj$7$?;~$K!"$=$l$KBP$7$F(J d $@$,$A$g$&$I(J
$@0l8D$@$1B8:_$9$k(J$@!"$H$$$&$3$H$G!"%0%i%U$,$?$/$5$s$"$k$N$O9=$o$J$$$N$G$9!#(J
b_r $@$H$7$F$O!"(Jx = {x} $@$rK~$?$9$?$@0l$D$N=89g(J x ($@$3$l$OIaDL(J\Omega $@$H$$(J
$@$&L>A0$G8F$P$l$F$$$^$9!#(J) $@$r$H$C$F!"(Jb_r = x ($@$9$Y$F$N(J r $@$K$D$$$F(J)$@$H$9(J
$@$l$P$$(J$@$$$G$9!#(J

$@$3$NJU$N$D$C$3$s$@OC$O!"$d$O$j(J Aczel $@$NK\$rFI$s$G$b$i$C$?$[$&$,$h$$$+(J
$@$H;W$$$^$9$,!"MN=q$J$N(J$@$G$9$0$K<j$KF~$i$J$$$+$H;W$&$N$G!";d$,JL$N5-;v(J
(Subject $@$,(J Situation Theory $@$K$J$C$F$k$d$D(J)$@$G>R2p$7$?(J$@!V$&$=$D$-!W$H$$(J
$@$&K\$NBh(J3$@>O$r$H$j$"$($:$4$i$s$K$J$k$H$h$$$+$H;W$$$^$9!#?t3XE*$K?<$$Fb(J
$@MF$O=q$$$F$"$j(J$@$^$;$s$,!"7k9=$o$+$j$d$9$$@bL@$,$"$j$^$9!#(JAFA $@$K4X$7$F!"(J
$@$9$0<j$KF~$kF|K\8l$N2r@b(J($@$3$l$OLu$G$9$1$I(J)$@$H(J$@$$$&$N$O!"$3$l$/$i$$$7$+;d(J
$@$OCN$j$^$;$s!#K\20$G$OBgDqE/3X=q$NC*$K$"$k$H;W$$$^$9!#$"$N(J Barwise $@$,(J
$@=q$$(J$@$F$$$k$N$@$+$i!"$^$"!"$"$^$jJQ$J;v$O=q$$$F$J$$$H;W$$$^$9!#(J

$@!V$&$=$D$-!W$G$O!"(JAFA $@$N$3$H$r!"!V(JMostowski $@$N(J Collapsing Lemma $@$r!"%0(J
$@%i%U$,(J well-founded $@$H$$$&2>Dj$r$O$:$7$?7A$K3HD%$7$?$h$&$J$b$N$@!W$H$$(J
$@$&$h$&$J46$8(J($@$3$NDL$j$N=q$-J}$G$O$J$$(J)$@$G@bL@$7$F$$$^$7$?!#$3$l$O$A$g$C(J
$@$H8xM}E*=89gO@$rCN$C$F$$$k?M$K(J$@$O$o$+$j$d$9$$@bL@$@$H;W$$$^$9!#(J

$@$b$A$m$s!"(JAFA $@$G$O!"(JCollapsing Lemma $@$H0c$C$F!"%0%i%U$,(J extensional $@$@(J
$@$H$$$&2>Dj$rCV$+$J$$$N$G!"%0%i%U$,(J \in $@4X78$HF17?$K$J$k$H$O8B$i$J$$$o(J
$@$1$G$9$,!"I,MW$J$i!"%0%i%U$r(J$@E,Ev$JF1CM4X78$G3d$C$F$D$V$7$F(J extensional 
$@$K$7$F$*$$$F$+$i$d$l$P$$$$$o$1$G$9!#$3$3$G!"E,Ev$H$$$C$?$N(J$@$O!"@53N$K$O!"(J
$@F1CM4X78$G3d$C$?;~$K(J extensional $@$K$J$k$h$&$J:G>.$NF1CM4X78$G3d$k$o$1(J
$@$G$9!#(J

$@$G!"<B?t(J$@$H$=$N>e$NBg>.4X78$r%0%i%U$H9M$($?;~!"$3$l$O(J extensional $@$G$J(J
$@$$$N$G$9$,!">e$G8@$C$?$h$&$K$7$F$D$V$7$F(J extensional $@$K$9$k$H!"(J1$@E@$H(J1
$@8D$N%k!<%W$@$1$+$i$J$k%0%i%U$K$J$j$^$9!#$3$&9M$($k$H!"(Jd $@$H$7$F!"A4$F$N(J
$@<B?t$K(J $@$5$C$-$N(J \Omega $@$rBP1~$5$;$k$b$N$r$H$l$P$h$$!"$H$$$&$3$H$OG<F@(J
$@$7$d$9$$$H;W$$$^$9!#(J

 |$@3{$5$s$N(J$@5DO@$r$A$g$C$H%b%G%#%U%!%$$9$l$P(J ZF-FA+AFA $@$G!$(J
 |
 |  $@A4$F$NM-8~%0%i%U(JG$@$KBP$7$F(J*$@C1<M(J* f:node(G)->V $@$G(J$@!$(Jnode(G)$@$N(J
 |  $@MWAG(Jx,y$@$KBP$7(J
 |    x$@$,(Jy$@$N;R@a(J   iff   f(x) \in f(y)
 |  $@$H$J$k$b$N$,B8:_$9$k!%(J
 |
 |$@$3$H$,>ZL@$G$-$k$h$&$G$9$M!%;d$O$3$l$GK~B-CW$7$^$7$?!%(J

$@$3$l$O3N$+$K>ZL@$G$-$k$H;W$$$^$9!#$5$C$-9M$($F(J$@$_$?$i4JC1$K$G$-$k$h$&$G(J
$@$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)