YES

Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
Call external tool:
ttt2 - trs 30
Input:
  ?1(s(0), x) -> x
  f(g(x)) -> ?1(x, x)
  g(s(x)) -> g(x)

 DP Processor:
  DPs:
   f#(g(x)) -> ?1#(x,x)
   g#(s(x)) -> g#(x)
  TRS:
   ?1(s(0()),x) -> x
   f(g(x)) -> ?1(x,x)
   g(s(x)) -> g(x)
  TDG Processor:
   DPs:
    f#(g(x)) -> ?1#(x,x)
    g#(s(x)) -> g#(x)
   TRS:
    ?1(s(0()),x) -> x
    f(g(x)) -> ?1(x,x)
    g(s(x)) -> g(x)
   graph:
    g#(s(x)) -> g#(x) -> g#(s(x)) -> g#(x)
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 1/4
    DPs:
     g#(s(x)) -> g#(x)
    TRS:
     ?1(s(0()),x) -> x
     f(g(x)) -> ?1(x,x)
     g(s(x)) -> g(x)
    Subterm Criterion Processor:
     simple projection:
      pi(g#) = 0
     problem:
      DPs:
       
      TRS:
       ?1(s(0()),x) -> x
       f(g(x)) -> ?1(x,x)
       g(s(x)) -> g(x)
     Qed