tests/gold/summary.sml

256 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NEXT-STATEP") (
271 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
286 "NEXT-STATES-IN-STATES") (mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym
287 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
289 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
293 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
298 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
301 "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (mkpair (mksym
302 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
332 "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
334 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
339 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
343 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
351 "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
353 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
358 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
360 mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
362 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
383 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
385 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
389 mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
392 mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
418 "ONLY-EVALUATIONS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
421 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
425 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
428 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
436 mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym
442 "ST") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym
448 "EVALUATION-EQ-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "M-STATES") (mkpair (
449 mksym "ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP"
451 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "M-STATES") (mksym "COMMON-LISP"
455 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "M-STATES") (
456 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N-STATES") (mkpair (mksym
459 mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
460 "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
469 "EVALUATION-EQ-SUBSET-P") (mkpair (mksym "ACL2" "M-STATES") (mkpair (mksym
470 "ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
472 mksym "ACL2" "M-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
476 "ACL2" "N-STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL"))))) (
500 mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "M") (mksym
502 mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym
507 mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
509 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
512 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
545 "ONLY-ALL-TRUTHS-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
548 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
553 "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
555 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
558 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
567 "LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
570 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
575 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
578 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
587 "WELL-FORMED-TRANSITION-P") (mkpair (mkpair (mksym "ACL2" "STATES-M") (mkpair (
588 mksym "ACL2" "TRANS-M") (mkpair (mksym "ACL2" "STATES-N") (mkpair (mksym
599 mksym "ACL2" "STATES-M") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
601 mksym "ACL2" "Q") (mkpair (mksym "ACL2" "STATES-N") (mksym "COMMON-LISP"
621 "TRANSITION-SUBSET-P") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
622 "ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "TRANS") (mksym "COMMON-LISP"
624 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
629 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "TRANS") (
630 mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "STATES-PRIME") (mksym
632 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
633 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "STATES-PRIME") (mkpair (
644 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
651 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
662 "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
666 "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (
674 "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
678 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
686 "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
688 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
696 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
698 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
703 "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
705 mksym "ACL2" "NEXT-STATES-IN-STATES") (mkpair (mksym "ACL2" "M") (mkpair (
707 mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
748 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
754 "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (
762 mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
767 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
775 "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP"
778 mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (
782 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
785 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
815 mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
819 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
824 mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
829 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
837 "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (
843 "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (mksym
850 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
853 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
858 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
861 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
996 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
1007 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (
1039 mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym
1041 mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym
1047 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
1050 "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mksym
1056 mkpair (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "STATES") (mksym
1058 mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym
1064 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
1067 "CDR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mksym
1074 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1077 "STATES") (mkpair (mkpair (mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (
1078 mkpair (mksym "ACL2" "REC-STATES") (mkpair (mksym "ACL2" "VARS") (mksym
1082 "ACL2" "REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym
1085 "REC-STATES") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
1089 "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "VARS") (mksym
1118 mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair (
1121 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
1123 mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
1126 "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2"
1128 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
1214 "PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "ACL2" "VARS") (mkpair (mksym
1225 "PRODUCE-NEXT-STATE") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
1254 (mkpair (mksym "ACL2" "DEFUN-SK") (mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") (
1262 mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym "ACL2" "PRODUCE-NEXT-STATE") (
1272 "CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "ACL2" "P") (mkpair (mksym
1273 "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
1276 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1279 mkpair (mksym "ACL2" "NEXT-STATE-IS-OK") (mkpair (mksym "ACL2" "P") (mkpair (
1280 mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym
1284 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1285 "ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (
1286 mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
1289 mkpair (mkpair (mksym "ACL2" "CREATE-NEXT-STATES-OF-P") (mkpair (mksym "ACL2"
1291 "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (mkpair (
1298 "CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
1299 "ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
1302 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
1305 mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym
1307 "CREATE-NEXT-STATES-OF-P") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
1308 mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1309 "ACL2" "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
1311 "CREATE-NEXT-STATES") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (
1312 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
1313 "STATES-PRIME") (mkpair (mksym "ACL2" "VARS") (mkpair (mksym "ACL2"
1322 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mkpair (
1323 mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (
1325 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mkpair (
1328 mksym "ACL2" "STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mksym
1331 "STATES") (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2"
1341 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (
1342 mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (
1344 mkpair (mksym "KEYWORD" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (
1345 mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "INITIAL-STATES") (
1346 mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (
1351 mksym "ACL2" "CREATE-NEXT-STATES") (mkpair (mkpair (mksym "ACL2" "SET-UNION") (
1352 mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym
1354 mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym
1356 "EQUATIONS") (mksym "COMMON-LISP" "NIL")))))) (mkpair (mksym "ACL2" "STATES") (
1357 mkpair (mksym "ACL2" "INITIAL-STATES") (mkpair (mksym "ACL2" "LABEL-FN") (
1361 "INITIAL-STATES") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL")))) (
1365 "ACL2" "VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2"
1366 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))))))) (mksym "COMMON-LISP"
1374 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL")))))) (mksym "COMMON-LISP" "NIL")))) (
1382 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (
1515 "CORRESPONDING-STATES") (mkpair (mkpair (mksym "ACL2" "INITS") (mkpair (mksym
1524 mkpair (mksym "ACL2" "CORRESPONDING-STATES") (mkpair (mkpair (mksym
1562 "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
1563 mksym "ACL2" "CORRESPONDING-STATES") (mkpair (mkpair (mksym "ACL2" "G") (
1565 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "C") (
1617 "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1628 "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1666 "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1675 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "N") (
1687 "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym
1696 "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "M") (
1702 "C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-M->N") (mkpair (mkpair (
1708 mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (
1722 "C-BISIMILAR-EQUIV-IMPLIES-BISIMILAR-INITIAL-STATES-N->M") (mkpair (mkpair (
1728 mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym "COMMON-LISP" "NIL"))) (
1742 "C-BISIMILAR-STATES-HAVE-LABELS-EQUAL") (mkpair (mkpair (mksym "ACL2"
1758 "C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N") (mkpair (mkpair (mksym "ACL2"
1763 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (
1767 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
1778 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
1785 "C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M") (mkpair (mkpair (mksym "ACL2"
1790 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "NEXT-STATEP") (mkpair (
1794 mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (mksym
1805 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
1812 "C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-M->N") (mkpair (mkpair (mksym
1817 "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (
1831 "C-BISIMILAR-WITNESS-PRODUCES-BISIMILAR-STATES-N->M") (mkpair (mkpair (mksym
1836 "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (
1855 "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mksym "ACL2" "R") (mkpair (
1859 "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mkpair (mksym
1873 "NEXT-STATEP") (mkpair (mksym "ACL2" "Q") (mkpair (mksym "ACL2" "R") (mkpair (
1877 "ACL2" "NEXT-STATEP") (mkpair (mksym "ACL2" "P") (mkpair (mkpair (mksym