tests/inputs/circuit-bisim.lisp

52   (implies (evaluation-eq-member-p p states vars)
57   (implies (evaluation-eq-member-p p states vars)
62   (forall v (implies (not (memberp v vars))
66   (implies (and (strict-evaluation-p st vars)
92           (implies (evaluation-p st vars)
101   (implies (and (evaluation-eq-subset-p m-states n-states vars)
117     (and (implies (equal (<- s (car vars)) T)
122   (implies (and (all-truthsp-label label s vars)
138   (implies (and (label-subset-vars states m vars)
146           (implies (and (evaluation-eq p q vars)
156   (implies (and (well-formed-transition-p states-m trans-m states-n trans-n vars)
175   (implies (and (transition-subset-p states states-prime trans)
235   (implies (and (evaluation-p st vars)
245 (defthm c-bisimilar-equiv-implies-init->init-n->m
246   (implies (and (c-bisim-equiv m n vars)
253 (defthm c-bisimilar-equiv-implies-init->init-m->n
254   (implies (and (c-bisim-equiv m n vars)
262   (implies (and (memberp s init)
268 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-m->n
269    (implies (and (c-bisim-equiv m n vars)
290 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-n->m
291    (implies (and (c-bisim-equiv m n vars)
321   (implies (and (only-truth-p states m)
328   (implies (and (only-all-truths-p states m vars)
335   (implies (memberp v (set-intersect x y))
343   (implies (and (evaluation-eq p q vars)
351   (implies (and (memberp v (set-intersect label vars))
357   (implies (and (equal (<- q v) T)
364   (implies (and (memberp v (set-intersect lp vars))
375   (implies (and (truthp-label lp p)
384   (implies (and (subset lp lq)
391   (implies (and (truthp-label lp p)
401   (implies (circuit-bisim p m q n vars)
418   (implies (circuit-bisim p m q n vars)
444   (implies (and (evaluation-p st variables)
449   (implies (and (only-evaluations-p states vars)
454   (implies (and (evaluation-eq p q vars)
468   (implies (and (circuit-bisim p m q n vars)
495   (implies (and (circuit-bisim p m q n vars)
531   (implies (and (circuit-bisim p m q n vars)
557   (implies (and (circuit-bisim p m q n vars)
591   (implies (and (circuit-bisim p m q n vars)
618   (implies (and (circuit-bisim p m q n vars)
660   (implies (circuit-modelp m)
679 ;; (DEFTHM circuit-bisim-implies-same-ltl-semantics
680 ;;   (implies (and (circuit-modelp m)
718 (defthm c-bisimilar-equiv-implies-init->init-m->n
719   (implies (and (c-bisim-equiv m n vars)
724 (defthm c-bisimilar-equiv-implies-init->init-n->m
725   (implies (and (c-bisim-equiv m n vars)
730 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-m->n
731    (implies (and (c-bisim-equiv m n vars)
737 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-n->m
738    (implies (and (c-bisim-equiv m n vars)
744   (implies (circuit-bisim p m q n vars)
750   (implies (and (circuit-bisim p m q n vars)
757   (implies (and (circuit-bisim p m q n vars)
764   (implies (and (circuit-bisim p m q n vars)
771   (implies (and (circuit-bisim p m q n vars)
778   (implies (and (circuit-bisim p m q n vars)
784   (implies (and (circuit-bisim p m q n vars)