1(in-package "ACL2")
2
3#|
4
5  circuit-bisim.lisp
6  ~~~~~~~~~~~~~~~~~~
7
8In this book, we define a specific bisimilarity relation
9evaluation-eq. Roughly, two "circuit states" are evaluation-eq if they match on
10a specific collection of variables. We prove that evaluation-eq is a
11bisimilarity relation. In a later book, we will prove that this bisimilarity
12relation holds between the "Kripke Structure of a circuit" and the "Kripke
13Structure of the cone of influence of the circuit". That will enable us to
14prove that the two kripke structures satisfy the same LTL formula when
15restricted by vars.
16
17|#
18
19(include-book "ltl")
20
21(in-theory (disable subset-of-empty-is-empty
22                    subset-of-nil-is-nil))
23
24(in-theory (enable subset set-intersect))
25
26(defun evaluation-eq (p q vars)
27  (if (endp vars) T
28    (and (equal (<- p (first vars))
29                (<- q (first vars)))
30         (evaluation-eq p q (rest vars)))))
31
32;; We prove evaluation-eq is symmetric here, but I dont want to deal with loop
33;; stoppers so we prove it only for the purpose of use hints.
34
35(defthm evaluation-eq-is-symmetric
36  (equal (evaluation-eq p q vars)
37         (evaluation-eq q p vars))
38  :rule-classes nil)
39
40(defun evaluation-eq-member-p (st states vars)
41  (if (endp states) nil
42    (if (evaluation-eq st (first states) vars) T
43      (evaluation-eq-member-p st (rest states) vars))))
44
45(defun evaluation-eq-member (st states vars)
46  (if (endp states) nil
47    (if (evaluation-eq st (first states) vars)
48        (first states)
49      (evaluation-eq-member st (rest states) vars))))
50
51(defthm member-is-memberp
52  (implies (evaluation-eq-member-p p states vars)
53           (memberp (evaluation-eq-member p states vars)
54                    states)))
55
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)
59                          vars)))
60
61(defun-sk strict-evaluation-p (st vars)
62  (forall v (implies (not (memberp v vars))
63                     (not (<- st v)))))
64
65(defthm strict-evaluation-p-expanded
66  (implies (and (strict-evaluation-p st vars)
67                (not (memberp v vars)))
68           (not (<- st v)))
69  :hints (("Goal"
70           :use strict-evaluation-p-necc)))
71
72(defun strict-evaluation-list-p (vars states)
73  (if (endp states) T
74    (and (strict-evaluation-p (first states) vars)
75         (strict-evaluation-list-p vars (rest states)))))
76
77(defun evaluation-p (st vars)
78  (if (endp vars) T
79    (and (booleanp (<- st (first vars)))
80         (evaluation-p st (rest vars)))))
81
82(defun only-evaluations-p (states vars)
83  (if (endp states) T
84    (and (evaluation-p (first states) vars)
85         (only-evaluations-p (rest states) vars))))
86
87;; I think we can remove the all-evaluations-p from defun-sk to
88;; defun. But I am feeling lazy at least now to do it.
89
90(defun-sk all-evaluations-p (states vars)
91  (forall st
92          (implies (evaluation-p st vars)
93                   (evaluation-eq-member-p st states vars))))
94
95(defun evaluation-eq-subset-p (m-states n-states vars)
96  (if (endp m-states) T
97    (and (evaluation-eq-member-p (first m-states) n-states vars)
98         (evaluation-eq-subset-p (rest m-states) n-states vars))))
99
100(defthm evaluation-eq-subset-to-member
101  (implies (and (evaluation-eq-subset-p m-states n-states vars)
102                (memberp p m-states))
103           (evaluation-eq-member-p p n-states vars)))
104
105(defun truthp-label (label s)
106  (if (endp label) t
107    (and (equal (<- s (first label)) T)
108         (truthp-label (rest label) s))))
109
110(defun only-truth-p (states m)
111  (if (endp states) T
112    (and (truthp-label (label-of (first states) m) (first states))
113         (only-truth-p (rest states) m))))
114
115(defun all-truthsp-label (label s vars)
116  (if (endp vars) T
117    (and (implies (equal (<- s (car vars)) T)
118                  (memberp (car vars) label))
119         (all-truthsp-label label s (rest vars)))))
120
121(defthm all-truthsp-label-expanded
122  (implies (and (all-truthsp-label label s vars)
123                (memberp v vars)
124                (equal (<- s v) T))
125           (memberp v label)))
126
127(defun only-all-truths-p (states m vars)
128  (if (endp states) T
129    (and (all-truthsp-label (label-of (first states) m) (first states) vars)
130         (only-all-truths-p (rest states) m vars))))
131
132(defun label-subset-vars (states m vars)
133  (if (endp states) T
134    (and (subset (label-of (first states) m) vars)
135         (label-subset-vars (rest states) m vars))))
136
137(defthm label-subset-subset-reduction
138  (implies (and (label-subset-vars states m vars)
139                (memberp p states))
140           (subset (label-of p m) vars)))
141
142;; Now for a few properties governing the next state.
143
144(defun-sk well-formed-transition-p (states-m trans-m states-n trans-n vars)
145  (forall (p q)
146          (implies (and (evaluation-eq p q vars)
147                        (evaluation-p p vars)
148                        (memberp p states-m)
149                        (memberp q states-n)
150                        (evaluation-p q vars))
151                   (evaluation-eq-subset-p (<- trans-m p)
152                                           (<- trans-n q)
153                                           vars))))
154
155(defthm well-formed-transition-p-expanded
156  (implies (and (well-formed-transition-p states-m trans-m states-n trans-n vars)
157                (evaluation-eq p q vars)
158                (evaluation-p p vars)
159                (memberp p states-m)
160                (memberp q states-n)
161                (evaluation-p q vars))
162           (evaluation-eq-subset-p (<- trans-m p) (<- trans-n q) vars))
163  :hints (("Goal"
164           :use well-formed-transition-p-necc)))
165
166(in-theory (disable well-formed-transition-p well-formed-transition-p-necc))
167
168
169(defun transition-subset-p (states states-prime trans)
170  (if (endp states) T
171    (and (subset (<- trans (first states)) states-prime)
172         (transition-subset-p (rest states) states-prime trans))))
173
174(defthm transition-subset-p-expanded
175  (implies (and (transition-subset-p states states-prime trans)
176                 (memberp p states)
177                 (memberp r (<- trans p)))
178            (memberp r states-prime)))
179
180
181(defun circuit-modelp (m)
182  (and (only-evaluations-p (states m) (variables m))
183       (all-evaluations-p (states m) (variables m))
184       (strict-evaluation-list-p (variables m) (states m))
185       (only-all-truths-p (states m) m (variables m))
186       (only-truth-p (states m) m)
187       (label-subset-vars (states m) m (variables m))
188       (transition-subset-p (states m) (states m) (transition m))
189       (subset (initial-states m) (states m))
190       (consp (states m))
191       (next-states-in-states m (states m))))
192
193;; And here is our bisimilarity relation
194
195(defun c-bisim-equiv (m n vars)
196  (and (circuit-modelp m)
197       (circuit-modelp n)
198       (subset vars (variables m))
199       (subset vars (variables n))
200       (well-formed-transition-p (states m) (transition m) (states n) (transition n) vars)
201       (well-formed-transition-p (states n) (transition n) (states m) (transition m) 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)))
204
205
206(defun circuit-bisim (p m q n vars)
207  (and (circuit-modelp m)
208       (circuit-modelp n)
209       (memberp p (states m))
210       (memberp q (states n))
211       (well-formed-transition-p (states m) (transition m) (states n) (transition n) vars)
212       (well-formed-transition-p (states n) (transition n) (states m) (transition 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)
215       (subset vars (variables m))
216       (subset vars (variables n))
217       (evaluation-eq p q vars)))
218
219
220;; Now that we have defined a bisimilar relation between circuit models, let us
221;; prove that this is actually a bisimilar relation.
222
223;; So what do we need to have? Given two circuit models m and m', we need to
224;; show that the bisimilarity witness from m to m' and from m' to m.
225
226(defun c-bisimilar-initial-state-witness-m->n (s m n vars)
227  (declare (ignore m))
228  (evaluation-eq-member s (initial-states n) vars))
229
230(defun c-bisimilar-initial-state-witness-n->m (m s n vars)
231  (declare (ignore n))
232  (evaluation-eq-member s (initial-states m) vars))
233
234(defthm all-evaluations-considers-an-evaluation-a-member
235  (implies (and (evaluation-p st vars)
236                (all-evaluations-p states vars))
237           (evaluation-eq-member-p st states vars))
238  :hints (("Goal"
239           :use all-evaluations-p-necc)))
240
241(in-theory (disable all-evaluations-p all-evaluations-p-necc))
242
243
244(local
245(defthm c-bisimilar-equiv-implies-init->init-n->m
246  (implies (and (c-bisim-equiv m n vars)
247                (memberp s (initial-states n)))
248           (memberp (c-bisimilar-initial-state-witness-n->m m s n vars)
249                    (initial-states m))))
250)
251
252(local
253(defthm c-bisimilar-equiv-implies-init->init-m->n
254  (implies (and (c-bisim-equiv m n vars)
255                (memberp s (initial-states m)))
256           (memberp (c-bisimilar-initial-state-witness-m->n s m n vars)
257                    (initial-states n))))
258)
259
260(local
261(defthm subset-transitive-member
262  (implies (and (memberp s init)
263		(subset init states))
264	   (memberp s states)))
265)
266
267(local
268(defthm c-bisimilar-equiv-implies-bisimilar-initial-states-m->n
269   (implies (and (c-bisim-equiv m n vars)
270                 (memberp s (initial-states m)))
271            (circuit-bisim s m
272                           (c-bisimilar-initial-state-witness-m->n s m n vars)
273                           n vars))
274   :otf-flg t
275   :hints (("Goal"
276            :do-not '(generalize eliminate-destructors)
277            :do-not-induct t
278	    :in-theory (disable member-is-memberp
279				evaluation-eq-subset-to-member)
280	    :use ((:instance evaluation-eq-subset-to-member
281			     (p s)
282			     (m-states (initial-states m))
283			     (n-states (initial-states n)))
284		  (:instance member-is-memberp
285			     (p s)
286			     (states (initial-states n)))))))
287)
288
289(local
290(defthm c-bisimilar-equiv-implies-bisimilar-initial-states-n->m
291   (implies (and (c-bisim-equiv m n vars)
292                 (memberp s (initial-states n)))
293            (circuit-bisim (c-bisimilar-initial-state-witness-n->m m s n vars)
294                           m s n vars))
295   :otf-flg t
296   :hints (("Goal"
297            :do-not '(generalize eliminate-destructors)
298            :do-not-induct t
299	    :in-theory (disable member-is-memberp
300				evaluation-eq-subset-to-member)
301	    :use ((:instance evaluation-eq-subset-to-member
302			     (p s)
303			     (m-states (initial-states n))
304			     (n-states (initial-states m)))
305		  (:instance member-is-memberp
306			     (p s)
307			     (states (initial-states m)))
308                  (:instance
309                   evaluation-eq-is-symmetric
310                   (p (evaluation-eq-member s (initial-states m) vars))
311                   (q s))))))
312)
313
314
315;; Now we go to our first difficult proof, showing that bisimilar
316;; states have equal labels.
317
318;; (label-of s m) are only truths.
319
320(defthm truthp-label-from-only-truthp
321  (implies (and (only-truth-p states m)
322                (memberp s states))
323           (truthp-label (label-of s m) s)))
324
325;; And all truths are present in the label.
326
327(defthm all-truths-p-from-only-all-truths-p
328  (implies (and (only-all-truths-p states m vars)
329                (memberp s states))
330           (all-truthsp-label (label-of s m) s vars)))
331
332;; For every variable in (and vars label) they re members of vars and label.
333
334(defthm memberp-to-intersect-reduction
335  (implies (memberp v (set-intersect x y))
336           (and (memberp v x)
337                (memberp v y)))
338  :rule-classes :forward-chaining)
339
340;; Since they are in vars, they must evaluate the same way in q.
341
342(defthm evaluation-eq-vars-reduction
343  (implies (and (evaluation-eq p q vars)
344                (memberp v vars))
345           (equal (<- p v)
346                  (<- q v))))
347
348;; Thus, variables in (label-of p m) and vars will evaluate to T in q.
349
350(defthm variables-in-label-are-T-in-q
351  (implies (and (memberp v (set-intersect label vars))
352		(truthp-label label p)
353		(evaluation-eq p q vars))
354	   (equal (<- q v) T)))
355
356(defthm only-truthsp-and-subset-to-subset
357  (implies (and (equal (<- q v) T)
358		(memberp v vars)
359		(subset vars variables)
360		(all-truthsp-label label q variables))
361	   (memberp v label)))
362
363(defthm truthp-label-to-subset
364  (implies (and (memberp v (set-intersect lp vars))
365		(truthp-label lp p)
366		(evaluation-eq p q vars)
367		(subset vars variables)
368		(all-truthsp-label lq q variables))
369	   (memberp v lq)))
370
371;; And let us do a little trick to get ACL2 from memberp to subset
372
373
374(defthm truthp-label-is-a-subset
375  (implies (and (truthp-label lp p)
376		(evaluation-eq p q vars)
377		(subset vars variables)
378		(all-truthsp-label lq q variables))
379	   (subset (set-intersect lp vars)
380		   lq)))
381
382(local
383(defthm subset-intersect-reduction
384  (implies (and (subset lp lq)
385		(subset lp vars))
386	   (subset lp (set-intersect lq vars))))
387)
388
389(local
390(defthm truthp-label-intersect-is-a-subset
391  (implies (and (truthp-label lp p)
392		(evaluation-eq p q vars)
393		(subset vars variables)
394		(all-truthsp-label lq q variables))
395	   (subset (set-intersect lp vars)
396		   (set-intersect lq vars))))
397)
398
399(local
400(defthm c-bisimilar-states-have-labels-equal-aux
401  (implies (circuit-bisim p m q n vars)
402           (subset (set-intersect (label-of p m) vars)
403		   (set-intersect (label-of q n) vars)))
404  :hints (("Goal"
405	   :in-theory (disable truthp-label-intersect-is-a-subset)
406	   :use ((:instance truthp-label-intersect-is-a-subset
407			    (lp (label-of p m))
408			    (lq (label-of q n))
409			    (variables (variables n)))))))
410)
411
412(local
413(in-theory (enable set-equal))
414)
415
416(local
417(defthm c-bisimilar-states-have-labels-equal
418  (implies (circuit-bisim p m q n vars)
419           (set-equal (set-intersect (label-of q n) vars)
420                      (set-intersect (label-of p m) vars)))
421  :hints (("Goal"
422	   :in-theory (disable c-bisimilar-states-have-labels-equal-aux)
423           :use ((:instance  c-bisimilar-states-have-labels-equal-aux
424                             (p q)
425                             (m n)
426                             (n m)
427                             (q p))
428                 (:instance  c-bisimilar-states-have-labels-equal-aux)))
429          ("Goal'''"
430           :use evaluation-eq-is-symmetric)))
431)
432
433;; Now we start with the next states.
434
435(defun c-bisimilar-transition-witness-m->n (p r m q n vars)
436  (declare (ignore p m))
437  (evaluation-eq-member r (<- (transition n) q) vars))
438
439(defun c-bisimilar-transition-witness-n->m (p m q r n vars)
440  (declare (ignore q n))
441  (evaluation-eq-member r (<- (transition m) p) vars))
442
443(defthm evaluationp-for-subset
444  (implies (and (evaluation-p st variables)
445                (subset vars variables))
446           (evaluation-p st vars)))
447
448(defthm evaluation-p-only-evaluations-reduction
449  (implies (and (only-evaluations-p states vars)
450                (memberp p states))
451           (evaluation-p p vars)))
452
453(defthm r-is-evaluation-eq-member-p
454  (implies (and (evaluation-eq p q vars)
455                (well-formed-transition-p states-m trans-m states-n trans-n vars)
456                (memberp p states-m)
457                (memberp q states-n)
458                (evaluation-p p vars)
459                (evaluation-p q vars)
460                (memberp r (<- trans-m p)))
461           (evaluation-eq-member-p r (<- trans-n q) vars))
462  :hints (("Goal"
463           :in-theory (disable well-formed-transition-p-expanded)
464           :use well-formed-transition-p-expanded)))
465
466(local
467(defthm c-bisimilar-witness-member-of-states-m->n
468  (implies (and (circuit-bisim p m q n vars)
469                (next-statep p r m)
470                (memberp r (states m)))
471           (memberp (c-bisimilar-transition-witness-m->n p r m q n vars)
472                    (states n)))
473  :hints (("Goal"
474           :do-not-induct t
475           :do-not '(eliminate-destructors generalize)
476           :in-theory (enable next-statep))
477          ("Goal'"
478           :in-theory (disable evaluationp-for-subset
479                               r-is-evaluation-eq-member-p)
480           :use ((:instance r-is-evaluation-eq-member-p
481                            (states-m (states m))
482                            (states-n (states n))
483                            (trans-m (transition m))
484                            (trans-n (transition n)))
485                 (:instance evaluationp-for-subset
486                            (st p)
487                            (variables (variables m)))
488                 (:instance evaluationp-for-subset
489                            (st q)
490                            (variables (variables n)))))))
491)
492
493(local
494(defthm c-bisimilar-witness-member-of-states-n->m
495  (implies (and (circuit-bisim p m q n vars)
496                (next-statep q r n)
497                (memberp r (states n)))
498           (memberp (c-bisimilar-transition-witness-n->m p m q r n vars)
499                    (states m)))
500  :otf-flg t
501  :hints (("Goal"
502           :do-not-induct t
503           :do-not '(eliminate-destructors generalize)
504           :in-theory (enable next-statep))
505          ("Goal'"
506           :in-theory (disable evaluationp-for-subset
507                               only-evaluations-p
508                               all-evaluations-p
509                               evaluation-p
510                               subset
511                               r-is-evaluation-eq-member-p)
512           :use ((:instance r-is-evaluation-eq-member-p
513                            (states-n (states m))
514                            (states-m (states n))
515                            (q p)
516                            (p q)
517                            (trans-m (transition n))
518                            (trans-n (transition m)))
519                 (:instance evaluationp-for-subset
520                            (st p)
521                            (variables (variables m)))
522                 (:instance evaluationp-for-subset
523                            (st q)
524                            (variables (variables n)))))
525          ("Goal'''"
526           :use evaluation-eq-is-symmetric)))
527)
528
529(local
530(defthm c-bisimilar-witness-matches-transition-m->n
531  (implies (and (circuit-bisim p m q n vars)
532                (next-statep p r m))
533           (next-statep q (c-bisimilar-transition-witness-m->n p r m q n vars)
534                        n))
535  :hints (("Goal"
536           :do-not '(eliminate-destructors generalize)
537           :do-not-induct t
538           :in-theory (enable next-statep))
539          ("Goal'"
540           :in-theory (disable evaluationp-for-subset
541                               r-is-evaluation-eq-member-p)
542           :use ((:instance r-is-evaluation-eq-member-p
543                            (states-m (states m))
544                            (states-n (states n))
545                            (trans-m (transition m))
546                            (trans-n (transition n)))
547                 (:instance evaluationp-for-subset
548                            (st p)
549                            (variables (variables m)))
550                 (:instance evaluationp-for-subset
551                             (st q)
552                             (variables (variables n)))))))
553)
554
555(local
556(defthm c-bisimilar-witness-matches-transition-n->m
557  (implies (and (circuit-bisim p m q n vars)
558                (next-statep q r n))
559           (next-statep p (c-bisimilar-transition-witness-n->m p m q r n vars)
560                        m))
561  :hints (("Goal"
562           :do-not '(eliminate-destructors generalize)
563           :do-not-induct t
564           :in-theory (enable next-statep))
565          ("Goal'"
566           :in-theory (disable evaluationp-for-subset
567                               only-evaluations-p
568                               all-evaluations-p
569                               evaluation-p
570                               subset
571                               r-is-evaluation-eq-member-p)
572           :use ((:instance r-is-evaluation-eq-member-p
573                            (q p)
574                            (p q)
575                            (states-n (states m))
576                            (states-m (states n))
577                            (trans-m (transition n))
578                            (trans-n (transition m)))
579                 (:instance evaluationp-for-subset
580                            (st p)
581                            (variables (variables m)))
582                 (:instance evaluationp-for-subset
583                            (st q)
584                            (variables (variables n)))))
585          ("Goal'''"
586           :use evaluation-eq-is-symmetric)))
587)
588
589(local
590(defthm c-bisimilar-witness-produces-bisimilar-states-m->n
591  (implies (and (circuit-bisim p m q n vars)
592                 (next-statep p r m))
593            (circuit-bisim r m
594                       (c-bisimilar-transition-witness-m->n p r m q n vars)
595                       n vars))
596  :hints (("Goal"
597           :do-not '(eliminate-destructors generalize)
598           :do-not-induct t
599           :in-theory (enable next-statep))
600          ("Goal'"
601           :in-theory (disable evaluationp-for-subset
602                               r-is-evaluation-eq-member-p)
603           :use ((:instance r-is-evaluation-eq-member-p
604                            (states-m (states m))
605                            (states-n (states n))
606                            (trans-m (transition m))
607                            (trans-n (transition n)))
608                 (:instance evaluationp-for-subset
609                            (st p)
610                            (variables (variables m)))
611                 (:instance evaluationp-for-subset
612                             (st q)
613                             (variables (variables n)))))))
614)
615
616(local
617(defthm c-bisimilar-witness-produces-bisimilar-states-n->m
618  (implies (and (circuit-bisim p m q n vars)
619                 (next-statep q r n))
620            (circuit-bisim
621             (c-bisimilar-transition-witness-n->m p m q r n vars)
622             m r n vars))
623  :hints (("Goal"
624           :do-not '(eliminate-destructors generalize)
625           :do-not-induct t
626           :in-theory (enable next-statep))
627          ("Goal'"
628           :in-theory (disable evaluationp-for-subset
629                               only-evaluations-p
630                               all-evaluations-p
631                               evaluation-p
632                               subset
633                               r-is-evaluation-eq-member-p)
634           :use ((:instance r-is-evaluation-eq-member-p
635                            (q p)
636                            (p q)
637                            (states-n (states m))
638                            (states-m (states n))
639                            (trans-m (transition n))
640                            (trans-n (transition m)))
641                 (:instance evaluationp-for-subset
642                            (st p)
643                            (variables (variables m)))
644                 (:instance evaluationp-for-subset
645                            (st q)
646                            (variables (variables n)))))
647          ("Subgoal 3"
648           :use evaluation-eq-is-symmetric)
649          ("Subgoal 2"
650           :use evaluation-eq-is-symmetric)
651          ("Subgoal 1"
652           :use ((:instance evaluation-eq-is-symmetric
653                            (p (evaluation-eq-member r (<- (transition m) p)
654                                                     vars))
655                            (q r))))))
656)
657
658(local
659(defthm circuit-modelp-is-modelp
660  (implies (circuit-modelp m)
661           (and (subset (initial-states m) (states m))
662                 (consp (states m))
663                 (next-states-in-states m (states m)))))
664)
665
666(local
667(in-theory (disable circuit-bisim circuit-modelp c-bisim-equiv
668                    c-bisimilar-initial-state-witness-m->n
669                    set-equal
670                    c-bisimilar-transition-witness-m->n
671                    c-bisimilar-initial-state-witness-n->m
672                    c-bisimilar-transition-witness-n->m))
673)
674
675;; (local
676;; (include-book "bisimilarity")
677;; )
678
679;; (DEFTHM circuit-bisim-implies-same-ltl-semantics
680;;   (implies (and (circuit-modelp m)
681;;                 (circuit-modelp n)
682;;                 (c-bisim-equiv m n vars)
683;;                 (subset vars (variables m))
684;;                 (subset vars (variables n))
685;;                 (restricted-formulap f vars))
686;;            (equal (ltl-semantics f m)
687;;                   (ltl-semantics f n)))
688;;   :hints (("Goal"
689;;            :do-not '(eliminate-destructors generalize)
690;;            :do-not-induct t
691;;            :use
692;;            ((:functional-instance
693;;              bisimilar-models-have-same-ltl-semantics
694;;              (bisimilar-equiv (lambda (m n vars)
695;;                                 (c-bisim-equiv m n vars)))
696;;              (modelp (lambda (m) (circuit-modelp m)))
697;;              (bisimilar (lambda (p m q n vars)
698;;                           (circuit-bisim
699;;                            p m q n vars)))
700;;              (bisimilar-initial-state-witness-m->n
701;;               (lambda (s m n vars)
702;;                 (c-bisimilar-initial-state-witness-m->n
703;;                  s m n vars)))
704;;              (bisimilar-initial-state-witness-n->m
705;;               (lambda (m s n vars)
706;;                 (c-bisimilar-initial-state-witness-n->m
707;;                  m s n vars)))
708;;              (bisimilar-transition-witness-m->n
709;;               (lambda (p r m q n vars)
710;;                 (c-bisimilar-transition-witness-m->n
711;;                  p r m q n vars)))
712;;              (bisimilar-transition-witness-n->m
713;;               (lambda (p m q r n vars)
714;;                 (c-bisimilar-transition-witness-n->m
715;;                  p m q r n vars))))))))
716
717
718(defthm c-bisimilar-equiv-implies-init->init-m->n
719  (implies (and (c-bisim-equiv m n vars)
720                (memberp s (initial-states m)))
721           (memberp (c-bisimilar-initial-state-witness-m->n s m n vars)
722                    (initial-states n))))
723
724(defthm c-bisimilar-equiv-implies-init->init-n->m
725  (implies (and (c-bisim-equiv m n vars)
726                (memberp s (initial-states n)))
727           (memberp (c-bisimilar-initial-state-witness-n->m m s n vars)
728                    (initial-states m))))
729
730(defthm c-bisimilar-equiv-implies-bisimilar-initial-states-m->n
731   (implies (and (c-bisim-equiv m n vars)
732                 (memberp s (initial-states m)))
733            (circuit-bisim s m
734                           (c-bisimilar-initial-state-witness-m->n s m n vars)
735                           n vars)))
736
737(defthm c-bisimilar-equiv-implies-bisimilar-initial-states-n->m
738   (implies (and (c-bisim-equiv m n vars)
739                 (memberp s (initial-states n)))
740            (circuit-bisim (c-bisimilar-initial-state-witness-n->m m s n vars)
741                           m s n vars)))
742
743(defthm c-bisimilar-states-have-labels-equal
744  (implies (circuit-bisim p m q n vars)
745           (set-equal (set-intersect (label-of q n) vars)
746                      (set-intersect (label-of p m) vars))))
747
748
749(defthm c-bisimilar-witness-member-of-states-m->n
750  (implies (and (circuit-bisim p m q n vars)
751                (next-statep p r m)
752                (memberp r (states m)))
753           (memberp (c-bisimilar-transition-witness-m->n p r m q n vars)
754                    (states n))))
755
756(defthm c-bisimilar-witness-member-of-states-n->m
757  (implies (and (circuit-bisim p m q n vars)
758                (next-statep q r n)
759                (memberp r (states n)))
760           (memberp (c-bisimilar-transition-witness-n->m p m q r n vars)
761                    (states m))))
762
763(defthm c-bisimilar-witness-produces-bisimilar-states-m->n
764  (implies (and (circuit-bisim p m q n vars)
765                 (next-statep p r m))
766            (circuit-bisim r m
767                       (c-bisimilar-transition-witness-m->n p r m q n vars)
768                       n vars)))
769
770(defthm c-bisimilar-witness-produces-bisimilar-states-n->m
771  (implies (and (circuit-bisim p m q n vars)
772                 (next-statep q r n))
773            (circuit-bisim
774             (c-bisimilar-transition-witness-n->m p m q r n vars)
775             m r n vars)))
776
777(defthm c-bisimilar-witness-matches-transition-m->n
778  (implies (and (circuit-bisim p m q n vars)
779                (next-statep p r m))
780           (next-statep q (c-bisimilar-transition-witness-m->n p r m q n vars)
781                        n)))
782
783(defthm c-bisimilar-witness-matches-transition-n->m
784  (implies (and (circuit-bisim p m q n vars)
785                (next-statep q r n))
786           (next-statep p (c-bisimilar-transition-witness-n->m p m q r n vars)
787                        m)))
788