Lines Matching defs:x2
106 val x2 = ("r2",``2w:word4``,``r2:word64``);
154 val mov_r10_xs = READ_XS x2 x10;
155 val mov_r10_xs = READ_XS x2 x11;
204 val mov_r10_ys = READ_YS x2 x10;
205 val mov_r11_ys = READ_YS x2 x11;
206 val mov_r12_ys = READ_YS x2 x12;
258 val mov_r10_zs = READ_ZS x2 x10;
327 val mov_zs_r10 = WRITE_ZS x2 x10;
1153 let (x1,x2) = single_mul_add p q k s in (x1,k,x2,s))``,
1432 ``(x64_single_div_pre (x2,x1,y) = x1 <+ y) /\
1433 (x64_single_div (x2,x1,y) = let (q,r) = single_div x1 x2 y in (q,r,y))``,
1438 \\ `w2n x2 < 18446744073709551616` by ALL_TAC THEN1
1439 (ASSUME_TAC (w2n_lt |> INST_TYPE [``:'a``|->``:64``] |> Q.SPEC `x2`)
1580 let (x1,x2) = single_mul_add p q k 0w in (x1,k,x2))``,
1792 r7 -- x2
2221 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x1 = x2) /\ (y1 = y2) ==> (f x1 y1 = f x2 y2)``)
2756 \\ `?x1 x2 x3. mw_simple_div 0x0w (REVERSE rs1) d = (x1,x2,x3)` by METIS_TAC [PAIR]