[
  (builtins.sub 7 11)
  (builtins.sub 7.9 11)
  (builtins.sub 7 11.9)
  (builtins.sub 7.2 11.9)
  (builtins.sub 7.9 11.9)
  (builtins.sub (builtins.sub 123 23) 58)
]