Searched refs:exp (Results 176 - 200 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DpreARMScript.sml178 read (regs,mem) (exp:EXP) =
179 case exp of
202 write (regs,mem) (exp:EXP) (v:DATA)=
203 case exp of
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DpreARMScript.sml174 read (regs,mem) (exp:EXP) =
175 case exp of
197 write (regs,mem) (exp:EXP) (v:DATA)=
198 case exp of
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dtutorial.ml39 [(``($**):num -> num -> num``,"exp")]
44 (* |- exp m arg = *)
55 (* val propagation_exp = |- nat (m ** arg) = exp (nat m) (nat arg) : thm *)
H A DtestACL2encoding.ml217 translate_simple_function [(``($**):num -> num -> num``,"exp")],
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DModel.sml363 and expName = Name.fromString "exp"
399 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
486 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DModel.sml363 and expName = Name.fromString "exp"
399 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
486 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
/seL4-l4v-master/HOL4/examples/algebra/monoid/
H A DmonoidOrderScript.sml128 ((Invertibles g).exp = $** )
1025 ((Invertibles g).exp = g.exp)``,
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffPolyScript.sml102 pfexp = (PolyRing (PF r)).prod.exp
1592 val _ = overload_on("pfexp", ``(PolyRing (PF r)).prod.exp``);
1602 ((PF r).prod.exp = $** ): thm
2545 and (PF r).prod.exp = $** by PF_property
2557 and (PF r).prod.exp = $** by PF_property
2770 Hence s.exp x (CARD B) = x by finite_field_fermat_thm
2781 Hence s.exp x (CARD B ** n) = x by finite_field_fermat_all
H A DffMasterScript.sml410 <=> s.prod.exp x n = x by poly_master_root
586 = (PolyModRing r p).prod.exp (X % p) (CARD (PolyModRing r p).carrier) by finite_field_fermat_thm
600 `X % p = (PolyModRing r p).prod.exp (X % p) (CARD (PolyModRing r p).carrier)` by rw[finite_field_fermat_thm] >>
618 <=> (PolyModRing r p).prod.exp x n = x by poly_master_root
619 <=> (PolyModRing r p).prod.exp (x % p) n = (x % p) by above
632 `!n. (PolyModRing r p).prod.exp (x % p) n = (x ** n) % p` by rw[poly_mod_field_exp] >>
3207 Thus g.exp x n IN G by group_exp_element
3208 g.exp x n
3209 = f*.exp x n by subgroup_exp
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyFieldModuloScript.sml4162 case OLEAST k. 0 < k /\ (((PolyModRing r z).prod excluding |0|).exp p k = |1|) of ... =
4163 case OLEAST k. 0 < k /\ (((PolyModRing r z).prod excluding |0|).exp (p % z) k = |1| of ...
4166 !k. ((PolyModRing r z).prod excluding |0|).exp p k = (p ** k) % z by poly_mod_exp_alt
4167 !k. ((PolyModRing r z).prod excluding |0|).exp (p % z) k = ((p % z) ** k) % z by poly_mod_exp_alt
4191 Hence ((PolyModRing r z).prod excluding |0|).exp (p % z) k
4212 `((PolyModRing r z).prod excluding |0|).exp (p % z) k = ((p % z) ** k) % z` by rw[poly_mod_exp_alt] >>
4310 Therefore !n. ((PolyModRing r z).prod excluding |0|).exp X n = (X ** n) % z by poly_mod_exp_alt
4312 Thus ((PolyModRing r z).prod excluding |0|).exp X m
4313 = ((PolyModRing r z).prod excluding |0|).exp X n by above
4336 `!n. ((PolyModRing r z).prod excluding |0|).exp
[all...]
H A DpolyMonicScript.sml59 ### = (poly_ring r).sum.exp |1|
60 |n| = (poly_ring r).sum.exp |1| n = ###n
61 |c| = (poly_ring r).sum.exp |1| c = ###c
682 val _ = overload_on ("##", ``r.sum.exp #1``);
683 val _ = overload_on ("###", ``(poly_ring r).sum.exp |1|``);
719 = (PolyRing r).sum.exp |1| 0 by notation
/seL4-l4v-master/graph-refine/
H A Dlogic.py1565 def inst_eq_at_visit (exp, vis):
1566 if not exp.is_op ('EqSelectiveWrapper'):
1568 [_, xs, ys] = exp.vals
H A Drep_graph.py222 for (exp, visit) in self.vals:
223 exp.serialise (ss)
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dmore_setScript.sml38 (* For errors try <exp> handle e => Raise e;
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleDiophSynt.sml487 writel "dioph_graph" ("gen exp sol" :: map graph_to_string graph);
H A DmleCombinSynt.sml525 writel "combin_graph" ("gen exp sol" :: map graph_to_string graph);
/seL4-l4v-master/HOL4/src/AI/proof_search/
H A DpsMCTS.sml142 (Math.pow (x, alpha - 1.0) * Math.exp (~ x)) / gamma_of alpha
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dlisp_finalScript.sml514 val th = SPEC_BOOL_FRAME_RULE th ``R_ev (s,FEMPTY) s2 /\ (exp = term2sexp s)``
519 lisp_eval (exp,Sym "nil",Sym "nil",Sym "nil",Sym "nil",Sym "nil",l) =
/seL4-l4v-master/HOL4/examples/PSL/regexp/
H A DmatcherScript.sml1186 ``!exp : 'a regexp. ?dfa : (num->bool,'a) da. sem exp = da_accepts dfa``,
/seL4-l4v-master/HOL4/examples/bootstrap/
H A DautomationLib.sml131 (���:exp���,���exp���),
/seL4-l4v-master/HOL4/src/parse/
H A Dselftest.sml638 fun ptpp msg exp t = tpp msg exp lfcop_g t
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dheapsizing.cpp560 pagingCost = PAGINGCOSTFACTOR * exp(factor);
/seL4-l4v-master/HOL4/polyml/
H A Dconfigure9248 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' >conftest.exp
9250 if test ! -s conftest.er2 || diff conftest.exp conftest.er2 >/dev/null; then
9396 lt_prog_compiler_static='-bnso -bI:/lib/syscalls.exp'
9656 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' >conftest.exp
9658 if test ! -s conftest.er2 || diff conftest.exp conftest.er2 >/dev/null; then
9709 $ECHO "$_lt_linker_boilerplate" | $SED '/^$/d' > conftest.exp
9711 if diff conftest.exp conftest.er2 >/dev/null; then
9767 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' > out/conftest.exp
9769 if test ! -s out/conftest.er2 || diff out/conftest.exp out/conftest.er2 >/dev/null; then
9822 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' > out/conftest.exp
[all...]
/seL4-l4v-master/HOL4/examples/fermat/little/
H A DFLTactionScript.sml74 Zadd_exp |- !n. 0 < n ==> !x m. (Zadd n).exp x m = (x * m) MOD n
193 (* |- !n. 0 < n ==> !x m. (Zadd n).exp x m = (x * m) MOD n *)
/seL4-l4v-master/HOL4/src/probability/
H A DextrealScript.sml313 `(extreal_exp (Normal x) = Normal (exp x)) /\
342 val _ = overload_on ("exp", Term `extreal_exp`);
2461 !x :extreal. 0 <= exp x
2475 !r. exp (Normal r) = Normal (exp r)
2489 exp 0 = (1 :extreal)
2542 ("EXP_LE_X_FULL", ``!x :real. &1 + x <= exp x``,
2552 >> Q.ABBREV_TAC `f = \x :real. exp x - (1 + x)`
2553 >> `exp x - (1 + x) = f x` by METIS_TAC [] >> POP_ORW
2554 >> Q.ABBREV_TAC `g = \x :real. exp
[all...]

Completed in 454 milliseconds

12345678910