Lines Matching defs:eq
212 (defun find-all-equations (vars equations eq-rec)
213 (if (endp vars) eq-rec
215 (-> eq-rec
338 (defthm evaluation-eq-subset-reduction
340 (evaluation-eq p q vars))
341 (evaluation-eq p q vars-prime)))
345 (defthm evaluation-eq-member-subset-reduction
346 (implies (and (evaluation-eq-member-p init inits vars)
348 (evaluation-eq-member-p init inits vars-prime)))
352 (defthm evaluation-eq-subset-subset-reduction
353 (implies (and (evaluation-eq-subset-p inits states vars)
355 (evaluation-eq-subset-p inits states vars-prime)))
359 (defthm corresponding-states-are-evaluation-eq
361 (evaluation-eq init (corresponding-state init vars) vars)))
372 (defthm evaluation-eq-memberp-of-corresponding-states
375 (evaluation-eq-member-p init (corresponding-states inits vars)
380 (defthm evaluation-eq-subsets-reduction
382 (evaluation-eq-subset-p inits (corresponding-states inits vars)
388 (defthm initial-states-are-evaluation-eq
390 (evaluation-eq-subset-p
402 (defthm corresponding-states-are-evaluation-eq-2
404 (evaluation-eq (corresponding-state init vars) init vars)))
408 (defthm evaluation-eq-memberp-of-corresponding-states-2
411 (evaluation-eq-member-p init inits
416 (defthm evaluation-eq-subsets-reduction-2
418 (evaluation-eq-subset-p (corresponding-states inits vars) inits
423 (defthm initial-states-are-evaluation-eq-2
425 (evaluation-eq-subset-p
735 ;; states are evaluation-eq with respect to vars, then the next states are
736 ;; evaluation-eq with respect to vars.
745 ;; We start with a couple of theorems about evaluation-eq
748 (defthm evaluation-eq-is-reflexive
749 (evaluation-eq x x vars))
753 (defthm evaluation-eq-is-transitive
754 (implies (and (evaluation-eq p q vars)
755 (evaluation-eq q r vars))
756 (evaluation-eq p r vars)))
785 (evaluation-eq r (produce-next-state vars p
792 (defthm thus-r-is-evaluation-eq-to-s
794 (evaluation-eq (produce-next-state vars-orig p
800 (evaluation-eq r s vars-cone))
803 evaluation-eq-subset-reduction
809 (:instance evaluation-eq-subset-reduction
819 ;; Thus r is evaluation-eq with respect to s if we can show that
820 ;; produce-next-state produces something evaluation-eq to s. Now to show that
821 ;; this implies r is evaluation-eq-member-p of transition of q, we need to show
830 (evaluation-eq q (produce-next-state vars p eqn) vars))
850 (evaluation-eq s (produce-next-state vars-cone q eqn) vars-cone))
863 (evaluation-eq s (produce-next-state vars-cone q eqn) vars-cone))
865 (evaluation-eq-member s states-cone vars-cone)
871 (s (evaluation-eq-member s states-cone vars-cone)))
872 (:instance evaluation-eq-is-symmetric
874 (q (evaluation-eq-member s states-cone vars-cone))
879 (defthm evaluation-eq-and-memberp-to-evaluation-eq-memberp
881 (evaluation-eq p q vars))
882 (evaluation-eq-member-p p states vars)))
885 (defthm evaluation-eq-memberp-from-all-evaluations-p
889 (evaluation-eq s (produce-next-state vars-cone q eqn)
891 (evaluation-eq-member-p
897 evaluation-eq-and-memberp-to-evaluation-eq-memberp)
898 :use ((:instance evaluation-eq-and-memberp-to-evaluation-eq-memberp
899 (q (evaluation-eq-member s states-cone vars-cone))
907 (defthm evaluation-eq-and-memberp-to-memberp
908 (implies (and (evaluation-eq p q vars)
909 (evaluation-eq-member-p q states vars))
910 (evaluation-eq-member-p p states vars)))
914 (defthm next-state-of-orig-to-evaluation-eq-member-p
917 (evaluation-eq (produce-next-state vars-orig p
926 (evaluation-eq s (produce-next-state vars-cone q eqn)
928 (evaluation-eq-member-p
933 :in-theory (disable thus-r-is-evaluation-eq-to-s)
934 :use thus-r-is-evaluation-eq-to-s)))
943 (defun create-corresponding-equation (vars equation-record vars-prime eqn eq-rec)
944 (if (endp vars) eq-rec
946 eqn eq-rec)
970 vars-orig eqn-orig eq-rec)
1016 eq-rec)
1021 vars-orig eqn eq-rec)
1027 ;; the cone. So the final proof requirement is that s is evaluation-eq to the
1067 (evaluation-eq p q vars))
1090 (defthm evaluation-eq-set-reduction
1091 (implies (and (evaluation-eq p q vars)
1093 (evaluation-eq (-> p v a) (-> q v b) vars)))
1097 (defthm produce-next-state-is-evaluation-eq
1104 (evaluation-eq p q vars-prime)
1107 (evaluation-eq
1121 (defthm produce-next-state-is-evaluation-eq-concretized
1124 (evaluation-eq p q vars-cone)
1129 (evaluation-eq
1136 (defthm produce-next-state-evaluation-eq-reduction
1140 (evaluation-eq (produce-next-state vars-orig p eqn-orig)
1149 (evaluation-eq p q vars-cone)
1156 (evaluation-eq (produce-next-state vars-orig p eqn-orig)
1162 :in-theory (disable evaluation-eq-is-transitive
1163 produce-next-state-is-evaluation-eq-concretized)
1164 :use ((:instance produce-next-state-is-evaluation-eq-concretized)
1165 (:instance evaluation-eq-is-transitive
1176 (evaluation-eq p q vars-cone)
1184 (evaluation-eq
1189 vars-cone equations-cone vars-orig eqn-orig eq-rec))
1235 (defthm r-is-evaluation-eq-member-p-with-respect-to-states
1240 (evaluation-eq p q vars-cone)
1250 (evaluation-eq-member-p
1256 :in-theory (disable next-state-of-orig-to-evaluation-eq-member-p)
1257 :use ((:instance next-state-of-orig-to-evaluation-eq-member-p
1265 eq-rec)))))
1293 (defthm evaluation-eq-subset-p-orig->cone
1298 (evaluation-eq p q vars-cone)
1308 (evaluation-eq-subset-p
1314 (defthm evaluation-eq-subset-orig->cone-concretized
1317 (evaluation-eq p q vars-cone)
1328 (evaluation-eq-subset-p
1334 :in-theory (disable evaluation-eq-subset-p-orig->cone)
1335 :use ((:instance evaluation-eq-subset-p-orig->cone
1360 eq-rec)
1371 vars-cone eqn-cone eq-rec)
1373 (<- eq-rec v))))
1381 vars-cone eqn-cone eq-rec)
1396 vars-cone eqn-cone eq-rec)
1407 (evaluation-eq p q vars-cone)
1416 (evaluation-eq
1420 vars-orig equations-orig vars-cone eqn-cone eq-rec))
1431 (evaluation-eq r (produce-next-state vars-orig p eqn)
1433 (evaluation-eq-member-p
1437 :in-theory (disable evaluation-eq-member-subset-reduction)
1438 :use ((:instance evaluation-eq-member-subset-reduction
1448 (defthm thus-r-is-evaluation-eq-to-s-2
1450 (evaluation-eq (produce-next-state
1457 (evaluation-eq s r vars-cone))
1465 (defthm thus-polished-r-is-evaluation-eq-to-s-2
1468 (evaluation-eq r (produce-next-state
1473 (evaluation-eq r s vars-cone))
1484 (:instance thus-r-is-evaluation-eq-to-s-2)
1485 (:instance evaluation-eq-is-symmetric
1489 (:instance evaluation-eq-is-symmetric
1499 (defthm evaluation-eq-member-p-from-memberp
1500 (implies (and (evaluation-eq s r vars)
1501 (evaluation-eq-member-p r states vars))
1502 (evaluation-eq-member-p s states vars)))
1506 (defthm next-state-of-orig-to-evaluation-eq-member-p-2
1509 (evaluation-eq r (produce-next-state
1520 (evaluation-eq r (produce-next-state vars-orig p eqn)
1522 (evaluation-eq-member-p
1527 :in-theory (disable ;; produce-next-state-evaluation-eq-reduction
1529 thus-polished-r-is-evaluation-eq-to-s-2)
1530 :use ((:instance thus-polished-r-is-evaluation-eq-to-s-2)
1532 (:instance evaluation-eq-is-symmetric
1567 (evaluation-eq p q vars-cone)
1580 (evaluation-eq-member-p
1588 next-state-of-orig-to-evaluation-eq-member-p-2)
1589 :use ((:instance next-state-of-orig-to-evaluation-eq-member-p-2
1596 eq-rec)))
1601 eq-rec)))
1609 eq-rec)))
1611 (eqn-rec eq-rec)
1623 (evaluation-eq p q vars-cone)
1636 (evaluation-eq-subset-p
1645 (evaluation-eq p q vars-cone)
1661 (evaluation-eq-subset-p
1699 (evaluation-eq p q vars-cone)
1712 (evaluation-eq-subset-p
1726 (evaluation-eq p q vars-cone)
1742 (evaluation-eq-subset-p
1756 (evaluation-eq q p vars-cone)
1772 (evaluation-eq-subset-p
1782 evaluation-eq-subset-p
1783 evaluation-eq-member-p
1787 (:instance evaluation-eq-is-symmetric