tests/inputs/cone-of-influence.lisp

785            (evaluation-eq r (produce-next-state vars p
794                 (evaluation-eq (produce-next-state vars-orig p
820 ;; produce-next-state produces something evaluation-eq to s. Now to show that
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))
889                 (evaluation-eq s (produce-next-state vars-cone q eqn)
917                (evaluation-eq (produce-next-state vars-orig p
926                 (evaluation-eq s (produce-next-state vars-cone q eqn)
939 ;; (produce-next-state vars-cone q eqn). Hence the only thing to prove is that
1075 (defthm produce-next-state-not-memberp-vars-reduction
1077            (equal (<- (produce-next-state vars p equations) v)
1082 (defthm produce-next-state-vars-reduction
1085            (equal (<- (produce-next-state vars p equations) v)
1097 (defthm produce-next-state-is-evaluation-eq
1108             (produce-next-state vars p eqn-orig)
1109             (produce-next-state vars q eqn-cone)
1121 (defthm produce-next-state-is-evaluation-eq-concretized
1130             (produce-next-state vars-cone p eqn-orig)
1131             (produce-next-state vars-cone q eqn-cone)
1136 (defthm produce-next-state-evaluation-eq-reduction
1140            (evaluation-eq (produce-next-state vars-orig p eqn-orig)
1141                           (produce-next-state vars-cone p eqn-orig)
1146 (defthm produce-next-state-fully-concretized
1156            (evaluation-eq (produce-next-state vars-orig p eqn-orig)
1157                           (produce-next-state vars-cone q eqn-cone)
1163                                produce-next-state-is-evaluation-eq-concretized)
1164            :use ((:instance produce-next-state-is-evaluation-eq-concretized)
1166                             (p (produce-next-state vars-orig p eqn-orig))
1167                             (q (produce-next-state vars-cone p eqn-orig))
1168                             (r (produce-next-state vars-cone q eqn-cone))
1173 (defthm produce-next-state-for-equation-of-choice
1185             (produce-next-state vars-orig p eqn-orig)
1186             (produce-next-state
1216 (defthm produce-next-state-is-evaluation-p
1222            (evaluation-p (produce-next-state vars p eqn) vars-prime)))
1231            (evaluation-p (produce-next-state vars p eqn) vars)))
1258                             (s (produce-next-state vars-orig p
1404 (defthm produce-next-state-for-equation-of-choice-2
1417             (produce-next-state
1421             (produce-next-state vars-cone q eqn-cone)
1431                  (evaluation-eq r (produce-next-state vars-orig p eqn)
1450                 (evaluation-eq  (produce-next-state
1468                 (evaluation-eq r (produce-next-state
1492                             (q (produce-next-state
1509                (evaluation-eq r (produce-next-state
1520                (evaluation-eq r (produce-next-state vars-orig p eqn)
1527            :in-theory (disable ;; produce-next-state-evaluation-eq-reduction
1590                               (r (produce-next-state