Lines Matching defs:record
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