🚀 go-pugleaf

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

In article <544@keu02.rtri.or.jp> r2230@L8221C.rtri.or.jp (Shingo Matsumoto) writes:

 |$@>>K\!w:G=*HG(J
 |
 |> |3.$@<B$O!">e$N#2$D$N$[$+$K(J1.$@!"(J2.$@$N$I$A$i$G$b$J$$!"$9$J$o$A(J$@!"(J
 |> |$@!!(Jx$@$,(J{},{0},{1},{0,1}$@$N$I$l$+$G$"$k$+!"$G$J$$$+$o$+$i$J$$(J
 |> |$@!!$H$$$&>l9g$,$"$k!#(J
 |> |$@!!$3(J$@$N>l9g(J
 |> |$@!!(Jx$@$,(J{0,1}$@$NItJ,=89g$G$"$k$H$$$&$N$O(J
 |> |$@!!%b%G%k$K$h$C$F??56CM$O$3$H$J$k!#(J
 |> |
 |> |$@!!(J$@$@$+$i!"%b%G%k$K$h$C$F$O(J
 |> |$@!!(J3.$@$N$h$&$J(J x$@$K$D$$$F(J
 |> |$@!!??56CM$,#1$G$"$k$H$9$l$P(J
 |> | $@!V%?%/%5%s(J$@!W$"$k$h$&$K$_$($k!#(J
 |
 |$@$H=q$-$^$7$?$,!"%b%G%k$NCf$G$O(J
 |$@Ey$7$$$H$bEy$7$/$J$$$HH=Dj$G$-$J$$$b$N$O(J
 |$@F1$8$b$N$H$b0c$&$b$N$H$b8@$($J$$$+$i(J
 |$@$d$O$j!JD>4Q<g5A$N%b%G%k>e$G$O!KItJ,=89g$N8D?t$O(J
 |$@!V?t$($i$l(J$@$J$$!W(J
 |$@$H9M$($k$7$+$J$$$h$&$G$9$M!#(J

$@$=$&$G$9$M!#?t$($i$l$J$$(J($@8D?t$H$7$F<+A3?t$rBP1~$5$;$i$l$J$$(J)$@$H(J$@9M$($i$l(J
$@$^$9!#(J

 |$@$d$O$j!"=89g$N!a$N301d@-(J
 |
 |All x (x in A <-> x in B) -> A = B
 |
 |$@$,7k9=!"6J<T(J$@$N$h$&$G$9!#(J

Heyting arithmetic $@$G$N!"<+A3?t$I$&$7$N(J equality $@$N$h$&$J$b$N$@$H!"(J
algorithmic $@$KEy$7$$(J$@$+Ey$7$/$J$$$+$r%A%'%C%/$G$-$k$o$1$G$9$,!"=89g$I$&(J
$@$7$N301d@-$K$h$k(J equality $@$O(J algorithmic $@$K%A%'%C%/(J$@$G$-$^$;$s$+$i$M!#(J

 |$@!t$A$J$_$K!"C]Fb@h@8$,$3$N$h$&$J%9%?%$%k$GD>4Q<g5A=89gO@$rD4$Y$?GX7J$K$O(J
 |$@!t&8(J$@$,0LAj6u4V!J$H$/$KB?MMBN!K$N3+=89g$N=89g$H$7$?$H$-$N!"4v2?3X$NDjM}$H(J
 |$@!t$N4X$o$j$K$D$$$FD4$Y$F$_$?$$(J$@$H$$$&$3$H$,$"$C$?$i$7$$!#AX$H$+%H%]%9$H$+(J
 |$@!t$H$$$&$N$O!"Be?t4v2?$G$b!"=P$F$/$k%O%J%7$N$h$&$@!#(J

$@$((J$@$(!"C]Fb@h@8$NF05!$O$=$&$$$&$3$H$@$C$?$h$&$G$9!#%k%=!<(J($@$D$E$j$,$o$+(J
$@$i$J$$(J)$@$i$N;E;v$K;I7c$5$l$?$N$+$J(J$@!#(J
--
			$@N6C+Bg3XM}9)3XIt?tM}>pJs3X2J(J    $@>.NS(J  $@Ao(J
			satoshi@whale.ryukoku.ac.jp
			0775-43-7523($@3X2J(J$@;vL3<<(J) 0775-43-7528($@8&5f<<(J)
			0775-43-7524(FAX)