tests/inputs/circuit-bisim.lisp

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