Library multi_one_s_prg

Require Import machine_int.
Require Import mips_cmd.
Require Import multi_zero_s_prg multi_negate_prg.
Import expr_m.

Local Open Scope mips_cmd_scope.

Definition multi_one_s rx rk a0 a1 a2 a3 :=
  lw a0 zero16 rx ;
  (If_beq a0 , r0 Then
    sw rk zero16 rx
  Else
    If_bltz a0 Then
      multi_negate rx a0
    Else
      nop) ;
  multi_zero_s' rx a0 a1 a2 a3 ;
  lw a0 four16 rx ;
  addiu a1 r0 one16 ;
  sw a1 zero16 a0.