tests/gold/ltl.sml

204 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NEXT-STATEP") (
219 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
234 "NEXT-STATES-IN-STATES") (mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym
235 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
237 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
241 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
246 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
249 "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym
250 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
258 "NEXT-STATES-IN-STATES-CLARIFIED-AUX") (mkpair (mkpair (mksym "ACL2"
260 "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "STATES") (
262 mkpair (mkpair (mksym "ACL2" "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2"
263 "M") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (
264 mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym
272 "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
278 "NEXT-STATES-IN-STATES-CLARIFIED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
280 "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym
282 "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
286 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
288 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (
296 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym