0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 QDPOrderProof (⇔)
↳16 QDP
↳17 QDPOrderProof (⇔)
↳18 QDP
↳19 DependencyGraphProof (⇔)
↳20 TRUE
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
f(0) → 0
f(s(x)) → -(s(x), g(f(x)))
g(0) → s(0)
g(s(x)) → -(s(x), f(g(x)))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
f(0) → 0
f(s(x)) → -(s(x), g(f(x)))
g(0) → s(0)
g(s(x)) → -(s(x), f(g(x)))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
-1(s(x), s(y)) → -1(x, y)
F(s(x)) → -1(s(x), g(f(x)))
F(s(x)) → G(f(x))
F(s(x)) → F(x)
G(s(x)) → -1(s(x), f(g(x)))
G(s(x)) → F(g(x))
G(s(x)) → G(x)
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
f(0) → 0
f(s(x)) → -(s(x), g(f(x)))
g(0) → s(0)
g(s(x)) → -(s(x), f(g(x)))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
-1(s(x), s(y)) → -1(x, y)
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
f(0) → 0
f(s(x)) → -(s(x), g(f(x)))
g(0) → s(0)
g(s(x)) → -(s(x), f(g(x)))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
-1(s(x), s(y)) → -1(x, y)
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
-1(s(x), s(y)) → -1(x, y)
From the DPs we obtained the following set of size-change graphs:
F(s(x)) → G(f(x))
G(s(x)) → F(g(x))
F(s(x)) → F(x)
G(s(x)) → G(x)
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
f(0) → 0
f(s(x)) → -(s(x), g(f(x)))
g(0) → s(0)
g(s(x)) → -(s(x), f(g(x)))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(x)) → F(x)
G(s(x)) → G(x)
POL(-(x1, x2)) = 1 + x1
POL(0) = 0
POL(F(x1)) = 1 + x1
POL(G(x1)) = 1 + x1
POL(f(x1)) = 1 + x1
POL(g(x1)) = 1 + x1
POL(s(x1)) = 1 + x1
-(x, 0) → x
g(s(x)) → -(s(x), f(g(x)))
g(0) → s(0)
-(s(x), s(y)) → -(x, y)
-(0, s(y)) → 0
f(s(x)) → -(s(x), g(f(x)))
f(0) → 0
F(s(x)) → G(f(x))
G(s(x)) → F(g(x))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
f(0) → 0
f(s(x)) → -(s(x), g(f(x)))
g(0) → s(0)
g(s(x)) → -(s(x), f(g(x)))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(x)) → G(f(x))
POL(-(x1, x2)) = x1
POL(0) = 1
POL(F(x1)) = x1
POL(G(x1)) = x1
POL(f(x1)) = x1
POL(g(x1)) = 1 + x1
POL(s(x1)) = 1 + x1
-(x, 0) → x
g(s(x)) → -(s(x), f(g(x)))
g(0) → s(0)
-(s(x), s(y)) → -(x, y)
-(0, s(y)) → 0
f(s(x)) → -(s(x), g(f(x)))
f(0) → 0
G(s(x)) → F(g(x))
-(x, 0) → x
-(0, s(y)) → 0
-(s(x), s(y)) → -(x, y)
f(0) → 0
f(s(x)) → -(s(x), g(f(x)))
g(0) → s(0)
g(s(x)) → -(s(x), f(g(x)))
-(x0, 0)
-(0, s(x0))
-(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))