Lines Matching defs:produce
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