examples/acl2-hol-ltl-paper-example/circuit-bisim.ml

230 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "TRUTHP-LABEL") (
231 mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (mksym
233 mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "LABEL") (mksym
238 mksym "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "S") (
241 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (
242 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "LABEL") (mksym
255 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (
256 mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
270 "ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym
284 "LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
285 mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2"
286 "LABEL") (mkpair (mksym "ACL2" "S") (mkpair (mkpair (mksym "COMMON-LISP"
295 "ALL-TRUTHSP-LABEL-EXPANDED") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
297 "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "S") (
310 "ACL2" "LABEL") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (
321 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (
322 mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP"
337 "LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "STATES") (mkpair (mksym
344 mksym "ACL2" "LABEL-OF") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (
347 "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LABEL-SUBSET-VARS") (
357 "LABEL-SUBSET-SUBSET-REDUCTION") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
359 "LABEL-SUBSET-VARS") (mkpair (mksym "ACL2" "STATES") (mkpair (mksym "ACL2"
365 "ACL2" "SUBSET") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym
517 "LABEL-SUBSET-VARS") (mkpair (mkpair (mksym "ACL2" "G") (mkpair (mkpair (
775 "TRUTHP-LABEL-FROM-ONLY-TRUTHP") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
782 "NIL"))))) (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mkpair (
783 mksym "ACL2" "LABEL-OF") (mkpair (mksym "ACL2" "S") (mkpair (mksym "ACL2" "M") (
797 "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (
834 "VARIABLES-IN-LABEL-ARE-T-IN-Q") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (
837 "SET-INTERSECT") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "VARS") (
839 mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (
840 mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "P") (mksym "COMMON-LISP"
867 "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LABEL") (mkpair (mksym "ACL2" "Q") (
875 "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "V") (mkpair (mksym "ACL2" "LABEL") (
881 "TRUTHP-LABEL-TO-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
886 "IF") (mkpair (mkpair (mksym "ACL2" "TRUTHP-LABEL") (mkpair (mksym "ACL2"
893 "NIL")))) (mkpair (mkpair (mksym "ACL2" "ALL-TRUTHSP-LABEL") (mkpair (mksym
909 "TRUTHP-LABEL-IS-A-SUBSET") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (
911 "TRUTHP-LABEL") (mkpair (mksym "ACL2" "LP") (mkpair (mksym "ACL2" "P") (mksym
918 "ALL-TRUTHSP-LABEL") (mkpair (mksym "ACL2" "LQ") (mkpair (mksym "ACL2" "Q") (
1113 "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (mksym
1116 "ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym "ACL2" "LABEL-OF") (mkpair (
1124 "C-BISIMILAR-WITNESS-MEMBER-OF-STATES-M->N") (mkpair (mkpair (mksym "ACL2"
1151 "C-BISIMILAR-WITNESS-MEMBER-OF-STATES-N->M") (mkpair (mkpair (mksym "ACL2"