Logiweb(TM)

14.273 Lemma P occurs on a page with a non-empty diagnose

Prev Up Next Page 744 of 800 Search internet


Origin: check. Landing-place: diagnose.

Lemma P occurs on a page with a non-empty diagnose. Avoid referencing that lemma.

When a proof references a lemma on another page, the verifier checks two things: First, that the other page has been proof checked. Second, that the outcome of verification was positive.

The verifier checks that the outcome of verification was positive by looking at the diagnose hook of the rack of the other page. The diagnose is empty or true when it has value true. The error indicates that the diagnose was not true and thus the referenced page was in error and the referenced lemma may be false.

Note that the verifier has no reservations about incorrect pages in general. Even if a page has a non-empty diagnose, it may contain useful definitions. But the verifier protests the moment one uses a lemma from an incorrect page.

Prev Up Next Page 744 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05