(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
minus(0, y) → 0
minus(s(x), 0) → s(x)
minus(s(x), s(y)) → minus(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
if(true, x, y) → x
if(false, x, y) → y
perfectp(0) → false
perfectp(s(x)) → f(x, s(0), s(x), s(x))
f(0, y, 0, u) → true
f(0, y, s(z), u) → false
f(s(x), 0, z, u) → f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) → if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))
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(s(x98022_1))), 0, 0, s(0)) →+ if(le(s(x98022_1), 0), f(s(s(x98022_1)), 0, 0, s(0)), if(le(x98022_1, 0), f(s(x98022_1), 0, 0, s(0)), f(x98022_1, s(0), 0, s(0))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [x98022_1 / s(x98022_1)].
The result substitution is [ ].
The rewrite sequence
f(s(s(s(x98022_1))), 0, 0, s(0)) →+ if(le(s(x98022_1), 0), f(s(s(x98022_1)), 0, 0, s(0)), if(le(x98022_1, 0), f(s(x98022_1), 0, 0, s(0)), f(x98022_1, s(0), 0, s(0))))
gives rise to a decreasing loop by considering the right hand sides subterm at position [2,1].
The pumping substitution is [x98022_1 / s(s(x98022_1))].
The result substitution is [ ].
(2) BOUNDS(2^n, INF)