tests/gold/circuit_bisim.sml

227 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "TRUTHP-LABEL") (
228 mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (mksym
230 mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "LABEL") (mksym
235 mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (
238 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (
239 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "LABEL") (mksym
252 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (
253 mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
267 "ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym
281 "LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
282 mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2"
283 "LABEL") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP"
292 "ALL-TRUTHSP-LABEL-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
294 "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (
307 "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
318 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (
319 mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP"
334 "LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
341 mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
344 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LABEL-SUBSET-VARS") (
354 "LABEL-SUBSET-SUBSET-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
356 "LABEL-SUBSET-VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2"
362 "ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym
514 "LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
772 "TRUTHP-LABEL-FROM-ONLY-TRUTHP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
779 "NIL"))))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mkpair (
780 mksym "ACL2" "LABEL-OF") (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (
794 "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (
831 "VARIABLES-IN-LABEL-ARE-T-IN-Q") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
834 "SET-INTERSECT") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "VARS") (
836 mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (
837 mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP"
864 "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "Q") (
872 "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "LABEL") (
878 "TRUTHP-LABEL-TO-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
883 "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mksym "ACL2"
890 "NIL")))) (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym
906 "TRUTHP-LABEL-IS-A-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
908 "TRUTHP-LABEL") (mkpair (mksym "ACL2" "LP") (mkpair (mksym "ACL2" "P") (mksym
915 "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LQ") (mkpair (mksym "ACL2" "Q") (
1110 "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym
1113 "ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (
1121 "C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N") (mkpair (mkpair (mksym "ACL2"
1148 "C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M") (mkpair (mkpair (mksym "ACL2"