0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔)
↳7 QDP
↳8 MRRProof (⇔)
↳9 QDP
↳10 MRRProof (⇔)
↳11 QDP
↳12 DependencyGraphProof (⇔)
↳13 QDP
↳14 UsableRulesProof (⇔)
↳15 QDP
↳16 MRRProof (⇔)
↳17 QDP
↳18 PisEmptyProof (⇔)
↳19 TRUE
↳20 QDP
↳21 UsableRulesProof (⇔)
↳22 QDP
↳23 QDPSizeChangeProof (⇔)
↳24 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)
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)
foldB(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)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
f'(triple(a, b, c), C) → triple(a, b, s(c))
FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → FOLDB(t, n)
POL(0) = 0
POL(A) = 0
POL(B) = 0
POL(C) = 0
POL(F(x1, x2)) = 1 + x1 + x2
POL(F'(x1, x2)) = 1 + x1 + x2
POL(F''(x1)) = x1
POL(FOLDB(x1, x2)) = x1 + x2
POL(FOLDC(x1, x2)) = x1 + x2
POL(f(x1, x2)) = 1 + x1 + x2
POL(f'(x1, x2)) = 1 + 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)) = x1 + x2 + x3
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)
foldB(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)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
f'(triple(a, b, c), C) → triple(a, b, s(c))
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), A) → f''(foldB(triple(s(a), 0, c), b))
POL(0) = 0
POL(A) = 2
POL(B) = 2
POL(C) = 2
POL(F(x1, x2)) = x1 + x2
POL(F'(x1, x2)) = x1 + x2
POL(F''(x1)) = x1
POL(FOLDB(x1, x2)) = x1 + 2·x2
POL(FOLDC(x1, x2)) = x1 + 2·x2
POL(f(x1, x2)) = x1 + x2
POL(f'(x1, x2)) = x1 + x2
POL(f''(x1)) = x1
POL(foldB(x1, x2)) = x1 + 2·x2
POL(foldC(x1, x2)) = x1 + 2·x2
POL(g(x1)) = x1
POL(s(x1)) = 1 + x1
POL(triple(x1, x2, x3)) = x1 + 2·x2 + 2·x3
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)
FOLDC(t, s(n)) → F(foldC(t, n), C)
FOLDB(t, s(n)) → F(foldB(t, n), B)
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), 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)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
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))
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), 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)
foldC(t, 0) → t
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
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
F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))
g(B) → A
g(C) → A
g(C) → B
POL(A) = 0
POL(B) = 2
POL(C) = 3
POL(F(x1, x2)) = 1 + x1 + x2
POL(F'(x1, x2)) = x1 + x2
POL(g(x1)) = x1
POL(triple(x1, x2, x3)) = x1 + x2 + x3
g(A) → A
g(B) → B
g(C) → C
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)
FOLD(t, x, s(n)) → FOLD(t, x, n)
From the DPs we obtained the following set of size-change graphs: