tests/gold/ltl.sml

8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-CONSTANTP") (
22 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-VARIABLEP") (
37 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "LTL-FORMULAP") (
41 mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") (
43 mksym "ACL2" "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP"
44 "NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-VARIABLEP") (mkpair (mksym "ACL2"
58 mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP"
60 "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (
78 mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (
90 "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "ACL2" "F") (mkpair (mksym
94 "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "LTL-CONSTANTP") (mkpair (
96 "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
98 "LTL-VARIABLEP") (mkpair (mksym "ACL2" "F") (mksym "COMMON-LISP" "NIL"))) (
115 mkpair (mkpair (mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym
118 mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP"
137 "ACL2" "RESTRICTED-FORMULAP") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (
149 "RESTRICTED-FORMULA-IS-AN-LTL-FORMULA") (mkpair (mkpair (mksym "ACL2"
150 "IMPLIES") (mkpair (mkpair (mksym "ACL2" "RESTRICTED-FORMULAP") (mkpair (
152 mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mksym "ACL2" "F") (
158 "CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym "ACL2" "F") (mksym
162 mkpair (mksym "ACL2" "LTL-CONSTANTP") (mkpair (mksym "ACL2" "F") (mksym
173 "SET-UNION") (mkpair (mkpair (mksym "ACL2" "CREATE-RESTRICTED-VAR-SET") (
176 "ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym "COMMON-LISP"
185 mkpair (mksym "ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mkpair (mksym
195 "LTL-FORMULA-IS-A-RESTRICTED-FORMULA") (mkpair (mkpair (mksym "ACL2"
196 "IMPLIES") (mkpair (mkpair (mksym "ACL2" "LTL-FORMULAP") (mkpair (mksym
198 "RESTRICTED-FORMULAP") (mkpair (mksym "ACL2" "F") (mkpair (mkpair (mksym
199 "ACL2" "CREATE-RESTRICTED-VAR-SET") (mkpair (mksym "ACL2" "F") (mksym