🚀 go-pugleaf

$@EDJU!wIY;NDL@n:j(J$@9)>l(J $@$G$9!%(J

>>Message-ID: <SHIMURA.93Mar10214412@octopus.cst.nihon-u.ac.jp> $@$N5-;v$G(J, 
>>$@;VB<(J( shimura@cst.nihon-u.ac.jp )$@$5$s(J:

$@;VB<(J> $@$3$3$G$$$&(J $@%0%i%U(J (G,R) $@$,(J extensional $@$G$"$k$H$O!"<!$N$3(J
$@;VB<(J> $@$H(J$@$@$H;W$$$^$9!#(J 
$@;VB<(J> a,b in G $@$N(J R $@$K$+$s$9$k(J $@?d0\E*JDJq$r$=$l$>$l(Jcl(a), cl(b)
$@;VB<(J> $@$H$7$?$H$-!"(J R $@$N(J cl(a), cl(b) $@$X$N@)8B$,(J"$@%0%i%U$H$7$F(J"$@F17?(J
$@;VB<(J> $@$J$i$P!"(Ja=b $@$G$"$k!#(J
($@N,(J)
$@;VB<(J> $@IaDL(J extensional $@$H(J$@$$$&$H$-$O!"(J{x : xRa}={x : xRb} $@$J$i$P(J
$@;VB<(J> a=b $@$r;X$9$H;W$&$N$G!"$3$N2r<a$N2<$G$O<B?t$N=89g$O(J 
$@;VB<(J> extensional $@$@$1$l$I$b!"%0%i%U$H$7$F$O$=$&$G$O$J$$$H$$$&$3(J
$@;VB<(J> $@$H$G$7$g$&!#(J

$@$J$k$[$I$J$k$[$I!%(J

$@$H8@$C$H$$$F$J$s$G$9$,!$MQ8l$N3NG'$r$5$;$F2<$5$$!%(J

(1) cl(a)$@$H$$$&$N$O(J
	x_0 = {a}
	x_(n+1) = {b \in G | bRy $@$J$k(J y \in x_n $@$,$"$k(J}
$@$HCV$$$?;~$N(J \bigcup{x_n | n $@$O<+A3?t(J} $@$N$3$H$G$9$M!%(J

(2) (G_1,R_1)$@$H(J(G_2,R_2)$@$,%0%i%U$H$7$FF17?$G$"$k$H8@$&$N$O!$(J
	f:G_1->G_2 $@$J$kA4C1<M$,B8:_$7$F(J
	  <g,h> \in R_1    iff   <f(g),f(h)> \in R_2
$@$H$$$&$3$H$G$h$$$G$9$+!)(J

$@;d$,5?Ld$K;W$C$F$$$k$N$O!$>e$NDj5A$G$$$/$H(J
	(G,R) = ({0,1},{<0,0>,<0,1>,<1,1>})
$@$_$?$$$J%0%i%U$O(J extensional $@$K$J$C$F$7$^$&$1$I!$$=$l$G$bNI(J
$@$$$N$+$J!)$H(J$@$+!$(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> $@$K$7$F$*$$$F$+$i$d$l$P$$$$$o$1$G$9!#$3$3$G!"E,Ev$H$$$C$?$N$O!"@53N$K(J$@$O!"(J
$@>.NS(J> $@F1CM4X78$G3d$C$?;~$K(J extensional $@$K$J$k$h$&$J:G>.$NF1CM4X78$G3d$k$o$1(J
$@>.NS(J> $@$G$9!#(J

$@!V:G>.(J$@$NF1CM4X78!W$,B8:_$9$k$H$O8B$i$J$$$h$&$K;W$o$l$k$H$+$G(J
$@$9!%(J


$@;VB<(J> extensional $@$J%0%i%U$@$1$r9M$($l$P(J$@NI$$$H$$$&$N$O!"(JAFA $@$K$*(J
$@;VB<(J> $@$1$k<LA|(J d $@$N0l0U@-$H!"301d@-8xM}(J (axiom of extensionality)
$@;VB<(J> $@$+$i(J$@$N5"7k$@$H;W$$$^$9!#(J

$@!V(Jextensional$@$J%0%i%U$@$1$r9M$($l$PNI$$!W$H$$$&$N$O!$!V(JAFA$@$N(J
$@%9%F!<%H%a%s%H$K$*(J$@$$$F!$(J``$@$9$Y$F$N%0%i%U(J''$@$r(J``$@$9$Y$F$N(J
extensional$@$J%0%i%U(J''$@$KCV$-49$($F$bL?Bj$N6/$5$OJQ$o$i$J$$!W(J
$@$H$$(J$@$&0UL#$G$7$g$&$+!)(J

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