20/10/16 19:35:21.99 r7KJySb3.net
>>146
URLリンク(web.sfc.keio.ac.jp)
で、証明させてみたら、あたりまえだけど、できたなw
ここでa1とかb1とかはそれぞれx1=0、y1=0を表す命題とする
!(!(a1)*!(b1)*(!(a2)*!(b2))*(a1+b2)*(a2+b1)) is provable in LK.
|- !(!(a1)*!(b1)*(!(a2)*!(b2))*(a1+b2)*(a2+b1))
--------------------------------------------------(|-!)
!(a1)*!(b1)*(!(a2)*!(b2))*(a1+b2)*(a2+b1) |-
-----------------------------------------------(*