Lines Matching defs:eq
9 evaluation-eq. Roughly, two "circuit states" are evaluation-eq if they match on
10 a specific collection of variables. We prove that evaluation-eq is a
26 (defun evaluation-eq (p q vars)
30 (evaluation-eq p q (rest vars)))))
32 ;; We prove evaluation-eq is symmetric here, but I dont want to deal with loop
35 (defthm evaluation-eq-is-symmetric
36 (equal (evaluation-eq p q vars)
37 (evaluation-eq q p vars))
40 (defun evaluation-eq-member-p (st states vars)
42 (if (evaluation-eq st (first states) vars) T
43 (evaluation-eq-member-p st (rest states) vars))))
45 (defun evaluation-eq-member (st states vars)
47 (if (evaluation-eq st (first states) vars)
49 (evaluation-eq-member st (rest states) vars))))
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))))
95 (defun evaluation-eq-subset-p (m-states n-states vars)
97 (and (evaluation-eq-member-p (first m-states) n-states vars)
98 (evaluation-eq-subset-p (rest m-states) n-states vars))))
100 (defthm evaluation-eq-subset-to-member
101 (implies (and (evaluation-eq-subset-p m-states n-states vars)
103 (evaluation-eq-member-p p n-states vars)))
146 (implies (and (evaluation-eq p q vars)
151 (evaluation-eq-subset-p (<- trans-m p)
157 (evaluation-eq p q vars)
162 (evaluation-eq-subset-p (<- trans-m p) (<- trans-n q) vars))
202 (evaluation-eq-subset-p (initial-states m) (initial-states n) vars)
203 (evaluation-eq-subset-p (initial-states n) (initial-states m) vars)))
213 (evaluation-eq-subset-p (initial-states m) (initial-states n) vars)
214 (evaluation-eq-subset-p (initial-states n) (initial-states m) vars)
217 (evaluation-eq p q vars)))
228 (evaluation-eq-member s (initial-states n) vars))
232 (evaluation-eq-member s (initial-states m) vars))
237 (evaluation-eq-member-p st states vars))
279 evaluation-eq-subset-to-member)
280 :use ((:instance evaluation-eq-subset-to-member
300 evaluation-eq-subset-to-member)
301 :use ((:instance evaluation-eq-subset-to-member
309 evaluation-eq-is-symmetric
310 (p (evaluation-eq-member s (initial-states m) vars))
342 (defthm evaluation-eq-vars-reduction
343 (implies (and (evaluation-eq p q vars)
353 (evaluation-eq p q vars))
366 (evaluation-eq p q vars)
376 (evaluation-eq p q vars)
392 (evaluation-eq p q vars)
430 :use evaluation-eq-is-symmetric)))
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
454 (implies (and (evaluation-eq p q vars)
461 (evaluation-eq-member-p r (<- trans-n q) vars))
479 r-is-evaluation-eq-member-p)
480 :use ((:instance r-is-evaluation-eq-member-p
511 r-is-evaluation-eq-member-p)
512 :use ((:instance r-is-evaluation-eq-member-p
526 :use evaluation-eq-is-symmetric)))
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
586 :use evaluation-eq-is-symmetric)))
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
648 :use evaluation-eq-is-symmetric)
650 :use evaluation-eq-is-symmetric)
652 :use ((:instance evaluation-eq-is-symmetric
653 (p (evaluation-eq-member r (<- (transition m) p)