tests/inputs/cone-of-influence.lisp

66   (implies (and (uniquep x)
94   (implies (memberp e x)
107   (implies (not (memberp e x))
113   (implies (not (equal v e))
120   (implies (and (not (memberp e x))
127   (implies (uniquep x)
132 (defthm uniquep-and-subset-implies-len-<=
133   (implies (and (uniquep x)
146   (implies (and (subset x z)
153   (implies (and (subset (set-union x y) z)
166   (implies (subset (del e y) x)
173    (implies (equal (len x) 0)
180   (implies (and (equal (len x) (len y))
259   (implies (and (uniquep vars)
285   (implies (and (uniquep x)
292   (implies (uniquep vars)
316   (implies (circuitp C)
339   (implies (and (subset vars-prime vars)
346   (implies (and (evaluation-eq-member-p init inits vars)
353   (implies (and (evaluation-eq-subset-p inits states vars)
360   (implies (uniquep vars)
366   (implies (memberp init inits)
373   (implies (and (uniquep vars)
381   (implies (uniquep vars)
389   (implies (circuitp C)
403   (implies (uniquep vars)
409   (implies (and (uniquep vars)
417   (implies (uniquep vars)
424   (implies (circuitp C)
443   (implies (and (evaluation-p p variables)
451   (implies (and (only-evaluations-p init variables)
459   (implies (circuitp C)
471   (implies (not (memberp v vars))
502   (implies (circuitp C)
522   (implies (equation-equal-p eqn-orig eqn-cone vars)
529   (implies (not (memberp v vars))
536   (implies (and (cons-list-p vars equations)
543   (implies (uniquep vars)
556   (implies (circuitp C)
575   (implies (memberp equation equations)
582   (implies (and (memberp v vars)
599   (implies (and (memberp v (find-all-variables vars variables equations))
621   (implies (and (subset vars variables)
659   (implies (and (equation-equal-p eqn-orig eqn-cone vars)
667   (implies (and (consistent-equation-record-p vars eqn-orig)
680   (implies (and (equation-equal-p eqn-orig eqn-cone vars)
701   (implies (circuitp C)
716   (implies (circuitp C)
725   (implies (circuitp C)
754   (implies (and (evaluation-eq p q vars)
765 (defthm next-state-member-implies-consistent-equation
766   (implies (memberp r (create-next-states-of-p p states vars equations))
775   (implies (next-state-is-ok p r vars equations)
784   (implies (next-state-is-ok p r vars equations)
793   (implies (and (next-state-is-ok p r vars-orig equations-orig)
821 ;; this implies r is evaluation-eq-member-p of transition of q, we need to show
829   (implies (and (consistent-p-equations vars eqn equations)
840   (implies (and (memberp s states-cone)
848   (implies (and (memberp s states-cone)
860   (implies (and (all-evaluations-p states-cone vars-cone)
880   (implies (and (memberp q states)
886   (implies (and (all-evaluations-p states-cone vars-cone)
908   (implies (and (evaluation-eq p q vars)
915   (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig
959   (implies (not (memberp v vars))
966   (implies (and (subset vars-cone vars-orig)
977   (implies (and (consistent-p-equations vars eqn equation-record)
987   (implies (and (consistent-p-equations vars eqn equations)
994   (implies (not (memberp v vars))
1001   (implies (and (equation-equal-p eqn-orig eqn-cone vars)
1008   (implies (and (consistent-p-equations vars-orig eqn eqn-orig)
1042   (implies (and (consistent-equation-record-p vars-prime equations)
1056   (implies (and (consistent-equation-record-p vars equations)
1064   (implies (and (evaluation-p p vars)
1076   (implies (not (memberp v vars))
1083   (implies (and (memberp v vars)
1091   (implies (and (evaluation-eq p q vars)
1098   (implies (and (evaluation-p p vars-prime)
1122   (implies (and (evaluation-p p vars-cone)
1137   (implies (and (uniquep vars-orig)
1147   (implies (and (evaluation-p p vars-cone)
1174   (implies (and (evaluation-p p vars-cone)
1199   (implies (and (evaluation-p p vars)
1208   (implies (and (booleanp a)
1217   (implies (and (evaluation-p p vars-prime)
1227   (implies (and (evaluation-p p vars)
1236   (implies (and (memberp r (create-next-states-of-p p states-orig vars-orig
1294   (implies (and (subset l (create-next-states-of-p p states-orig vars-orig
1315   (implies (and (evaluation-p p vars-cone)
1349   (implies (not (memberp v vars))
1356   (implies (and (memberp v vars-cone)
1369   (implies (not (memberp v vars-orig))
1378   (implies (and (not (memberp v vars-cone))
1390   (implies (and (subset vars-cone vars-orig)
1405   (implies (and (evaluation-p p vars-cone)
1427    (implies (and (all-evaluations-p states-orig vars-orig)
1449   (implies (and (next-state-is-ok q s vars-cone equations-cone)
1466   (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone
1477                                next-state-member-implies-consistent-equation)
1478            :use ((:instance next-state-member-implies-consistent-equation
1500   (implies (and (evaluation-eq s r vars)
1507   (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone
1540   (implies (and (consistent-p-equations vars-cone eqn equations-cone)
1563    (implies (and (memberp s (create-next-states-of-p q states-cone vars-cone
1619    (implies (and (subset l (create-next-states-of-p q states-cone vars-cone
1643    (implies (and (evaluation-p p vars-cone)
1679   (implies (not (memberp p states))
1687   (implies (memberp p states)
1697    (implies (and (evaluation-p p vars-cone)
1724    (implies (and (evaluation-p p vars-cone)
1754    (implies (and (evaluation-p p vars-cone)
1813   (implies (circuitp C)
1873   (implies (circuitp C)
1940   (implies (circuitp C)
1952   (implies (and (restricted-formulap f vars)
1958 ;;   (implies (and (restricted-formulap f (cone-variables vars C))
1966 ;;                                circuit-bisim-implies-same-ltl-semantics)
1967 ;;            :use ((:instance circuit-bisim-implies-same-ltl-semantics
1976 ;;   (implies (and (subset interesting-vars (cone-variables vars C))
1990   (implies (circuitp C)
1998   (implies (circuitp C)