ACL2 !>:pe po d 1 (ENCAPSULATE (((WRITEP *) => *) ((READP *) => *) ((ADDR *) => *) ((PROC *) => *) ((PO * *) => *) ((RF * *) => *) ((CO * *) => *) ((RF-INV-FN *) => *)) (LOCAL (DEFUN WRITEP (X) (DECLARE (IGNORE X)) T)) (LOCAL (DEFUN READP (X) (DECLARE (IGNORE X)) NIL)) (LOCAL (DEFUN ADDR (X) (DECLARE (IGNORE X)) 0)) (LOCAL (DEFUN PROC (X) (DECLARE (IGNORE X)) 0)) (DEFTHM WRITEP-BOOLEANP (BOOLEANP (WRITEP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION WRITEP-BOOLEANP))) (DEFTHM READP-BOOLEANP (BOOLEANP (READP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION READP-BOOLEANP))) (DEFTHM READ-WRITE-EXCLUSIVE (IMPLIES (READP X) (NOT (WRITEP X))) :RULE-CLASSES :FORWARD-CHAINING) (LOCAL (DEFUN PO (X Y) (AND (LEXORDER X Y) (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y))))) (LOCAL (DEFUN RF (X Y) (AND (WRITEP X) (READP Y) (EQUAL (ADDR X) (ADDR Y)) (LEXORDER X Y)))) (LOCAL (DEFUN CO (X Y) (AND (LEXORDER X Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y))))) (DEFTHM PO-BOOLEANP (BOOLEANP (PO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION PO-BOOLEANP))) (DEFTHM RF-BOOLEANP (BOOLEANP (RF X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION RF-BOOLEANP))) (DEFTHM CO-BOOLEANP (BOOLEANP (CO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION CO-BOOLEANP))) (LOCAL (DEFUN RF-INV-FN (X) (NOT X))) (DEFTHMD PO-PROC (IMPLIES (PO X Y) (EQUAL (PROC X) (PROC Y)))) (DEFTHM PO-READ-OR-WRITE-1 (IMPLIES (AND (PO X Y) (NOT (READP X))) (WRITEP X))) (DEFTHM PO-READ-OR-WRITE-2 (IMPLIES (AND (PO X Y) (NOT (READP Y))) (WRITEP Y))) (DEFTHM PO-IRREFLEXIVE (NOT (PO X X))) (DEFTHM PO-TRANSITIVE (IMPLIES (AND (PO X Y) (PO Y Z)) (PO X Z)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ALL))) (DEFTHM PO-TOTAL (IMPLIES (AND (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y)) (NOT (PO X Y))) (PO Y X))) (DEFTHM RF-INV-FN-IRREFLEXIVE (NOT (EQUAL (RF-INV-FN X) X))) (DEFTHM RF-INV-FN-READ-WRITE (IMPLIES (READP R) (WRITEP (RF-INV-FN R)))) (DEFTHM RF-WRITE-READ (IMPLIES (RF W R) (AND (WRITEP W) (READP R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-ADDR (IMPLIES (RF W R) (EQUAL (ADDR W) (ADDR R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-RF-INV-FN (EQUAL (READP R) (RF (RF-INV-FN R) R))) (DEFTHM RF-WRITE-UNIQUE (IMPLIES (SYNTAXP (NOT (EQUAL W (CONS 'RF-INV-FN (CONS X 'NIL))))) (EQUAL (RF W X) (AND (READP X) (EQUAL W (RF-INV-FN X)))))) (DEFTHM CO-WRITE-WRITE (IMPLIES (CO X Y) (AND (WRITEP X) (WRITEP Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD CO-ADDR (IMPLIES (CO X Y) (EQUAL (ADDR X) (ADDR Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHM CO-IRREFLEXIVE (NOT (CO X X))) (DEFTHM CO-TRANSITIVE (IMPLIES (AND (CO X Y) (CO Y Z)) (CO X Z))) (DEFTHM CO-TOTAL (IMPLIES (AND (WRITEP X) (WRITEP Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y)) (NOT (CO X Y))) (CO Y X)))) ACL2 !>:pc po-proc d 1 (ENCAPSULATE (((WRITEP *) => *) ((READP *) => *) ((ADDR *) => *) ((PROC *) => *) ((PO * *) => *) ((RF * *) => *) ((CO * *) => *) ((RF-INV-FN *) => *)) (LOCAL (DEFUN WRITEP (X) (DECLARE (IGNORE X)) T)) (LOCAL (DEFUN READP (X) (DECLARE (IGNORE X)) NIL)) (LOCAL (DEFUN ADDR (X) (DECLARE (IGNORE X)) 0)) (LOCAL (DEFUN PROC (X) (DECLARE (IGNORE X)) 0)) (DEFTHM WRITEP-BOOLEANP (BOOLEANP (WRITEP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION WRITEP-BOOLEANP))) (DEFTHM READP-BOOLEANP (BOOLEANP (READP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION READP-BOOLEANP))) (DEFTHM READ-WRITE-EXCLUSIVE (IMPLIES (READP X) (NOT (WRITEP X))) :RULE-CLASSES :FORWARD-CHAINING) (LOCAL (DEFUN PO (X Y) (AND (LEXORDER X Y) (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y))))) (LOCAL (DEFUN RF (X Y) (AND (WRITEP X) (READP Y) (EQUAL (ADDR X) (ADDR Y)) (LEXORDER X Y)))) (LOCAL (DEFUN CO (X Y) (AND (LEXORDER X Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y))))) (DEFTHM PO-BOOLEANP (BOOLEANP (PO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION PO-BOOLEANP))) (DEFTHM RF-BOOLEANP (BOOLEANP (RF X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION RF-BOOLEANP))) (DEFTHM CO-BOOLEANP (BOOLEANP (CO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION CO-BOOLEANP))) (LOCAL (DEFUN RF-INV-FN (X) (NOT X))) (DEFTHMD PO-PROC (IMPLIES (PO X Y) (EQUAL (PROC X) (PROC Y)))) (DEFTHM PO-READ-OR-WRITE-1 (IMPLIES (AND (PO X Y) (NOT (READP X))) (WRITEP X))) (DEFTHM PO-READ-OR-WRITE-2 (IMPLIES (AND (PO X Y) (NOT (READP Y))) (WRITEP Y))) (DEFTHM PO-IRREFLEXIVE (NOT (PO X X))) (DEFTHM PO-TRANSITIVE (IMPLIES (AND (PO X Y) (PO Y Z)) (PO X Z)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ALL))) (DEFTHM PO-TOTAL (IMPLIES (AND (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y)) (NOT (PO X Y))) (PO Y X))) (DEFTHM RF-INV-FN-IRREFLEXIVE (NOT (EQUAL (RF-INV-FN X) X))) (DEFTHM RF-INV-FN-READ-WRITE (IMPLIES (READP R) (WRITEP (RF-INV-FN R)))) (DEFTHM RF-WRITE-READ (IMPLIES (RF W R) (AND (WRITEP W) (READP R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-ADDR (IMPLIES (RF W R) (EQUAL (ADDR W) (ADDR R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-RF-INV-FN (EQUAL (READP R) (RF (RF-INV-FN R) R))) (DEFTHM RF-WRITE-UNIQUE (IMPLIES (SYNTAXP (NOT (EQUAL W (CONS 'RF-INV-FN (CONS X 'NIL))))) (EQUAL (RF W X) (AND (READP X) (EQUAL W (RF-INV-FN X)))))) (DEFTHM CO-WRITE-WRITE (IMPLIES (CO X Y) (AND (WRITEP X) (WRITEP Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD CO-ADDR (IMPLIES (CO X Y) (EQUAL (ADDR X) (ADDR Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHM CO-IRREFLEXIVE (NOT (CO X X))) (DEFTHM CO-TRANSITIVE (IMPLIES (AND (CO X Y) (CO Y Z)) (CO X Z))) (DEFTHM CO-TOTAL (IMPLIES (AND (WRITEP X) (WRITEP Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y)) (NOT (CO X Y))) (CO Y X)))) ACL2 !>:pf po-proc (IMPLIES (PO X Y) (EQUAL (PROC X) (PROC Y))) ACL2 !>:pf po-total (IMPLIES (AND (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y)) (NOT (PO X Y))) (PO Y X)) ACL2 !>:pf co-total (IMPLIES (AND (WRITEP X) (WRITEP Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y)) (NOT (CO X Y))) (CO Y X)) ACL2 !>:pf rf-rf-inv-fn (EQUAL (READP R) (RF (RF-INV-FN R) R)) ACL2 !>:pf rf-write-unique (IMPLIES (SYNTAXP (NOT (EQUAL W (CONS 'RF-INV-FN (CONS X 'NIL))))) (EQUAL (RF W X) (AND (READP X) (EQUAL W (RF-INV-FN X))))) ACL2 !>:pc fr d 5 (DEFUN-SK FR (X Z) (EXISTS Y (AND (RF Y X) (CO Y Z)))) ACL2 !>:pc fr-rewrite D 6 (DEFTHM FR-REWRITE (EQUAL (FR X Z) (AND (RF (RF-INV-FN X) X) (CO (RF-INV-FN X) Z))) :HINTS (("Goal" :USE ((:INSTANCE FR-SUFF (Y (RF-INV-FN X))))))) ACL2 !>:pc com L 9 (DEFUN COM (X Y) (OR (RF X Y) (CO X Y) (FR X Y))) ACL2 !>:pc com-pathp L d 43 (DEFUN COM-PATHP (PATH X Y) (COND ((ENDP PATH) (COM X Y)) (T (AND (COM X (CAR PATH)) (COM-PATHP (CDR PATH) (CAR PATH) Y))))) ACL2 !>:pc com+ d 46 (DEFUN-SK COM+ (X Y) (EXISTS PATH (COM-PATHP PATH X Y))) ACL2 !>:pc rewrite-com+ D 71 (DEFTHM REWRITE-COM+ (EQUAL (COM+ X Y) (COM+-ALT X Y) ) :HINTS (("Goal" :IN-THEORY (ENABLE REWRITE-COM+-IFF)))) ACL2 !>:pc com+-alt L d 55 (DEFUN COM+-ALT (X Y) (OR (COM X Y) (CO->RF X Y) (FR->RF X Y))) ACL2 !>:pc co->rf d 14 (DEFUN-SK CO->RF (X Z) (EXISTS Y (AND (CO X Y) (RF Y Z)))) ACL2 !>:pc fr->rf d 18 (DEFUN-SK FR->RF (X Z) (EXISTS Y (AND (FR X Y) (RF Y Z)))) ACL2 !>:pc pol L d 73 (DEFUN POL (X Y) (AND (PO X Y) (EQUAL (ADDR X) (ADDR Y)))) ACL2 !>:pc pol-com L 78 (DEFUN POL-COM (X Y) (OR (POL X Y) (COM X Y))) ACL2 !>:pc pol-com-cyclep L d 80 (DEFUN POL-COM-CYCLEP (CYCLE X) (POL-COM-PATHP CYCLE X X)) ACL2 !>:pc sc-per-location-1 d 107 (DEFUN-SK SC-PER-LOCATION-1 NIL (FORALL (X POTENTIAL-CYCLE) (NOT (POL-COM-CYCLEP POTENTIAL-CYCLE X)))) ACL2 !>:pc sc-per-location-2 d 108 (DEFUN-SK SC-PER-LOCATION-2 NIL (FORALL (X Y) (IMPLIES (POL X Y) (NOT (COM+ Y X))))) ACL2 !>:pc sc-per-location-1-implies-2 125 (DEFTHM SC-PER-LOCATION-1-IMPLIES-2 (IMPLIES (SC-PER-LOCATION-1) (SC-PER-LOCATION-2)) :HINTS (("Goal" :IN-THEORY (DISABLE SC-PER-LOCATION-1 POL)))) ACL2 !>:pc com+-alt-totality 64 (DEFTHM COM+-ALT-TOTALITY (IMPLIES (AND (OR (READP X) (WRITEP X)) (OR (READP Y) (WRITEP Y)) (EQUAL (ADDR X) (ADDR Y)) (NOT (COM+-ALT X Y)) (NOT (AND (WRITEP X) (WRITEP Y) (EQUAL X Y))) (NOT (AND (READP X) (READP Y) (EQUAL (RF-INV-FN X) (RF-INV-FN Y))))) (COM+-ALT Y X))) ACL2 !>:pc cycle-n 132 (DEFTHM CYCLE-N (IMPLIES (AND (POL-COM+-CYCLEP (LIST* P1 P2 RST) X) (NOT (POL-COM+-CYCLEP (LIST* P2 RST) X)) (NOT (POL-COM+-CYCLEP RST X)) (NOT (POL-COM+-CYCLEP (LIST P2) P1))) (POL-COM+-CYCLEP (LIST P1) X)) :HINTS (("Goal" :CASES ((COM+-ALT X P2) (AND (WRITEP X) (WRITEP P2) (EQUAL X P2)) (AND (READP X) (READP P2) (EQUAL (RF-INV-FN X) (RF-INV-FN P2))) (COM+-ALT P2 X))))) ACL2 !>:pc collapse-cycle L d 134 (DEFUN COLLAPSE-CYCLE (CYCLE X) (LET* ((P1 (CAR CYCLE)) (P2 (CADR CYCLE)) (RST (CDDR CYCLE))) (COND ((ENDP CYCLE) (MV NIL X)) ((ENDP (CDR CYCLE)) (IF (POL X (CAR CYCLE)) (MV X (CAR CYCLE)) (MV (CAR CYCLE) X))) ((POL-COM+-CYCLEP (LIST* P2 RST) X) (COLLAPSE-CYCLE (LIST* P2 RST) X)) ((POL-COM+-CYCLEP RST X) (COLLAPSE-CYCLE RST X)) ((POL-COM+-CYCLEP (LIST P2) P1) (COLLAPSE-CYCLE (LIST P2) P1)) (T (COLLAPSE-CYCLE (LIST P1) X))))) ACL2 !>:pc sc-per-location-2-implies-1-unquantified 138 (DEFTHM SC-PER-LOCATION-2-IMPLIES-1-UNQUANTIFIED (IMPLIES (SC-PER-LOCATION-2) (NOT (POL-COM-CYCLEP CYCLE A))) :HINTS (("Goal" :IN-THEORY (DISABLE SC-PER-LOCATION-2 MV-NTH) :USE ((:INSTANCE SC-PER-LOCATION-2-NECC (X (MV-LET (NEW-X NEW-Y) (COLLAPSE-CYCLE CYCLE A) (DECLARE (IGNORE NEW-Y)) NEW-X)) (Y (MV-LET (NEW-X NEW-Y) (COLLAPSE-CYCLE CYCLE A) (DECLARE (IGNORE NEW-X)) NEW-Y))))))) ACL2 !>:pc com+ d 46 (DEFUN-SK COM+ (X Y) (EXISTS PATH (COM-PATHP PATH X Y))) ACL2 !>:pc com+-alt L d 55 (DEFUN COM+-ALT (X Y) (OR (COM X Y) (CO->RF X Y) (FR->RF X Y))) ACL2 !>:pc sc-per-location-2-implies- ACL2 Error in :PC: The object SC-PER-LOCATION-2-IMPLIES- is not a logical name. See :DOC logical-name. ACL2 !>:pc sc-per-location-2-implies-1 139 (DEFTHM SC-PER-LOCATION-2-IMPLIES-1 (IMPLIES (SC-PER-LOCATION-2) (SC-PER-LOCATION-1))) ACL2 !>(rebuild "~/research/jade/executions.lisp" :all) ACL2 loading "~/research/jade/executions.lisp". "ACL2" :REDUNDANT :REDUNDANT ACL2 Observation in ( DEFTHM RF-INV-FN-ADDR ...): The :TRIGGER-TERMS for the :FORWARD-CHAINING rule RF-INV-FN-ADDR will consist of the list containing (READP X). :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) ACL2 Observation in ( DEFTHM FR-READ-WRITE ...): The :TRIGGER-TERMS for the :FORWARD-CHAINING rule FR-READ-WRITE will consist of the list containing (FR X Y). :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) ACL2 Observation in ( DEFTHM CO->RF-WRITE-READ ...): The :TRIGGER- TERMS for the :FORWARD-CHAINING rule CO->RF-WRITE-READ will consist of the list containing (CO->RF X Y). :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT ACL2 Observation in ( DEFTHM FR->RF-READ-READ ...): The :TRIGGER- TERMS for the :FORWARD-CHAINING rule FR->RF-READ-READ will consist of the list containing (FR->RF X Y). :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:DEFTHMD FR->RF-REWRITE-LEMMA1) (:DEFTHMD FR->RF-REWRITE-LEMMA2) (:NUMBER-OF-ENABLED-RUNES 3213) (:DEFTHMD FR->RF-REWRITE-IFF) (:NUMBER-OF-ENABLED-RUNES 3211) (:DEFTHMD FR->RF-REWRITE) :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT :REDUNDANT ACL2 Observation in ( DEFTHM COM+-ALT-READ-OR-WRITE ...): The :TRIGGER- TERMS for the :FORWARD-CHAINING rule COM+-ALT-READ-OR-WRITE will consist of the list containing (COM+-ALT X Y). :REDUNDANT ACL2 Observation in ( DEFTHM COM+-ALT-ADDR ...): The :TRIGGER-TERMS for the :FORWARD-CHAINING rule COM+-ALT-ADDR will consist of the list containing (COM+-ALT X Y). :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) (:NUMBER-OF-ENABLED-RUNES 3213) (:DEFTHMD REWRITE-COM+-IFF) (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT Finished loading "~/research/jade/executions.lisp". T ACL2 !>(rebuild "~/research/jade/sc-per-location.lisp" :all) ACL2 loading "~/research/jade/sc-per-location.lisp". "ACL2" :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT ACL2 Observation in ( DEFTHM POL-READ-OR-WRITE-FC ...): The :TRIGGER- TERMS for the :FORWARD-CHAINING rule POL-READ-OR-WRITE-FC will consist of the list containing (POL X Y). :REDUNDANT ACL2 Observation in ( DEFTHM POL-ADDR ...): The :TRIGGER-TERMS for the :FORWARD-CHAINING rule POL-ADDR will consist of the list containing (POL X Y). :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT :REDUNDANT (:DEFTHMD HAT-REWRITE-1) (:DEFTHMD HAT-REWRITE-2) (:NUMBER-OF-ENABLED-RUNES 3212) (:DEFTHMD HAT-REWRITE-IFF) (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:DEFTHMD SC-PER-LOCATION-3-LEMMA1) :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:DEFTHMD SC-PER-LOCATION-2-LEMMA1) :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT :REDUNDANT ACL2 Observation in ( DEFTHM CYCLE-N-LEMMA1 ...): The :TRIGGER-TERMS for the :FORWARD-CHAINING rule CYCLE-N-LEMMA1 will consist of the list containing (POL-COM+-CYCLEP (LIST* P1 P2 RST) X). :REDUNDANT :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT :REDUNDANT (:NUMBER-OF-ENABLED-RUNES 3211) :REDUNDANT :REDUNDANT :REDUNDANT Finished loading "~/research/jade/sc-per-location.lisp". T ACL2 !>(pe 'po) d 1 (ENCAPSULATE (((WRITEP *) => *) ((READP *) => *) ((ADDR *) => *) ((PROC *) => *) ((PO * *) => *) ((RF * *) => *) ((CO * *) => *) ((RF-INV-FN *) => *)) (LOCAL (DEFUN WRITEP (X) (DECLARE (IGNORE X)) T)) (LOCAL (DEFUN READP (X) (DECLARE (IGNORE X)) NIL)) (LOCAL (DEFUN ADDR (X) (DECLARE (IGNORE X)) 0)) (LOCAL (DEFUN PROC (X) (DECLARE (IGNORE X)) 0)) (DEFTHM WRITEP-BOOLEANP (BOOLEANP (WRITEP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION WRITEP-BOOLEANP))) (DEFTHM READP-BOOLEANP (BOOLEANP (READP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION READP-BOOLEANP))) (DEFTHM READ-WRITE-EXCLUSIVE (IMPLIES (READP X) (NOT (WRITEP X))) :RULE-CLASSES :FORWARD-CHAINING) (LOCAL (DEFUN PO (X Y) (AND (LEXORDER X Y) (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y))))) (LOCAL (DEFUN RF (X Y) (AND (WRITEP X) (READP Y) (EQUAL (ADDR X) (ADDR Y)) (LEXORDER X Y)))) (LOCAL (DEFUN CO (X Y) (AND (LEXORDER X Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y))))) (DEFTHM PO-BOOLEANP (BOOLEANP (PO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION PO-BOOLEANP))) (DEFTHM RF-BOOLEANP (BOOLEANP (RF X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION RF-BOOLEANP))) (DEFTHM CO-BOOLEANP (BOOLEANP (CO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION CO-BOOLEANP))) (LOCAL (DEFUN RF-INV-FN (X) (NOT X))) (DEFTHMD PO-PROC (IMPLIES (PO X Y) (EQUAL (PROC X) (PROC Y)))) (DEFTHM PO-READ-OR-WRITE-1 (IMPLIES (AND (PO X Y) (NOT (READP X))) (WRITEP X))) (DEFTHM PO-READ-OR-WRITE-2 (IMPLIES (AND (PO X Y) (NOT (READP Y))) (WRITEP Y))) (DEFTHM PO-IRREFLEXIVE (NOT (PO X X))) (DEFTHM PO-TRANSITIVE (IMPLIES (AND (PO X Y) (PO Y Z)) (PO X Z)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ALL))) (DEFTHM PO-TOTAL (IMPLIES (AND (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y)) (NOT (PO X Y))) (PO Y X))) (DEFTHM RF-INV-FN-IRREFLEXIVE (NOT (EQUAL (RF-INV-FN X) X))) (DEFTHM RF-INV-FN-READ-WRITE (IMPLIES (READP R) (WRITEP (RF-INV-FN R)))) (DEFTHM RF-WRITE-READ (IMPLIES (RF W R) (AND (WRITEP W) (READP R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-ADDR (IMPLIES (RF W R) (EQUAL (ADDR W) (ADDR R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-RF-INV-FN (EQUAL (READP R) (RF (RF-INV-FN R) R))) (DEFTHM RF-WRITE-UNIQUE (IMPLIES (SYNTAXP (NOT (EQUAL W (CONS 'RF-INV-FN (CONS X 'NIL))))) (EQUAL (RF W X) (AND (READP X) (EQUAL W (RF-INV-FN X)))))) (DEFTHM CO-WRITE-WRITE (IMPLIES (CO X Y) (AND (WRITEP X) (WRITEP Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD CO-ADDR (IMPLIES (CO X Y) (EQUAL (ADDR X) (ADDR Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHM CO-IRREFLEXIVE (NOT (CO X X))) (DEFTHM CO-TRANSITIVE (IMPLIES (AND (CO X Y) (CO Y Z)) (CO X Z))) (DEFTHM CO-TOTAL (IMPLIES (AND (WRITEP X) (WRITEP Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y)) (NOT (CO X Y))) (CO Y X)))) ACL2 !>(pe 'po) d 1 (ENCAPSULATE (((WRITEP *) => *) ((READP *) => *) ((ADDR *) => *) ((PROC *) => *) ((PO * *) => *) ((RF * *) => *) ((CO * *) => *) ((RF-INV-FN *) => *)) (LOCAL (DEFUN WRITEP (X) (DECLARE (IGNORE X)) T)) (LOCAL (DEFUN READP (X) (DECLARE (IGNORE X)) NIL)) (LOCAL (DEFUN ADDR (X) (DECLARE (IGNORE X)) 0)) (LOCAL (DEFUN PROC (X) (DECLARE (IGNORE X)) 0)) (DEFTHM WRITEP-BOOLEANP (BOOLEANP (WRITEP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION WRITEP-BOOLEANP))) (DEFTHM READP-BOOLEANP (BOOLEANP (READP X)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION READP-BOOLEANP))) (DEFTHM READ-WRITE-EXCLUSIVE (IMPLIES (READP X) (NOT (WRITEP X))) :RULE-CLASSES :FORWARD-CHAINING) (LOCAL (DEFUN PO (X Y) (AND (LEXORDER X Y) (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y))))) (LOCAL (DEFUN RF (X Y) (AND (WRITEP X) (READP Y) (EQUAL (ADDR X) (ADDR Y)) (LEXORDER X Y)))) (LOCAL (DEFUN CO (X Y) (AND (LEXORDER X Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y))))) (DEFTHM PO-BOOLEANP (BOOLEANP (PO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION PO-BOOLEANP))) (DEFTHM RF-BOOLEANP (BOOLEANP (RF X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION RF-BOOLEANP))) (DEFTHM CO-BOOLEANP (BOOLEANP (CO X Y)) :RULE-CLASSES (:REWRITE :TYPE-PRESCRIPTION)) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION CO-BOOLEANP))) (LOCAL (DEFUN RF-INV-FN (X) (NOT X))) (DEFTHMD PO-PROC (IMPLIES (PO X Y) (EQUAL (PROC X) (PROC Y)))) (DEFTHM PO-READ-OR-WRITE-1 (IMPLIES (AND (PO X Y) (NOT (READP X))) (WRITEP X))) (DEFTHM PO-READ-OR-WRITE-2 (IMPLIES (AND (PO X Y) (NOT (READP Y))) (WRITEP Y))) (DEFTHM PO-IRREFLEXIVE (NOT (PO X X))) (DEFTHM PO-TRANSITIVE (IMPLIES (AND (PO X Y) (PO Y Z)) (PO X Z)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ALL))) (DEFTHM PO-TOTAL (IMPLIES (AND (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y)) (NOT (PO X Y))) (PO Y X))) (DEFTHM RF-INV-FN-IRREFLEXIVE (NOT (EQUAL (RF-INV-FN X) X))) (DEFTHM RF-INV-FN-READ-WRITE (IMPLIES (READP R) (WRITEP (RF-INV-FN R)))) (DEFTHM RF-WRITE-READ (IMPLIES (RF W R) (AND (WRITEP W) (READP R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-ADDR (IMPLIES (RF W R) (EQUAL (ADDR W) (ADDR R))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD RF-RF-INV-FN (EQUAL (READP R) (RF (RF-INV-FN R) R))) (DEFTHM RF-WRITE-UNIQUE (IMPLIES (SYNTAXP (NOT (EQUAL W (CONS 'RF-INV-FN (CONS X 'NIL))))) (EQUAL (RF W X) (AND (READP X) (EQUAL W (RF-INV-FN X)))))) (DEFTHM CO-WRITE-WRITE (IMPLIES (CO X Y) (AND (WRITEP X) (WRITEP Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHMD CO-ADDR (IMPLIES (CO X Y) (EQUAL (ADDR X) (ADDR Y))) :RULE-CLASSES :FORWARD-CHAINING) (DEFTHM CO-IRREFLEXIVE (NOT (CO X X))) (DEFTHM CO-TRANSITIVE (IMPLIES (AND (CO X Y) (CO Y Z)) (CO X Z))) (DEFTHM CO-TOTAL (IMPLIES (AND (WRITEP X) (WRITEP Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y)) (NOT (CO X Y))) (CO Y X)))) ACL2 !>(pf 'po-proc) (IMPLIES (PO X Y) (EQUAL (PROC X) (PROC Y))) ACL2 !>(pf 'po-total) (IMPLIES (AND (EQUAL (PROC X) (PROC Y)) (NOT (EQUAL X Y)) (NOT (PO X Y))) (PO Y X)) ACL2 !>(pf 'co-total) (IMPLIES (AND (WRITEP X) (WRITEP Y) (EQUAL (ADDR X) (ADDR Y)) (NOT (EQUAL X Y)) (NOT (CO X Y))) (CO Y X)) ACL2 !>(pf 'rf-rf-inv-fn) (EQUAL (READP R) (RF (RF-INV-FN R) R)) ACL2 !>(pf 'rf-write-unique) (IMPLIES (SYNTAXP (NOT (EQUAL W (CONS 'RF-INV-FN (CONS X 'NIL))))) (EQUAL (RF W X) (AND (READP X) (EQUAL W (RF-INV-FN X))))) ACL2 !>(pc 'fr) d 5 (DEFUN-SK FR (X Z) (EXISTS Y (AND (RF Y X) (CO Y Z)))) ACL2 !>(pc 'fr-rewrite) D 6 (DEFTHM FR-REWRITE (EQUAL (FR X Z) (AND (RF (RF-INV-FN X) X) (CO (RF-INV-FN X) Z))) :HINTS (("Goal" :USE ((:INSTANCE FR-SUFF (Y (RF-INV-FN X))))))) ACL2 !>(pc 'com) L 9 (DEFUN COM (X Y) (OR (RF X Y) (CO X Y) (FR X Y))) ACL2 !>(pc 'com-pathp) L d 43 (DEFUN COM-PATHP (PATH X Y) (COND ((ENDP PATH) (COM X Y)) (T (AND (COM X (CAR PATH)) (COM-PATHP (CDR PATH) (CAR PATH) Y))))) ACL2 !>(pc 'com+) d 46 (DEFUN-SK COM+ (X Y) (EXISTS PATH (COM-PATHP PATH X Y))) ACL2 !>(pc 'com+-alt) L d 55 (DEFUN COM+-ALT (X Y) (OR (COM X Y) (CO->RF X Y) (FR->RF X Y))) ACL2 !>(pc 'rewrite-com+) D 71 (DEFTHM REWRITE-COM+ (EQUAL (COM+ X Y) (COM+-ALT X Y)) :HINTS (("Goal" :IN-THEORY (ENABLE REWRITE-COM+-IFF)))) ACL2 !>(pc 'pol) L d 73 (DEFUN POL (X Y) (AND (PO X Y) (EQUAL (ADDR X) (ADDR Y)))) ACL2 !>(pc 'pol-com) L 78 (DEFUN POL-COM (X Y) (OR (POL X Y) (COM X Y))) ACL2 !>(pc 'pol-com-cyclep) L d 80 (DEFUN POL-COM-CYCLEP (CYCLE X) (POL-COM-PATHP CYCLE X X)) ACL2 !>(pc 'sc-per-location-1) d 107 (DEFUN-SK SC-PER-LOCATION-1 NIL (FORALL (X POTENTIAL-CYCLE) (NOT (POL-COM-CYCLEP POTENTIAL-CYCLE X)))) ACL2 !>(pc 'sc-per-location-2) d 108 (DEFUN-SK SC-PER-LOCATION-2 NIL (FORALL (X Y) (IMPLIES (POL X Y) (NOT (COM+ Y X))))) ACL2 !>(pc 'sc-per-location-1-implies-2) 125 (DEFTHM SC-PER-LOCATION-1-IMPLIES-2 (IMPLIES (SC-PER-LOCATION-1) (SC-PER-LOCATION-2)) :HINTS (("Goal" :IN-THEORY (DISABLE SC-PER-LOCATION-1 POL)))) ACL2 !>(pc 'com+-alt-totality) 64 (DEFTHM COM+-ALT-TOTALITY (IMPLIES (AND (OR (READP X) (WRITEP X)) (OR (READP Y) (WRITEP Y)) (EQUAL (ADDR X) (ADDR Y)) (NOT (COM+-ALT X Y)) (NOT (AND (WRITEP X) (WRITEP Y) (EQUAL X Y))) (NOT (AND (READP X) (READP Y) (EQUAL (RF-INV-FN X) (RF-INV-FN Y))))) (COM+-ALT Y X))) ACL2 !>(pc 'cycle-n) 132 (DEFTHM CYCLE-N (IMPLIES (AND (POL-COM+-CYCLEP (LIST* P1 P2 RST) X) (NOT (POL-COM+-CYCLEP (LIST* P2 RST) X)) (NOT (POL-COM+-CYCLEP RST X)) (NOT (POL-COM+-CYCLEP (LIST P2) P1))) (POL-COM+-CYCLEP (LIST P1) X)) :HINTS (("Goal" :CASES ((COM+-ALT X P2) (AND (WRITEP X) (WRITEP P2) (EQUAL X P2)) (AND (READP X) (READP P2) (EQUAL (RF-INV-FN X) (RF-INV-FN P2))) (COM+-ALT P2 X))))) ACL2 !>(pc 'collapse-cycle) L d 134 (DEFUN COLLAPSE-CYCLE (CYCLE X) (LET* ((P1 (CAR CYCLE)) (P2 (CADR CYCLE)) (RST (CDDR CYCLE))) (COND ((ENDP CYCLE) (MV NIL X)) ((ENDP (CDR CYCLE)) (IF (POL X (CAR CYCLE)) (MV X (CAR CYCLE)) (MV (CAR CYCLE) X))) ((POL-COM+-CYCLEP (LIST* P2 RST) X) (COLLAPSE-CYCLE (LIST* P2 RST) X)) ((POL-COM+-CYCLEP RST X) (COLLAPSE-CYCLE RST X)) ((POL-COM+-CYCLEP (LIST P2) P1) (COLLAPSE-CYCLE (LIST P2) P1)) (T (COLLAPSE-CYCLE (LIST P1) X))))) ACL2 !>(pc 'sc-per-location-2-implies-1-unquantified) 138 (DEFTHM SC-PER-LOCATION-2-IMPLIES-1-UNQUANTIFIED (IMPLIES (SC-PER-LOCATION-2) (NOT (POL-COM-CYCLEP CYCLE A))) :HINTS (("Goal" :IN-THEORY (DISABLE SC-PER-LOCATION-2 MV-NTH) :USE ((:INSTANCE SC-PER-LOCATION-2-NECC (X (MV-LET (NEW-X NEW-Y) (COLLAPSE-CYCLE CYCLE A) (DECLARE (IGNORE NEW-Y)) NEW-X)) (Y (MV-LET (NEW-X NEW-Y) (COLLAPSE-CYCLE CYCLE A) (DECLARE (IGNORE NEW-X)) NEW-Y))))))) ACL2 !>(pc 'sc-per-location-2-implies-1) 139 (DEFTHM SC-PER-LOCATION-2-IMPLIES-1 (IMPLIES (SC-PER-LOCATION-2) (SC-PER-LOCATION-1))) ACL2 !>