[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: ? about "complete"/"incomplete" proof status

The M-x status-proofchain and related commands provide the information
you need.   A proof can be incomplete for several reasons:
a) it may use lemmas that have not been proved (or whose proofs have
   not been rechecked since some change)
b) there may be undischarged TCCs in the theory concerned or
   (recursively) in some theory that it imports
c) there may be undischarged assumptions on some imported theory.

M-x status-proof and related commands just tell whether *this* claim
is proved in a local sense (and warn you by the "incomplete"
annotation when you need to examine the more global context); the M-x
status-proofchain commands examine that global context.