Searched refs:ok2 (Results 1 - 14 of 14) sorted by relevance

/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_execScript.sml44 (!a fns s1 s2 t ts ok ok2.
46 MR_ev (Or ts,a,ctxt,fns,ok1) (s2,ok2) ==>
47 MR_ev (Or (t::ts),a,ctxt,fns,ok) (s2,ok2))
49 (!e1 e2 e3 s1 s a ok1 ok2.
51 MR_ev (e3,a,ctxt,fns,ok1) (s,ok2)
53 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2))
55 (!e1 e2 e3 s1 s a ok1 ok2.
57 MR_ev (e2,a,ctxt,fns,ok1) (s,ok2)
59 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2))
61 (!e xs ys fns a ok1 ok2
[all...]
H A Dmilawa_initScript.sml27 (!xs fns io exp s fns2 io2 ok2 io3 ok3.
28 R_ev (sexp2term exp,FEMPTY,fns,io,T) (s,fns2,io2,ok2) /\
30 R_aux_exec (exp::xs,fns,io) (io3,ok2 /\ ok3))`;
49 ``R_ev (sexp2term x1,FEMPTY,fns1,io1,T) (ans1,fns2,io2',ok2) /\
61 R_aux_exec ([x1;x2;x3;x4;x5;x6],fns1,io1) (io7,ok2 /\ ok3 /\ ok4 /\ ok5 /\ ok6 /\ ok7)``,
65 \\ Q.LIST_EXISTS_TAC [`ans1`,`fns2`,`io2'`,`ok2`]
H A Dmilawa_proofpScript.sml2519 !x1 x2 x3 x4 io ok. ?res ok2 io2.
2520 R_ap (Fun name,[x1;x2;x3;x4],ARB,k,io,ok) (res,k,io ++ io2,ok2) /\
2521 (ok2 ==> (io2 = "")) /\
2527 (x3 = list2sexp (MAP f2sexp thms)) /\ (x4 = atbl) /\ ok2 ==>
2606 let (res,k2,io2,ok2) = y in
2608 R_ap (f,args,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\
2611 let (res,k2,io2,ok2) = y in
2613 R_evl (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\
2616 let (res,k2,io2,ok2) = y in
2618 R_ev (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2))``,
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/
H A Dlisp_alt_semanticsScript.sml38 RR_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==>
39 RR_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2))
43 RR_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2)
45 RR_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
49 RR_ev (e2,a,fns1,io1,ok1) (s,fns2,io2,ok2)
51 RR_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
55 RR_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2)
57 RR_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2))
60 RR_evl (el,a,fns,io,ok) (args,fns1,io1,ok1) /\ RR_ap (fc,args,a,fns1,io1,ok1) (x,fns2,io2,ok2) /\
63 RR_ev (App fc el,a,fns,io,ok) (x,fns2,io2,ok2))
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/spec/
H A Dlisp_semanticsScript.sml184 (!a fns io s1 fns1 io1 s2 fns2 io2 t ts ok ok2.
186 R_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==>
187 R_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2))
189 (!e1 e2 e3 s1 s a ok1 ok2.
191 R_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2)
193 R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
195 (!e1 e2 e3 s1 s a ok1 ok2.
197 R_ev (e2,a,fns1,io1,ok1) (s,fns2,io2,ok2)
199 R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
201 (!e xs ys fns a ok1 ok2
[all...]
/seL4-l4v-master/HOL4/examples/Crypto/IDEA/
H A DideaScript.sml103 `InverseKeys (ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9) =
105 InverseKey ok5,InverseKey ok4,InverseKey ok3,InverseKey ok2,
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 DMain.C111 bool ok1 = false, ok2 = false; local
127 ok2 = true;
131 if (!ok1 || !ok2)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_correctnessScript.sml37 (!input fns io ok input2 exp rest s fns2 io2 io3 ok2 ok3.
40 R_ev (sexp2term exp,FEMPTY,fns,io,ok) (s,fns2,io2,ok2) /\
41 R_exec (rest,fns2,io2 ++ sexp2string s ++ "\n",ok2) (io3,ok3) ==>
229 !input fns output output2 ok2. (x = (input,fns,output)) /\ (y = (output2,ok2)) ==>
237 (zERROR_MESSAGE ex \/ ~zS * zPC ^pc * zLISP_OUTPUT (IO_STREAMS "" output2,ok2))``,
262 BC_REFINES (fns2,io2) bc8 /\ bc_inv bc8 /\ (ok2 <=> bc8.ok)` by
293 |> (fn th => SPEC_BOOL_FRAME_RULE th ``R_exec (input,fns,"") (output2,ok2)``)
305 \\ REVERSE (Cases_on `ok2`) THEN1
310 |> Q.GEN `output2` |> Q.GEN `ok2` |>
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractScript.sml52 ``(by ==> R_ev (y,e,fns1,io1,ok1) (ans2,fns2,io2,ok2)) /\
60 if isTrue ans1 then ok2 else ok3)``,
126 ``R_evl (el,a,fns1,io1,ok1) (sl,fns2,io2,ok2) ==>
128 R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2)``,
133 ``(bl ==> R_evl (el,a,fns1,io1,ok1) (sl,fns2,io2,ok2)) ==>
135 (b /\ bl ==> R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2))``,
358 (b2 ==> R_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2)) ==>
360 R_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2)``,
366 (b2 ==> R_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2)) ==>
368 R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) (x,fns2,io2,ok2)``,
[all...]
H A Dlisp_extractLib.sml402 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
469 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
912 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp113 bool ok1 = false, ok2 = false; local
129 ok2 = true;
133 if (!ok1 || !ok2)
/seL4-l4v-master/HOL4/src/update/
H A DupdateLib.sml285 val ok2 = Lib.can (Type.match_type (ty --> ty)) value
291 val _ = c_form orelse ok2 tm_ty andalso is_o_expr tm
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Drules.tex2416 \ 2.\ ok2\isanewline
2425 \ 3.\ ok2
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Drules.tex2416 \ 2.\ ok2\isanewline
2425 \ 3.\ ok2

Completed in 63 milliseconds