| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
| H A D | lisp_alt_semanticsScript.sml | 29 RR_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
30 RR_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
33 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==>
34 RR_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1))
37 RR_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\
38 RR_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==>
42 RR_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~isTrue s1 /\
43 RR_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2)
48 RR_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 /\
49 RR_ev (e2,a,fns1,io1,ok1) (
[all...] |
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/spec/ |
| H A D | lisp_semanticsScript.sml | 176 (!a fns io ok s fns1 io1 ok1.
177 R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
178 R_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
181 R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==>
182 R_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1))
185 R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\
186 R_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==>
189 (!e1 e2 e3 s1 s a ok1 ok2.
190 R_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~isTrue s1 /\
191 R_ev (e3,a,fns1,io1,ok1) (
[all...] |
| /seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
| H A D | milawa_execScript.sml | 36 (!a fns ok s ok1.
37 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==>
38 MR_ev (Or [],a,ctxt,fns,ok) (s,ok1))
41 MR_ev (t,a,ctxt,fns,ok) (s1,ok1) /\ isTrue s1 ==>
42 MR_ev (Or (t::ts),a,ctxt,fns,ok) (s1,ok1))
45 MR_ev (t,a,ctxt,fns,ok) (s1,ok1) /\ ~(isTrue s1) /\
46 MR_ev (Or ts,a,ctxt,fns,ok1) (s2,ok2) ==>
49 (!e1 e2 e3 s1 s a ok1 ok2.
50 MR_ev (e1,a,ctxt,fns,ok) (s1,ok1) /\ ~isTrue s1 /\
51 MR_ev (e3,a,ctxt,fns,ok1) (
[all...] |
| H A D | milawa_initScript.sml | 92 (ans,fns1,io1,ok1) =
94 (io1 = io) /\ (ok1 = ~(name IN FDOM fns))``,
|
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractScript.sml | 52 ``(by ==> R_ev (y,e,fns1,io1,ok1) (ans2,fns2,io2,ok2)) /\
53 (bz ==> R_ev (z,e,fns1,io1,ok1) (ans3,fns3,io3,ok3)) ==>
54 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
65 ``(by ==> R_ev (y,e,fns1,io1,ok1) res2) /\
66 (bz ==> R_ev (z,e,fns1,io1,ok1) res3) ==>
67 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
77 ``(bz ==> R_ev (Or (y::xs),e,fns1,io1,ok1) (ans3,fns3,io3,ok3)) ==>
78 (bx ==> R_ev (x,e,fns,io,ok) (ans1,fns1,io1,ok1)) ==>
84 if isTrue ans1 then ok1 else ok3)``,
89 ``(bz ==> R_ev (Or (y::xs),e,fns1,io1,ok1) res
[all...] |
| /seL4-l4v-master/HOL4/examples/Crypto/IDEA/ |
| H A D | ideaScript.sml | 103 `InverseKeys (ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9) =
106 InverseKey ok1) : OddKeySched`;
216 ((ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9): OddKeySched) =
217 ListToOddKeys t ((k1,k2,k3,k4),ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8)) /\
219 ((ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9): OddKeySched) =
220 ListToOddKeys t ((k1,k2,k3,k4),ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8))`;
|
| /seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Main.C | 111 bool ok1 = false, ok2 = false; local
114 ok1 = true, p = main[i];
131 if (!ok1 || !ok2)
|
| /seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
| H A D | zc2hs.cpp | 113 bool ok1 = false, ok2 = false; local
116 ok1 = true, p = main[i];
133 if (!ok1 || !ok2)
|
| /seL4-l4v-master/HOL4/src/update/ |
| H A D | updateLib.sml | 284 val ok1 = Lib.can (Type.match_type ty) value
290 val c_form = ok1 tm_ty andalso is_c_expr tm
|
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_opsScript.sml | 2197 val post = set_pc th ``SEP_EXISTS io1 ok1 zX z0 z1. zLISP_R ^STAT (if ok1 then z0 else zX,if ok1 then z1 else Sym "NIL",Sym "NIL",
2198 Sym "NIL",x4,x5,xs,xs1,io1,xbp,qs,code,amnt,ok) * zPC p * ~zS * cond (if ok1 then FST (next_token (getINPUT io)) = (z0,z1) else isVal zX) * cond (ok1 ==> (IO_INPUT_APPLY (SND o next_token) io = io1))``
2207 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`io2`,`ok1`,`zX`,`z0`,`z1`]
2243 \\ REPEAT STRIP_TAC \\ REVERSE (Cases_on `ok1`)
|
| H A D | lisp_symbolsScript.sml | 1871 ?ok1 zX z0 z1 w0i w1i w2i w3i io2 gi fi sa2.
1876 (if ok1 then z0 else zX,if ok1 then z1 else Sym "NIL",Sym "NIL",Sym "NIL",x4,x5,^VAR_REST)
1878 (ok1 ==> (REPLACE_INPUT_IO zs2 io = io2)) /\
1879 (if ok1 then (z = (z0,z1)) else isVal zX)``,
|
| /seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
| H A D | rules.tex | 2415 \ 1.\ ok1\isanewline
2424 \ 2.\ ok1\isanewline
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | rules.tex | 2415 \ 1.\ ok1\isanewline
2424 \ 2.\ ok1\isanewline
|