Lines Matching defs:rn
329 RD_INVARIANT A (rm:word32) rs rn n =
334 (if A then rn else 0w)`;
360 `!a rm rs rn.
361 RD_INVARIANT a rm rs rn (MLA_MUL_DUR rs) =
362 rm * rs + (if a then rn else 0w)`,
522 `!n a rm rs rn. 2 * (n + 1) <= 32 ==>
523 (RD_INVARIANT a rm rs rn (n + 1) =
527 ALU6_MUL borrow2 mul (RD_INVARIANT a rm rs rn n)
549 RD_INVARIANT a rm rs rn n
552 RD_INVARIANT a rm rs rn n +
557 RD_INVARIANT a rm rs rn n -
560 RD_INVARIANT a rm rs rn (n + 1))`,
648 and rn = REG_READ6 reg nbs ((15 >< 12) ireg) in
655 (if ireg %% 21 then rn else 0w))
656 psr (pc + 4w) ireg alua rn dout)
663 let rd = RD_INVARIANT (ireg %% 21) rm rs rn (n - 1)
667 let rd' = RD_INVARIANT (ireg %% 21) rm rs rn n
690 (if n = 0 then rn else rm << w2n mshift)
710 \\ ABBREV_TAC `rn = REG_READ6 reg nbs ((15 >< 12) ireg)`