fun x x0 : word64 * word64 * word64 * word64 * word64 =>
Eta.InterpEta
  (fun var : Syntax.base_type -> Type =>
   λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core,
   uint128_t x20 = (uint128_t) x5 * (uint128_t) x18;
   uint128_t x21 = (uint128_t) x7 * (uint128_t) x19;
   uint128_t x22 = (uint128_t) x9 * (uint128_t) x17;
   uint128_t x23 = (uint128_t) x11 * (uint128_t) x15;
   uint128_t x24 = (uint128_t) x10 * (uint128_t) x13;
   uint128_t x25 = x23 + x24;
   uint128_t x26 = x22 + x25;
   uint128_t x27 = x21 + x26;
   uint128_t x28 = x20 + x27;
   uint128_t x29 = (uint128_t) x5 * (uint128_t) x19;
   uint128_t x30 = (uint128_t) x7 * (uint128_t) x17;
   uint128_t x31 = (uint128_t) x9 * (uint128_t) x15;
   uint128_t x32 = (uint128_t) x11 * (uint128_t) x13;
   uint128_t x33 = x31 + x32;
   uint128_t x34 = x30 + x33;
   uint128_t x35 = x29 + x34;
   uint128_t x36 = (uint128_t) x10 * (uint128_t) x18;
   uint128_t x37 = (uint128_t) 0x13 * x36;
   uint128_t x38 = x35 + x37;
   uint128_t x39 = (uint128_t) x5 * (uint128_t) x17;
   uint128_t x40 = (uint128_t) x7 * (uint128_t) x15;
   uint128_t x41 = (uint128_t) x9 * (uint128_t) x13;
   uint128_t x42 = x40 + x41;
   uint128_t x43 = x39 + x42;
   uint128_t x44 = (uint128_t) x11 * (uint128_t) x18;
   uint128_t x45 = (uint128_t) x10 * (uint128_t) x19;
   uint128_t x46 = x44 + x45;
   uint128_t x47 = (uint128_t) 0x13 * x46;
   uint128_t x48 = x43 + x47;
   uint128_t x49 = (uint128_t) x5 * (uint128_t) x15;
   uint128_t x50 = (uint128_t) x7 * (uint128_t) x13;
   uint128_t x51 = x49 + x50;
   uint128_t x52 = (uint128_t) x9 * (uint128_t) x18;
   uint128_t x53 = (uint128_t) x11 * (uint128_t) x19;
   uint128_t x54 = (uint128_t) x10 * (uint128_t) x17;
   uint128_t x55 = x53 + x54;
   uint128_t x56 = x52 + x55;
   uint128_t x57 = (uint128_t) 0x13 * x56;
   uint128_t x58 = x51 + x57;
   uint128_t x59 = (uint128_t) x5 * (uint128_t) x13;
   uint128_t x60 = (uint128_t) x7 * (uint128_t) x18;
   uint128_t x61 = (uint128_t) x9 * (uint128_t) x19;
   uint128_t x62 = (uint128_t) x11 * (uint128_t) x17;
   uint128_t x63 = (uint128_t) x10 * (uint128_t) x15;
   uint128_t x64 = x62 + x63;
   uint128_t x65 = x61 + x64;
   uint128_t x66 = x60 + x65;
   uint128_t x67 = (uint128_t) 0x13 * x66;
   uint128_t x68 = x59 + x67;
   uint64_t x69 = (uint64_t) (x68 >> 0x33);
   uint128_t x70 = (uint128_t) x69 + x58;
   uint64_t x71 = (uint64_t) (x70 >> 0x33);
   uint128_t x72 = (uint128_t) x71 + x48;
   uint64_t x73 = (uint64_t) (x72 >> 0x33);
   uint128_t x74 = (uint128_t) x73 + x38;
   uint64_t x75 = (uint64_t) (x74 >> 0x33);
   uint128_t x76 = (uint128_t) x75 + x28;
   uint64_t x77 = (uint64_t) x68 & 0x7ffffffffffff;
   uint64_t x78 = (uint64_t) (x76 >> 0x33);
   uint64_t x79 = 0x13 * x78;
   uint64_t x80 = x77 + x79;
   uint64_t x81 = (uint64_t) (x80 >> 0x33);
   uint64_t x82 = (uint64_t) x70 & 0x7ffffffffffff;
   uint64_t x83 = x81 + x82;
   uint64_t x84 = (uint64_t) x76 & 0x7ffffffffffff;
   uint64_t x85 = (uint64_t) x74 & 0x7ffffffffffff;
   uint64_t x86 = (uint64_t) (x83 >> 0x33);
   uint64_t x87 = (uint64_t) x72 & 0x7ffffffffffff;
   uint64_t x88 = x86 + x87;
   uint64_t x89 = x83 & 0x7ffffffffffff;
   uint64_t x90 = x80 & 0x7ffffffffffff;
   (Return x84, Return x85, Return x88, Return x89, Return x90)) 
  (x, x0)%core
     : word64 * word64 * word64 * word64 * word64 ->
       word64 * word64 * word64 * word64 * word64 ->
       interp_flat_type
         (fun v : Syntax.base_type =>
          match v with
          | Syntax.TZ => Z
          | Syntax.TWord 0 => word (2 ^ 0)
          | Syntax.TWord 1 => word (2 ^ 1)
          | Syntax.TWord 2 => word (2 ^ 2)
          | Syntax.TWord 3 => word (2 ^ 3)
          | Syntax.TWord 4 => word (2 ^ 4)
          | Syntax.TWord 5 => word32
          | Syntax.TWord 6 => word64
          | Syntax.TWord 7 => word128
          | Syntax.TWord (S (S (S (S (S (S (S (S n6)))))))) =>
              word (2 ^ S (S (S (S (S (S (S (S n6))))))))
          end) (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)