tests/inputs/circuits.lisp

65 (defun assign-T (v states)
68           (assign-T v (rest states)))))
70 (defun assign-nil (v states)
73           (assign-nil v (rest states)))))
80       (append (assign-t (car vars) rec-states)
81               (assign-nil (car vars) rec-states)))))
444 (defthm assign-t-produces-boolean-p
445   (boolean-p-states v (assign-T v states)))
449 (defthm assign-nil-produces-boolean-p
450   (boolean-p-states v (assign-nil v states)))
454 (defthm assign-T-remains-same-for-not-v
456            (equal (boolean-p-states v (assign-T v-prime states))
461 (defthm assign-nil-remains-same-for-not-v
463            (equal (boolean-p-states v (assign-nil v-prime states))
575          (assign-t (first vars)
577         (t (assign-nil (first vars)
609 (defthm assign-nil-produces-nil-member
610   (implies (memberp q (assign-nil v states))
615 (defthm assign-t-produces-t-member
616   (implies (memberp q (assign-t v states))
621 (defthm assign-nil-produces-nil
624            (not (<- (nth i (assign-nil v states)) v)))
627            :cases ((>= i (len (assign-nil v states))))
632                             (x (assign-nil v states)))))))
636 (defthm assign-t-has-same-len
637   (equal (len (assign-t v states))
642 (defthm assign-nil-has-same-len
643   (equal (len (assign-nil v states))
655 (defthm assign-t-produces-t
659            (equal (<- (nth i (assign-t v states)) v) t))
664                             (x (assign-t v states)))))))
668 (defthm assign-t-does-not-fuss
673            (equal (<- (nth i (assign-t v states)) v-prime)
678 (defthm assign-nil-does-not-fuss
683            (equal (<- (nth i (assign-nil v states)) v-prime)
777 (defthm member-assign-t-reduction
780                     (assign-t v x))))
784 (defthm assign-t-subset-reduction
786            (subset (assign-t v x)
787                    (assign-t v y))))
791 (defthm member-assign-nil-reduction
794                     (assign-nil v x))))
798 (defthm assign-nil-subset-reduction
800            (subset (assign-nil v x)
801                    (assign-nil v y))))
932 (defthm assign-t-strict-evaluations-reduction
939            (not (<- (nth i (assign-t v states)) v-prime)))
942            :in-theory (disable assign-t-does-not-fuss)
943            :use ((:instance assign-t-does-not-fuss)
950 (defthm assign-nil-strict-evaluations-reduction
957            (not (<- (nth i (assign-nil v states)) v-prime)))
960            :in-theory (disable assign-nil-does-not-fuss)
961            :use ((:instance assign-nil-does-not-fuss)
968 (defthm strict-evaluations-assign-t-reduction
974            (strict-evaluation-p (nth i (assign-t v states)) vars)))
978 (defthm strict-evaluations-assign-nil-reduction
984            (strict-evaluation-p (nth i (assign-nil v states)) vars)))
1009 (defthm strict-evaluation-for-memberp-assign-t
1013                 (memberp st (assign-t v states)))
1017            :in-theory (disable assign-t-strict-evaluations-reduction
1019            :use ((:instance strict-evaluations-assign-t-reduction
1020                             (i (find-index st (assign-t v states))))))))
1024 (defthm strict-evaluation-for-memberp-assign-nil
1028                 (memberp st (assign-nil v states)))
1032            :in-theory (disable assign-nil-strict-evaluations-reduction
1034            :use ((:instance strict-evaluations-assign-nil-reduction
1035                             (i (find-index st (assign-nil v states))))))))
1043 (defthm strict-evaluations-for-assign-t
1047            (strict-evaluation-list-p vars (assign-t v states))))
1051 (defthm strict-evaluations-for-assign-nil
1055            (strict-evaluation-list-p vars (assign-nil v states))))
1082 (defthm strict-evaluation-p-assign-reduction-t
1084            (strict-evaluation-list-p (cons v vars) (assign-t v states))))
1088 (defthm strict-evaluation-p-assign-reduction-nil
1090            (strict-evaluation-list-p (cons v vars) (assign-nil v states))))
1119            :in-theory (disable strict-evaluation-p-assign-reduction-t
1120                                strict-evaluation-p-assign-reduction-nil)
1121            :use ((:instance strict-evaluation-p-assign-reduction-t
1125                  (:instance strict-evaluation-p-assign-reduction-nil