tests/inputs/cone-of-influence.lisp

106 (defthm del-not-member-reduction
107   (implies (not (memberp e x))
113   (implies (not (equal v e))
120   (implies (and (not (memberp e x))
140            :do-not '(eliminate-destructors generalize)
141            :do-not-induct t)))
172  (defthm len-not-consp
174             (not (consp x)))
187            :do-not '(eliminate-destructors generalize)
188            :do-not-induct t)
199                            :do-not-induct t
201                            :do-not '(eliminate-destructors generalize)))))
202   (if (or (not (uniquep variables))
203           (not (uniquep vars))
204           (not (subset vars variables)))
208       (if (not (subset new-vars variables)) nil
322            :do-not-induct t)))
470 (defthm not-memberp-to-corresponding-state
471   (implies (not (memberp v vars))
472            (not (<- (corresponding-state init vars) v))))
528 (defthm find-equations-for-not-member-p
529   (implies (not (memberp v vars))
550            :do-not '(eliminate-destructors generalize)
551            :do-not-induct t)))
587            :do-not-induct t
588            :do-not '(eliminate-destructors generalize)
608            :do-not '(eliminate-destructors generalize)
609            :do-not-induct t)
629            :do-not-induct t
685            :do-not-induct t
805            :do-not-induct t
847 (defthm memberp-not-using-next-states
868            :do-not-induct t
869            :in-theory (disable memberp-not-using-next-states)
870            :use ((:instance memberp-not-using-next-states
895            :do-not-induct t
932            :do-not-induct t
959   (implies (not (memberp v vars))
993 (defthm consistent-set-not-member
994   (implies (not (memberp v vars))
1022            :do-not '(eliminate-destructors generalize)
1023            :do-not-induct t)))
1048            :do-not '(eliminate-destructors generalize)
1049            :do-not-induct t)))
1075 (defthm produce-next-state-not-memberp-vars-reduction
1076   (implies (not (memberp v vars))
1092                 (not (memberp v vars)))
1112            :do-not '(eliminate-destructors generalize)
1160            :do-not '(eliminate-destructors generalize)
1161            :do-not-induct t
1255            :do-not-induct t
1349   (implies (not (memberp v vars))
1368 (defthm not-memberp-to-create-equation
1369   (implies (not (memberp v vars-orig))
1378   (implies (and (not (memberp v vars-cone))
1400            :do-not '(eliminate-destructors generalize))))
1475            :do-not-induct t
1526            :do-not-induct t
1553           :do-not-induct t)
1585             :do-not-induct t
1678 (defthm not-member-p-to-next-states
1679   (implies (not (memberp p states))
1825            :do-not '(eliminate-destructors generalize fertilize)
1826            :do-not-induct t
1885            :do-not '(eliminate-destructors generalize fertilize)
1886            :do-not-induct t