0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 DependencyGraphProof (⇔)
↳11 QDP
↳12 QDPOrderProof (⇔)
↳13 QDP
↳14 QDPOrderProof (⇔)
↳15 QDP
↳16 PisEmptyProof (⇔)
↳17 TRUE
↳18 QDP
↳19 QDPOrderProof (⇔)
↳20 QDP
↳21 PisEmptyProof (⇔)
↳22 TRUE
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDB(t, s(n)) → FOLDB(t, n)
FOLDC(t, s(n)) → F(foldC(t, n), C)
FOLDC(t, s(n)) → FOLDC(t, n)
F(t, x) → F'(t, g(x))
F(t, x) → G(x)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
FOLD(t, x, s(n)) → F(fold(t, x, n), x)
FOLD(t, x, s(n)) → FOLD(t, x, n)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
FOLDC(t, s(n)) → F(foldC(t, n), C)
FOLDC(t, s(n)) → FOLDC(t, n)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDB(t, s(n)) → FOLDB(t, n)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → FOLDB(t, n)
POL(0) = 0
POL(A) = 0
POL(B) = 1
POL(C) = 1
POL(F(x1, x2)) = x1 + x2
POL(F'(x1, x2)) = 0
POL(F''(x1)) = 1
POL(FOLDB(x1, x2)) = x1 + x2
POL(FOLDC(x1, x2)) = x1 + x2
POL(f(x1, x2)) = x1 + x2
POL(f'(x1, x2)) = x1 + x2
POL(f''(x1)) = x1
POL(foldB(x1, x2)) = x1 + x2
POL(foldC(x1, x2)) = x1 + x2
POL(g(x1)) = x1
POL(s(x1)) = 1 + x1
POL(triple(x1, x2, x3)) = 1 + x2 + x3
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
f'(triple(a, b, c), C) → triple(a, b, s(c))
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
FOLDC(t, s(n)) → F(foldC(t, n), C)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDC(t, s(n)) → F(foldC(t, n), C)
POL(0) = 0
POL(A) = 0
POL(B) = 0
POL(C) = 1
POL(F(x1, x2)) = x1
POL(F'(x1, x2)) = x1
POL(F''(x1)) = x1
POL(FOLDB(x1, x2)) = x1
POL(FOLDC(x1, x2)) = x1 + x2
POL(f(x1, x2)) = x1 + x2
POL(f'(x1, x2)) = x1 + x2
POL(f''(x1)) = x1
POL(foldB(x1, x2)) = x1
POL(foldC(x1, x2)) = x1 + x2
POL(g(x1)) = x1
POL(s(x1)) = 1 + x1
POL(triple(x1, x2, x3)) = x3
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
f'(triple(a, b, c), C) → triple(a, b, s(c))
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)
POL(0) = 0
POL(A) = 0
POL(B) = 1
POL(C) = 1
POL(F(x1, x2)) = x1 + x2
POL(F'(x1, x2)) = 0
POL(FOLDB(x1, x2)) = x1 + x2
POL(f(x1, x2)) = x1
POL(f'(x1, x2)) = x1
POL(f''(x1)) = x1
POL(foldB(x1, x2)) = x1 + x2
POL(foldC(x1, x2)) = x1
POL(g(x1)) = 0
POL(s(x1)) = 1 + x1
POL(triple(x1, x2, x3)) = x2
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
foldC(t, 0) → t
f'(triple(a, b, c), C) → triple(a, b, s(c))
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
POL(A) = 0
POL(B) = 1
POL(C) = 1
POL(F(x1, x2)) = 0
POL(F'(x1, x2)) = 0
POL(g(x1)) = x1
POL(triple(x1, x2, x3)) = x2 + x3
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
FOLD(t, x, s(n)) → FOLD(t, x, n)
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FOLD(t, x, s(n)) → FOLD(t, x, n)
POL(FOLD(x1, x2, x3)) = 1 + x1 + x2
POL(s(x1)) = 1 + x1
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)