tests/inputs/cone-of-influence.lisp

58 (defthm uniquep-member-reduction
106 (defthm del-not-member-reduction
112 (defthm member-del-reduction
119 (defthm subset-del-member
273 (defthm member-remove-duplicate-reduction
345 (defthm evaluation-eq-member-subset-reduction
346   (implies (and (evaluation-eq-member-p init inits vars)
348            (evaluation-eq-member-p init inits vars-prime)))
365 (defthm corresponding-state-is-member-of-corresponding-states
375            (evaluation-eq-member-p init (corresponding-states inits vars)
411            (evaluation-eq-member-p  init inits
528 (defthm find-equations-for-not-member-p
658 (defthm equation-equal-p-member-reduction
765 (defthm next-state-member-implies-consistent-equation
821 ;; this implies r is evaluation-eq-member-p of transition of q, we need to show
822 ;; that s is a member of states-cone and that there is a consistent equation
854 ;; OK, so now, how do we show that s is a member of states? This is because
859 (defthm member-of-next-states-from-all-evaluations-p
865             (evaluation-eq-member s states-cone vars-cone)
871                             (s (evaluation-eq-member s states-cone vars-cone)))
874                             (q (evaluation-eq-member s states-cone vars-cone))
882            (evaluation-eq-member-p p states vars)))
891            (evaluation-eq-member-p
899                             (q (evaluation-eq-member s states-cone vars-cone))
909                 (evaluation-eq-member-p q states vars))
910            (evaluation-eq-member-p p states vars)))
914 (defthm next-state-of-orig-to-evaluation-eq-member-p
928            (evaluation-eq-member-p
993 (defthm consistent-set-not-member
1235 (defthm r-is-evaluation-eq-member-p-with-respect-to-states
1250             (evaluation-eq-member-p
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
1433             (evaluation-eq-member-p
1437             :in-theory (disable evaluation-eq-member-subset-reduction)
1438             :use ((:instance evaluation-eq-member-subset-reduction
1477                                next-state-member-implies-consistent-equation)
1478            :use ((:instance next-state-member-implies-consistent-equation
1499 (defthm evaluation-eq-member-p-from-memberp
1501                 (evaluation-eq-member-p r states vars))
1502            (evaluation-eq-member-p s states vars)))
1506 (defthm next-state-of-orig-to-evaluation-eq-member-p-2
1522            (evaluation-eq-member-p
1580             (evaluation-eq-member-p
1588                         next-state-of-orig-to-evaluation-eq-member-p-2)
1589             :use ((:instance next-state-of-orig-to-evaluation-eq-member-p-2
1678 (defthm not-member-p-to-next-states
1783                                 evaluation-eq-member-p