Lines Matching refs:a1
272 `!a0: word8 a1: word8 a2: word8 a3: word8 a4: word8 a5: word8 a6: word8
274 let w = a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0
277 ((15 >< 0) w = (a1 @@ a0) : word16) /\
278 ((23 >< 0) w = (a2 @@ a1 @@ a0) : word24) /\
279 ((31 >< 0) w = (a3 @@ a2 @@ a1 @@ a0) : word32) /\
280 ((39 >< 0) w = (a4 @@ a3 @@ a2 @@ a1 @@ a0) : 40 word) /\
281 ((47 >< 0) w = (a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : word48) /\
282 ((55 >< 0) w = (a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : 56 word) /\
288 ((31 >< 8) w = (a3 @@ a2 @@ a1) : word24) /\
291 ((63 >< 8) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1) : 56 word) /\