Searched refs:i2 (Results 1 - 25 of 105) sorted by relevance

12345

/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/errors/
H A Daddrlocal.c11 void swap(int *i1, int *i2) argument
15 *i1 = *i2;
16 *i2 = tmp;
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/
H A Dmux.ml4 (`NAND_SPEC`, "!i1 i2 o. NAND_SPEC(i1,i2,o) = o = ~(i1 /\ i2)");;
10 (`MUX_SPEC`, "!c i1 i2 o. MUX_SPEC(c,i1,i2,o) = o = (c => i1 | i2)");;
14 "!c i1 i2 o.
15 MUX_IMP(c,i1,i2,o) =
18 NAND_SPEC(l1,i2,l2) /\
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/MISC/
H A Dmyfun.ml8 |- !i1 i2 m n t.
9 MULT_FUN((i1,i2),m,n,t) =
12 MULT_FUN((i1,i2),((i1=0)=>m|i2+m),n-1,((((n-1)-1)=0) \/ (i2=0))))
20 "!i1 i2 m n.
21 MULT_FUN((i1,i2),m,n,T) = (m,n,T)",
29 "!i1 i2 m n.
30 MULT_FUN((i1,i2),m,n,F) =
31 MULT_FUN((i1,i2),((i
[all...]
H A Dmk_COUNT.ml23 "MUX(switch,i1:^sig,i2:^sig,o:^sig) = (o = (switch -> i1 | i2))");;
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/
H A Dgates.ml19 let nand = new_definition (`nand`,"nand (i1,i2) = ~(i1 /\ i2)");;
20 let and = new_definition (`and`,"and (i1,i2) = (i1 /\ i2)");;
21 let xor = new_definition (`xor`,"xor (i1,i2) = (i1 /\ ~i2) \/ (~i1 /\ i2)");;
35 "NAND_IMP (i1:^wire,i2:^wire,o:^wire) =
39 Ptran (i2,w1,w3) /\
43 Ntran (i2,w
[all...]
H A Dmuxn.ml18 let mux = new_definition (`mux`,"mux (cntl,i1:*,i2:*) = cntl => i1 | i2");;
22 "CMUX_IMP (cntl:^wire,cntlbar:^wire,i1:^wire,i2:^wire,o:^wire) =
29 Ptran (cntl,i2,w5) /\
30 Ntran (cntlbar,i2,w6)");;
34 "CMUXn_IMP n (cntl:^wire,cntlbar:^wire,i1:^bus,i2:^bus,o:^bus) =
37 (cntl,cntlbar,DEST_BUS i1 m,DEST_BUS i2 m,DEST_BUS o m)");;
41 "MUXn_IMP n (cntl:^wire,i1:^bus,i2:^bus,o:^bus) =
43 INV_IMP (cntl,cntlbar) /\ CMUXn_IMP n (cntl,cntlbar,i1,i2,o)");;
77 "!cntl cntlbar i1 i2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/bmark/
H A DBmark.sml241 def = --`(MULT_FUN_CURRY 0 i1 i2 m t =
242 (if t then (m,0,t) else (if i1=0 then m else i2+m,0,T)))
244 (MULT_FUN_CURRY (SUC n) i1 i2 m t =
246 else MULT_FUN_CURRY n i1 i2 (if i1=0 then m else i2+m)
247 (((n-1)=0) \/ (i2=0))))`--};
257 * --`!i1 i2 m n t.
258 * MULT_FUN_CURRY n i1 i2 m t =
260 * else MULT_FUN_CURRY (n-1) i1 i2 (if i1=0 then m else i2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/
H A DmatcherScript.sml535 let (i2,t2,a2) = regexp2na r2 in
536 (i1 + i2 + 1,
538 if s <= i2 then t2 s x s'
539 else if s' <= i2 then a1 (s - (i2 + 1)) /\ t2 i2 x s'
540 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))),
541 \s. if s <= i2 then a2 s else a2 i2 /\ a
[all...]
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DOrdered.sml14 fun compare ((i1,j1),(i2,j2)) =
15 case Int.compare (i1,i2) of
H A DNameArity.sml34 fun compare ((n1,i1),(n2,i2)) =
37 | EQUAL => Int.compare (i1,i2)
40 fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2;
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DOrdered.sml14 fun compare ((i1,j1),(i2,j2)) =
15 case Int.compare (i1,i2) of
H A DNameArity.sml34 fun compare ((n1,i1),(n2,i2)) =
37 | EQUAL => Int.compare (i1,i2)
40 fun equal (n1,i1) (n2,i2) = i1 = i2 andalso Name.equal n1 n2;
/seL4-l4v-10.1.1/HOL4/src/ring/src/
H A DquoteScript.sml32 ���!i1 i2. (index_compare i1 i2 = EQUAL) = (i1 = i2)���,
42 val index_lt_def = Define ` index_lt i1 i2 = (index_compare i1 i2 = LESS) `;
/seL4-l4v-10.1.1/isabelle/lib/browser/GraphBrowser/
H A DGraphBrowserFrame.java19 MenuItem i1, i2; field in class:GraphBrowserFrame
25 i2.setEnabled(false);
28 i2.setEnabled(true);
109 m1.add(i2 = new MenuItem("Export to EPS"));
112 i2.addActionListener(this);
/seL4-l4v-10.1.1/l4v/isabelle/lib/browser/GraphBrowser/
H A DGraphBrowserFrame.java19 MenuItem i1, i2; field in class:GraphBrowserFrame
25 i2.setEnabled(false);
28 i2.setEnabled(true);
109 m1.add(i2 = new MenuItem("Export to EPS"));
112 i2.addActionListener(this);
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/cmos/
H A Dmk_XOR.ml30 i2-- | --- | ---------------------| |---o
70 i2---| | | ------- | -- |
157 "BAD_XOR(i1,i2,o) =
161 PTRAN(i2,i1,o) /\ NTRAN(i2,o,p3)");;
170 "GOOD_XOR(i1,i2,o) =
174 PTRAN(i2,i1,o) /\ NTRAN(i2,o,p3) /\
175 PTRAN(i1,i2,o) /\ NTRAN(p3,i2,
[all...]
H A Dmk_cmos.ml141 "!i1:^sig. !i2:^sig. !o:^sig.
142 J(i1,i2,o) = !t. o t = (i1 t) U1 (i2 t)");;
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DRationals.sml74 fun rat_plus (rat (i1,j1)) (rat (i2,j2)) =
78 val (i,j) = ((i1 * d2) + (i2 * d1),(j1 * d2))
82 fun rat_minus (rat (i1,j1)) (rat (i2,j2)) =
86 val (i,j) = ((i1 * d2) - (i2 * d1),(j1 * d2))
90 fun rat_mult (rat (i1,j1)) (rat (i2,j2)) =
91 if ((i1 = zero) orelse (i2 = zero))
94 and h = gcd (abs i2,j1)
95 val i = (i1 div g) * (i2 div h)
100 fun rat_div (rat (i1,j1)) (rat (i2,j2)) =
101 if (i2
[all...]
/seL4-l4v-10.1.1/HOL4/tools/cmp/
H A Dcmp.sml22 val i2 = BinIO.inputN(is2, 1024) value
25 if i1 = i2 then
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_icacheScript.sml13 X86_ICACHE ((r,e,s,m,i):x86_state) ((r2,e2,s2,m2,i2):x86_state) =
16 (i2 = \addr. if addr IN insert then m addr else
43 THEN `?r2 e2 t2 m2 i2. t = (r2,e2,t2,m2,i2)` by METIS_TAC [PAIR]
52 ``X86_ICACHE (r,e,s,m,i) (r2,e2,s2,m2,i2) =
54 (r2,e2,s2,m2,i2) = (r,e,s,m,icache update m i)``,
83 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dx64_icacheScript.sml13 X64_ICACHE ((r,e,s,m,i):x64_state) ((r2,e2,s2,m2,i2):x64_state) =
16 (i2 = \addr. if addr IN insert then m addr else
43 THEN `?r2 e2 t2 m2 i2. t = (r2,e2,t2,m2,i2)` by METIS_TAC [PAIR]
52 ``X64_ICACHE (r,e,s,m,i) (r2,e2,s2,m2,i2) =
54 (r2,e2,s2,m2,i2) = (r,e,s,m,icache update m i)``,
83 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR]
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A Dselftest.sml14 fun m10cmp (i1,i2) = Int.compare(i1 mod 10, i2 mod 10)
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dsymbolic_semi_automatonScript.sml115 `(IS_TRANSITION A s1 i1 s2 i2 =
116 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 s1, INPUT_RUN_STATE_UNION A i2 s2))`;
154 (!s1 i1 i2. EXISTS_AT_MOST_ONE s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`;
161 (!s1 i1 i2. ?s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))`;
175 (!s1 i1 i2. ?!s2. ((s2 SUBSET A.S) /\ IS_TRANSITION A s1 i1 s2 i2))``,
351 ``!A. IS_TOTAL_SYMBOLIC_SEMI_AUTOMATON A ==> ?R_FUNC. !s1 s2 i1 i2. (R_FUNC s1 i1 i2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A DARM_prover_toolsLib.sml90 val (rcs, i2) = dest_comb rcst
93 val (thm, _) = prove_it comp i1 i2 unt simp
173 COMB (rcs, i2)
177 COMB (rel, comp) => if ((i2 = ``mode_mix:(arm_state->bool)``) andalso ((unt = ``priv_mode_constraints_v2a``) andalso (sim=``priv_mode_similar``)))
193 COMB (rcs, i2)
197 COMB (rel, comp) => if (i2 = ``little_mode_mix:(arm_state->bool)``)
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DKernelSig.sml24 fun id_compare(i1, i2) =
25 case (!i1, !i2) of ((n1,_), (n2,_)) =>
26 if i1 = i2 then EQUAL else name_compare(n1,n2)

Completed in 413 milliseconds

12345