Subject: Fragments

Keywords: ::Thin

Title: Thin Fragments

--------------------------------------------------

A fragment is thinned when no unnecessary hyps occur in the 
Fragment step goal. A hyp is unnecessary if the proof can be
efficiently completed using other thin fragments with the
hyp thinned. Efficency is judged relative to the cost of 
refining the step with the hyp. Sometimes, hyps are asserted
with the express intent of making the proof more efficient.
In some cases thinning such a hyp can make the step run
exceedingly slowly. In such cases thinning is to be avoided.
⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home