YES(O(1),O(1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict Trs:
  { f(g(x), g(y)) -> f(p(f(g(x), s(y))), g(s(p(x))))
  , g(s(p(x))) -> p(x)
  , p(0()) -> g(0()) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

We add the following weak dependency pairs:

Strict DPs:
  { f^#(g(x), g(y)) -> c_1(f^#(p(f(g(x), s(y))), g(s(p(x)))))
  , g^#(s(p(x))) -> c_2(p^#(x))
  , p^#(0()) -> c_3(g^#(0())) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs:
  { f^#(g(x), g(y)) -> c_1(f^#(p(f(g(x), s(y))), g(s(p(x)))))
  , g^#(s(p(x))) -> c_2(p^#(x))
  , p^#(0()) -> c_3(g^#(0())) }
Strict Trs:
  { f(g(x), g(y)) -> f(p(f(g(x), s(y))), g(s(p(x))))
  , g(s(p(x))) -> p(x)
  , p(0()) -> g(0()) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Consider the dependency graph:

  1: f^#(g(x), g(y)) -> c_1(f^#(p(f(g(x), s(y))), g(s(p(x)))))
  
  2: g^#(s(p(x))) -> c_2(p^#(x)) -->_1 p^#(0()) -> c_3(g^#(0())) :3
  
  3: p^#(0()) -> c_3(g^#(0()))
  

Only the nodes {3} are reachable from nodes {3} that start
derivation from marked basic terms. The nodes not reachable are
removed from the problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict DPs: { p^#(0()) -> c_3(g^#(0())) }
Strict Trs:
  { f(g(x), g(y)) -> f(p(f(g(x), s(y))), g(s(p(x))))
  , g(s(p(x))) -> p(x)
  , p(0()) -> g(0()) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

We estimate the number of application of {1} by applications of
Pre({1}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: p^#(0()) -> c_3(g^#(0())) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Strict Trs:
  { f(g(x), g(y)) -> f(p(f(g(x), s(y))), g(s(p(x))))
  , g(s(p(x))) -> p(x)
  , p(0()) -> g(0()) }
Weak DPs: { p^#(0()) -> c_3(g^#(0())) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs: { p^#(0()) -> c_3(g^#(0())) }
Obligation:
  runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(1))