🚀 go-pugleaf

$@EDJU!wIY;N(J$@DL@n:j9)>l(J $@$G$9!%(J

>>Message-ID: <SATOSHI.93Mar9193044@whale.math.ryukoku.ac.jp> $@$N5-;v$G(J, 
>>$@>.NS(J( satoshi@whale.math.ryukoku.ac.jp )$@$5$s(J:

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

$@$4$V$5$?$7$F$$$^$9!%(J

# $@$H8@$C$F(J$@$b3P$($F$$$i$C$7$c$i$J$$$+$bCN$l$^$;$s$,!$3XIt$N;~$K(J
# $@FqGH@h@8$N%<%_$G$*@$OC$K$J$j$^$7$?!%(J

In article <TANABE.93Mar9132043@Polaris.ai.cs.Fujitsu.Co.JP> tanabe@ai.cs.Fujitsu.Co.JP (Yoshinori TANABE) writes:
$@EDJU(J> $@$H$$$&$N$,8m$j$G$3$3$GHsB8:_$,$o$+$k$N$O(J
$@EDJU(J>     $@=89gB2(J{b_r|r$@$O<B?t(J}$@$G!$(Jb_r={b_s|s$@$O(Jr$@$h(J$@$jBg$-$J<B?t(J}
$@EDJU(J>     $@$H$J$k$b$N(J
$@EDJU(J> $@$G$7$?!%!J:#EY$O9g$C$F$$$FM_$7$$$J$"!%!K(J

$@>.NS(J> $@$$$$$(!"$3$&(J$@$$$&$N$bB8:_$7$^$9!#(J

$@$3$l$O;d$NI=8=$,ITE,Ev$G$7$?!%(J``$@=89gB2(J{b_r|r$@$O<B?t(J}''$@$NI=8=(J
$@$G(J``$@0[$J$k(Jr$@$KBP$9$k(Jb_r$@$O0[$J$k(J''$@$3$H$rI=$7$?$D$b$j$K$J$C$F$$(J
$@$^$7$?!%$G$9$+$i!$(J

$@>.NS(J> d$@$N0l0U@-$,LdBj$K$J$k$H;W$o$l$?$h(J$@$&$G$9$,!"(Jd $@$N(J
$@>.NS(J> $@0l0U@-$H$$$&$N$O!"%0%i%U$r0l$D8GDj$7$?;~$K!"$=$l$KBP$7$F(J d $@$,$A$g$&$I(J
$@>.NS(J> $@0l8D(J$@$@$1B8:_$9$k!"$H$$$&$3$H$G!"%0%i%U$,$?$/$5$s$"$k$N$O9=$o$J$$$N$G$9!#(J

$@$H$$$&$3$H$OM}2r$7$F$$$k$D$b$j$G(J$@$9!%(J

$@$G!$$/$I$$$G$9$,$"$i$?$a$F=q$-$^$9$H!$(JZF-FA+AFA $@$G!$(J

  $@<B?tA4BN$N=89g$rDj5A0h$H$9$kC1<M(Jb$@$G!$A4(J$@$F$N<B?t(Jr$@$KBP$7$F(J
  b(r)={b(s)|s$@$O(Jr$@$h$jBg$-$J<B?t(J}$@$r$_$?$9$b$N(J $@$OB8:_$7$J$$!%(J

$@$,@.$jN)$D$o$1$G$9$M!%(J

$@>.NS(J> $@;d$,JL$N5-;v(J
$@>.NS(J> (Subject $@$,(J Situation Theory $@$K$J$C$F$k$d$D(J)$@$G>R2p$7$?(J

$@$9$_$^$;$s!%$3$N5-(J$@;v$,8+Ev$?$i$J$$$N$G$9$,(J(fj.sci.math$@$G$9$h(J
$@$M!)(J)$@!$$b$7$h$m$7$+$C$?$i%a!<%k$G$G$bAw$C$FD:$1$^$;$s$+!)(J

$@>.NS(J> $@!V$&$=$D$-!W$G$O!"(JAFA $@$N$3$H$r!"!V(JMostowski $@$N(J Collapsing Lemma $@$r!"%0(J
$@>.NS(J> $@%i%U$,(J well-founded $@$H$$$&2>Dj$r$O$:$7$?7A$K3HD%$7$?$h$&$J$b$N$@!W$H$$(J
$@>.NS(J> $@$&$h$&$J46$8(J($@$3$NDL$j$N=q$-J}$G$O$J$$(J)$@$G@b(J$@L@$7$F$$$^$7$?!#(J

$@$J$k$[$I!%$3$l$O$o$+$j$d$9$$$G$9$M!%$G$9$,!$(J

$@>.NS(J> $@$b$A$m$s!"(JAFA $@$G$O!"(JCollapsing Lemma $@$H0c$C$F!"%0%i%U$,(J extensional $@$@(J
$@>.NS(J> $@$H$$$&2>Dj$rCV$+$J$$$N$G!"%0%i%U$,(J \in $@4X78$HF17?$K$J$k(J$@$H$O8B$i$J$$$o(J
$@>.NS(J> $@$1$G$9(J

$@$3$3$,$A$g$C$H$o$+$j$^$;$s!%(J``extensional''$@$H$$$&$N$O(J
Collapsing Lemma $@$K(J$@=P$F$/$k$d$D!$$D$^$j!$%0%i%U(JG$@$G(J
(x$@$,(Jy$@$N;R@a$G$"$k$3$H$r(JxGy$@$H=q$/$3$H$K$7$F!$(J)
  [$@A4$F$N(JG$@$N@a(Jx$@$K$D$$$F(J [xGa <-> xGb]] -> a=b
$@$,@.$jN)$D$3$H$G$9$+!)$@$H$9$k$H!$(J

$@>.NS(J> $@$G!"<B?t$H$=$N>e$NBg>.4X78$r%0%i%U$H(J$@9M$($?;~!"$3$l$O(J extensional $@$G$J(J
$@>.NS(J> $@$$$N$G$9$,!"(J

$@$H$N$3$H$G$9$,!$<B?t>e$NBg>.4X78$O(J extensional $@$K$J$k$H;W$$(J
$@$^$9$,!%(J


$@$D$$$G$K!J$?$@$N46A[$J$s$G$9$,!K=q$$$A$c$$$^$9$H!$(J

$@EDJU(J>   $@A4$F$NM-8~%0%i%U(JG$@$KBP$7$F(J*$@C1<M(J* f:node(G)->V $@$G!$(Jnode(G)$@$N(J
$@EDJU(J>   $@MWAG(Jx,y$@$KBP$7(J
$@EDJU(J>     x$@$,(Jy$@$N;R@a(J   iff   f(x) \in f(y)
$@EDJU(J>   $@$H$J$k$b$N$,B8:_$9$k!%(J
$@EDJU(J> $@$3$H$,>ZL@$G$-$k$h$&$G$9$M!%;d$O$3$l$GK~B-CW$7$^$7$?!%(J

$@$H(J$@=q$$$?$N$G$9$,!$!VK~B-$7$?!W$H$$$&$N$O<B$O$A$g$C$H13$G$7$F!$(J
AFA$@$N!V$9$Y$F$NM-8~%0%i%U!W$r!V$9$Y$F$N(Jextensional$@$JM-8~%0%i(J
$@%U!W$K!$!V!A$J$k(Jd$@$,0l0U$KB8:_$9$k!W$r!V!A$J$kC1<M(Jd$@$,0l0U$KB8(J
$@:_$9$k!W$K$=$l$>$lJQ(J$@$($?$b$N$NJ}$,0u>]E*$J$N$K$J$"!%$H;W$$$^(J
$@$7$?!%(J

$@L5L7=b$K$J$k$N$+$b$o$+$i$J$$$7!$$J$C$?$H$7$F$3$&JQ$((J$@$k$H1~MQ(J
$@>e$&$^$/$J$$$N$+$b$7$l$J$$$G$9$1$I!%(J

--
                      |        $@EDJU(J $@NIB'(J $@!w(J $@IY;NDL(J $@@n:j9)>l(J
                      |  E-mail: tanabe@ai.cs.fujitsu.co.jp