R
↳Dependency Pair Analysis
F(a, f(a, x)) -> F(c, f(b, x))
F(a, f(a, x)) -> F(b, x)
F(b, f(b, x)) -> F(a, f(c, x))
F(b, f(b, x)) -> F(c, x)
F(c, f(c, x)) -> F(b, f(a, x))
F(c, f(c, x)) -> F(a, x)
R
↳DPs
→DP Problem 1
↳Modular Removal of Rules
F(c, f(c, x)) -> F(a, x)
F(b, f(b, x)) -> F(c, x)
F(a, f(a, x)) -> F(b, x)
F(b, f(b, x)) -> F(a, f(c, x))
F(c, f(c, x)) -> F(b, f(a, x))
F(a, f(a, x)) -> F(c, f(b, x))
f(a, f(a, x)) -> f(c, f(b, x))
f(b, f(b, x)) -> f(a, f(c, x))
f(c, f(c, x)) -> f(b, f(a, x))
F(c, f(c, x)) -> F(a, x)
F(b, f(b, x)) -> F(c, x)
F(a, f(a, x)) -> F(b, x)
F(b, f(b, x)) -> F(a, f(c, x))
F(c, f(c, x)) -> F(b, f(a, x))
F(a, f(a, x)) -> F(c, f(b, x))
f(c, f(c, x)) -> f(b, f(a, x))
f(a, f(a, x)) -> f(c, f(b, x))
f(b, f(b, x)) -> f(a, f(c, x))
C(c(x)) -> A(x)
B(b(x)) -> C(x)
A(a(x)) -> B(x)
B(b(x)) -> A(c(x))
C(c(x)) -> B(a(x))
A(a(x)) -> C(b(x))
c(c(x)) -> b(a(x))
b(b(x)) -> a(c(x))
a(a(x)) -> c(b(x))
POL(c(x1)) = x1 POL(C(x1)) = x1 POL(B(x1)) = x1 POL(b(x1)) = x1 POL(a(x1)) = x1 POL(A(x1)) = x1
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Modular Removal of Rules
C(c(x)) -> A(x)
B(b(x)) -> C(x)
A(a(x)) -> B(x)
B(b(x)) -> A(c(x))
C(c(x)) -> B(a(x))
A(a(x)) -> C(b(x))
c(c(x)) -> b(a(x))
b(b(x)) -> a(c(x))
a(a(x)) -> c(b(x))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
c(c(x)) -> b(a(x))
a(a(x)) -> c(b(x))
b(b(x)) -> a(c(x))
POL(c(x1)) = 1 + x1 POL(C(x1)) = x1 POL(B(x1)) = x1 POL(b(x1)) = 1 + x1 POL(a(x1)) = 1 + x1 POL(A(x1)) = x1
C(c(x)) -> A(x)
B(b(x)) -> C(x)
A(a(x)) -> B(x)
R
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳MRR
...
→DP Problem 3
↳RFC Match Bounds
B(b(x)) -> A(c(x))
C(c(x)) -> B(a(x))
A(a(x)) -> C(b(x))
c(c(x)) -> b(a(x))
b(b(x)) -> a(c(x))
a(a(x)) -> c(b(x))
The certificate consists of the following enumerated nodes:
32, 33, 34, 35, 36, 37, 38, 39
Node 32 is start node and node 33 is final node.
Those nodes are connect through the following edges: