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.