(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(S(x'), S(x)) → h(g(x', S(x)), f(S(S(S(x'))), x))
g(S(x), S(x')) → h(f(S(x), S(x')), g(x, S(S(S(x')))))
h(0, S(x)) → h(0, x)
h(0, 0) → 0
g(S(x), 0) → 0
f(S(x), 0) → 0
h(S(x), x2) → h(x, x2)
g(0, x2) → 0
f(0, x2) → 0
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
f(S(S(x14_1)), S(x)) →+ h(h(h(g(x14_1, S(x)), f(S(S(S(x14_1))), x)), g(x14_1, S(S(S(x))))), f(S(S(S(S(x14_1)))), x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,1].
The pumping substitution is [x / S(x)].
The result substitution is [x14_1 / S(x14_1)].
The rewrite sequence
f(S(S(x14_1)), S(x)) →+ h(h(h(g(x14_1, S(x)), f(S(S(S(x14_1))), x)), g(x14_1, S(S(S(x))))), f(S(S(S(S(x14_1)))), x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [x / S(x)].
The result substitution is [x14_1 / S(S(x14_1))].
(2) BOUNDS(2^n, INF)