Lines Matching defs:MEMBERP
33 (DEFTHM MEMBER-IS-MEMBERP
35 (MEMBERP (EVALUATION-EQ-MEMBER P STATES VARS)
45 (IMPLIES (NOT (MEMBERP V VARS))
50 (NOT (MEMBERP V VARS))
92 (MEMBERP P M-STATES)
115 (MEMBERP (CAR VARS) LABEL))
121 (IF (MEMBERP V VARS)
125 (MEMBERP V LABEL)))
145 (MEMBERP P STATES)
154 (IF (MEMBERP P STATES-M)
155 (IF (MEMBERP Q STATES-N)
171 (IF (MEMBERP P STATES-M)
172 (IF (MEMBERP Q STATES-N)
195 (IF (MEMBERP P STATES)
196 (MEMBERP R (G P TRANS))
199 (MEMBERP R STATES-PRIME)))
266 (IF (MEMBERP P (G ':STATES M))
267 (IF (MEMBERP Q (G ':STATES N))
316 (MEMBERP S STATES)
322 (MEMBERP S STATES)
327 (DEFTHM MEMBERP-TO-INTERSECT-REDUCTION
328 (IMPLIES (MEMBERP V (SET-INTERSECT X Y))
329 (IF (MEMBERP V X) (MEMBERP V Y) 'NIL)))
333 (MEMBERP V VARS)
338 (IMPLIES (IF (MEMBERP V (SET-INTERSECT LABEL VARS))
347 (IF (MEMBERP V VARS)
353 (MEMBERP V LABEL)))
356 (IMPLIES (IF (MEMBERP V (SET-INTERSECT LP VARS))
365 (MEMBERP V LQ)))
395 (MEMBERP P STATES)
404 (IF (MEMBERP P STATES-M)
405 (IF (MEMBERP Q STATES-N)
408 (MEMBERP R (G P TRANS-M))
420 (MEMBERP S (G ':INITIAL-STATES M))
422 (MEMBERP (C-BISIMILAR-INITIAL-STATE-WITNESS-M->N S M N VARS)
427 (MEMBERP S (G ':INITIAL-STATES N))
429 (MEMBERP (C-BISIMILAR-INITIAL-STATE-WITNESS-N->M M S N VARS)
435 (MEMBERP S (G ':INITIAL-STATES M))
444 (MEMBERP S (G ':INITIAL-STATES N))
458 (MEMBERP R (G ':STATES M))
461 (MEMBERP (C-BISIMILAR-TRANSITION-WITNESS-M->N P R M Q N VARS)
468 (MEMBERP R (G ':STATES N))
471 (MEMBERP (C-BISIMILAR-TRANSITION-WITNESS-N->M P M Q R N VARS)