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 (FOO A) (APPEND (BAR B) (MUM C)))
(defthm subsetp-append-2-weak (implies (or (subsetp x y) (subsetp x z)) (subsetp x (append y z))))
The rule generated from this is: ``if you ever encounter (an instance of)
This does not fully characterize the situation though. For example,
However, no obvious equivalence comes to mind — indeed, to express any of the ideas floating around here requires defining and introducing more functions, which is not recommended unless those functions are already in the problem.
For example, if you defined the concept of ``
(defthm subset-append-2-strong-but-messy (equal (subsetp x (append y z)) (and (subsetp (set-minus x z) y) (subsetp (set-minus x y) z))))
But this rewrite rule would ``trade''
We recommend sticking with the weak version of the rule,
(defthm subsetp-append-2-weak (implies (or (subsetp x y) (subsetp x z)) (subsetp x (append y z)))).
This illustrates the fact that sometimes there is no strong version of a rule!
Use your browser's Back Button now to return to practice-formulating-strong-rules.