🚀 go-pugleaf

$@>.NSAo(J@$@N6C+Bg3X$G$9!#$^$??t3XE*$JOC$K$J$C$F$7(J$@$^$C$?$N$G!"(Jfj.sci.math 
$@$K$b%/%m%9%]%9%H$7$^$9!#(J(Followup-To $@$O$I$&$9$k$Y$-$+$J$"!#$A$g$C$HLB(J
$@$&$N$G(J$@$3$N$^$^$K$7$H$-$^$9!#(J)

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

 |  Leipniz equality$@$H$$$&$N$O!"$$$o$f$k?t3X$G$$$&$H$3$m$N301dE*$J(Jequality$@$N$3(J
 |$@$H$H;W$$$^$9!#$U$D$&$N?t3X$G$O!"(Jequality$@$O301dE*$K$H$i$($F$^$9$,!"(Jequality$@$N(J

$@>/$74*0c$$$5$l$F(J$@$$$k$h$&$G$9!#(JLeibniz equality $@$O301dE*$J(J equality
(extensional equality)$@$H$O0[$J$j$^$9!#(J

$@0J2<!"(JLeibniz equality $@$r(J LeibEq, extensional equality $@$r(J ExtEq $@$H$=$l(J
$@$>$l=q$/$3$H$K$7$^$9!#N><T$NDj5A$r=q$$$F(J$@$_$k$H!"(J

    a LeibEq b = all P.(P(a) <-> P(b))
    P ExtEq Q  = all x.(P(x) <-> Q(x))

$@$H$J$j$^$9!#(JOperator $@$H(J operand $@$N4X78$,5U$K$J$C$F$$$k$3$H$KCm0U$7$F2<(J
$@$5$$!#(J

$@$b$C$H$b!"(Jextensional equality $@$H$$(J$@$&$N$O!"2?$K$D$$$F$N(J equality $@$r9M(J
$@$($F$$$k$+$K$h$C$FDj5A$,0c$$$^$9!#>e$N(J P ExtEq Q $@$O(J2$@$D$N=R8l$rHf$Y(J$@$k;~(J
$@$N(J extensional equality $@$G$9!#=89g$I$&$7$rHf$Y$k$N$J$i!"(J
    a ExtEq b = all x.(x in a <-> x in b)
$@$G$9$7!"<+A3?t$+$i<+A3?t$X$N4X?t$rHf$Y$k$N$J$i!"(J
    f ExtEq g = all x.(f(x) = g(x))  ($@1&JU$N(J '=' $@$O<+A3?t$I$&$7$NEy9f(J)
$@$G$9!#(J1$@JQ?t(J($@ItJ,(J)$@5"G<E*4X?t$NHf3S$J$i!"(J
    f ExtEq g = all x.((f(x)$@"-(J or g(x)$@"-(J) -> f(x) = g(x))
$@$G$9!#$?$@$7!"$3$3$K(J f(x)$@"-$O!"(Jf(x) $@$NCM$,Dj5A$5$l$F$$$k!"$H$$$&0UL#$G(J
$@$9!#JL$N=q$-(J$@J}$r$9$k$H!"(J
    f ExtEq g = all x,y.(f(x) = y <-> g(x) = y)
$@$H$J$j$^$9(J($@$3$N$[$&$,$o$+$j$d$9$$(J?)$@!#(J

$@$3(J$@$N$h$&$K!">l9g$K$h$C$FDj5A$,0c$&$o$1$G$9$,!"$$$:$l$K$7$F$b!"!V$I$s$J(J
$@0z?t$KBP$7$F$b(J a $@$H(J b $@$,F1$8$h$&(J$@$K$U$k$^$&$3$H!W$H$$$&$N$,(J extensional
equality $@$G$9$+$i!"(JLeibniz equality $@$HHf$Y$k$H(J operand $@$H(J operator $@$N(J
$@4X78$,5U$K$J$C$F$$$k$N$G$9!#$J$*!"=89g$N>l9g$K$O0z?t$H$$$&8@MU$r;H$&$N(J
$@$O$A$g$C$HJQ$J$N$G$9$,(J$@!"(Jx in a $@$H$$$&$N$,!"9b3,O@M}$N>l9g$N(J a(x) $@$KAj(J
$@Ev$9$k$H9M$($i$l$k$N$G!"(Jx in a $@$K$*$$$F(J x $@$N$[$&$,0z?t(J$@$K$"$?$j$^$9!#(J

$@$5$F!"$b$&>/$7N><T$N0c$$$r$O$C$-$j$5$;$^$7$g$&!#(J

$@:#!"$9$G$K(J object $@$N4V$K(J equality '=' $@$,M?$($i$l$F$$$F!"$=$l$K4X$7$FBe(J
$@F~8xM}$b@.N)$7$F$$$k$H$7$^$9!#$9$k$H!"(Jx LeibEq y $@$O(J x = y $@$KF1CM$K(J$@$J$j(J
$@$^$9!#$J$<$+$H8@$&$H!"$^$:!"(Jx = y -> all P.(P(x) <-> P(y)) $@$OBeF~8xM}(J
$@$+$iD>$A$K=P$^$9!#5U$K!"(Jall P.(P(x) <-> P(y)) $@$r2>Dj$9$k$H!"(JP(x) $@$H$7(J
$@$F(J x = y $@$r$H$l$P!"(Jx = y <-> y = y $@$H$J$k$N$G!"(Jx = y $@$,F3(J$@$1$^$9!#(J

$@$5$F!"(J2$@3,$N<+A3?tO@$r9M$($^$9!#$3$NM}O@$G$O!"$9$G$K(J object $@$N4V$K(J 
equality '=' $@$,M?$($i$l$F(J$@$$$^$9!#$9$J$o$A!"<+A3?t$I$&$7$NDL>o$N(J 
equality $@$G$9!#0lJ}!"$3$NM}O@$NCf$G!"ItJ,5"G<E*4X?t$K$D$$$F5D(J$@O@$9$k$H(J
$@$7$^$9$H!"$=$l$i4X?t$I$&$7$N(J extensional equality $@$O!"(J'=' $@$H$O0[$J$k$b(J
$@$N$K$J$j$^$9!#(J($@$4B8$8(J$@$H$O;W$$$^$9$,0lHL$NFI<T$N$?$a$K(J)$@>/$7JdB-$7$^$9$H!"(J
$@<+A3?tO@$NCf$G$OItJ,5"G<E*4X?t$O$=$N(J index $@$K$h$C(J$@$FI=$5$l$^$9!#(Jindex 
$@$H$$$&$N$O!"(JGodel number $@$H$b8F$P$l$F$$$^$9$,!"MW$9$k$K!"$=$N4X?t$,$I(J
$@$N$h$&$KDj(J$@5A$5$l$F$$$k$+!"$=$NDj5A$r<+A3?t$K$h$C$F%3!<%G%#%s%0$7$?$b$N(J
$@$G$9!#(J2$@$D$N5"G<E*4X?t(J f $@$H(J g $@$,??$KF10l$G(J$@$"$k!"$H$$$&$N$O!"(Jindex $@$H$7(J
$@$F$_$?$H$-$KA4$/F1$8<+A3?t$G$"$k$3$H$G$9!#$9$J$o$A!"4X?t$H$7$F$N$U$k$^(J
$@$$(J$@$,F1$8$H$$$&$@$1$G$J$/$F!"A4$/F1$8$h$&$KDj5A$5$l$F$$$k;~$KEy$7$$$H$$(J
$@$&$N$G$9!#$3$l$O<+A3?t$I$&$7$NDL(J$@>o$N(J equality $@$@$+$i!"7hDj2DG=$G$9!#0l(J
$@$DA0$N%Q%i%0%i%U$G@bL@$7$?$3$H$+$i!"(JLeibniz equality $@$O$3$N(J equality 
$@$H0lCW$7$^$9!#(J
  $@$7$+$7!"(Jextensional equality $@$O!"$h$/CN$i$l$F$$$k$h$&$K7hDjIT2DG=$G(J
$@$9!#$3$N(J$@$3$H$K$D$$$F$O!">>K\$5$s$,(J

 |$@H=Dj$N<jB3$-$J$s$F$$$&$3$H$r9M$($F$7$^$&$H!"301dE*$J(Jequality$@$O!"$d$C$Q$j(J$@ET9g(J
 |$@$,0-$$$G$9!#(J

 |  $@Nc$($P!"F10l$NF~NO$KBP$7$F!">o$KF1$8=PNO$rJV$9%W%m%0%i%`$r!"%"%k%4%j%:%`$N(J
 |$@0c$$$rL5;k$7$F!"F1$8$b$N$G$"$k$H8+Pv$7$?>l9g!"$=$N(Jequality$@$r!">o$K$O!"H=Dj$G(J
 |$@$-$J$$$@$m$&$+$i$G$9!#(J

$@$H=q$+$l$?DL$j$G$9!#(J

 |  $@$b$A$m$s!"$=$N$3$H$H!"?M$,!VF1$8!W$r$I$N$h$&$KG'<1$7$F$$$k$+$O!"JL$NLdBj$G(J
 |$@$7$g$&!#?M4V$O!"DL>o$O!"F1$8$H$$$&$3$H$r9M$($k$N$K!"!VL5L7=b!W$H$+!V40A4!W$H(J
 |$@$$$&$3$H$^$G$O9MN8$7(J$@$F$J$$$G$7$g$&$+$i!#(J

$@$=$l$O$=$&$G$7$g$&$M!#(J

$@$H$3$m$G!">e$NOC$GLLGr$$$H;W$&$N$O!"(JLeibniz equality $@$H(J extensional
equality $@$rHf$Y$?;~!"A0<T$N$[$&$,$:$C$HD61[E*$JDj5A$K$J$C$F$$$k(J($@A0<T$O(J 
impredicative $@$J(J$@M}O@$G9M$($k$b$N$@$,!"8e<T$O(J predicative $@$JDj5A$G!"$=(J
$@$b$=$b(J1$@3,$NM}O@$G$bDj5A$G$-$k(J)$@$K$b4X$o$i$:!"(Jequality $@$NH=Dj$OA0<T$N$[(J
$@$&$,4JC1$G$"$k$3$H$G$9!#$I$&$b(J fj.ai $@$G$N5DO@$r8+$F$$$k$H!"(JLeibniz
equality $@$r(J$@!VDj5A$K=>$C$F!WH=Dj(J($@$"$k$$$OG'<1(J)$@$9$k(J($@$D$^$j!"A4$F$N(J P $@$K(J
$@$D$$$F(J P(x) <-> P(y) $@$+$I$&$+$r8+$k(J)$@$N$OET(J$@9g$,0-$$!"$_$?$$$JOC$K$J$C$F(J
$@$$$k$h$&$G$9$1$I!"2?$bDj5ADL$j$K$d$kI,MW$O$J$$$o$1$G$9!#>e$N$h$&$K!"<B(J
$@:](J$@$K$O$b$C$HC1=c$KH=Dj$G$-$F$7$^$&$+$bCN$l$J$$$o$1$G$9!#$^$"!">e$NNc$G(J
$@$O$9$G$K(J object $@$N4V$K4JC1$J(J equality '=' $@$,M?$($i$l$F$$$k$h$&$J>l9g$r(J
$@9M$($?$N$G$D$^$i$J$$$o$1$G$9$,!"(Jequality $@$,A0$b$C$FM?$($i$l$F$$(J$@$J$$>l(J
$@9g$G$b!"(JLeibniz equality $@$,7k2LE*$KHs>o$KH=Dj$7$d$9$$$b$N$K$J$C$F$7$^(J
$@$&$3$H$O$"$jF@$k$o$1$G$9(J$@!#(J

$@$3$&$$$&;v$+$i9M$($F$b!"!VF1$8!W$H$$$&35G0$NDj5A$=$N$b$N$H!"$=$NG'<1$N(J
$@;EJ}$H$O!"$O$C$-$jJ,$1$F9M(J$@$($J$1$l$P$J$i$J$$$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)