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