R
↳Dependency Pair Analysis
-'(s(x), s(y)) -> -'(x, y)
<='(s(x), s(y)) -> <='(x, y)
PERFECTP(s(x)) -> F(x, s(0), s(x), s(x))
F(s(x), 0, z, u) -> F(x, u, -(z, s(x)), u)
F(s(x), 0, z, u) -> -'(z, s(x))
F(s(x), s(y), z, u) -> IF(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
F(s(x), s(y), z, u) -> <='(x, y)
F(s(x), s(y), z, u) -> F(s(x), -(y, x), z, u)
F(s(x), s(y), z, u) -> -'(y, x)
F(s(x), s(y), z, u) -> F(x, u, z, u)
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
-'(s(x), s(y)) -> -'(x, y)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
<='(s(x), s(y)) -> <='(x, y)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
F(s(x), s(y), z, u) -> F(x, u, z, u)
F(s(x), 0, z, u) -> F(x, u, -(z, s(x)), u)
F(s(x), s(y), z, u) -> F(s(x), -(y, x), z, u)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
-'(s(x), s(y)) -> -'(x, y)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
<='(s(x), s(y)) -> <='(x, y)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
F(s(x), s(y), z, u) -> F(x, u, z, u)
F(s(x), 0, z, u) -> F(x, u, -(z, s(x)), u)
F(s(x), s(y), z, u) -> F(s(x), -(y, x), z, u)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
-'(s(x), s(y)) -> -'(x, y)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
<='(s(x), s(y)) -> <='(x, y)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))
F(s(x), s(y), z, u) -> F(x, u, z, u)
F(s(x), 0, z, u) -> F(x, u, -(z, s(x)), u)
F(s(x), s(y), z, u) -> F(s(x), -(y, x), z, u)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
<=(0, y) -> true
<=(s(x), 0) -> false
<=(s(x), s(y)) -> <=(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, -(z, s(x)), u)
f(s(x), s(y), z, u) -> if(<=(x, y), f(s(x), -(y, x), z, u), f(x, u, z, u))