Searched refs:g2 (Results 1 - 25 of 75) sorted by relevance

123

/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A Dclosure.sml13 let g2 x = x + 2 in
14 (twice(g1,z),twice(g2,z))`;
29 val g2'_def = Define `
30 g2' x = x + 2`;
36 G2 -> g2' i
45 let g2:clos = G2 in
46 (twice1(g1,z),twice1(g2,z))`;
57 twice_def, dispatch_def,g1'_def, g2'_def]
H A Dgr_t.sml207 val (r,g2) = gfoldn (f c) g1
208 in (d (l,r),g2) end
212 val (y,g2) = gfoldn l g1
213 in (b (x,y),g2) end
283 val (r,g2) = gfoldn (f c) g1
284 in (d (l,r),g2) end
288 val (y,g2) = gfoldn l g1
289 in (b (x,y),g2) end
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A Dclosure.sml13 let g2 x = x + 2 in
14 (twice(g1,z),twice(g2,z))`;
29 val g2'_def = Define `
30 g2' x = x + 2`;
36 G2 -> g2' i
45 let g2:clos = G2 in
46 (twice1(g1,z),twice1(g2,z))`;
57 RW_TAC std_ss [g1'_def, g2'_def]
H A Dgr_t.sml207 val (r,g2) = gfoldn (f c) g1
208 in (d (l,r),g2) end
212 val (y,g2) = gfoldn l g1
213 in (b (x,y),g2) end
283 val (r,g2) = gfoldn (f c) g1
284 in (d (l,r),g2) end
288 val (y,g2) = gfoldn l g1
289 in (b (x,y),g2) end
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A Dclosure.sml13 let g2 x = x + 2 in
14 (twice(g1,z),twice(g2,z))`;
29 val g2'_def = Define `
30 g2' x = x + 2`;
36 G2 -> g2' i
45 let g2:clos = G2 in
46 (twice1(g1,z),twice1(g2,z))`;
57 RW_TAC std_ss [g1'_def, g2'_def]
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Dmultidim_arrays.c31 int g2(struct s* sptr, int i, int j) function
43 return g2(&global2, i, j);
H A Djiraver439.c26 unsigned g2(void) function
H A Dautomatic_modifies.c28 void g2(int j) function
/seL4-l4v-10.1.1/HOL4/examples/miller/groups/
H A Dabelian_groupScript.sml138 !g1 g2 :: gset G. ?h :: gset G. gord G h = lcm (gord G g1) (gord G g2)``,
141 `!g. !g1 g2 :: gset G.
142 (gcd (gord G g1) (gord G g2) = g) ==>
143 ?h :: gset G. gord G h = lcm (gord G g1) (gord G g2)`
145 ++ Q.PAT_X_ASSUM `!g. P g` (MP_TAC o Q.SPEC `gcd (gord G g1) (gord G g2)`)
151 ++ Q_RESQ_EXISTS_TAC `gop G g1 g2`
155 ++ MP_TAC (Q.SPECL [`gord G g1`, `gord G g2`] FACTOR_GCD)
161 ++ Know `p * gord G (gpow G g2 p) = gord G g2`
[all...]
H A DgroupScript.sml260 ``!G H g1 g2 h1 h2.
261 gop (prod_group G H) (g1, h1) (g2, h2) = (gop G g1 g2, gop H h1 h2)``,
504 ``!G :: group. !H :: subgroup G. !g1 g2 :: gset G.
505 (lcoset G g1 H = lcoset G g2 H)
506 \/ DISJOINT (lcoset G g1 H) (lcoset G g2 H)``,
510 /\ g IN lcoset G g2 H`)
517 ++ Suff `!v. v IN lcoset G g1 H = v IN lcoset G g2 H`
522 ++ Q.SPEC_TAC (`g2`, `g2`)
[all...]
/seL4-l4v-10.1.1/HOL4/examples/generic_finite_graphs/
H A DgfgScript.sml79 `wfg g ��� (addEdge i (e,s) g = SOME g2) ==> wfg g2`,
96 `(addEdge i (e,s) g) = SOME g2 ==> (g.nodeInfo = g2.nodeInfo)`,
102 `wfg g ��� (updateNode id n g = SOME g2) ==> wfg g2`,
111 `updateNode id n g = SOME g2
112 ==> (g.followers = g2.followers)
113 ��� (g.preds = g2.preds)`,
120 `updateNode id n g = SOME g2
[all...]
/seL4-l4v-10.1.1/HOL4/src/tfl/examples/
H A DctlScript.sml144 /\ (ACTLSTAR_PATH (g1 \/ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)
145 /\ (ACTLSTAR_PATH (g1 /\ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)
149 /\ (ACTLSTAR_PATH (g1 U g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)
150 /\ (ACTLSTAR_PATH (g1 R g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)`;
259 /\ (PATHSAT (M,PI) (g1 \/ g2) = PATHSAT (M,PI) g1 \/ PATHSAT (M,PI) g2)
[all...]
/seL4-l4v-10.1.1/HOL4/src/tfl/src/test/
H A Dpattern_matchingScript.sml61 val _ = def "g2"
62 `(g2 ([]:'a list, CONS a (CONS b x)) = 1) /\
63 (g2 (CONS a (CONS b x), y) = 2) /\
64 (g2 (z, CONS a y) = 3)`;
/seL4-l4v-10.1.1/HOL4/src/new-datatype/
H A DNDDB.sml109 prove(``!f1 g1 f2 g2.
110 ((sum_retrieve g1 g2)o h) o ((sum_map f1 f2)o h) =
111 ((sum_retrieve (g1 o f1) (g2 o f2)) o h)``
119 val sum_inj_pair_thm = prove(``!f1 g1 f2 g2.
121 (inj_pair f2 g2) ==>
122 (inj_pair (sum_map f1 f2) (sum_retrieve g1 g2))``,
130 val sum_retrieve_map_thm = prove(``!f1 g1 f2 g2.
131 (sum_retrieve g1 g2) o (sum_map f1 f2) =
132 (sum_retrieve (g1 o f1) (g2 o f2))
178 val prod_inj_pair_thm = prove(``!f1 g1 f2 g2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A Dencap1.lisp56 ; Definition. g2 = some g2 . (integerp (mv-nth 0 (g2 x)))
57 ; |- forall x . |= (integerp (mv-nth 0 (g2 x)))
59 ((g2 (x) (mv t t)))
60 (local (defun g2 (x)
63 (defthm integerp-first-g2
64 (integerp (mv-nth 0 (g2 x)))))
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/encap/
H A Dexample.lisp54 ; Definition. g2 = some g2 . (integerp (mv-nth 0 (g2 x)))
55 ; |- forall x . |= (integerp (mv-nth 0 (g2 x)))
57 ((g2 (x) (mv t t)))
58 (local (defun g2 (x)
61 (defthm integerp-first-g2
62 (integerp (mv-nth 0 (g2 x)))))
/seL4-l4v-10.1.1/l4v/proof/infoflow/tools/
H A Dauthority2infoflow-CaML.ml268 let g2=[("T",ASyncSend,"AEP1");("T",ASyncSend,"AEP2");("CTR",Receive,"AEP1");("CTR",Read,"C");("CTR",Write,"C");
276 map (fun l -> subjectReads g2 l) (nodes g2);;
277 map (fun l-> subjectAffects g2 l) (nodes g2);;
288 nodes g2;;
290 map (fun l -> subjectReads g2 l) (nodes g2);;
291 map (fun l-> subjectAffects g2 l) (nodes g2);;
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dgraph_display.scala53 (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dgraph_display.scala53 (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/
H A Dconcrltl2waaScript.sml541 >> qabbrev_tac `g2 = (��ls2 e1 sofar.
546 >- (`MEM y (FOLDR (g2 (trans_concr f)) [] (trans_concr f'))` by (
547 qunabbrev_tac `g1` >> qunabbrev_tac `g2` >> fs[]
549 >> `!ls1 ls2. (MEM y (FOLDR (g2 ls2) [] ls1)) ==>
556 >> qunabbrev_tac `g2` >> qunabbrev_tac `g1` >> fs[MEM_MAP]
627 (FOLDR (��e1 sofar. g2 ls2 e1 sofar) [] ls1)` by (
629 >> qunabbrev_tac `g1` >> qunabbrev_tac `g2`
666 (FOLDR (��e1 sofar. g2 ls2 e1 sofar) [] ls1)` by (
668 >> qunabbrev_tac `g1` >> qunabbrev_tac `g2`
750 in let g2
[all...]
H A DconcrRepScript.sml771 ``!g1 g2.
772 set (graphStatesWithId g1) = set (graphStatesWithId g2)
773 ==> (set (graphStates g1) = set (graphStates g2))``,
776 >- (`MEM (q,r.frml) (graphStatesWithId g2)`
970 ``!g g2. (g.followers = g2.followers)
971 ��� (domain g.nodeInfo = domain g2.nodeInfo)
973 = first_flw_has_max_counter g2)``,
1092 ``!g g2 f. (wfg g ��� unique_node_formula g ��� (addFrmlToGraph g f = g2))
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/
H A Dafp.scala57 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
58 try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/
H A Dafp.scala57 (g1 /: session_entries.get(s).filterNot(_ == e1)) { case (g2, e2) =>
58 try { g2.default_node(e2, ()).add_edge_acyclic(e2, e1) }
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/
H A Dgr_t.sml207 val (r,g2) = gfoldn (f c) g1
208 in (d (l,r),g2) end
212 val (y,g2) = gfoldn l g1
213 in (b (x,y),g2) end
283 val (r,g2) = gfoldn (f c) g1
284 in (d (l,r),g2) end
288 val (y,g2) = gfoldn l g1
289 in (b (x,y),g2) end
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/
H A Dcomputer_imp.ml106 g2:^sigtri16,g3:^sigtri16,g4:^sigtri16,bus:^sig16) =
109 DEST_TRI16 (memout t U16 g0 t U16 g1 t U16 g2 t U16 g3 t U16 g4 t)"
118 ?g0 g1 g2 g3 g4 memout alu bus.
128 G2(acc,racc,g2) /\
132 BUS(memout,g0,g1,g2,g3,g4,bus)"

Completed in 201 milliseconds

123