tests/inputs/cone-of-influence.lisp

620 (defthm find-all-variables-is-equation-record-p
624            (consistent-equation-record-p
631            :use ((:instance (:definition consistent-equation-record-p)
636                                        (consistent-equation-record-p-witness
642                                      (consistent-equation-record-p-witness
648 ;; So we have proved that find-all-variables produces a consistent record for
650 ;; equation-equal-p, then they are consistent-equation-record-p at the same
654 (in-theory (disable consistent-equation-record-p))
666 (defthm consistent-eqn-record-p-expanded
667   (implies (and (consistent-equation-record-p vars eqn-orig)
674            :use ((:instance consistent-equation-record-p-necc
682                 (consistent-equation-record-p vars eqn-orig))
683            (consistent-equation-record-p vars eqn-cone))
686            :in-theory (disable consistent-equation-record-p
687                                consistent-equation-record-p-necc
689            :expand (consistent-equation-record-p vars eqn-cone)
690            :use ((:instance  consistent-equation-record-p-necc
695 (in-theory (disable consistent-equation-record-p
696                     consistent-equation-record-p-necc))
702            (consistent-equation-record-p
943 (defun create-corresponding-equation (vars equation-record vars-prime eqn eq-rec)
945     (-> (create-corresponding-equation (rest vars) equation-record vars-prime
950           (first (<- equation-record (first vars)))))))
954 ;; the cone of influence is well-formed-equation-record-p, and equation-equal-p
977   (implies (and (consistent-p-equations vars eqn equation-record)
978                 (memberp equation (<- equation-record v)))
980                                    equation-record))
1031 (defun closed-eqn-record-p (eqn vars vars-prime)
1034          (closed-eqn-record-p eqn (rest vars) vars-prime))))
1038 ;; vars-prime. Now let us show that this notion follows from equation-record-p.
1041 (defthm closed-eqn-record-p-from-consistent-equation-record-p
1042   (implies (and (consistent-equation-record-p vars-prime equations)
1046            (closed-eqn-record-p eqn vars vars-prime))
1055 (defthm closed-eqn-record-p-true-concretized
1056   (implies (and (consistent-equation-record-p vars equations)
1059            (closed-eqn-record-p eqn vars vars)))
1105                 (closed-eqn-record-p eqn-cone vars vars-prime)
1126                 (consistent-equation-record-p vars-cone equations-cone)
1153                 (consistent-equation-record-p vars-cone equations-cone)
1182                 (consistent-equation-record-p vars-cone equations-cone)
1221                 (closed-eqn-record-p eqn vars vars-prime))
1229                 (consistent-equation-record-p vars equations)
1241                 (consistent-equation-record-p vars-orig equations-orig)
1248                 (consistent-equation-record-p vars-cone equations-cone)
1299                 (consistent-equation-record-p vars-orig equations-orig)
1306                 (consistent-equation-record-p vars-cone equations-cone)
1318                 (consistent-equation-record-p vars-orig equations-orig)
1326                 (consistent-equation-record-p vars-cone equations-cone)
1413                 (consistent-equation-record-p vars-cone equations-cone)
1414                 (consistent-equation-record-p vars-orig equations-orig)
1568                 (consistent-equation-record-p vars-orig equations-orig)
1577                 (consistent-equation-record-p vars-orig equations-orig)
1578                 (consistent-equation-record-p vars-cone equations-cone)
1624                 (consistent-equation-record-p vars-orig equations-orig)
1633                 (consistent-equation-record-p vars-orig equations-orig)
1634                 (consistent-equation-record-p vars-cone equations-cone)
1646                  (consistent-equation-record-p vars-orig equations-orig)
1658                  (consistent-equation-record-p vars-orig equations-orig)
1659                  (consistent-equation-record-p vars-cone equations-cone)
1700                 (consistent-equation-record-p vars-orig equations-orig)
1710                 (consistent-equation-record-p vars-cone equations-cone)
1727                  (consistent-equation-record-p vars-orig equations-orig)
1739                  (consistent-equation-record-p vars-orig equations-orig)
1740                  (consistent-equation-record-p vars-cone equations-cone)
1757                  (consistent-equation-record-p vars-orig equations-orig)
1769                  (consistent-equation-record-p vars-orig equations-orig)
1770                  (consistent-equation-record-p vars-cone equations-cone)
1801                     consistent-equation-record-p