Searched refs:l2 (Results 1 - 25 of 322) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/
H A Dreturn_sl.c9 static long return_sl(long l1, long l2) argument
11 return l1 - l2;
20 unsigned long l1, l2; local
25 values[1] = &l2;
31 l2 = 1073741824L;
34 printf("res: %ld, %ld\n", (long)res, l1 - l2);
/seL4-l4v-10.1.1/HOL4/src/sort/
H A DpermLib.sig12 (* Given a term of the form "PERM l1 l2" this
14 l1 and l2. It knows about APPEND and CONS.
18 PERM_ELIM_DUPLICATES_CONV ``PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4)``
20 |- PERM (x::l1 ++ y::l2 ++ l3) (y::l3 ++ z::l2 ++ l4) <=>
25 (* Given a term of the form "PERM l1 l2" this
27 l1 and l2. It uses that resorting is allowed inside permutations.
31 PERM_TAKE_DROP_CONV ``PERM (DROP n l1++l2++TAKE n l1) (l1++TAKE n l2
[all...]
H A DsortingScript.sml52 `!l1 l2. PERM l1 l2 = PERM l2 l1`,
67 `!l1 l2 x. PERM l1 l2 ==> PERM (x::l1) (x::l2)`,
73 (`PERM (x::l1) (x::l2) ==> PERM l1 l2`,
144 `!l1 l2. PERM (APPEND l1 l2) (APPEN
[all...]
H A DmergesortScript.sml18 `!R l1 l2 x y.
20 SORTED R (l1 ++ l2) /\
22 MEM y l2
31 stable R l1 l2 =
32 !p. (!x y. p x /\ p y ==> R x y) ==> FILTER p l1 = FILTER p l2`;
62 (merge R (x::l1) (y::l2) =
64 x::merge R l1 (y::l2)
66 y::merge R (x::l1) l2)`;
127 (merge_tail negate R (x::l1) (y::l2) acc =
129 merge_tail negate R l1 (y::l2) (
[all...]
H A DternaryComparisonsScript.sml63 /\ (list_compare cmp [] l2 = LESS)
65 /\ (list_compare cmp (x::l1) (y::l2) =
68 | EQUAL => list_compare cmp l1 l2
77 !l1 l2. (list_compare cmp l1 l2 = EQUAL) = (l1 = l2)���,
86 /\ (list_merge a_lt [] l2 = l2)
87 /\ (list_merge a_lt (x:'a :: l1) (y::l2) =
89 then x::list_merge a_lt l1 (y::l2)
[all...]
H A DpermLib.sml42 val t = ``PERM (x1::l1 ++ (l2 ++ (x2::x3::l3) ++ x4::l4)) (x1::l1 ++ ((x2::x3::l3) ++ x4::l4 ++ l2))``
43 val t1 = ``x1::x2::x3::(l1 ++ (x2::x3::l3 ++ x4::l4 ++ l2 ++ l4))``
44 val t2 = ``x1::x2::x8::(x4::l4 ++ l2++l4)``
127 val l2 = (rand o rand o rhs o concl o valOf) l_thm_opt value
129 SOME (MP (ISPECL [x,l,e,l2] PERM_FUN_CONS_11_SWAP_AT_FRONT)
136 val (l1,l2) = listSyntax.dest_append (rand t)
139 PERM_MOVE_CONS_TO_FRONT e (mk_icomb (PERM_tm, l2))
145 SOME (MP (ISPECL [l2,l1,e,l1'] PERM_FUN_CONS_APPEND_1)
150 val l2'
174 val l2 = (rand o rhs o concl) thm1; value
211 val l2 = (rand o rand o rhs o concl o valOf) l'_thm_opt value
277 val l2 = (rand o rhs o concl) thm1; value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dtemporal_deep_simplificationsLibScript.sml639 (!l1 l1' l2 l2'. LTL_EQUIVALENT l1 l1' ==>
640 LTL_EQUIVALENT l2 l2' ==>
641 (LTL_EQUIVALENT_INITIAL l1 l2 =
642 LTL_EQUIVALENT_INITIAL l1' l2')) /\
654 (!l1 l2 l1' l2'. LTL_EQUIVALENT l1 l1' ==>
655 LTL_EQUIVALENT l2 l2'
[all...]
/seL4-l4v-10.1.1/HOL4/src/tfl/examples/sorting/
H A DpartitionScript.sml22 `(part P [] l1 l2 = (l1,l2))
23 /\ (part P (h::rst) l1 l2 =
24 if P h then part P rst (h::l1) l2
25 else part P rst l1 (h::l2))`;
43 `!P L l1 l2 p q.
44 ((p,q) = part P L l1 l2)
45 ==> (LENGTH L + LENGTH l1 + LENGTH l2 = LENGTH p + LENGTH q)`,
54 `!P L l1 l2 p q.
55 ((p,q) = part P L l1 l2)
[all...]
H A DpermScript.sml48 `!l1 l2. PERM l1 l2 = PERM l2 l1`,
69 `!l1 l2 x. PERM l1 l2 ==> PERM (x::l1) (x::l2)`,
75 Q.prove(`PERM (x::l1) (x::l2) ==> PERM l1 l2`,
95 `!h l1 l2. APPEND (FILTER ($=h) l1) (h::l2)
[all...]
/seL4-l4v-10.1.1/l4v/tools/autocorres/tools/stats/
H A Dprofile.zsh25 l1=0.0; l2=0.0; hl=0.0; wa=0.0; ts=0.0
30 if [ $stage = '(L2)' ]; then l2=$(($l2 + $time)); fi;
37 printf "L2: %10.3fs\n" "$l2"
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DindexedListsScript.sml67 ``!l1 l2 f1 f2.
68 l1 = l2 /\ (!x n. MEM x l2 ==> f1 n x = f2 n x) ==>
69 MAPi f1 l1 = MAPi f2 l2``,
74 ``l1 = l2 ==> (!x n. (x = EL n l2) ==> n < LENGTH l2 ==> f1 n x = f2 n x) ==>
75 MAPi f1 l1 = MAPi f2 l2``,
76 map_every qid_spec_tac [`f1`, `f2`, `l2`] >> Induct_on `l1` >>
96 ``!l1 l2
[all...]
H A DlistScript.sml168 (!l1 l2 h. APPEND (h::l1) l2 = h::APPEND l1 l2)���};
386 ���!l1 l2. ~(l1 = l2) ==> !h1:'a. !h2. ~(h1::l1 = h2::l2)���,
392 ���!h1:'a. !h2. ~(h1 = h2) ==> !l1 l2. ~(h1::l1 = h2::l2)���,
398 ���!h1:'a.!h2.(h1=h2) ==> !l1 l2. (l1 = l2)
[all...]
H A DlistSimps.sml50 val (l1, l2) = dest_append t
51 val _ = if is_list l1 andalso is_list l2 then () else raise UNCHANGED
64 val (l1, l2) = dest_append t
66 val _ = if is_list l2 andalso is_list l12 then () else raise UNCHANGED
80 (* |- x1::x2::l1 ++ (SNOC x3 (x4::l2 ++ *)
82 (* [x1; x2] ++ l1 ++ [x4] ++ l2 ++ REVERSE l5 ++ REVERSE l4 ++ *)
108 (* |- x1::x2::l1 ++ (SNOC x3 (x4::l2 ++ *)
110 (* x1::x2::(l1 ++ [x4] ++ l2 ++ REVERSE l5 ++ REVERSE l4 ++ *)
124 val t = ``[x1;x2] ++ l1 ++ l2 ++ [x3] ++ l3 = x1::x2'::l1' ++ l3``
125 |- ([x1; x2] ++ l1 ++ l2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/
H A DcongToolsLibScript.sml9 Define `LIST_AS_SET_CONGRUENCE_RELATION R l1 l2 =
10 ((!x1. MEM x1 l1 ==> (?x2. MEM x2 l2 /\ R x1 x2)) /\
11 (!x2. MEM x2 l2 ==> (?x1. MEM x1 l1 /\ R x1 x2)))`
24 ``!R. (!x1 x2 x3. (R x1 x2 /\ R x2 x3) ==> R x1 x3) ==> (!l1 l2 l3. LIST_AS_SET_CONGRUENCE_RELATION R l1 l2 /\ LIST_AS_SET_CONGRUENCE_RELATION R l2 l3 ==> LIST_AS_SET_CONGRUENCE_RELATION R l1 l3)``,
/seL4-l4v-10.1.1/HOL4/src/update/
H A DupdateScript.sml95 `!h l1 l2.
97 (FIND (\x. FST x = FST h) (l1 ++ l2) = FIND (\x. FST x = FST h) l2)`,
101 `!y l1 l2.
103 (FIND (\x. FST x = y) (l1 ++ h::l2) =
104 FIND (\x. FST x = y) (l1 ++ l2))`,
108 `!l1 l2 y.
109 ALL_DISTINCT (MAP FST l1) /\ PERM l1 l2 ==>
110 (FIND (\x. FST x = y) l1 = FIND (\x. FST x = y) l2)`,
126 `!l1 l2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/
H A Dquicksort.ml5 let l1,l2 = partition (curry $> x) l' in
6 quicksort l1 @ [x] @ quicksort l2
30 (\l [l1;l2]. l1 @ [hd l] @ l2),
58 (\l [l1;l2]. l1 @ [hd l] @ l2),
H A Dmux.ml16 ?l1 l2 l3.
18 NAND_SPEC(l1,i2,l2) /\
20 NAND_SPEC(l2,l3,o)");;
H A DPARITY.ml49 ?l1 l2 l3 l4 l5. NOT(l2,l1) /\
50 MUX(in,l1,l2,l3) /\
51 REG(out,l2) /\
76 THEN FILTER_ASM_REWRITE_TAC(lines`l2`)[]
H A DRESET_REG.ml37 % | |------|l2 %
62 ?l1 l2 l3. ONE l1 /\
63 MUX(reset,l1,in,l2) /\
64 REG(l2,l3) /\
65 MUX(reset,l2,l3,out)");;
/seL4-l4v-10.1.1/HOL4/examples/countable/
H A DcountableScript.sml9 ``���l1 l2 f f'. (l1 = l2) ��� (���x. MEM x l2 ��� (f x = f' x)) ��� (count_list_aux f l1 = count_list_aux f' l2)``,
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DSALScript.sml93 (Reduce (l1, ASG l1 v w l2, l2) (w,v)) (* inst *) /\
94 (Reduce (l1, S1, l2) (v,v) /\ (* nop *)
95 Reduce (l2, S2, l3) value ==> Reduce (l1, S1 |++| S2, l3) value) /\
96 (Reduce (l1, S1, l2) e1 /\ (* skip *)
97 Reduce (l3, S2, l4) e2 ==> Reduce (l1, S1 |++| S2, l2) e1) /\
98 (Reduce (l1, S1, l2) (e,v) /\ (* seq *)
99 Reduce (l2, S2, l3) (f v, w) ==> Reduce (l1, S1 |++| S2, l3)
102 Reduce (l1, IFGOTO l1 c l2 l3, l2) (
[all...]
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl-transformations/
H A Dltl_translationsScript.sml15 (LOGIC_TO_TEMPORAL_DEEP (F_CONJ l1 l2) = (LTL_AND (LOGIC_TO_TEMPORAL_DEEP l1, LOGIC_TO_TEMPORAL_DEEP l2))) /\
18 (LOGIC_TO_TEMPORAL_DEEP (F_U l1 l2) = (LTL_SUNTIL (LOGIC_TO_TEMPORAL_DEEP l1, LOGIC_TO_TEMPORAL_DEEP l2)))`;
75 (TEMPORAL_DEEP_TO_LOGIC (LTL_AND (l1, l2)) = (F_CONJ (TEMPORAL_DEEP_TO_LOGIC l1) (TEMPORAL_DEEP_TO_LOGIC l2))) /\
79 (TEMPORAL_DEEP_TO_LOGIC (LTL_SUNTIL (l1, l2)) = (F_U (TEMPORAL_DEEP_TO_LOGIC l1) (TEMPORAL_DEEP_TO_LOGIC l2)))`;
150 (TEMPORAL_DEEP_TO_TEMPORAL (LTL_AND (l1, l2)) w =
152 (TEMPORAL_DEEP_TO_TEMPORAL l2
[all...]
/seL4-l4v-10.1.1/HOL4/src/ring/src/
H A DcanonicalScript.sml52 (canonical_sum_merge (Cons_monom c1 l1 t1) (Cons_monom c2 l2 t2) =
53 compare (list_compare index_compare l1 l2)
54 (Cons_monom c1 l1 (canonical_sum_merge t1 (Cons_monom c2 l2 t2)))
56 (Cons_monom c2 l2 (canonical_sum_merge (Cons_monom c1 l1 t1) t2)))
57 /\ (canonical_sum_merge (Cons_monom c1 l1 t1) (Cons_varlist l2 t2) =
58 compare (list_compare index_compare l1 l2)
59 (Cons_monom c1 l1 (canonical_sum_merge t1 (Cons_varlist l2 t2)))
61 (Cons_varlist l2 (canonical_sum_merge (Cons_monom c1 l1 t1) t2)))
62 /\ (canonical_sum_merge (Cons_varlist l1 t1) (Cons_monom c2 l2 t2) =
63 compare (list_compare index_compare l1 l2)
[all...]
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttNumber.sml67 fun prefix l1 l2 = case (l1,l2) of
75 fun replace_at (l1,lrep) l2 = case l2 of
79 let val r = prefix l1 l2 in lrep @ r end
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/MISC/
H A Dmk_COUNT.ml35 "COUNT_IMP (sw,i,o) = ?l1 l2.
36 MUX (sw,i,l2,l1) /\
38 INCR (o,l2)");;

Completed in 188 milliseconds

1234567891011>>