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