Searched refs:h3 (Results 1 - 21 of 21) sorted by relevance

/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Djiraver439.c45 unsigned h3(unsigned x) function
/seL4-l4v-10.1.1/HOL4/examples/hfs/
H A DhfbScript.sml13 (���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 Dencap1.lisp95 (((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 Dpattern_matchingScript.sml95 `(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 Dexample.lisp93 (((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 Dmy_listScript.sml106 \\ 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 Dmy_listScript.sml106 \\ 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 DgeneralHelpersScript.sml915 >> 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 DSHA1Script.sml247 `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 DreachTools.sml54 val _ = print " h3\n"*)
/seL4-l4v-10.1.1/HOL4/examples/computability/lambda/
H A DchurchlistScript.sml230 @@ (ccons @@ h3 @@ XXX)) -w->*
231 h3``,
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A Dimproved_gcScript.sml842 ?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 Darm_improved_gcScript.sml503 ?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 Dstop_and_copyScript.sml864 ?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 DwalkstarScript.sml36 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 DnwalkstarScript.sml139 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 Djit_incrementalScript.sml1626 \\ 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 Dlisp_parseScript.sml2840 \\ 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 Dlisp_printScript.sml1710 \\ Q.ABBREV_TAC `h3 = (a - 0x4w =+ r7) ((a - 0x8w =+ r9) h)`
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A Drich_listScript.sml2959 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 Ddecidable_separationLogicScript.sml5579 !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

Completed in 177 milliseconds