Create a Mizar text (article) file using the environ block from NAT_1.miz.

Write and check with Mizar the proof skeletons of three theorems of your choice in NAT_1. Submit the Mizar checked result to show that the only errors remaining are on the conclusion statements ("::> 4 This inference is not accepted" or in the case of a contradiction "::> *1: It is not true").

Also report which Mizar checker (version, etc.) you used.

[ Back ]