tests/gold/circuit-bisim.lisp

80 (DEFUN EVALUATION-EQ-SUBSET-P
86                (EVALUATION-EQ-SUBSET-P (CDR M-STATES)
90 (DEFTHM EVALUATION-EQ-SUBSET-TO-MEMBER
91         (IMPLIES (IF (EVALUATION-EQ-SUBSET-P M-STATES N-STATES VARS)
136 (DEFUN LABEL-SUBSET-VARS (STATES M VARS)
139            (IF (SUBSET (LABEL-OF (CAR STATES) M) VARS)
140                (LABEL-SUBSET-VARS (CDR STATES) M VARS)
143 (DEFTHM LABEL-SUBSET-SUBSET-REDUCTION
144         (IMPLIES (IF (LABEL-SUBSET-VARS STATES M VARS)
147                  (SUBSET (LABEL-OF P M) VARS)))
161                            (EVALUATION-EQ-SUBSET-P (G P TRANS-M)
179         (EVALUATION-EQ-SUBSET-P (G P TRANS-M)
183 (DEFUN TRANSITION-SUBSET-P
187            (IF (SUBSET (G (CAR STATES) TRANS)
189                (TRANSITION-SUBSET-P (CDR STATES)
193 (DEFTHM TRANSITION-SUBSET-P-EXPANDED
194         (IMPLIES (IF (TRANSITION-SUBSET-P STATES STATES-PRIME TRANS)
212                      (IF (LABEL-SUBSET-VARS (G ':STATES M)
214                          (IF (TRANSITION-SUBSET-P (G ':STATES M)
217                              (IF (SUBSET (G ':INITIAL-STATES M)
235            (IF (SUBSET VARS (G ':VARIABLES M))
236                (IF (SUBSET VARS (G ':VARIABLES N))
247                            (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES M)
250                                (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES N)
278                        (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES M)
281                            (IF (EVALUATION-EQ-SUBSET-P (G ':INITIAL-STATES N)
284                                (IF (SUBSET VARS (G ':VARIABLES M))
285                                    (IF (SUBSET VARS (G ':VARIABLES N))
345 (DEFTHM ONLY-TRUTHSP-AND-SUBSET-TO-SUBSET
348                          (IF (SUBSET VARS VARIABLES)
355 (DEFTHM TRUTHP-LABEL-TO-SUBSET
359                              (IF (SUBSET VARS VARIABLES)
367 (DEFTHM TRUTHP-LABEL-IS-A-SUBSET
370                          (IF (SUBSET VARS VARIABLES)
375                  (SUBSET (SET-INTERSECT LP VARS) LQ)))
387 (DEFTHM EVALUATIONP-FOR-SUBSET
389                      (SUBSET VARS VARIABLES)