Lines Matching defs:STATES
17 (DEFUN EVALUATION-EQ-MEMBER-P (ST STATES VARS)
18 (IF (ENDP STATES)
20 (IF (EVALUATION-EQ ST (CAR STATES) VARS)
22 (EVALUATION-EQ-MEMBER-P ST (CDR STATES)
25 (DEFUN EVALUATION-EQ-MEMBER (ST STATES VARS)
26 (IF (ENDP STATES)
28 (IF (EVALUATION-EQ ST (CAR STATES) VARS)
29 (CAR STATES)
30 (EVALUATION-EQ-MEMBER ST (CDR STATES)
34 (IMPLIES (EVALUATION-EQ-MEMBER-P P STATES VARS)
35 (MEMBERP (EVALUATION-EQ-MEMBER P STATES VARS)
36 STATES)))
39 (IMPLIES (EVALUATION-EQ-MEMBER-P P STATES VARS)
40 (EVALUATION-EQ P (EVALUATION-EQ-MEMBER P STATES VARS)
54 (DEFUN STRICT-EVALUATION-LIST-P (VARS STATES)
55 (IF (ENDP STATES)
57 (IF (STRICT-EVALUATION-P (CAR STATES) VARS)
58 (STRICT-EVALUATION-LIST-P VARS (CDR STATES))
68 (DEFUN ONLY-EVALUATIONS-P (STATES VARS)
69 (IF (ENDP STATES)
71 (IF (EVALUATION-P (CAR STATES) VARS)
72 (ONLY-EVALUATIONS-P (CDR STATES) VARS)
75 (DEFUN-SK ALL-EVALUATIONS-P (STATES VARS)
78 (EVALUATION-EQ-MEMBER-P ST STATES VARS))))
81 (M-STATES N-STATES VARS)
82 (IF (ENDP M-STATES)
84 (IF (EVALUATION-EQ-MEMBER-P (CAR M-STATES)
85 N-STATES VARS)
86 (EVALUATION-EQ-SUBSET-P (CDR M-STATES)
87 N-STATES VARS)
91 (IMPLIES (IF (EVALUATION-EQ-SUBSET-P M-STATES N-STATES VARS)
92 (MEMBERP P M-STATES)
94 (EVALUATION-EQ-MEMBER-P P N-STATES VARS)))
103 (DEFUN ONLY-TRUTH-P (STATES M)
104 (IF (ENDP STATES)
106 (IF (TRUTHP-LABEL (LABEL-OF (CAR STATES) M)
107 (CAR STATES))
108 (ONLY-TRUTH-P (CDR STATES) M)
127 (DEFUN ONLY-ALL-TRUTHS-P (STATES M VARS)
128 (IF (ENDP STATES)
130 (IF (ALL-TRUTHSP-LABEL (LABEL-OF (CAR STATES) M)
131 (CAR STATES)
133 (ONLY-ALL-TRUTHS-P (CDR STATES) M VARS)
136 (DEFUN LABEL-SUBSET-VARS (STATES M VARS)
137 (IF (ENDP STATES)
139 (IF (SUBSET (LABEL-OF (CAR STATES) M) VARS)
140 (LABEL-SUBSET-VARS (CDR STATES) M VARS)
144 (IMPLIES (IF (LABEL-SUBSET-VARS STATES M VARS)
145 (MEMBERP P STATES)
150 (STATES-M TRANS-M STATES-N TRANS-N VARS)
154 (IF (MEMBERP P STATES-M)
155 (IF (MEMBERP Q STATES-N)
168 (IF (WELL-FORMED-TRANSITION-P STATES-M TRANS-M STATES-N TRANS-N VARS)
171 (IF (MEMBERP P STATES-M)
172 (IF (MEMBERP Q STATES-N)
184 (STATES STATES-PRIME TRANS)
185 (IF (ENDP STATES)
187 (IF (SUBSET (G (CAR STATES) TRANS)
188 STATES-PRIME)
189 (TRANSITION-SUBSET-P (CDR STATES)
190 STATES-PRIME TRANS)
194 (IMPLIES (IF (TRANSITION-SUBSET-P STATES STATES-PRIME TRANS)
195 (IF (MEMBERP P STATES)
199 (MEMBERP R STATES-PRIME)))
203 (IF (ONLY-EVALUATIONS-P (G ':STATES M)
205 (IF (ALL-EVALUATIONS-P (G ':STATES M)
208 (G ':STATES M))
209 (IF (ONLY-ALL-TRUTHS-P (G ':STATES M)
211 (IF (ONLY-TRUTH-P (G ':STATES M) M)
212 (IF (LABEL-SUBSET-VARS (G ':STATES M)
214 (IF (TRANSITION-SUBSET-P (G ':STATES M)
215 (G ':STATES M)
217 (IF (SUBSET (G ':INITIAL-STATES M)
218 (G ':STATES M))
219 (IF (CONSP (G ':STATES M))
220 (NEXT-STATES-IN-STATES M (G ':STATES M))
237 (IF (WELL-FORMED-TRANSITION-P (G ':STATES M)
239 (G ':STATES N)
242 (IF (WELL-FORMED-TRANSITION-P (G ':STATES N)
244 (G ':STATES M)
247 (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES M)
248 (G ':INITIAL-STATES N)
250 (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES N)
251 (G ':INITIAL-STATES M)
266 (IF (MEMBERP P (G ':STATES M))
267 (IF (MEMBERP Q (G ':STATES N))
268 (IF (WELL-FORMED-TRANSITION-P (G ':STATES M)
270 (G ':STATES N)
273 (IF (WELL-FORMED-TRANSITION-P (G ':STATES N)
275 (G ':STATES M)
278 (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES M)
279 (G ':INITIAL-STATES N)
281 (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES N)
282 (G ':INITIAL-STATES M)
300 (EVALUATION-EQ-MEMBER S (G ':INITIAL-STATES N)
305 (EVALUATION-EQ-MEMBER S (G ':INITIAL-STATES M)
310 (ALL-EVALUATIONS-P STATES VARS)
312 (EVALUATION-EQ-MEMBER-P ST STATES VARS)))
315 (IMPLIES (IF (ONLY-TRUTH-P STATES M)
316 (MEMBERP S STATES)
321 (IMPLIES (IF (ONLY-ALL-TRUTHS-P STATES M VARS)
322 (MEMBERP S STATES)
394 (IMPLIES (IF (ONLY-EVALUATIONS-P STATES VARS)
395 (MEMBERP P STATES)
403 (IF (WELL-FORMED-TRANSITION-P STATES-M TRANS-M STATES-N TRANS-N VARS)
404 (IF (MEMBERP P STATES-M)
405 (IF (MEMBERP Q STATES-N)
420 (MEMBERP S (G ':INITIAL-STATES M))
423 (G ':INITIAL-STATES N))))
427 (MEMBERP S (G ':INITIAL-STATES N))
430 (G ':INITIAL-STATES M))))
433 C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-M->N
435 (MEMBERP S (G ':INITIAL-STATES M))
442 C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-N->M
444 (MEMBERP S (G ':INITIAL-STATES N))
449 (DEFTHM C-BISIMILAR-STATES-HAVE-LABELS-EQUAL
455 C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N
458 (MEMBERP R (G ':STATES M))
462 (G ':STATES N))))
465 C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M
468 (MEMBERP R (G ':STATES N))
472 (G ':STATES M))))
475 C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-M->N
484 C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-N->M