Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 2 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

FOLDC(t, s(n)) → FOLDC(t, n)
FOLDB(t, s(n)) → FOLDB(t, n)

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(A) = 0   
POL(B) = 0   
POL(C) = 0   
POL(F(x₁, x₂)) = 1 + x₁ + x₂   
POL(F'(x₁, x₂)) = 1 + x₁ + x₂   
POL(F''(x₁)) = x₁   
POL(FOLDB(x₁, x₂)) = x₁ + x₂   
POL(FOLDC(x₁, x₂)) = x₁ + x₂   
POL(f(x₁, x₂)) = 1 + x₁ + x₂   
POL(f'(x₁, x₂)) = 1 + x₁ + x₂   
POL(f''(x₁)) = x₁   
POL(foldB(x₁, x₂)) = x₁ + x₂   
POL(foldC(x₁, x₂)) = x₁ + x₂   
POL(g(x₁)) = x₁   
POL(s(x₁)) = 1 + x₁   
POL(triple(x₁, x₂, x₃)) = x₁ + x₂ + x₃   

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

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)

Strictly oriented rules of the TRS R:

f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(A) = 2   
POL(B) = 2   
POL(C) = 2   
POL(F(x₁, x₂)) = x₁ + x₂   
POL(F'(x₁, x₂)) = x₁ + x₂   
POL(F''(x₁)) = x₁   
POL(FOLDB(x₁, x₂)) = x₁ + 2·x₂   
POL(FOLDC(x₁, x₂)) = x₁ + 2·x₂   
POL(f(x₁, x₂)) = x₁ + x₂   
POL(f'(x₁, x₂)) = x₁ + x₂   
POL(f''(x₁)) = x₁   
POL(foldB(x₁, x₂)) = x₁ + 2·x₂   
POL(foldC(x₁, x₂)) = x₁ + 2·x₂   
POL(g(x₁)) = x₁   
POL(s(x₁)) = 1 + x₁   
POL(triple(x₁, x₂, x₃)) = x₁ + 2·x₂ + 2·x₃   

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))

The TRS R consists of the following rules:

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))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))

The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

F'(triple(a, b, c), B) → F(triple(a, b, c), A)
F(t, x) → F'(t, g(x))

Strictly oriented rules of the TRS R:

g(B) → A
g(C) → A
g(C) → B

Used ordering: Polynomial interpretation [POLO]:

POL(A) = 0   
POL(B) = 2   
POL(C) = 3   
POL(F(x₁, x₂)) = 1 + x₁ + x₂   
POL(F'(x₁, x₂)) = x₁ + x₂   
POL(g(x₁)) = x₁   
POL(triple(x₁, x₂, x₃)) = x₁ + x₂ + x₃   

(17) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

g(A) → A
g(B) → B
g(C) → C

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(19) TRUE

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FOLD(t, x, s(n)) → FOLD(t, x, n)

The TRS R consists of the following rules:

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)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FOLD(t, x, s(n)) → FOLD(t, x, n)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• FOLD(t, x, s(n)) → FOLD(t, x, n)
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

(24) TRUE