Lines Matching defs:orig
513 (defun equation-equal-p (eqn-orig eqn-cone vars)
515 (and (equal (<- eqn-orig (first vars))
517 (equation-equal-p eqn-orig eqn-cone (rest vars)))))
522 (implies (equation-equal-p eqn-orig eqn-cone vars)
524 (cons-list-p vars eqn-orig))))
542 (defthm equations-of-cone-and-orig-are-equal
565 (eqn-orig (equations C))
659 (implies (and (equation-equal-p eqn-orig eqn-cone vars)
662 (<- eqn-orig v))))
667 (implies (and (consistent-equation-record-p vars eqn-orig)
670 (memberp equation (<- eqn-orig v)))
675 (equations eqn-orig))))))
680 (implies (and (equation-equal-p eqn-orig eqn-cone vars)
682 (consistent-equation-record-p vars eqn-orig))
691 (equation eqn-orig))))))
707 (eqn-orig (equations C))
793 (implies (and (next-state-is-ok p r vars-orig equations-orig)
794 (evaluation-eq (produce-next-state vars-orig p
795 (next-state-is-ok-witness p r vars-orig
796 equations-orig))
799 (subset vars-cone vars-orig))
807 (vars vars-orig)
808 (equations equations-orig))
815 (vars vars-orig)
914 (defthm next-state-of-orig-to-evaluation-eq-member-p
915 (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig
916 equations-orig))
917 (evaluation-eq (produce-next-state vars-orig p
918 (next-state-is-ok-witness p r vars-orig
919 equations-orig))
922 (subset vars-cone vars-orig)
960 (equal (equation-equal-p eqn-orig (-> eqn-cone v a) vars)
961 (equation-equal-p eqn-orig eqn-cone vars))))
966 (implies (and (subset vars-cone vars-orig)
968 (equation-equal-p eqn-orig (create-corresponding-equation
970 vars-orig eqn-orig eq-rec)
1001 (implies (and (equation-equal-p eqn-orig eqn-cone vars)
1002 (consistent-p-equations vars eqn eqn-orig))
1008 (implies (and (consistent-p-equations vars-orig eqn eqn-orig)
1010 (equation-equal-p eqn-orig eqn-cone vars-cone)
1011 (uniquep vars-orig)
1015 (create-corresponding-equation vars-cone eqn-cone vars-orig eqn
1021 vars-orig eqn eq-rec)
1106 (equation-equal-p eqn-orig eqn-cone vars))
1108 (produce-next-state vars p eqn-orig)
1128 (equation-equal-p eqn-orig eqn-cone vars-cone))
1130 (produce-next-state vars-cone p eqn-orig)
1137 (implies (and (uniquep vars-orig)
1139 (subset vars-cone vars-orig))
1140 (evaluation-eq (produce-next-state vars-orig p eqn-orig)
1141 (produce-next-state vars-cone p eqn-orig)
1150 (uniquep vars-orig)
1152 (subset vars-cone vars-orig)
1155 (equation-equal-p eqn-orig eqn-cone vars-cone))
1156 (evaluation-eq (produce-next-state vars-orig p eqn-orig)
1166 (p (produce-next-state vars-orig p eqn-orig))
1167 (q (produce-next-state vars-cone p eqn-orig))
1178 (uniquep vars-orig)
1180 (equation-equal-p equations-orig equations-cone vars-cone)
1181 (consistent-p-equations vars-orig eqn-orig equations-orig)
1183 (subset vars-cone vars-orig))
1185 (produce-next-state vars-orig p eqn-orig)
1189 vars-cone equations-cone vars-orig eqn-orig eq-rec))
1236 (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig
1237 equations-orig))
1241 (consistent-equation-record-p vars-orig equations-orig)
1242 (subset vars-cone vars-orig)
1243 (evaluation-p p vars-orig)
1244 (uniquep vars-orig)
1247 (equation-equal-p equations-orig equations-cone vars-cone)
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
1258 (s (produce-next-state vars-orig p
1259 (next-state-is-ok-witness p r vars-orig
1260 equations-orig)))
1262 vars-cone equations-cone vars-orig
1263 (next-state-is-ok-witness p r vars-orig
1264 equations-orig)
1271 p r vars-orig equations-orig))
1272 (equations equations-orig)
1273 (vars vars-orig))
1279 (variables vars-orig)
1285 (eqn-orig equations-orig)
1287 (eqn (next-state-is-ok-witness p r vars-orig
1288 equations-orig)))))))
1293 (defthm evaluation-eq-subset-p-orig->cone
1294 (implies (and (subset l (create-next-states-of-p p states-orig vars-orig
1295 equations-orig))
1299 (consistent-equation-record-p vars-orig equations-orig)
1300 (subset vars-cone vars-orig)
1301 (evaluation-p p vars-orig)
1302 (uniquep vars-orig)
1305 (equation-equal-p equations-orig equations-cone vars-cone)
1314 (defthm evaluation-eq-subset-orig->cone-concretized
1318 (consistent-equation-record-p vars-orig equations-orig)
1319 (subset vars-cone vars-orig)
1320 (only-evaluations-p states-orig vars-orig)
1321 (memberp p states-orig)
1322 (uniquep vars-orig)
1325 (equation-equal-p equations-orig equations-cone vars-cone)
1329 (create-next-states-of-p p states-orig vars-orig
1330 equations-orig)
1334 :in-theory (disable evaluation-eq-subset-p-orig->cone)
1335 :use ((:instance evaluation-eq-subset-p-orig->cone
1336 (l (create-next-states-of-p p states-orig vars-orig
1337 equations-orig)))))))
1342 (equal (equation-equal-p eqn-orig eqn-cone vars)
1343 (equation-equal-p eqn-cone eqn-orig vars))
1350 (equal (equation-equal-p (-> eqn-orig v a) eqn-cone vars)
1351 (equation-equal-p eqn-orig eqn-cone vars))))
1357 (memberp v vars-orig))
1358 (equal (<- (create-corresponding-equation vars-orig eqn-orig
1364 :cases ((equal v (car vars-orig))))))
1369 (implies (not (memberp v vars-orig))
1370 (equal (<- (create-corresponding-equation vars-orig eqn-orig
1379 (memberp v vars-orig))
1380 (equal (<- (create-corresponding-equation vars-orig eqn-orig
1383 (first (<- eqn-orig v))))
1385 :cases ((equal v (car vars-orig))))))
1390 (implies (and (subset vars-cone vars-orig)
1392 (uniquep vars-orig)
1395 vars-orig eqn-orig
1408 (cons-list-p vars-orig equations-orig)
1409 (uniquep vars-orig)
1411 (equation-equal-p equations-orig equations-cone vars-cone)
1414 (consistent-equation-record-p vars-orig equations-orig)
1415 (subset vars-cone vars-orig))
1418 vars-orig p
1420 vars-orig equations-orig vars-cone eqn-cone eq-rec))
1427 (implies (and (all-evaluations-p states-orig vars-orig)
1428 (evaluation-p r vars-orig)
1429 (subset vars-cone vars-orig)
1430 (consistent-p-equations vars-orig eqn equations-orig)
1431 (evaluation-eq r (produce-next-state vars-orig p eqn)
1432 vars-orig))
1434 r (create-next-states-of-p p states-orig vars-orig equations-orig)
1440 (vars vars-orig)
1443 p states-orig vars-orig
1444 equations-orig)))))))
1506 (defthm next-state-of-orig-to-evaluation-eq-member-p-2
1514 (uniquep vars-orig)
1516 (subset vars-cone vars-orig)
1517 (all-evaluations-p states-orig vars-orig)
1518 (evaluation-p r vars-orig)
1519 (consistent-p-equations vars-orig eqn equations-orig)
1520 (evaluation-eq r (produce-next-state vars-orig p eqn)
1521 vars-orig))
1523 s (create-next-states-of-p p states-orig vars-orig equations-orig)
1541 (cons-list-p vars-orig equations-orig)
1542 (equation-equal-p equations-orig equations-cone vars-cone)
1543 (uniquep vars-orig)
1546 vars-orig
1548 vars-orig equations-orig vars-cone eqn eqn-rec)
1549 equations-orig))
1552 vars-orig equations-orig vars-cone eqn eqn-rec)
1557 (v (car vars-orig))
1562 (defthm next-state-cone->orig-thus-settled
1568 (consistent-equation-record-p vars-orig equations-orig)
1569 (subset vars-cone vars-orig)
1570 (evaluation-p p vars-orig)
1572 (all-evaluations-p states-orig vars-orig)
1573 (uniquep vars-orig)
1575 (cons-list-p vars-orig equations-orig)
1576 (equation-equal-p equations-orig equations-cone vars-cone)
1577 (consistent-equation-record-p vars-orig equations-orig)
1581 s (create-next-states-of-p p states-orig vars-orig equations-orig)
1588 next-state-of-orig-to-evaluation-eq-member-p-2)
1589 :use ((:instance next-state-of-orig-to-evaluation-eq-member-p-2
1591 vars-orig p
1593 vars-orig equations-orig vars-cone
1598 vars-orig equations-orig vars-cone
1603 (vars vars-orig)
1604 (equations equations-orig)
1606 vars-orig equations-orig vars-cone
1618 (defthm next-state-cone->orig-concretized
1624 (consistent-equation-record-p vars-orig equations-orig)
1625 (subset vars-cone vars-orig)
1626 (evaluation-p p vars-orig)
1628 (all-evaluations-p states-orig vars-orig)
1629 (uniquep vars-orig)
1631 (cons-list-p vars-orig equations-orig)
1632 (equation-equal-p equations-orig equations-cone vars-cone)
1633 (consistent-equation-record-p vars-orig equations-orig)
1637 l (create-next-states-of-p p states-orig vars-orig equations-orig)
1642 (defthm and-fully-concretized-cone->orig
1646 (consistent-equation-record-p vars-orig equations-orig)
1647 (subset vars-cone vars-orig)
1648 (only-evaluations-p states-orig vars-orig)
1650 (memberp p states-orig)
1653 (all-evaluations-p states-orig vars-orig)
1654 (uniquep vars-orig)
1656 (cons-list-p vars-orig equations-orig)
1657 (equation-equal-p equations-orig equations-cone vars-cone)
1658 (consistent-equation-record-p vars-orig equations-orig)
1664 (create-next-states-of-p p states-orig vars-orig equations-orig)
1667 :in-theory (disable next-state-cone->orig-concretized)
1668 :use ((:instance next-state-cone->orig-concretized
1696 (defthm well-formed-transition-p-aux-orig->cone
1700 (consistent-equation-record-p vars-orig equations-orig)
1701 (subset vars-cone vars-orig)
1702 (only-evaluations-p states-orig vars-orig)
1703 (memberp p states-orig)
1704 (uniquep vars-orig)
1709 (equation-equal-p equations-orig equations-cone vars-cone)
1713 (<- (create-next-states states-orig states-orig vars-orig
1714 equations-orig)
1723 (defthm well-formed-transition-p-aux-cone->orig
1727 (consistent-equation-record-p vars-orig equations-orig)
1728 (subset vars-cone vars-orig)
1729 (only-evaluations-p states-orig vars-orig)
1731 (memberp p states-orig)
1734 (all-evaluations-p states-orig vars-orig)
1735 (uniquep vars-orig)
1737 (cons-list-p vars-orig equations-orig)
1738 (equation-equal-p equations-orig equations-cone vars-cone)
1739 (consistent-equation-record-p vars-orig equations-orig)
1746 (<- (create-next-states states-orig states-orig vars-orig
1747 equations-orig)
1753 (defthm well-formed-transition-p-aux-cone->orig-concretized
1757 (consistent-equation-record-p vars-orig equations-orig)
1758 (subset vars-cone vars-orig)
1759 (only-evaluations-p states-orig vars-orig)
1761 (memberp p states-orig)
1764 (all-evaluations-p states-orig vars-orig)
1765 (uniquep vars-orig)
1767 (cons-list-p vars-orig equations-orig)
1768 (equation-equal-p equations-orig equations-cone vars-cone)
1769 (consistent-equation-record-p vars-orig equations-orig)
1776 (<- (create-next-states states-orig states-orig vars-orig
1777 equations-orig)
1781 :in-theory (disable and-fully-concretized-cone->orig
1784 next-state-cone->orig-concretized
1785 well-formed-transition-p-aux-cone->orig)
1786 :use ((:instance well-formed-transition-p-aux-cone->orig)
1812 (defthm orig-cone-cone-is-well-formed-transition-p
1827 :in-theory (disable well-formed-transition-p-aux-orig->cone
1829 :use ((:instance well-formed-transition-p-aux-orig->cone
1830 (states-orig (states (create-kripke C)))
1835 (vars-orig (variables C))
1838 (equations-orig (equations C))
1872 (defthm cone-orig-is-well-formed-transition-p
1887 :in-theory (disable well-formed-transition-p-aux-orig->cone
1889 :use ((:instance well-formed-transition-p-aux-cone->orig-concretized
1890 (states-orig (states (create-kripke C)))
1895 (vars-orig (variables C))
1898 (equations-orig (equations C))