Lines Matching +defs:INITIAL +defs:STATES
75 (DEFUN INITIAL-STATEP (P M) (MEMBERP P (G ':INITIAL-STATES M)))
79 (DEFUN NEXT-STATES-IN-STATES (M STATES)
80 (IF (ENDP STATES)
82 (IF (SUBSET (G (CAR STATES) (G ':TRANSITION M))
83 (G ':STATES M))
84 (NEXT-STATES-IN-STATES M (CDR STATES))
87 (DEFTHM NEXT-STATES-IN-STATES-CLARIFIED-AUX
88 (IMPLIES (IF (MEMBERP P STATES)
89 (IF (NEXT-STATES-IN-STATES M STATES)
93 (MEMBERP Q (G ':STATES M))))
95 (DEFTHM NEXT-STATES-IN-STATES-CLARIFIED
96 (IMPLIES (IF (NEXT-STATES-IN-STATES M (G ':STATES M))
97 (IF (MEMBERP P (G ':STATES M))
101 (MEMBERP Q (G ':STATES M))))