Lines Matching defs:implies
184 (forall v (implies (not (memberp v vars))
207 (implies (evaluation-p st vars)
216 (implies (and (evaluation-eq-subset-p m-states n-states vars)
232 (and (implies (equal (<- s (car vars)) T)
248 (implies (and (evaluation-eq p q vars)
320 (implies (and (uniquep vars)
513 (implies (circuitp C)
521 (implies (circuitp C)
531 (implies (circuitp C)
566 (defthm c-bisimilar-equiv-implies-init->init-m->n
567 (implies (and (c-bisim-equiv m n vars)
572 (defthm c-bisimilar-equiv-implies-init->init-n->m
573 (implies (and (c-bisim-equiv m n vars)
578 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-m->n
579 (implies (and (c-bisim-equiv m n vars)
585 (defthm c-bisimilar-equiv-implies-bisimilar-initial-states-n->m
586 (implies (and (c-bisim-equiv m n vars)
592 (implies (circuit-bisim p m q n vars)
598 (implies (and (circuit-bisim p m q n vars)
605 (implies (and (circuit-bisim p m q n vars)
612 (implies (and (circuit-bisim p m q n vars)
619 (implies (and (circuit-bisim p m q n vars)
626 (implies (and (circuit-bisim p m q n vars)
632 (implies (and (circuit-bisim p m q n vars)