Searched +refs:NEXT +refs:STATES +refs:IN +refs:STATES (Results 1 - 9 of 9) sorted by relevance

/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dltl.ml207 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NEXT-STATEP") (
222 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
237 "NEXT-STATES-IN-STATES") (mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym
238 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
240 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
244 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
249 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
[all...]
H A Dcircuit-bisim.ml44 "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
46 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
51 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
55 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
63 "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
65 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
70 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
72 mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
74 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
83 "STATES") (mkpai
[all...]
H A Dsummary.ml260 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "NEXT-STATEP") (
275 "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "INITIAL-STATES") (mksym
290 "NEXT-STATES-IN-STATES") (mkpair (mkpair (mksym "ACL2" "M") (mkpair (mksym
291 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
293 mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
297 "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
302 mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "KEYWORD" "STATES") (
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/gold/
H A Dltl.sml204 (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") (
[all...]
H A Dcircuit_bisim.sml41 "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
43 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
48 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
52 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (
60 "ACL2" "STATES") (mkpair (mksym "ACL2" "VARS") (mksym "COMMON-LISP" "NIL")))) (
62 "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP"
67 "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "VARS") (
69 mkpair (mksym "ACL2" "STATES") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (
71 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "STATES") (mksym
80 "STATES") (mkpai
[all...]
H A Dsummary.sml256 (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") (
[all...]
H A Dm1_story.sml8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXT-INST") (
232 "M1" "DO-INST") (mkpair (mkpair (mksym "M1" "NEXT-INST") (mkpair (mksym "M1"
576 "COLLECT-VARS-IN-EXPR") (mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym
584 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (
585 mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (
597 "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (
602 "M1" "COLLECT-VARS-IN-STMT*") (mkpair (mkpair (mksym "M1"
603 "COLLECT-VARS-IN-STMT") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym
609 "COLLECT-VARS-IN-STMT") (mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym
617 "COLLECT-VARS-IN
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/
H A DLTLScript.sml56 | NEXT of formula (* X *)
69 (Formula Vars (ATOMIC a) = a IN Vars)
81 (Formula Vars (NEXT f) = Formula Vars f)
146 M.S0 SUBSET M.S /\ (!s s'. s IN M.S /\ (s,s') IN M.R ==> s' IN M.S)`;
157 val States_def = Define `States = (ksym "STATES")`;
158 val InitialStates_def = Define `InitialStates = (ksym "INITIAL-STATES")`;
348 ``!M s p. s IN M.S /\ PATH M s p /\ MODEL M ==> !n. (p n) IN
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A Dm1_story.sml8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXT-INST") (
232 "M1" "DO-INST") (mkpair (mkpair (mksym "M1" "NEXT-INST") (mkpair (mksym "M1"
576 "COLLECT-VARS-IN-EXPR") (mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym
584 "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (
585 mkpair (mkpair (mksym "M1" "COLLECT-VARS-IN-EXPR") (mkpair (mksym "M1" "VARS") (
597 "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "COLLECT-VARS-IN-STMT*") (mkpair (
602 "M1" "COLLECT-VARS-IN-STMT*") (mkpair (mkpair (mksym "M1"
603 "COLLECT-VARS-IN-STMT") (mkpair (mksym "M1" "VARS") (mkpair (mkpair (mksym
609 "COLLECT-VARS-IN-STMT") (mkpair (mkpair (mksym "M1" "VARS") (mkpair (mksym
617 "COLLECT-VARS-IN
[all...]

Completed in 105 milliseconds