Searched refs:mult (Results 1 - 25 of 43) sorted by relevance

12

/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Dlocvarfncall.c9 int mult(int x, int y) function
20 r = mult(f(7), g(7));
26 return mult(f(i),g(i+1));
31 int x = mult(f(i), g(i+1));
H A Dfncall.c9 int mult(int x, int y) function
24 total = mult(factor, total);
/seL4-l4v-master/HOL4/examples/elliptic/
H A DgroupScript.sml471 mult : 'a -> 'a -> 'a |>`;
477 (!x y :: (g.carrier). g.mult x y IN g.carrier) /\
479 (!x :: (g.carrier). g.mult g.id x = x) /\
480 (!x :: (g.carrier). g.mult (g.inv x) x = g.id) /\
481 (!x y z :: (g.carrier). g.mult (g.mult x y) z = g.mult x (g.mult y z)) }`;
485 (group_exp G g (SUC n) = G.mult g (group_exp G g n))`;
490 g IN Group /\ !x y :: (g.carrier). g.mult
[all...]
H A DgroupTools.sml61 key = ``g.mult x y``,
H A DfieldScript.sml167 val field_add_def = Define `field_add (f : 'a field) = f.sum.mult`;
172 val field_mult_def = Define `field_mult (f : 'a field) = f.prod.mult`;
769 >> (Suff `f.prod.mult x f.prod.id IN f.prod.carrier`
773 ++ Suff `f.prod.mult x (f.sum.inv f.prod.id) IN f.prod.carrier`
833 ++ Suff `f.prod.mult x y IN f.prod.carrier`
916 ++ Suff `f.prod.mult x y IN f.prod.carrier`
2456 mult := (\x y. if x = zero_elt then y
2462 mult := (\x y. if x = zero_elt then zero_elt
H A DfieldTools.sml736 val _ = not (is_field_mult a) orelse raise Bug "a is a mult"
737 and _ = not (is_field_mult b) orelse raise Bug "b is a mult"
804 NONE => raise Bug "a not a mult"
809 NONE => raise Bug "b not a mult"
/seL4-l4v-master/HOL4/src/ring/src/
H A DnumRingScript.sml36 val _ = temp_overload_on("mult",���$* : num->num->num���);
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dhol_defaxioms_proofsScript.sml135 [acl2_numberp (add x y); acl2_numberp (mult x y);
143 [acl2_numberp (add x y); acl2_numberp (mult x y);
232 |- |= equal (mult (mult x y) z) (mult x (mult y z)),
238 ``|= equal (mult (mult x y) z) (mult x (mult
[all...]
H A DtranslateScript.sml936 val INTEGERP_MULT = store_thm("INTEGERP_MULT",``!a b. (|= integerp a) /\ (|= integerp b) ==> |= integerp (mult a b)``,
962 val INT_MULT = store_thm("INT_MULT",``!a b. int (a * b) = mult (int a) (int b)``,
1025 ``!a b. nat (a * b) = mult (nat a) (nat b)``,
1052 val RATIONALP_MULT = store_thm("RATIONALP_MULT",``!a b. (|= rationalp a) /\ (|= rationalp b) ==> |= rationalp (mult a b)``,
1069 val RAT_MULT = store_thm("RAT_MULT",``!a b. rat (a * b) = mult (rat a) (rat b)``,
1079 ``!a b. ~(b = 0) ==> (rat (a / b) = mult (rat a) (reciprocal (rat b)))``,
1102 val ACL2_NUMBERP_MULT = store_thm("ACL2_NUMBERP_MULT",``!a b. |= acl2_numberp (mult a b)``,
1113 val COM_MULT = store_thm("COM_MULT",``!a b. num (a * b) = mult (num a) (num b)``,RW_TAC std_ss [mult_def]);
1122 val COM_DIV = store_thm("COM_DIV",``!a b. ~(b = com_0) ==> (num (a / b) = mult (num a) (reciprocal (num b)))``,
1312 ``!a b. (|= natp a) /\ (|= natp b) ==> |= natp (mult
[all...]
H A Dhol_defaxiomsScript.sml2015 (let q = mult i (reciprocal j) in
2030 (let q = mult i (reciprocal j) in
2043 (let q = mult i (reciprocal j) in
2055 (let q = mult i (reciprocal j) in
2064 (integerp (mult fl (reciprocal (nat 2))),fl)]
2071 (integerp (mult cl (reciprocal (nat 2))),cl)]
2077 |- mod x y = add x (unary_minus (mult (floor x y) y)),
2083 `mod x y = add x (unary_minus (mult (floor x y) y))`;
2088 |- x rem y = add x (unary_minus (mult (truncate x y) y)),
2093 |- evenp x = integerp (mult
[all...]
H A DextendTranslateScript.sml70 then (mult (reciprocal r) (acl2_expt r (add i (int 1))))
71 else (mult r (acl2_expt r (add i (unary_minus (int 1)))))))
171 let q = mult a (reciprocal b) in
183 let q = mult a (reciprocal b) in
400 (numerator (mult (int a) (reciprocal (int b))) =
402 (denominator (mult (int a) (reciprocal (int b))) =
598 `acl2_mod x y = add x (unary_minus (mult (acl2_floor x y) y))`;
601 `acl2_rem x y = add x (unary_minus (mult (acl2_truncate x y) y))`;
838 `acl2_evenp x = integerp (mult x (reciprocal (int 2)))`;
908 `acl2_ash i c = acl2_floor (mult (ifi
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/test/
H A Drefined_format.sml178 mult(x:word32,y) =
188 |- mult (x,y) =
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DSolve_ineqs.sml157 val mult = lcm (coeff1,coeff2) value
158 val mult1 = mult div coeff1
159 and mult2 = mult div coeff2
H A DGen_arith.sml128 val _ = Int.>(length ms, 1) orelse failwith "not a mult"
/seL4-l4v-master/HOL4/examples/dev/AES/tupled/
H A DRoundOpScript.sml383 val [mult] = decls "**"; value
418 THEN RESTR_EVAL_TAC [mult,B_HEX,D_HEX,E_HEX,TWO,THREE,NINE]
/seL4-l4v-master/HOL4/examples/dev/AES/word8/
H A DRoundOpScript.sml379 val mult = Term `Mult$**`; value
409 THEN RESTR_EVAL_TAC [mult,n2w]
/seL4-l4v-master/HOL4/examples/Crypto/AES/
H A DRoundOpScript.sml376 val mult = Term `Mult$**`; value
406 THEN RESTR_EVAL_TAC [mult,n2w]
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A Dhol_defaxiomsScript.sml2030 (let q = mult i (reciprocal j) in
2045 (let q = mult i (reciprocal j) in
2060 (let q = mult i (reciprocal j) in
2073 (let q = mult i (reciprocal j) in
2085 (let q = mult i (reciprocal j) in
2094 (integerp (mult fl (reciprocal (nat 2))),fl)]
2101 (integerp (mult cl (reciprocal (nat 2))),cl)]
2107 |- mod x y = add x (unary_minus (mult (floor x y) y)),
2113 `mod x y = add x (unary_minus (mult (floor x y) y))`;
2118 `mod x y = add x (unary_minus (mult (floo
[all...]
/seL4-l4v-master/HOL4/examples/dev/AES/curried/
H A DRoundOpScript.sml408 val [mult] = decls "**"; value
443 THEN RESTR_EVAL_TAC [mult,B_HEX,D_HEX,E_HEX,TWO,THREE,NINE]
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dhol_defaxiomsScript.sml2019 (let q = mult i (reciprocal j) in
2034 (let q = mult i (reciprocal j) in
2047 (let q = mult i (reciprocal j) in
2059 (let q = mult i (reciprocal j) in
2068 (integerp (mult fl (reciprocal (nat 2))),fl)]
2075 (integerp (mult cl (reciprocal (nat 2))),cl)]
2081 |- mod x y = add x (unary_minus (mult (floor x y) y)),
2087 `mod x y = add x (unary_minus (mult (floor x y) y))`;
2092 |- x rem y = add x (unary_minus (mult (truncate x y) y)),
2097 |- evenp x = integerp (mult
[all...]
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Drealconv.cpp865 mult
1009 b1 = mult(b, p5);
1019 p51 = p5->next = mult(p5,p5);
1024 p51 = p5->next = mult(p5,p5);
3124 bb1 = mult(bs, bb);
4196 b1 = mult(mhi, b);
/seL4-l4v-master/HOL4/src/AI/
H A DaiLib.sml625 let val mult = pow 10.0 n in value
626 Real.fromInt (Real.round (r * mult)) / mult
/seL4-l4v-master/graph-refine/
H A Dstack_logic.py125 for (x, mult) in vs:
130 new_vs[v] += var[v] * mult
131 const += c * mult
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffExtendScript.sml517 The GF(2) is simple: add x y = (x + y) MOD 2, mult x y = (x * y) MOD 2,
547 mult x y = if (x == 0) then 0 else if (y == 0) then 0 else 1 + (((x - 1) + (y - 1)) MOD 3)
551 GF(4).mult x y = GF(2).mult x y
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleDiophSynt.sml57 then raise ERR "apply_move_poly" "mult"

Completed in 361 milliseconds

12