/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | jiraver439.c | 45 unsigned h3(unsigned x) function
|
/seL4-l4v-10.1.1/HOL4/examples/hfs/ |
H A D | hfbScript.sml | 13 (���h1 h2 h3. hfb0_equiv h1 h2 ��� hfb0_equiv h2 h3 ��� hfb0_equiv h1 h3)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | encap1.lisp | 95 (((h3 *) => *) 97 (local (defun h3 (x) x)) 99 (defthm h3-prop 101 (integerp (h3 x)))) 102 (defun h5 (x) (h3 x))
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/test/ |
H A D | pattern_matchingScript.sml | 95 `(g8 (CONS h1 (CONS h2 (CONS h3 (CONS h4 (CONS h5 h6))))) = 96 CONS [h1;h2;h3;h4;h5] [h6]) /\ 100 `(g9 (CONS h1 (CONS h2 (CONS h3 (CONS h4 (CONS h5 h6))))) = 101 CONS [h1;h2;h3;h4;h5] [h6]) /\
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/encap/ |
H A D | example.lisp | 93 (((h3 *) => *) 95 (local (defun h3 (x) x)) 97 (defthm h3-prop 99 (integerp (h3 x))))
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | my_listScript.sml | 106 \\ MAP_EVERY X_GEN_TAC [`h1`,`h2`,`h3`,`h4`] 108 \\ `LENGTH (h1::c) = LENGTH (h3::d)` 110 \\ `ZIP (a,b) ++ ZIP (h1::c,h3::d) = ZIP (a ++ h1::c,b ++ h3::d)`
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | my_listScript.sml | 106 \\ MAP_EVERY X_GEN_TAC [`h1`,`h2`,`h3`,`h4`] 108 \\ `LENGTH (h1::c) = LENGTH (h3::d)` 110 \\ `ZIP (a,b) ++ ZIP (h1::c,h3::d) = ZIP (a ++ h1::c,b ++ h3::d)`
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | generalHelpersScript.sml | 915 >> rename[`GROUP_BY R (h3::t2) = h4::t3`] 916 >- (`R h3 y` by ( 918 >> Cases_on `SPAN (R h3) t2` >> fs[] 919 >> `!x. MEM x (FST (q,r)) ==> (R h3 x)` 921 >> Cases_on `y = h3` >> fs[] 927 >- (`P h3 H` by ( 928 Cases_on `y = h3` >> rw[] 932 `FLAT (GROUP_BY R (h3::t2)) = h3::t2` 934 >> `MEM y (FLAT (GROUP_BY R (h3 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/Crypto/SHA-1/ |
H A D | SHA1Script.sml | 247 `digestBlock (block:word8 list) (h0,h1,h2,h3,h4) = 249 let (hbar1,wlist1) = Round (Helper f1) 0 (h0,h1,h2,h3,h4) wlist in 255 (h0+a, h1+b, h2+c, h3+d, h4+e)`;
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | reachTools.sml | 54 val _ = print " h3\n"*)
|
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/ |
H A D | churchlistScript.sml | 230 @@ (ccons @@ h3 @@ XXX)) -w->* 231 h3``,
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | improved_gcScript.sml | 842 ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\ 863 \\ Q.LIST_EXISTS_TAC [`h3`,`f3`] \\ `j <= j4` by DECIDE_TAC 938 ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i2,j2,e,b2,e2,m2,D1(CUT(i2,j2)m2)) /\ 959 \\ FULL_SIMP_TAC std_ss [] \\ Q.LIST_EXISTS_TAC [`h3 |+ (i,ADDR_MAP f3 xs,n,d)`,`f3`] 992 \\ Q.EXISTS_TAC `(h3,D0 (CUT (b,i) m3),D0 (CUT (i,j3) m3), 1090 \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h3,f3) ttt` MP_TAC
|
H A D | arm_improved_gcScript.sml | 503 ?f2 h3 f3. 507 ok_memory m2 /\ gc_inv (h1,roots1,h3,f3) 556 ?f2 h3 f3. 560 ok_memory m2 /\ gc_inv (h1,roots1,h3,f3) 680 \\ `?f2 h3 f3. 688 gc_inv (h1,roots1,h3,f3) 857 \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h3,f3) ttt` MP_TAC
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/garbage-collector/ |
H A D | stop_and_copyScript.sml | 864 ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\ 885 \\ Q.LIST_EXISTS_TAC [`h3`,`f3`] \\ `j <= j4` by DECIDE_TAC 960 ?h3 f3. gc_inv (h1,roots1,h3,f3) (b,i2,j2,e,b2,e2,m2,D1(CUT(i2,j2)m2)) /\ 981 \\ FULL_SIMP_TAC std_ss [] \\ Q.LIST_EXISTS_TAC [`h3 |+ (i,ADDR_MAP f3 xs,n,d)`,`f3`] 1021 \\ Q.EXISTS_TAC `(h3,D0 (CUT (b,i) m3),D0 (CUT (i,j3) m3), 1123 \\ Q.PAT_X_ASSUM `gc_inv (h,roots,h3,f3) ttt` MP_TAC
|
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/first-order/ |
H A D | walkstarScript.sml | 36 val [h2,h1,h3] = hyp (inst_walkstar pre_walkstar_def) 73 val th3 = Q.store_thm("walkstar_thWF",`wfs s ��� ^h3`,
|
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/nominal/ |
H A D | nwalkstarScript.sml | 139 val [h3,h1,h2,h4] = hyp (inst_nwalkstar pre_nwalkstar_def) value 180 val th3 = prove(``nwfs s ��� ^(h3)``,
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_incrementalScript.sml | 1626 \\ Q.PAT_ABBREV_TAC `h3 = (r7 - 0x20w:word32 =+ (n2w n):word32) fff` 1630 MAP_INV r7 0 j cs) (fun2set (h3,dh))` by 1633 \\ Q.EXISTS_TAC `y''''''` \\ Q.UNABBREV_TAC `h3` \\ SEP_WRITE_TAC) 1635 (`h (r7 - 0x24w) = h3 (r7 - 0x24w)` by (Q.UNABBREV_TAC `h3` 1651 then 0x0w else 0x1w,n2w n,r7,df,f,dg,g,dh,h3)`` 1730 (eax,edx,edi,w,0w,ebx,ebp,dh,h3,df,f3,dg,g)`` x86_inc_th 1816 \\ Q.EXISTS_TAC `h3` 1829 val th = QGENL [`w`,`pi`,`j`,`h3`,`h`,`g`,`f3`,`f`,`cp`,`edi`,`ebp`,`dh`,`dg`,`df`] th
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_parseScript.sml | 2840 \\ Q.ABBREV_TAC `h3 = (r5 =+ r5 + n2w (8 * sexp_lex_space (sexp2string s)) + 0x8w) 2850 (Q.UNABBREV_TAC `h3` 2855 (Q.UNABBREV_TAC `h3` 2862 (Q.UNABBREV_TAC `h3` 2866 (Q.UNABBREV_TAC `h3` 2932 SEP_FILL (sa,xi)) (fun2set (h3,dh))` by 2933 (Q.PAT_X_ASSUM `ppp (fun2set (hi,dh))` MP_TAC \\ Q.UNABBREV_TAC `h3` 2947 SEP_FILL (sa,xi)) (fun2set (h3,dh 3022 \\ `SEP_FILL (sa,xi) (fun2set (h3,ch_active_set2 (r5 + 0x8w,0,ll)))` by
|
H A D | lisp_printScript.sml | 1710 \\ Q.ABBREV_TAC `h3 = (a - 0x4w =+ r7) ((a - 0x8w =+ r9) h)`
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | rich_listScript.sml | 2959 THEN MAP_EVERY Q.X_GEN_TAC [`h1`,`h2`,`h3`,`h4`] 2961 THEN `LENGTH (h1::c) = LENGTH (h3::d)` by ASM_SIMP_TAC list_ss [] 2962 THEN `ZIP (a, b) ++ ZIP (h1::c, h3::d) = ZIP (a ++ h1::c, b ++ h3::d)`
|
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
H A D | decidable_separationLogicScript.sml | 5579 !h3. ((DISJOINT (FDOM h2) (FDOM h3)) /\ 5580 (SF_SEM s h3 (sf_ls e2 e3)) /\ (DS_POINTER_DANGLES s h3 e4)) ==> 5581 SF_SEM s (FUNION h3 h2) (sf_ls e1 e4))``, 5653 `SF_SEM s (FUNION h1 h3) (sf_ls e1 e3)` by ( 5680 `SF_SEM s (FUNION (FUNION h1 h3) h2) (sf_ls e1 e4)` by ( 5695 `FUNION h3 (FUNION h1 h2) = FUNION (FUNION h1 h3) h2` suffices_by (STRIP_TAC THEN
|