Lines Matching defs:implies
11 (implies (and (memberp p states)
19 (implies (and (memberp p (g :states M)) ; sadly, seems necessary
26 (defthm subset-implies-memberp
27 (implies (and (subset x y)
32 (implies (and (circuit-modelp M)
49 (implies (and (subset x y)
54 (defthm set-equal-implies-equal-memberp
55 (implies (set-equal x y)
62 (implies (circuit-bisim p m q n vars)
69 set-equal-implies-equal-memberp)
71 (:instance set-equal-implies-equal-memberp
74 (:instance set-equal-implies-equal-memberp
80 (implies (and (memberp a vars)