MAYBE
Time: 0.110027
TRS:
 {  f(s x, x) -> f(s x, round s x),
  round s s x -> s s round x,
  round s 0() -> s 0(),
    round 0() -> s 0(),
    round 0() -> 0()}
 DP:
  DP:
   {  f#(s x, x) -> f#(s x, round s x),
      f#(s x, x) -> round# s x,
    round# s s x -> round# x}
  TRS:
  {  f(s x, x) -> f(s x, round s x),
   round s s x -> s s round x,
   round s 0() -> s 0(),
     round 0() -> s 0(),
     round 0() -> 0()}
  EDG:
   {(f#(s x, x) -> f#(s x, round s x), f#(s x, x) -> round# s x)
    (f#(s x, x) -> f#(s x, round s x), f#(s x, x) -> f#(s x, round s x))
    (f#(s x, x) -> round# s x, round# s s x -> round# x)
    (round# s s x -> round# x, round# s s x -> round# x)}
   STATUS:
    arrows: 0.555556
    SCCS (2):
     Scc:
      {f#(s x, x) -> f#(s x, round s x)}
     Scc:
      {round# s s x -> round# x}
     
     SCC (1):
      Strict:
       {f#(s x, x) -> f#(s x, round s x)}
      Weak:
      {  f(s x, x) -> f(s x, round s x),
       round s s x -> s s round x,
       round s 0() -> s 0(),
         round 0() -> s 0(),
         round 0() -> 0()}
      Fail
     
     SCC (1):
      Strict:
       {round# s s x -> round# x}
      Weak:
      {  f(s x, x) -> f(s x, round s x),
       round s s x -> s s round x,
       round s 0() -> s 0(),
         round 0() -> s 0(),
         round 0() -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = x0 + 1,
        
        [round](x0) = x0 + 1,
        
        [0] = 0,
        
        [round#](x0) = x0
       Strict:
        round# s s x -> round# x
        2 + 1x >= 0 + 1x
       Weak:
        round 0() -> 0()
        1 >= 0
        round 0() -> s 0()
        1 >= 1
        round s 0() -> s 0()
        2 >= 1
        round s s x -> s s round x
        3 + 1x >= 3 + 1x
        f(s x, x) -> f(s x, round s x)
        2 + 2x >= 4 + 2x
      Qed