(
  declare-fun
    g
      (
        ü