R
↳Dependency Pair Analysis
NORM(g(x, y)) -> NORM(x)
F(x, g(y, z)) -> F(x, y)
REM(g(x, y), s(z)) -> REM(x, z)
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
NORM(g(x, y)) -> NORM(x)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
F(x, g(y, z)) -> F(x, y)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
REM(g(x, y), s(z)) -> REM(x, z)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
NORM(g(x, y)) -> NORM(x)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
F(x, g(y, z)) -> F(x, y)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
REM(g(x, y), s(z)) -> REM(x, z)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
NORM(g(x, y)) -> NORM(x)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
F(x, g(y, z)) -> F(x, y)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)
REM(g(x, y), s(z)) -> REM(x, z)
norm(nil) -> 0
norm(g(x, y)) -> s(norm(x))
f(x, nil) -> g(nil, x)
f(x, g(y, z)) -> g(f(x, y), z)
rem(nil, y) -> nil
rem(g(x, y), 0) -> g(x, y)
rem(g(x, y), s(z)) -> rem(x, z)