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)
↳ QTRS
↳ DependencyPairsProof
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)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
F(t, x) → G(x)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
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) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
F(t, x) → G(x)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
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) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDC(t, s(n)) → F(foldC(t, n), C)
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) → F''(foldB(triple(s(a), 0, c), b))
FOLDB(t, s(n)) → FOLDB(t, n)
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FOLDB(t, s(n)) → F(foldB(t, n), B)
FOLDB(t, s(n)) → FOLDB(t, n)
Used ordering: Polynomial interpretation [25,35]:
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDC(t, s(n)) → F(foldC(t, n), C)
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) → F''(foldB(triple(s(a), 0, c), b))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
The value of delta used in the strict ordering is 2.
POL(F''(x1)) = (4)x_1
POL(f''(x1)) = (4)x_1
POL(f(x1, x2)) = x_1
POL(g(x1)) = 0
POL(C) = 0
POL(FOLDC(x1, x2)) = (4)x_1
POL(A) = 0
POL(triple(x1, x2, x3)) = x_2
POL(0) = 0
POL(f'(x1, x2)) = x_1
POL(foldC(x1, x2)) = x_1
POL(F'(x1, x2)) = (2)x_1
POL(B) = 0
POL(foldB(x1, x2)) = (2)x_1
POL(s(x1)) = 1 + x_1
POL(FOLDB(x1, x2)) = (4)x_1 + (2)x_2
POL(F(x1, x2)) = (2)x_1
foldB(t, 0) → t
foldC(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
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), C) → triple(a, b, s(c))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
FOLDC(t, s(n)) → FOLDC(t, n)
F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), 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)
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
FOLDC(t, s(n)) → FOLDC(t, n)
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)
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)
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)
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))
Used ordering: Polynomial interpretation [25,35]:
FOLDC(t, s(n)) → F(foldC(t, n), C)
F(t, x) → F'(t, g(x))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
The value of delta used in the strict ordering is 1.
POL(F''(x1)) = (4)x_1
POL(f''(x1)) = 3 + x_1
POL(f(x1, x2)) = 3 + x_1 + x_2
POL(g(x1)) = x_1
POL(C) = 1
POL(FOLDC(x1, x2)) = (4)x_1 + (4)x_2
POL(A) = 0
POL(triple(x1, x2, x3)) = (4)x_2 + x_3
POL(0) = 0
POL(f'(x1, x2)) = 3 + x_1 + x_2
POL(foldC(x1, x2)) = 3 + x_1 + x_2
POL(F'(x1, x2)) = 1 + (4)x_1 + x_2
POL(B) = 1
POL(foldB(x1, x2)) = x_1 + x_2
POL(s(x1)) = 4 + x_1
POL(F(x1, x2)) = 1 + (4)x_1 + (3)x_2
foldB(t, 0) → t
g(C) → C
foldC(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f(t, x) → f'(t, g(x))
foldC(t, s(n)) → f(foldC(t, n), C)
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), C) → triple(a, b, s(c))
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
FOLDC(t, s(n)) → F(foldC(t, n), C)
F(t, x) → F'(t, g(x))
F''(triple(a, b, c)) → FOLDC(triple(a, b, 0), c)
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)