Definition theta2_tbl r : Z :=
  match r with
  | 1 => 11529215046068469760
  | 2 => 14411518807585587200
  | 3 => 18014398509481984000
  | 4 => 11258999068426240000
  | 5 => 14073748835532800000
  | 6 => 17592186044416000000
  | 7 => 10995116277760000000
  | 8 => 13743895347200000000
  | 9 => 17179869184000000000
  |10 => 10737418240000000000
  |11 => 13421772800000000000
  |12 => 16777216000000000000
  |13 => 10485760000000000000
  |14 => 13107200000000000000
  |15 => 16384000000000000000
  |16 => 10240000000000000000
  |_ => 0
  end.