Lines Matching defs:member
40 (defun evaluation-eq-member-p (st states vars)
43 (evaluation-eq-member-p st (rest states) vars))))
45 (defun evaluation-eq-member (st states vars)
49 (evaluation-eq-member st (rest states) vars))))
51 (defthm member-is-memberp
52 (implies (evaluation-eq-member-p p states vars)
53 (memberp (evaluation-eq-member p states vars)
56 (defthm member-is-evaluation-eq
57 (implies (evaluation-eq-member-p p states vars)
58 (evaluation-eq p (evaluation-eq-member p states vars)
93 (evaluation-eq-member-p st states vars))))
97 (and (evaluation-eq-member-p (first m-states) n-states vars)
100 (defthm evaluation-eq-subset-to-member
103 (evaluation-eq-member-p p n-states vars)))
228 (evaluation-eq-member s (initial-states n) vars))
232 (evaluation-eq-member s (initial-states m) vars))
234 (defthm all-evaluations-considers-an-evaluation-a-member
237 (evaluation-eq-member-p st states vars))
261 (defthm subset-transitive-member
278 :in-theory (disable member-is-memberp
279 evaluation-eq-subset-to-member)
280 :use ((:instance evaluation-eq-subset-to-member
284 (:instance member-is-memberp
299 :in-theory (disable member-is-memberp
300 evaluation-eq-subset-to-member)
301 :use ((:instance evaluation-eq-subset-to-member
305 (:instance member-is-memberp
310 (p (evaluation-eq-member s (initial-states m) vars))
437 (evaluation-eq-member r (<- (transition n) q) vars))
441 (evaluation-eq-member r (<- (transition m) p) vars))
453 (defthm r-is-evaluation-eq-member-p
461 (evaluation-eq-member-p r (<- trans-n q) vars))
467 (defthm c-bisimilar-witness-member-of-states-m->n
479 r-is-evaluation-eq-member-p)
480 :use ((:instance r-is-evaluation-eq-member-p
494 (defthm c-bisimilar-witness-member-of-states-n->m
511 r-is-evaluation-eq-member-p)
512 :use ((:instance r-is-evaluation-eq-member-p
541 r-is-evaluation-eq-member-p)
542 :use ((:instance r-is-evaluation-eq-member-p
571 r-is-evaluation-eq-member-p)
572 :use ((:instance r-is-evaluation-eq-member-p
602 r-is-evaluation-eq-member-p)
603 :use ((:instance r-is-evaluation-eq-member-p
633 r-is-evaluation-eq-member-p)
634 :use ((:instance r-is-evaluation-eq-member-p
653 (p (evaluation-eq-member r (<- (transition m) p)
749 (defthm c-bisimilar-witness-member-of-states-m->n
756 (defthm c-bisimilar-witness-member-of-states-n->m