Major Section: MISCELLANEOUS
The value of this flag is normally
nil. If you want to prevent the
theorem prover from abandoning its initial work upon pushing the
second subgoal, set
Suppose you submit a conjecture to the theorem prover and the system
splits it up into many subgoals. Any subgoal not proved by other
methods is eventually set aside for an attempted induction proof.
But upon setting aside the second such subgoal, the system chickens
out and decides that rather than prove n>1 subgoals inductively, it
will abandon its initial work and attempt induction on the
originally submitted conjecture. The
:otf-flg (Onward Thru the Fog)
allows you to override this chickening out. When
system will push all the initial subgoals and proceed to try to
prove each, independently, by induction.
Even when you don't expect induction to be used or to succeed,
:otf-flg is a good way to force the system to generate
and display all the initial subgoals.
:otf-flg is a keyword argument that is a peer to
hints. It may be supplied as in the following
examples; also see defthm.
(thm (my-predicate x y) :rule-classes nil :otf-flg t) (defthm append-assoc (equal (append (append x y) z) (append x (append y z))) :hints (("Goal" :induct t)) :otf-flg t)The
:otf-flgmay be supplied to
xargsdeclare option. When you supply an
defun, the flag is effective for the termination proofs and the guard proofs, if any.