Library multi_is_even_u_and_prg

Require Import multi_is_even_u_prg.
Require Import mips_cmd simu.

Local Open Scope mips_cmd_scope.

Definition multi_is_even_u_and rk rx ry a0 a1 :=
  multi_is_even_u rk rx a0 ;
  multi_is_even_u rk ry a1 ;
  cmd_and a0 a0 a1.