1(in-package "ACL2")
2
3#||
4
5  summary.lisp
6  ~~~~~~~~~~~~
7
8Author: Sandip Ray
9Date: Sat Nov  8 15:27:38 2008
10
11In this book, we summarize the theorems that demonstrate that the
12conee of influence reduction of a circuit produces a Kripke Structure
13which is bisimilar to the circuit.  I locally include some of the
14earlier books by Ray/Matthews/Tuttle to show this.  The book here only
15states the theorems previously proven in the above books nonlocally.
16These theorems correspond to the "easy part" of showing that cone of
17influence reduction preserves LTL semantics.  The hard part, that
18bisimulation preserves LTL semantics, should be an easy problem for
19HOL.
20
21||#
22
23;; I now locally include the cone of influence book, which has all the
24;; proofs.  Here I non-locally state the theorems.
25(local (include-book "cone-of-influence"))
26
27
28;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
29;;  Section 1: Some Preliminaries
30;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
31
32;; This records book is similar to what is distributed with ACL2 (I
33;; hope).  But this was done in Summer 2002 when all this was in flux.
34;; So I used a version of the records book which might be
35;; non-standard.  At some point I need to sit and understand how to
36;; get everything working with the distributed records book.
37
38(include-book "records")
39
40(defmacro <- (x a) `(g ,a ,x))
41(defmacro -> (x a v) `(s ,a ,v ,x))
42
43(defun update-macro (upds result)
44  (declare (xargs :guard (keyword-value-listp upds)))
45  (if (endp upds) result
46    (update-macro (cddr upds)
47                  (list 's (car upds) (cadr upds) result))))
48
49(defmacro update (old &rest updates)
50  (declare (xargs :guard (keyword-value-listp updates)))
51  (update-macro updates old))
52
53(defmacro >_ (&rest upds) `(update nil ,@upds))
54
55(local (include-book "cone-of-influence"))
56
57;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
58;;  Section 2: Set Operations
59;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
60
61;; Note that this work was done in Summer 2002, when there was no good
62;; set book that suited my purpose.  So I rolled my own little set of
63;; set theorems.  If I were doing it today, I probably would have made
64;; use of the distributed set theory books.
65
66(defun memberp (a x)
67  (and (consp x)
68       (or (equal a (first x))
69           (memberp a (rest x)))))
70
71(defun subset (x y)
72  (if (endp x) T
73    (and (memberp (first x) y)
74         (subset (rest x) y))))
75
76(defun set-intersect (x y)
77  (cond ((endp x) nil)
78        ((memberp (first x) y)
79         (cons (first x) (set-intersect (rest x) y)))
80        (t (set-intersect (rest x) y))))
81
82(defun set-union (x y)
83  (cond ((endp x) y)
84        ((memberp (first x) y)
85         (set-union (rest x) y))
86        (t (cons (first x) (set-union (rest x) y)))))
87
88(defun set-equal (x y)
89  (and (subset x y)
90       (subset y x)))
91
92
93
94;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
95;;  Section 3: LTL formulas and their structure
96;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
97
98;; Why do I need an LTL formula, if all we are doing is bisimulation
99;; proof?  Because the correctness of cone of influence reduction is
100;; stated as the following theorem.  Suppose f be an LTL formula, and
101;; C a circuit.  Reduce the circuit with the cone of influence of the
102;; variables in f.  Then the reduced circuit satisfies f if and only
103;; if the original does.
104
105(defun ltl-constantp (f)
106  (or (equal f 'true)
107      (equal f 'false)))
108
109(defun ltl-variablep (f)
110  (and (symbolp f)
111       (not (memberp f '(+ & U W X F G)))))
112
113(defun ltl-formulap (f)
114  (cond ((atom f) (or (ltl-constantp f)
115                      (ltl-variablep f)))
116        ((equal (len f) 3)
117         (and (memberp (second f) '(+ & U W))
118              (ltl-formulap (first f))
119              (ltl-formulap (third f))))
120        ((equal (len f) 2)
121         (and (memberp (first f) '(~ X F G))
122              (ltl-formulap (second f))))
123        (t nil)))
124
125;; A formula is called restricted with respect to a collection vars of
126;; variables if it mentions no variable other than those in vars. Here
127;; is the recursive definition.
128
129(defun restricted-formulap (f v-list)
130  (cond ((atom f) (or (ltl-constantp f)
131                      (and (ltl-variablep f)
132                           (memberp f v-list))))
133        ((equal (len f) 3) (and (memberp (second f) '(& + U W))
134                                (restricted-formulap (first f) v-list)
135                                (restricted-formulap (third f) v-list)))
136        ((equal (len f) 2) (and (memberp (first f) '(~ X F G))
137                                (restricted-formulap (second f) v-list)))
138        (t nil)))
139
140
141;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
142;;  Section 4: Kripke Structures from Circuits, and a bisimulation relation
143;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
144
145(defmacro initial-states (m) `(<- ,m :initial-states))
146(defmacro transition     (m) `(<- ,m :transition))
147(defmacro label-fn       (m) `(<- ,m :label-fn))
148(defmacro states         (m) `(<- ,m :states))
149(defmacro variables      (m) `(<- ,m :variables))
150
151(defun next-statep (p q m)
152  (memberp q (<- (transition m) p)))
153
154(defun initial-statep (p m)
155  (memberp p (initial-states m)))
156
157(defun label-of (s m)
158  (<- (label-fn m) s))
159
160(defun next-states-in-states (m states)
161  (if (endp states) T
162    (and (subset (<- (transition m) (first states))
163                 (states m))
164         (next-states-in-states m (rest states)))))
165
166(defun evaluation-eq (p q vars)
167  (if (endp vars) T
168    (and (equal (<- p (first vars))
169                (<- q (first vars)))
170         (evaluation-eq p q (rest vars)))))
171
172(defun evaluation-eq-member-p (st states vars)
173  (if (endp states) nil
174    (if (evaluation-eq st (first states) vars) T
175      (evaluation-eq-member-p st (rest states) vars))))
176
177(defun evaluation-eq-member (st states vars)
178  (if (endp states) nil
179    (if (evaluation-eq st (first states) vars)
180        (first states)
181      (evaluation-eq-member st (rest states) vars))))
182
183(defun-sk strict-evaluation-p (st vars)
184  (forall v (implies (not (memberp v vars))
185                     (not (<- st v)))))
186
187(defun strict-evaluation-list-p (vars states)
188  (if (endp states) T
189    (and (strict-evaluation-p (first states) vars)
190         (strict-evaluation-list-p vars (rest states)))))
191
192(defun evaluation-p (st vars)
193  (if (endp vars) T
194    (and (booleanp (<- st (first vars)))
195         (evaluation-p st (rest vars)))))
196
197(defun only-evaluations-p (states vars)
198  (if (endp states) T
199    (and (evaluation-p (first states) vars)
200         (only-evaluations-p (rest states) vars))))
201
202;; I think we can remove the all-evaluations-p from defun-sk to
203;; defun. But I am feeling lazy at least now to do it.
204
205(defun-sk all-evaluations-p (states vars)
206  (forall st
207          (implies (evaluation-p st vars)
208                   (evaluation-eq-member-p st states vars))))
209
210(defun evaluation-eq-subset-p (m-states n-states vars)
211  (if (endp m-states) T
212    (and (evaluation-eq-member-p (first m-states) n-states vars)
213         (evaluation-eq-subset-p (rest m-states) n-states vars))))
214
215(defthm evaluation-eq-subset-to-member
216  (implies (and (evaluation-eq-subset-p m-states n-states vars)
217                (memberp p m-states))
218           (evaluation-eq-member-p p n-states vars)))
219
220(defun truthp-label (label s)
221  (if (endp label) t
222    (and (equal (<- s (first label)) T)
223         (truthp-label (rest label) s))))
224
225(defun only-truth-p (states m)
226  (if (endp states) T
227    (and (truthp-label (label-of (first states) m) (first states))
228         (only-truth-p (rest states) m))))
229
230(defun all-truthsp-label (label s vars)
231  (if (endp vars) T
232    (and (implies (equal (<- s (car vars)) T)
233                  (memberp (car vars) label))
234         (all-truthsp-label label s (rest vars)))))
235
236(defun only-all-truths-p (states m vars)
237  (if (endp states) T
238    (and (all-truthsp-label (label-of (first states) m) (first states) vars)
239         (only-all-truths-p (rest states) m vars))))
240
241(defun label-subset-vars (states m vars)
242  (if (endp states) T
243    (and (subset (label-of (first states) m) vars)
244         (label-subset-vars (rest states) m vars))))
245
246(defun-sk well-formed-transition-p (states-m trans-m states-n trans-n vars)
247  (forall (p q)
248          (implies (and (evaluation-eq p q vars)
249                        (evaluation-p p vars)
250                        (memberp p states-m)
251                        (memberp q states-n)
252                        (evaluation-p q vars))
253                   (evaluation-eq-subset-p (<- trans-m p)
254                                           (<- trans-n q)
255                                           vars))))
256
257(defun transition-subset-p (states states-prime trans)
258  (if (endp states) T
259    (and (subset (<- trans (first states)) states-prime)
260         (transition-subset-p (rest states) states-prime trans))))
261
262(defun circuit-modelp (m)
263  (and (only-evaluations-p (states m) (variables m))
264       (all-evaluations-p (states m) (variables m))
265       (strict-evaluation-list-p (variables m) (states m))
266       (only-all-truths-p (states m) m (variables m))
267       (only-truth-p (states m) m)
268       (label-subset-vars (states m) m (variables m))
269       (transition-subset-p (states m) (states m) (transition m))
270       (subset (initial-states m) (states m))
271       (consp (states m))
272       (next-states-in-states m (states m))))
273
274;; And here is our bisimilarity relation
275
276(defun c-bisim-equiv (m n vars)
277  (and (circuit-modelp m)
278       (circuit-modelp n)
279       (subset vars (variables m))
280       (subset vars (variables n))
281       (well-formed-transition-p (states m) (transition m) (states n) (transition n) vars)
282       (well-formed-transition-p (states n) (transition n) (states m) (transition m) vars)
283       (evaluation-eq-subset-p (initial-states m) (initial-states n) vars)
284       (evaluation-eq-subset-p (initial-states n) (initial-states m) vars)))
285
286(defun circuit-bisim (p m q n vars)
287  (and (circuit-modelp m)
288       (circuit-modelp n)
289       (memberp p (states m))
290       (memberp q (states n))
291       (well-formed-transition-p (states m) (transition m) (states n) (transition n) vars)
292       (well-formed-transition-p (states n) (transition n) (states m) (transition m) vars)
293       (evaluation-eq-subset-p (initial-states m) (initial-states n) vars)
294       (evaluation-eq-subset-p (initial-states n) (initial-states m) vars)
295       (subset vars (variables m))
296       (subset vars (variables n))
297       (evaluation-eq p q vars)))
298
299;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
300;;  Section 5: Circuit Structure and Kripke Structure from Circuit
301;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
302
303(defmacro equations (c) `(<- ,c :equations))
304
305;; Now we define what it means for the equations to be consistent with the
306;; variables of the circuit.
307
308(defun find-variables (equation)
309  (cond ((and (atom equation) (not (booleanp equation)))
310         (list equation))
311        ((and (equal (len equation) 3) (memberp (second equation) '(& +)))
312         (set-union (find-variables (first equation))
313                    (find-variables (third equation))))
314        ((and (equal (len equation) 2) (equal (first equation) '~))
315         (find-variables (second equation)))
316        (t nil)))
317
318(defun-sk consistent-equation-record-p (vars equations)
319  (forall (v equation)
320          (implies (and (uniquep vars)
321                        (memberp v vars)
322                        (memberp equation (<- equations v)))
323                   (subset (find-variables equation) vars))))
324
325(defun cons-list-p (vars equations)
326  (if (endp vars) T
327    (and (consp (<- equations (first vars)))
328         (cons-list-p (rest vars) equations))))
329
330;; OK, now let us define the function circuitp.
331
332(defun circuitp (C)
333  (and (only-evaluations-p (initial-states C) (variables C))
334       (strict-evaluation-list-p (variables C) (initial-states C))
335       (uniquep (variables C))
336       (cons-list-p (variables C) (equations C))
337       (consistent-equation-record-p (variables C) (equations C))))
338
339;; Now let us try to create a Kripke Structure from the circuit. We need to
340;; show that under (circuitp C), the kripke structure we produce is a
341;; circuit-model-p.
342
343(defun assign-T (v states)
344  (if (endp states) nil
345    (cons (-> (first states) v T)
346          (assign-T v (rest states)))))
347
348(defun assign-nil (v states)
349  (if (endp states) nil
350    (cons (-> (first states) v nil)
351          (assign-nil v (rest states)))))
352
353;; Now we create all the states of the model.
354
355(defun create-all-evaluations (vars states)
356  (if (endp vars) states
357    (let ((rec-states (create-all-evaluations (cdr vars) states)))
358      (append (assign-t (car vars) rec-states)
359              (assign-nil (car vars) rec-states)))))
360
361;; Now let us create the label function.
362
363(defun label-fn-of-st (st vars)
364  (if (endp vars) nil
365    (if (equal (<- st (first vars)) T)
366        (cons (first vars)
367              (label-fn-of-st st (rest vars)))
368      (label-fn-of-st st (rest vars)))))
369
370(defun create-label-fn (states vars label)
371  (if (endp states) label
372    (create-label-fn (rest states) vars
373                     (-> label (first states)
374                         (label-fn-of-st (first states) vars)))))
375
376;; And finally the transitions.
377
378(defun apply-equation (equation st)
379  (cond ((atom equation) (if (booleanp equation)
380                             equation
381                           (<- st equation)))
382        ((equal (len equation) 2)
383         (case (first equation)
384           (~ (not (apply-equation (second equation) st)))
385           (t nil)))
386        ((equal (len equation) 3)
387         (case (second equation)
388           (& (and (apply-equation (first equation) st)
389                   (apply-equation (third equation) st)))
390           (+ (or (apply-equation (first equation) st)
391                  (apply-equation (third equation) st)))
392           (t nil)))
393        (t nil)))
394
395(defun produce-next-state (vars st equations)
396  (if (endp vars) st
397    (-> (produce-next-state (rest vars) st equations)
398        (first vars)
399        (apply-equation (<- equations (first vars)) st))))
400
401(defun consistent-p-equations (vars eqn equations)
402  (if (endp vars) T
403    (and (memberp (<- eqn (first vars)) (<- equations (first vars)))
404         (consistent-p-equations (rest vars) eqn equations))))
405
406(defun-sk next-state-is-ok (p q vars equations)
407  (exists eqn (and (consistent-p-equations vars eqn equations)
408                   (evaluation-eq q (produce-next-state vars p eqn) vars))))
409
410(defun create-next-states-of-p (p states vars equations)
411  (if (endp states) nil
412    (if (next-state-is-ok p (first states) vars equations)
413        (cons (first states) (create-next-states-of-p
414                              p (rest states) vars equations))
415      (create-next-states-of-p p (rest states) vars equations))))
416
417(defun create-next-states (states states-prime vars equations)
418  (if (endp states) ()
419    (->
420     (create-next-states (rest states) states-prime vars equations)
421     (first states)
422     (create-next-states-of-p (first states) states-prime vars equations))))
423
424(defun create-kripke (C)
425  (let ((vars (variables C))
426        (equations (equations C))
427        (initial-states (initial-states C)))
428    (let* ((states (create-all-evaluations vars (list ())))
429           (label-fn (create-label-fn (set-union initial-states states) vars ()))
430           (transition (create-next-states (set-union initial-states states)
431                                           (set-union initial-states states)
432                                           vars equations)))
433      (>_ :states (set-union initial-states states)
434          :initial-states initial-states
435          :label-fn label-fn
436          :transition transition
437          :variables vars))))
438
439;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
440;;  Section 6: Cone of Influence Reduction
441;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
442
443(defun find-variables* (equation-list)
444  (if (endp equation-list) nil
445    (set-union (find-variables (first equation-list))
446                      (find-variables* (rest equation-list)))))
447
448(defun find-all-variables-1-pass (vars equations)
449  (if (endp vars) nil
450    (set-union (find-variables* (<- equations (first vars)))
451                      (find-all-variables-1-pass (rest vars) equations))))
452
453(defun find-all-variables (vars variables equations)
454  (declare (xargs :measure (nfix (- (len variables) (len vars)))
455                  :hints (("Goal"
456                           :do-not-induct t
457                           :in-theory (enable set-equal)
458                           :do-not '(eliminate-destructors generalize)))))
459  (if (or (not (uniquep variables))
460          (not (uniquep vars))
461          (not (subset vars variables)))
462      vars
463    (let ((new-vars (set-union (find-all-variables-1-pass vars equations)
464                               vars)))
465      (if (not (subset new-vars variables)) nil
466        (if (set-equal vars new-vars) vars
467          (find-all-variables new-vars variables equations))))))
468
469(defun find-all-equations (vars equations eq-rec)
470  (if (endp vars) eq-rec
471    (find-all-equations (rest vars) equations
472                        (-> eq-rec
473                            (first vars)
474                            (<- equations (first vars))))))
475
476(defun remove-duplicate-occurrences (x)
477  (cond ((endp x) x)
478        ((memberp (first x) (rest x)) (remove-duplicate-occurrences (rest x)))
479        (t (cons (first x) (remove-duplicate-occurrences (rest x))))))
480
481(defun corresponding-state (init vars)
482  (if (endp vars) nil
483    (-> (corresponding-state init (rest vars))
484        (first vars)
485        (<- init (first vars)))))
486
487(defun corresponding-states (inits vars)
488  (if (endp inits) nil
489    (cons (corresponding-state (first inits) vars)
490          (corresponding-states (rest inits) vars))))
491
492(defun cone-variables (vars C)
493  (find-all-variables
494   (set-intersect (remove-duplicate-occurrences vars)
495                  (variables C))
496   (variables C)
497   (equations C)))
498
499(defun cone-of-influence-reduction (C vars)
500  (let ((variables (cone-variables vars C)))
501   (>_ :variables variables
502       :initial-states (corresponding-states (initial-states C) variables)
503       :equations (find-all-equations variables (equations C) ()))))
504
505;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
506;;  Section 7: Final Theorems
507;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
508
509;; We first show that cone of influence reduction produces a circuit,
510;; and also that it satisfies the bisimulation relation c-bisim-equiv.
511
512(defthm cone-of-influence-reduction-is-circuit-p
513  (implies (circuitp C)
514           (circuitp (cone-of-influence-reduction C vars)))
515  :hints (("Goal"
516           :in-theory (disable circuitp cone-of-influence-reduction)
517           :expand (circuitp (cone-of-influence-reduction C vars)))))
518
519
520(defthm cone-of-influence-is-c-bisimi-equiv
521  (implies (circuitp C)
522           (c-bisim-equiv (create-kripke C)
523                           (create-kripke (cone-of-influence-reduction C vars))
524                           (cone-variables vars C))))
525
526
527;; We then show that the Kripke Structure produced from a circuit is
528;; indeed a Kripke Structure.
529
530(defthm create-kripke-produces-circuit-model
531  (implies (circuitp C)
532           (circuit-modelp (create-kripke C))))
533
534;; Now we will show that c-bisim-equiv is indeed a bisimulation
535;; relation over Kripke Structures.  This probably does not require
536;; that we have a Kripke Structure in our hands.  But what the heck,
537;; we have proven this above.  The next few theorems are
538;; (non-closed-form) characterization of bisimulation.  When proving
539;; that bisimulation preserves LTL semantics we had proven that if
540;; there is _any_ bisimulation relation between two Kripke Sturctures,
541;; then they preserve the LTL semantics.
542
543;; Bisimulation requires an existential quantification in several
544;; spots.  For example, we have to say that for each initial state in
545;; m there is an initial state in n, that is bisim-equiv.  Instead of
546;; quantifying, we create such a state (for m to n) and (n to m).
547
548(defun c-bisimilar-initial-state-witness-m->n (s m n vars)
549  (declare (ignore m))
550  (evaluation-eq-member s (initial-states n) vars))
551
552(defun c-bisimilar-initial-state-witness-n->m (m s n vars)
553  (declare (ignore n))
554  (evaluation-eq-member s (initial-states m) vars))
555
556(defun c-bisimilar-transition-witness-m->n (p r m q n vars)
557  (declare (ignore p m))
558  (evaluation-eq-member r (<- (transition n) q) vars))
559
560(defun c-bisimilar-transition-witness-n->m (p m q r n vars)
561  (declare (ignore q n))
562  (evaluation-eq-member r (<- (transition m) p) vars))
563
564;; Now we can state the theorems.
565
566(defthm c-bisimilar-equiv-implies-init->init-m->n
567  (implies (and (c-bisim-equiv m n vars)
568                (memberp s (initial-states m)))
569           (memberp (c-bisimilar-initial-state-witness-m->n s m n vars)
570                    (initial-states n))))
571
572(defthm c-bisimilar-equiv-implies-init->init-n->m
573  (implies (and (c-bisim-equiv m n vars)
574                (memberp s (initial-states n)))
575           (memberp (c-bisimilar-initial-state-witness-n->m m s n vars)
576                    (initial-states m))))
577
578(defthm c-bisimilar-equiv-implies-bisimilar-initial-states-m->n
579   (implies (and (c-bisim-equiv m n vars)
580                 (memberp s (initial-states m)))
581            (circuit-bisim s m
582                           (c-bisimilar-initial-state-witness-m->n s m n vars)
583                           n vars)))
584
585(defthm c-bisimilar-equiv-implies-bisimilar-initial-states-n->m
586   (implies (and (c-bisim-equiv m n vars)
587                 (memberp s (initial-states n)))
588            (circuit-bisim (c-bisimilar-initial-state-witness-n->m m s n vars)
589                           m s n vars)))
590
591(defthm c-bisimilar-states-have-labels-equal
592  (implies (circuit-bisim p m q n vars)
593           (set-equal (set-intersect (label-of q n) vars)
594                      (set-intersect (label-of p m) vars))))
595
596
597(defthm c-bisimilar-witness-member-of-states-m->n
598  (implies (and (circuit-bisim p m q n vars)
599                (next-statep p r m)
600                (memberp r (states m)))
601           (memberp (c-bisimilar-transition-witness-m->n p r m q n vars)
602                    (states n))))
603
604(defthm c-bisimilar-witness-member-of-states-n->m
605  (implies (and (circuit-bisim p m q n vars)
606                (next-statep q r n)
607                (memberp r (states n)))
608           (memberp (c-bisimilar-transition-witness-n->m p m q r n vars)
609                    (states m))))
610
611(defthm c-bisimilar-witness-produces-bisimilar-states-m->n
612  (implies (and (circuit-bisim p m q n vars)
613                 (next-statep p r m))
614            (circuit-bisim r m
615                       (c-bisimilar-transition-witness-m->n p r m q n vars)
616                       n vars)))
617
618(defthm c-bisimilar-witness-produces-bisimilar-states-n->m
619  (implies (and (circuit-bisim p m q n vars)
620                 (next-statep q r n))
621            (circuit-bisim
622             (c-bisimilar-transition-witness-n->m p m q r n vars)
623             m r n vars)))
624
625(defthm c-bisimilar-witness-matches-transition-m->n
626  (implies (and (circuit-bisim p m q n vars)
627                (next-statep p r m))
628           (next-statep q (c-bisimilar-transition-witness-m->n p r m q n vars)
629                        n)))
630
631(defthm c-bisimilar-witness-matches-transition-n->m
632  (implies (and (circuit-bisim p m q n vars)
633                (next-statep q r n))
634           (next-statep p (c-bisimilar-transition-witness-n->m p m q r n vars)
635                        m)))
636