R
↳Dependency Pair Analysis
F(f(a, b), x) -> F(a, f(a, x))
F(f(a, b), x) -> F(a, x)
F(f(b, a), x) -> F(b, f(b, x))
F(f(b, a), x) -> F(b, x)
F(x, f(y, z)) -> F(f(x, y), z)
F(x, f(y, z)) -> F(x, y)
R
↳DPs
→DP Problem 1
↳Modular Removal of Rules
F(f(b, a), x) -> F(b, x)
F(f(b, a), x) -> F(b, f(b, x))
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x) -> F(a, x)
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, b), x) -> F(a, f(a, x))
f(f(a, b), x) -> f(a, f(a, x))
f(f(b, a), x) -> f(b, f(b, x))
f(x, f(y, z)) -> f(f(x, y), z)
innermost
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
f(f(b, a), x) -> f(b, f(b, x))
f(f(a, b), x) -> f(a, f(a, x))
f(x, f(y, z)) -> f(f(x, y), z)
POL(b) = 0 POL(a) = 0 POL(F(x1, x2)) = x1 + x2 POL(f(x1, x2)) = 1 + x1 + x2
F(f(b, a), x) -> F(b, x)
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x) -> F(a, x)
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Instantiation Transformation
F(f(b, a), x) -> F(b, f(b, x))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, b), x) -> F(a, f(a, x))
f(f(a, b), x) -> f(a, f(a, x))
f(f(b, a), x) -> f(b, f(b, x))
f(x, f(y, z)) -> f(f(x, y), z)
innermost
two new Dependency Pairs are created:
F(x, f(y, z)) -> F(f(x, y), z)
F(a, f(y', z')) -> F(f(a, y'), z')
F(b, f(y', z')) -> F(f(b, y'), z')
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Inst
...
→DP Problem 3
↳Semantic Labelling
F(b, f(y', z')) -> F(f(b, y'), z')
F(f(b, a), x) -> F(b, f(b, x))
f(f(a, b), x) -> f(a, f(a, x))
f(f(b, a), x) -> f(b, f(b, x))
f(x, f(y, z)) -> f(f(x, y), z)
innermost
F(x0, x1) = 0 f(x0, x1) = x0 b = 1 a = 0
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Inst
...
→DP Problem 4
↳Semantic Labelling
F(a, f(y', z')) -> F(f(a, y'), z')
F(f(a, b), x) -> F(a, f(a, x))
f(f(a, b), x) -> f(a, f(a, x))
f(f(b, a), x) -> f(b, f(b, x))
f(x, f(y, z)) -> f(f(x, y), z)
innermost
F(x0, x1) = 0 a = 0 f(x0, x1) = x0 b = 1