YES

Problem:
 f(s(x),y) -> f(x,g(x,y))
 f(0(),y) -> y
 g(x,y) -> y

Proof:
 DP Processor:
  DPs:
   f#(s(x),y) -> g#(x,y)
   f#(s(x),y) -> f#(x,g(x,y))
  TRS:
   f(s(x),y) -> f(x,g(x,y))
   f(0(),y) -> y
   g(x,y) -> y
  Usable Rule Processor:
   DPs:
    f#(s(x),y) -> g#(x,y)
    f#(s(x),y) -> f#(x,g(x,y))
   TRS:
    g(x,y) -> y
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     g(x,y) -> y
    interpretation:
     [g#](x0, x1) = x0,
     
     [f#](x0, x1) = x0,
     
     [g](x0, x1) = 8x0 + 10x1 + 12,
     
     [s](x0) = 7x0 + -2
    orientation:
     f#(s(x),y) = 7x + -2 >= x = g#(x,y)
     
     f#(s(x),y) = 7x + -2 >= x = f#(x,g(x,y))
     
     g(x,y) = 8x + 10y + 12 >= y = y
    problem:
     DPs:
      
     TRS:
      g(x,y) -> y
    Qed