DoubleCheck your theorems
Carl Eastlund · 2009
Theorem proving in ACL2 is a complex undertaking. Initial attempts to admit a lemma often fail, in which case the programmer must either redirect ACL2's efforts or change the lemma. ACL2's output does not always indicate whether the formulation of the lemma or the proof process is at fault.