Library multi_one_u_prg

Require Import machine_int.
Require Import mips_cmd.
Import expr_m.
Require Import multi_zero_u_prg.

Local Open Scope mips_cmd_scope.

Definition multi_one_u k z ext Z_ :=
  multi_zero_u k z ext Z_;
  addiu ext r0 one16 ;
  sw ext zero16 z.