Jubilee book for A.Trybulec - submitted paper examples

This page presents listings of examples that should have been enclosed in the submitted paper for the Jubilee book for A.Trybulec. However due to the page constraint they remains available online on this page.

Listings of examples

1. Mizar Formal Proof Sketch representation of H.Barendregt's approach to the proof of Pythagoras Theorem - pythHBfps.miz.
2. Full formalisation of Pythagoras example verified by the Mizar system - pythHBfull.miz.

Both presented versions have been checked and verified by Mizar system version 7.8.03 and using MML version 4.76.959.