f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))
↳ QTRS
↳ DependencyPairsProof
f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))
G(x) → F(g(x))
F(g(a)) → F(s(g(b)))
F(g(a)) → G(b)
G(x) → G(x)
f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
G(x) → F(g(x))
F(g(a)) → F(s(g(b)))
F(g(a)) → G(b)
G(x) → G(x)
f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
G(x) → F(g(x))
F(g(a)) → G(b)
G(x) → G(x)
f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(g(a)) → G(b)
Used ordering: Polynomial interpretation [25,35]:
G(x) → F(g(x))
G(x) → G(x)
The value of delta used in the strict ordering is 16.
POL(a) = 4
POL(f(x1)) = 0
POL(g(x1)) = (2)x_1
POL(G(x1)) = (4)x_1
POL(b) = 0
POL(s(x1)) = (3)x_1
POL(F(x1)) = (2)x_1
f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
G(x) → F(g(x))
G(x) → G(x)
f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
G(x) → G(x)
f(g(a)) → f(s(g(b)))
f(f(x)) → b
g(x) → f(g(x))