tests/inputs/cone-of-influence.lisp

36 (defun find-all-variables-1-pass (vars equations)
39                       (find-all-variables-1-pass (rest vars) equations))))
41 ;; The following function find-all-variables is a difficult function to
82 (defthm find-all-variables-1-pass-is-unique
83   (uniquep (find-all-variables-1-pass vars equations)))
196 (defun find-all-variables (vars variables equations)
206     (let ((new-vars (set-union (find-all-variables-1-pass vars equations)
210           (find-all-variables new-vars variables equations))))))
212 (defun find-all-equations (vars equations eq-rec)
214     (find-all-equations (rest vars) equations
236   (find-all-variables
246        :equations (find-all-equations variables (equations C) ()))))
258 (defthm find-all-variables-subset-of-variables
262   (subset (find-all-variables vars variables equations) variables))
268 ;; OK, so we know find-all-variables-is-a-subset. We need to prove that vars is
291 (defthm find-all-variables-is-unique
293            (uniquep (find-all-variables vars variables equations)))
530            (equal (<- (find-all-equations vars equations eqn-rec) v)
545                              (find-all-equations
549            :induct (find-all-equations vars equations eqn-rec)
562            :in-theory (disable find-all-equations find-all-variables
585                    (find-all-variables-1-pass vars equations)))
598 (defthm find-all-variables-computes-closure
599   (implies (and (memberp v (find-all-variables vars variables equations))
605                    (find-all-variables vars variables equations)))
607            :induct (find-all-variables vars variables equations)
616 (in-theory (disable find-all-variables))
620 (defthm find-all-variables-is-equation-record-p
625             (find-all-variables vars variables equations)
630            :in-theory (disable  find-all-variables-computes-closure)
632                             (vars (find-all-variables vars variables
634                  (:instance find-all-variables-computes-closure
637                                         (find-all-variables vars variables
643                                       (find-all-variables vars variables
648 ;; So we have proved that find-all-variables produces a consistent record for
855 ;; states are all-evaluations-p, and s is an evaluation-p as we will see.
859 (defthm member-of-next-states-from-all-evaluations-p
860   (implies (and (all-evaluations-p states-cone vars-cone)
885 (defthm evaluation-eq-memberp-from-all-evaluations-p
886   (implies (and (all-evaluations-p states-cone vars-cone)
923                 (all-evaluations-p states-cone vars-cone)
1249                 (all-evaluations-p states-cone vars-cone))
1307                 (all-evaluations-p states-cone vars-cone))
1327                 (all-evaluations-p states-cone vars-cone))
1427    (implies (and (all-evaluations-p states-orig vars-orig)
1517                (all-evaluations-p states-orig vars-orig)
1572                 (all-evaluations-p states-orig vars-orig)
1579                 (all-evaluations-p states-cone vars-cone))
1628                 (all-evaluations-p states-orig vars-orig)
1635                 (all-evaluations-p states-cone vars-cone))
1653                  (all-evaluations-p states-orig vars-orig)
1660                  (all-evaluations-p states-cone vars-cone))
1711                 (all-evaluations-p states-cone vars-cone))
1734                  (all-evaluations-p states-orig vars-orig)
1741                  (all-evaluations-p states-cone vars-cone))
1764                  (all-evaluations-p states-orig vars-orig)
1771                  (all-evaluations-p states-cone vars-cone))
1792 (in-theory (disable create-all-evaluations find-all-variables
1794                     all-evaluations-p
1796                     only-all-truths-p
1804                     find-all-equations create-label-fn))