  | `Pb(setaa0, setlk1, k2) -> 
      B
       (Sail_values.to_vec0 true (Nat_big_num.of_int 24,Nat_big_num.of_int (trans_li_setaa_setlk_k setaa0 setlk1 k2)),
        int_to_bit (trans_aa setaa0),
        int_to_bit (trans_lk setlk1))

  | `Pbc(setaa0, setlk1, k2, k3, k4) -> 
      Bc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k3),
        Sail_values.to_vec0 true (Nat_big_num.of_int 14,Nat_big_num.of_int (trans_bd_setaa_setlk_k_k_k setaa0 setlk1 k2 k3 k4)),
        int_to_bit (trans_aa setaa0),
        int_to_bit (trans_lk setlk1))

  | `Pbclr(setlk0, k1, k2, k3) -> 
      Bclr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2),
        Sail_values.to_vec0 true (Nat_big_num.of_int 2,Nat_big_num.of_int k3),
        int_to_bit (trans_lk setlk0))

  | `Pbcctr(setlk0, k1, k2, k3) -> 
      Bcctr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2),
        Sail_values.to_vec0 true (Nat_big_num.of_int 2,Nat_big_num.of_int k3),
        int_to_bit (trans_lk setlk0))

  | `Pcrand(k0, k1, k2) -> 
      Crand
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pcrnand(k0, k1, k2) -> 
      Crnand
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pcror(k0, k1, k2) -> 
      Cror
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pcrxor(k0, k1, k2) -> 
      Crxor
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pcrnor(k0, k1, k2) -> 
      Crnor
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pcreqv(k0, k1, k2) -> 
      Creqv
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pcrandc(k0, k1, k2) -> 
      Crandc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pcrorc(k0, k1, k2) -> 
      Crorc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pmcrf(crindex0, k1) -> 
      Mcrf
       (Sail_values.to_vec0 true (Nat_big_num.of_int 3,Nat_big_num.of_int crindex0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 3,Nat_big_num.of_int k1))

  | `Psc(k0) -> 
      Sc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 7,Nat_big_num.of_int k0))

  | `Pscv(k0) -> 
      Scv
       (Sail_values.to_vec0 true (Nat_big_num.of_int 7,Nat_big_num.of_int k0))

  | `Plbz(reg0, k1, reg2) -> 
      Lbz
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plbzx(reg0, reg1, reg2) -> 
      Lbzx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plbzu(reg0, k1, reg2) -> 
      Lbzu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plbzux(reg0, reg1, reg2) -> 
      Lbzux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plhz(reg0, k1, reg2) -> 
      Lhz
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plhzx(reg0, reg1, reg2) -> 
      Lhzx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plhzu(reg0, k1, reg2) -> 
      Lhzu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plhzux(reg0, reg1, reg2) -> 
      Lhzux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plha(reg0, k1, reg2) -> 
      Lha
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plhax(reg0, reg1, reg2) -> 
      Lhax
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plhau(reg0, k1, reg2) -> 
      Lhau
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plhaux(reg0, reg1, reg2) -> 
      Lhaux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plwz(reg0, k1, reg2) -> 
      Lwz
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plwzx(reg0, reg1, reg2) -> 
      Lwzx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plwzu(reg0, k1, reg2) -> 
      Lwzu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plwzux(reg0, reg1, reg2) -> 
      Lwzux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plwa(reg0, ds1, reg2) -> 
      Lwa
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 14,Nat_big_num.of_int ds1))

  | `Plwax(reg0, reg1, reg2) -> 
      Lwax
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plwaux(reg0, reg1, reg2) -> 
      Lwaux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pld(reg0, ds1, reg2) -> 
      Ld
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 14,Nat_big_num.of_int ds1))

  | `Pldx(reg0, reg1, reg2) -> 
      Ldx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pldu(reg0, ds1, reg2) -> 
      Ldu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 14,Nat_big_num.of_int ds1))

  | `Pldux(reg0, reg1, reg2) -> 
      Ldux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstb(reg0, k1, reg2) -> 
      Stb
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Pstbx(reg0, reg1, reg2) -> 
      Stbx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstbu(reg0, k1, reg2) -> 
      Stbu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Pstbux(reg0, reg1, reg2) -> 
      Stbux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Psth(reg0, k1, reg2) -> 
      Sth
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Psthx(reg0, reg1, reg2) -> 
      Sthx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Psthu(reg0, k1, reg2) -> 
      Sthu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Psthux(reg0, reg1, reg2) -> 
      Sthux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstw(reg0, k1, reg2) -> 
      Stw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Pstwx(reg0, reg1, reg2) -> 
      Stwx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstwu(reg0, k1, reg2) -> 
      Stwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Pstwux(reg0, reg1, reg2) -> 
      Stwux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstd(reg0, ds1, reg2) -> 
      Std
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 14,Nat_big_num.of_int ds1))

  | `Pstdx(reg0, reg1, reg2) -> 
      Stdx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstdu(reg0, ds1, reg2) -> 
      Stdu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 14,Nat_big_num.of_int ds1))

  | `Pstdux(reg0, reg1, reg2) -> 
      Stdux
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plq(k0, k1, reg2, k3) -> 
      Lq
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 12,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 4,Nat_big_num.of_int k3))

  | `Pstq(k0, ds1, reg2) -> 
      Stq
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 14,Nat_big_num.of_int ds1))

  | `Plhbrx(reg0, reg1, reg2) -> 
      Lhbrx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Psthbrx(reg0, reg1, reg2) -> 
      Sthbrx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plwbrx(reg0, reg1, reg2) -> 
      Lwbrx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstwbrx(reg0, reg1, reg2) -> 
      Stwbrx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pldbrx(reg0, reg1, reg2) -> 
      Ldbrx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstdbrx(reg0, reg1, reg2) -> 
      Stdbrx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Plmw(reg0, k1, reg2) -> 
      Lmw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Pstmw(reg0, k1, reg2) -> 
      Stmw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k1))

  | `Plswi(k0, reg1, k2) -> 
      Lswi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Plswx(reg0, reg1, reg2) -> 
      Lswx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstswi(k0, reg1, k2) -> 
      Stswi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2))

  | `Pstswx(k0, reg1, reg2) -> 
      Stswx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Paddi(reg0, reg1, k2) -> 
      Addi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Paddis(reg0, reg1, k2) -> 
      Addis
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Padd(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Add
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Psubf(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Subf
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Paddic(reg0, reg1, k2) -> 
      Addic
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Paddicdot(reg0, reg1, k2) -> 
      AddicDot
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Psubfic(reg0, reg1, k2) -> 
      Subfic
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Paddc(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Addc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Psubfc(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Subfc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Padde(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Adde
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Psubfe(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Subfe
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Paddme(setsoov0, setcr01, reg2, reg3) -> 
      Addme
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Psubfme(setsoov0, setcr01, reg2, reg3) -> 
      Subfme
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Paddze(setsoov0, setcr01, reg2, reg3) -> 
      Addze
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Psubfze(setsoov0, setcr01, reg2, reg3) -> 
      Subfze
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pneg(setsoov0, setcr01, reg2, reg3) -> 
      Neg
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmulli(reg0, reg1, k2) -> 
      Mulli
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Pmullw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Mullw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmulhw(setcr00, reg1, reg2, reg3) -> 
      Mulhw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmulhwu(setcr00, reg1, reg2, reg3) -> 
      Mulhwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pdivw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pdivwu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pdivwe(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divwe
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pdivweu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divweu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmulld(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Mulld
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmulhd(setcr00, reg1, reg2, reg3) -> 
      Mulhd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmulhdu(setcr00, reg1, reg2, reg3) -> 
      Mulhdu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pdivd(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pdivdu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divdu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pdivde(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divde
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pdivdeu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Divdeu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pcmpi(crindex0, k1, reg2, k3) -> 
      Cmpi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 3,Nat_big_num.of_int crindex0),
        int_to_bit k1,
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k3))

  | `Pcmp(crindex0, k1, reg2, reg3) -> 
      Cmp
       (Sail_values.to_vec0 true (Nat_big_num.of_int 3,Nat_big_num.of_int crindex0),
        int_to_bit k1,
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)))

  | `Pcmpli(crindex0, k1, reg2, k3) -> 
      Cmpli
       (Sail_values.to_vec0 true (Nat_big_num.of_int 3,Nat_big_num.of_int crindex0),
        int_to_bit k1,
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k3))

  | `Pcmpl(crindex0, k1, reg2, reg3) -> 
      Cmpl
       (Sail_values.to_vec0 true (Nat_big_num.of_int 3,Nat_big_num.of_int crindex0),
        int_to_bit k1,
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)))

  | `Pisel(reg0, reg1, reg2, k3) -> 
      Isel
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k3))

  | `Pandi(reg0, reg1, k2) -> 
      Andi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Pandis(reg0, reg1, k2) -> 
      Andis
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Pori(reg0, reg1, k2) -> 
      Ori
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Poris(reg0, reg1, k2) -> 
      Oris
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Pxori(reg0, reg1, k2) -> 
      Xori
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Pxoris(reg0, reg1, k2) -> 
      Xoris
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 16,Nat_big_num.of_int k2))

  | `Pand(setcr00, reg1, reg2, reg3) -> 
      And
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pxor(setcr00, reg1, reg2, reg3) -> 
      Xor
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pnand(setcr00, reg1, reg2, reg3) -> 
      Nand
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Por(setcr00, reg1, reg2, reg3) -> 
      Or
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pnor(setcr00, reg1, reg2, reg3) -> 
      Nor
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Peqv(setcr00, reg1, reg2, reg3) -> 
      Eqv
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pandc(setcr00, reg1, reg2, reg3) -> 
      Andc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Porc(setcr00, reg1, reg2, reg3) -> 
      Orc
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pextsb(setcr00, reg1, reg2) -> 
      Extsb
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        int_to_bit (trans_cr0 setcr00))

  | `Pextsh(setcr00, reg1, reg2) -> 
      Extsh
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        int_to_bit (trans_cr0 setcr00))

  | `Pcntlzw(setcr00, reg1, reg2) -> 
      Cntlzw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        int_to_bit (trans_cr0 setcr00))

  | `Pcmpb(reg0, k1, reg2) -> 
      Cmpb
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k1),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Ppopcntb(reg0, reg1) -> 
      Popcntb
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Ppopcntw(reg0, reg1) -> 
      Popcntw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Pprtyd(reg0, reg1) -> 
      Prtyd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Pprtyw(reg0, reg1) -> 
      Prtyw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Pextsw(setcr00, reg1, reg2) -> 
      Extsw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        int_to_bit (trans_cr0 setcr00))

  | `Pcntlzd(setcr00, reg1, reg2) -> 
      Cntlzd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        int_to_bit (trans_cr0 setcr00))

  | `Ppopcntd(reg0, reg1) -> 
      Popcntd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Pbpermd(reg0, reg1, reg2) -> 
      Bpermd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Prlwinm(setcr00, reg1, reg2, k3, k4, k5) -> 
      Rlwinm
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k3),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k4),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k5),
        int_to_bit (trans_cr0 setcr00))

  | `Prlwnm(setcr00, reg1, reg2, reg3, k4, k5) -> 
      Rlwnm
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k4),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k5),
        int_to_bit (trans_cr0 setcr00))

  | `Prlwimi(setcr00, reg1, reg2, k3, k4, k5) -> 
      Rlwimi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k3),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k4),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k5),
        int_to_bit (trans_cr0 setcr00))

  | `Prldicl(setcr00, reg1, reg2, k3, k4) -> 
      Rldicl
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k3),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k4),
        int_to_bit (trans_cr0 setcr00))

  | `Prldicr(setcr00, reg1, reg2, k3, k4) -> 
      Rldicr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k3),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k4),
        int_to_bit (trans_cr0 setcr00))

  | `Prldic(setcr00, reg1, reg2, k3, k4) -> 
      Rldic
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k3),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k4),
        int_to_bit (trans_cr0 setcr00))

  | `Prldcl(setcr00, reg1, reg2, reg3, k4) -> 
      Rldcl
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k4),
        int_to_bit (trans_cr0 setcr00))

  | `Prldcr(setcr00, reg1, reg2, reg3, k4) -> 
      Rldcr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k4),
        int_to_bit (trans_cr0 setcr00))

  | `Prldimi(setcr00, reg1, reg2, k3, k4) -> 
      Rldimi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k3),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k4),
        int_to_bit (trans_cr0 setcr00))

  | `Pslw(setcr00, reg1, reg2, reg3) -> 
      Slw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Psrw(setcr00, reg1, reg2, reg3) -> 
      Srw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Psrawi(setcr00, reg1, reg2, k3) -> 
      Srawi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k3),
        int_to_bit (trans_cr0 setcr00))

  | `Psraw(setcr00, reg1, reg2, reg3) -> 
      Sraw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Psld(setcr00, reg1, reg2, reg3) -> 
      Sld
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Psrd(setcr00, reg1, reg2, reg3) -> 
      Srd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Psradi(setcr00, reg1, reg2, k3) -> 
      Sradi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 6,Nat_big_num.of_int k3),
        int_to_bit (trans_cr0 setcr00))

  | `Psrad(setcr00, reg1, reg2, reg3) -> 
      Srad
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pcdtbcd(reg0, reg1) -> 
      Cdtbcd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Pcbcdtd(reg0, reg1) -> 
      Cbcdtd
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Paddg6s(reg0, reg1, reg2) -> 
      Addg6s
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pmtspr(k0, reg1) -> 
      Mtspr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 10,Nat_big_num.of_int k0))

  | `Pmfspr(reg0, k1) -> 
      Mfspr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 10,Nat_big_num.of_int k1))

  | `Pmtcrf(crmask0, reg1) -> 
      Mtcrf
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 8,Nat_big_num.of_int crmask0))

  | `Pmfcr(reg0) -> 
      Mfcr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)))

  | `Pmtocrf(crmask0, reg1) -> 
      Mtocrf
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 8,Nat_big_num.of_int crmask0))

  | `Pmfocrf(reg0, crmask1) -> 
      Mfocrf
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 8,Nat_big_num.of_int crmask1))

  | `Pmcrxr(crindex0) -> 
      Mcrxr
       (Sail_values.to_vec0 true (Nat_big_num.of_int 3,Nat_big_num.of_int crindex0))

  | `Pdlmzb(setcr00, reg1, reg2, reg3) -> 
      Dlmzb
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmacchw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Macchw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmacchws(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Macchws
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmacchwu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Macchwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmacchwsu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Macchwsu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmachhw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Machhw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmachhws(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Machhws
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmachhwu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Machhwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmachhwsu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Machhwsu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmaclhw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Maclhw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmaclhws(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Maclhws
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmaclhwu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Maclhwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmaclhwsu(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Maclhwsu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pmulchw(setcr00, reg1, reg2, reg3) -> 
      Mulchw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmulchwu(setcr00, reg1, reg2, reg3) -> 
      Mulchwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmulhhw(setcr00, reg1, reg2, reg3) -> 
      Mulhhw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmulhhwu(setcr00, reg1, reg2, reg3) -> 
      Mulhhwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmullhw(setcr00, reg1, reg2, reg3) -> 
      Mullhw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pmullhwu(setcr00, reg1, reg2, reg3) -> 
      Mullhwu
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        int_to_bit (trans_cr0 setcr00))

  | `Pnmacchw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Nmacchw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pnmacchws(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Nmacchws
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pnmachhw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Nmachhw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pnmachhws(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Nmachhws
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pnmaclhw(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Nmaclhw
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Pnmaclhws(setsoov0, setcr01, reg2, reg3, reg4) -> 
      Nmaclhws
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg3)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg4)),
        int_to_bit (trans_soov setsoov0),
        int_to_bit (trans_cr0 setcr01))

  | `Picbi(reg0, reg1) -> 
      Icbi
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)))

  | `Picbt(k0, reg1, reg2) -> 
      Icbt
       (Sail_values.to_vec0 true (Nat_big_num.of_int 4,Nat_big_num.of_int k0),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pdcba(reg0, reg1) -> 
      Dcba
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)))

  | `Pdcbt(reg0, reg1, k2) -> 
      Dcbt
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)))

  | `Pdcbtst(reg0, reg1, k2) -> 
      Dcbtst
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int k2),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)))

  | `Pdcbz(reg0, reg1) -> 
      Dcbz
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)))

  | `Pdcbst(reg0, reg1) -> 
      Dcbst
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)))

  | `Pdcbf(reg0, reg1, k2) -> 
      Dcbf
       (Sail_values.to_vec0 true (Nat_big_num.of_int 2,Nat_big_num.of_int k2),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)))

  | `Pisync -> 
      Isync

  | `Plbarx(reg0, reg1, reg2, k3) -> 
      Lbarx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        int_to_bit k3)

  | `Plharx(reg0, reg1, reg2, k3) -> 
      Lharx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        int_to_bit k3)

  | `Plwarx(reg0, reg1, reg2, k3) -> 
      Lwarx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        int_to_bit k3)

  | `Pstbcx(reg0, reg1, reg2) -> 
      Stbcx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Psthcx(reg0, reg1, reg2) -> 
      Sthcx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pstwcx(reg0, reg1, reg2) -> 
      Stwcx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Pldarx(reg0, reg1, reg2, k3) -> 
      Ldarx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)),
        int_to_bit k3)

  | `Pstdcx(reg0, reg1, reg2) -> 
      Stdcx
       (Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg0)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg1)),
        Sail_values.to_vec0 true (Nat_big_num.of_int 5,Nat_big_num.of_int (int_of_reg reg2)))

  | `Psync(k0) -> 
      Sync
       (Sail_values.to_vec0 true (Nat_big_num.of_int 2,Nat_big_num.of_int k0))

  | `Peieio -> 
      Eieio

  | `Pwait(k0) -> 
      Wait
       (Sail_values.to_vec0 true (Nat_big_num.of_int 2,Nat_big_num.of_int k0))

