tests/inputs/circuits.lisp

31   (cond ((and (atom equation) (not (booleanp equation)))
106            (~ (not (apply-equation (second equation) st)))
213 (defthm create-label-fn-does-not-mess-with-non-members
214   (implies (not (memberp s states))
231            :do-not-induct t)))
264           :do-not-induct t)))
337 (defthm not-memberp-next-states-reduction
338   (implies (not (memberp s states))
454 (defthm assign-T-remains-same-for-not-v
455   (implies (not (equal v v-prime))
461 (defthm assign-nil-remains-same-for-not-v
462   (implies (not (equal v v-prime))
476   (implies (not (memberp v vars))
481            :do-not-induct t)))
490            :do-not-induct t)
512     (if (not (booleanp (<- st (first vars))))
624            (not (<- (nth i (assign-nil v states)) v)))
628            :do-not-induct t)
668 (defthm assign-t-does-not-fuss
672                 (not (equal v v-prime)))
678 (defthm assign-nil-does-not-fuss
682                 (not (equal v v-prime)))
705            :do-not '(eliminate-destructors generalize)
706            :do-not-induct t)
716     (if (not (equal (<- p (first vars))
730 (defthm falsifier-not-member-to-evaluation-eq
731   (implies (not (memberp (falsifier-evaluation-eq p q vars) vars))
744            :cases ((not (memberp
752  (defthm len-not-consp
754             (not (consp x)))
861            :do-not '(eliminate-destructors generalize)
862            :do-not-induct t
938                 (not (memberp v-prime vars)))
939            (not (<- (nth i (assign-t v states)) v-prime)))
941            :do-not-induct t
942            :in-theory (disable assign-t-does-not-fuss)
943            :use ((:instance assign-t-does-not-fuss)
956                 (not (memberp v-prime vars)))
957            (not (<- (nth i (assign-nil v states)) v-prime)))
959            :do-not-induct t
960            :in-theory (disable assign-nil-does-not-fuss)
961            :use ((:instance assign-nil-does-not-fuss)
1016            :do-not-induct t
1031            :do-not-induct t
1116            :do-not '(eliminate-destructors generalize)
1117            :do-not-induct t)