about the automatic proof of an easy theorem

["渡辺 稔彦" <toshi-w@avisnet.or.jp>]

Hello!

  I heard that the one who has an interest about the automatic proof of
an easy theorem be to Mizar forum.  Therefore, I think that I want to
write about the program that made in a university era.  
  When I was learning it about Mizar at Shinshu university before 4
years, I made the program of the automatic proof that used Mizar.  It
prepared the proof express statement of the same value nature of 2
expressions by using theorem that has already been proved with Mizar. 
When I write a proof express statement, it helped me.

Toshihiko Watanabe