Lines Matching +defs:INITIAL +defs:STATES
94 (DEFUN INITIAL-STATEP (P M) (MEMBERP P (G ':INITIAL-STATES M)))
98 (DEFUN NEXT-STATES-IN-STATES (M STATES)
99 (IF (ENDP STATES)
101 (IF (SUBSET (G (CAR STATES) (G ':TRANSITION M))
102 (G ':STATES M))
103 (NEXT-STATES-IN-STATES M (CDR STATES))
114 (DEFUN EVALUATION-EQ-MEMBER-P (ST STATES VARS)
115 (IF (ENDP STATES)
117 (IF (EVALUATION-EQ ST (CAR STATES) VARS)
119 (EVALUATION-EQ-MEMBER-P ST (CDR STATES)
122 (DEFUN EVALUATION-EQ-MEMBER (ST STATES VARS)
123 (IF (ENDP STATES)
125 (IF (EVALUATION-EQ ST (CAR STATES) VARS)
126 (CAR STATES)
127 (EVALUATION-EQ-MEMBER ST (CDR STATES)
135 (DEFUN STRICT-EVALUATION-LIST-P (VARS STATES)
136 (IF (ENDP STATES)
138 (IF (STRICT-EVALUATION-P (CAR STATES) VARS)
139 (STRICT-EVALUATION-LIST-P VARS (CDR STATES))
149 (DEFUN ONLY-EVALUATIONS-P (STATES VARS)
150 (IF (ENDP STATES)
152 (IF (EVALUATION-P (CAR STATES) VARS)
153 (ONLY-EVALUATIONS-P (CDR STATES) VARS)
156 (DEFUN-SK ALL-EVALUATIONS-P (STATES VARS)
159 (EVALUATION-EQ-MEMBER-P ST STATES VARS))))
162 (M-STATES N-STATES VARS)
163 (IF (ENDP M-STATES)
165 (IF (EVALUATION-EQ-MEMBER-P (CAR M-STATES)
166 N-STATES VARS)
167 (EVALUATION-EQ-SUBSET-P (CDR M-STATES)
168 N-STATES VARS)
172 (IMPLIES (IF (EVALUATION-EQ-SUBSET-P M-STATES N-STATES VARS)
173 (MEMBERP P M-STATES)
175 (EVALUATION-EQ-MEMBER-P P N-STATES VARS)))
184 (DEFUN ONLY-TRUTH-P (STATES M)
185 (IF (ENDP STATES)
187 (IF (TRUTHP-LABEL (LABEL-OF (CAR STATES) M)
188 (CAR STATES))
189 (ONLY-TRUTH-P (CDR STATES) M)
200 (DEFUN ONLY-ALL-TRUTHS-P (STATES M VARS)
201 (IF (ENDP STATES)
203 (IF (ALL-TRUTHSP-LABEL (LABEL-OF (CAR STATES) M)
204 (CAR STATES)
206 (ONLY-ALL-TRUTHS-P (CDR STATES) M VARS)
209 (DEFUN LABEL-SUBSET-VARS (STATES M VARS)
210 (IF (ENDP STATES)
212 (IF (SUBSET (LABEL-OF (CAR STATES) M) VARS)
213 (LABEL-SUBSET-VARS (CDR STATES) M VARS)
217 (STATES-M TRANS-M STATES-N TRANS-N VARS)
221 (IF (MEMBERP P STATES-M)
222 (IF (MEMBERP Q STATES-N)
233 (STATES STATES-PRIME TRANS)
234 (IF (ENDP STATES)
236 (IF (SUBSET (G (CAR STATES) TRANS)
237 STATES-PRIME)
238 (TRANSITION-SUBSET-P (CDR STATES)
239 STATES-PRIME TRANS)
244 (IF (ONLY-EVALUATIONS-P (G ':STATES M)
246 (IF (ALL-EVALUATIONS-P (G ':STATES M)
249 (G ':STATES M))
250 (IF (ONLY-ALL-TRUTHS-P (G ':STATES M)
252 (IF (ONLY-TRUTH-P (G ':STATES M) M)
253 (IF (LABEL-SUBSET-VARS (G ':STATES M)
255 (IF (TRANSITION-SUBSET-P (G ':STATES M)
256 (G ':STATES M)
258 (IF (SUBSET (G ':INITIAL-STATES M)
259 (G ':STATES M))
260 (IF (CONSP (G ':STATES M))
261 (NEXT-STATES-IN-STATES M (G ':STATES M))
278 (IF (WELL-FORMED-TRANSITION-P (G ':STATES M)
280 (G ':STATES N)
283 (IF (WELL-FORMED-TRANSITION-P (G ':STATES N)
285 (G ':STATES M)
288 (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES M)
289 (G ':INITIAL-STATES N)
291 (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES N)
292 (G ':INITIAL-STATES M)
307 (IF (MEMBERP P (G ':STATES M))
308 (IF (MEMBERP Q (G ':STATES N))
309 (IF (WELL-FORMED-TRANSITION-P (G ':STATES M)
311 (G ':STATES N)
314 (IF (WELL-FORMED-TRANSITION-P (G ':STATES N)
316 (G ':STATES M)
319 (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES M)
320 (G ':INITIAL-STATES N)
322 (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES N)
323 (G ':INITIAL-STATES M)
374 (IF (ONLY-EVALUATIONS-P (G ':INITIAL-STATES C)
377 (G ':INITIAL-STATES C))
388 (DEFUN ASSIGN-T (V STATES)
389 (IF (ENDP STATES)
391 (CONS (S V 'T (CAR STATES))
392 (ASSIGN-T V (CDR STATES)))))
394 (DEFUN ASSIGN-NIL (V STATES)
395 (IF (ENDP STATES)
397 (CONS (S V 'NIL (CAR STATES))
398 (ASSIGN-NIL V (CDR STATES)))))
400 (DEFUN CREATE-ALL-EVALUATIONS (VARS STATES)
402 STATES
403 ((LAMBDA (REC-STATES VARS)
404 (BINARY-APPEND (ASSIGN-T (CAR VARS) REC-STATES)
405 (ASSIGN-NIL (CAR VARS) REC-STATES)))
407 STATES)
418 (DEFUN CREATE-LABEL-FN (STATES VARS LABEL)
419 (IF (ENDP STATES)
421 (CREATE-LABEL-FN (CDR STATES)
423 (S (CAR STATES)
424 (LABEL-FN-OF-ST (CAR STATES) VARS)
483 (DEFUN CREATE-NEXT-STATES-OF-P
484 (P STATES VARS EQUATIONS)
485 (IF (ENDP STATES)
487 (IF (NEXT-STATE-IS-OK P (CAR STATES)
489 (CONS (CAR STATES)
490 (CREATE-NEXT-STATES-OF-P P (CDR STATES)
492 (CREATE-NEXT-STATES-OF-P P (CDR STATES)
495 (DEFUN CREATE-NEXT-STATES
496 (STATES STATES-PRIME VARS EQUATIONS)
497 (IF (ENDP STATES)
499 (S (CAR STATES)
500 (CREATE-NEXT-STATES-OF-P (CAR STATES)
501 STATES-PRIME VARS EQUATIONS)
502 (CREATE-NEXT-STATES (CDR STATES)
503 STATES-PRIME VARS EQUATIONS))))
508 (VARS EQUATIONS INITIAL-STATES)
510 (STATES EQUATIONS VARS INITIAL-STATES)
511 ((LAMBDA (LABEL-FN EQUATIONS VARS STATES INITIAL-STATES)
512 ((LAMBDA (TRANSITION STATES INITIAL-STATES LABEL-FN VARS)
519 (S ':INITIAL-STATES
520 INITIAL-STATES
521 (S ':STATES
522 (SET-UNION INITIAL-STATES STATES)
524 (CREATE-NEXT-STATES (SET-UNION INITIAL-STATES STATES)
525 (SET-UNION INITIAL-STATES STATES)
527 STATES INITIAL-STATES LABEL-FN VARS))
528 (CREATE-LABEL-FN (SET-UNION INITIAL-STATES STATES)
530 EQUATIONS VARS STATES INITIAL-STATES))
532 EQUATIONS VARS INITIAL-STATES))
535 (G ':INITIAL-STATES C)))
595 (DEFUN CORRESPONDING-STATES (INITS VARS)
599 (CORRESPONDING-STATES (CDR INITS)
613 (S ':INITIAL-STATES
614 (CORRESPONDING-STATES (G ':INITIAL-STATES C)
635 (DEFUN C-BISIMILAR-INITIAL-STATE-WITNESS-M->N
637 (EVALUATION-EQ-MEMBER S (G ':INITIAL-STATES N)
640 (DEFUN C-BISIMILAR-INITIAL-STATE-WITNESS-N->M
642 (EVALUATION-EQ-MEMBER S (G ':INITIAL-STATES M)
657 (MEMBERP S (G ':INITIAL-STATES M))
659 (MEMBERP (C-BISIMILAR-INITIAL-STATE-WITNESS-M->N S M N VARS)
660 (G ':INITIAL-STATES N))))
664 (MEMBERP S (G ':INITIAL-STATES N))
666 (MEMBERP (C-BISIMILAR-INITIAL-STATE-WITNESS-N->M M S N VARS)
667 (G ':INITIAL-STATES M))))
670 C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-M->N
672 (MEMBERP S (G ':INITIAL-STATES M))
675 (C-BISIMILAR-INITIAL-STATE-WITNESS-M->N S M N VARS)
679 C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-N->M
681 (MEMBERP S (G ':INITIAL-STATES N))
683 (CIRCUIT-BISIM (C-BISIMILAR-INITIAL-STATE-WITNESS-N->M M S N VARS)
686 (DEFTHM C-BISIMILAR-STATES-HAVE-LABELS-EQUAL
692 C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N
695 (MEMBERP R (G ':STATES M))
699 (G ':STATES N))))
702 C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M
705 (MEMBERP R (G ':STATES N))
709 (G ':STATES M))))
712 C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-M->N
721 C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-N->M