Rules suggested by
What rules come to mind when looking at the following subterm of a Key Checkpoint? Think of strong rules (see strong-rewrite-rules).
(SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))
(defthm subsetp-append-1-strong (equal (subsetp (append x y) z) (and (subsetp x z) (subsetp y z))))
We put the ``
This strong rule is better than the conditional rule;
(defthm subsetp-append-1-weak (implies (and (subsetp x z) (subsetp y z)) (subsetp (append x y) z)))
for all the usual reasons.
Use your browser's Back Button now to return to practice-formulating-strong-rules.