Term Rewriting System R:

   [t, n, x, a, b, 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)
   fold(t, x, 0) -> t
   fold(t, x, s(n)) -> f(fold(t, x, n), x)

Termination of R to be shown.


R contains the following Dependency Pairs: 


   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)
   FOLDB(t, s(n)) -> F(foldB(t, n), B)
   FOLDB(t, s(n)) -> FOLDB(t, n)
   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)

Furthermore, R contains two SCCs.


SCC1:

FOLDB(t, s(n)) -> FOLDB(t, n)
FOLDB(t, s(n)) -> F(foldB(t, n), B)
F'(triple(a, b, c), A) -> FOLDB(triple(s(a), 0, c), b)
FOLDC(t, s(n)) -> FOLDC(t, n)
F''(triple(a, b, c)) -> FOLDC(triple(a, b, 0), c)
F'(triple(a, b, c), A) -> F''(foldB(triple(s(a), 0, c), b))
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, x) -> F'(t, g(x))
FOLDC(t, s(n)) -> F(foldC(t, n), C)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(g(x_1)) = x_1
POL(f''(x_1)) = x_1
POL(s(x_1)) = x_1
POL(B) = 0
POL(F(x_1, x_2)) = x_1 + x_2
POL(F'(x_1, x_2)) = x_1 + x_2
POL(f'(x_1, x_2)) = x_1 + x_2
POL(f(x_1, x_2)) = x_1 + x_2
POL(foldB(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(C) = 0
POL(F''(x_1)) = x_1
POL(triple(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(FOLDB(x_1, x_2)) = x_1 + x_2
POL(foldC(x_1, x_2)) = x_1 + x_2
POL(A) = 0
POL(FOLDC(x_1, x_2)) = x_1 + x_2

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   fold(t, x, 0) -> t
   fold(t, x, s(n)) -> f(fold(t, x, n), x)


 This transformation is resulting in one new subcycle:


SCC1.MRR1:

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)) -> FOLDC(triple(a, b, 0), c)
F'(triple(a, b, c), A) -> F''(foldB(triple(s(a), 0, c), b))
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, x) -> F'(t, g(x))
FOLDB(t, s(n)) -> F(foldB(t, n), B)
FOLDB(t, s(n)) -> FOLDB(t, n)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(g(x_1)) = x_1
POL(f''(x_1)) = x_1
POL(s(x_1)) = 1 + x_1
POL(B) = 0
POL(F'(x_1, x_2)) = 1 + x_1 + x_2
POL(F(x_1, x_2)) = 1 + x_1 + x_2
POL(f'(x_1, x_2)) = 1 + x_1 + x_2
POL(f(x_1, x_2)) = 1 + x_1 + x_2
POL(foldB(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(C) = 0
POL(F''(x_1)) = x_1
POL(triple(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(FOLDB(x_1, x_2)) = x_1 + x_2
POL(foldC(x_1, x_2)) = x_1 + x_2
POL(A) = 0
POL(FOLDC(x_1, x_2)) = x_1 + x_2

The following Dependency Pairs can be deleted:

   FOLDC(t, s(n)) -> FOLDC(t, n)
   FOLDB(t, s(n)) -> FOLDB(t, n)

No rules of R can be deleted.


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1:

FOLDC(t, s(n)) -> F(foldC(t, n), C)
F''(triple(a, b, c)) -> FOLDC(triple(a, b, 0), c)
F'(triple(a, b, c), A) -> F''(foldB(triple(s(a), 0, c), b))
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, x) -> F'(t, g(x))
FOLDB(t, s(n)) -> F(foldB(t, n), B)
F'(triple(a, b, c), A) -> FOLDB(triple(s(a), 0, c), b)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   f''(triple(a, b, c)) -> foldC(triple(a, b, 0), c)
   foldC(t, s(n)) -> f(foldC(t, n), C)
   foldC(t, 0) -> t
   f(t, x) -> f'(t, g(x))
   f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
   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))
   foldB(t, s(n)) -> f(foldB(t, n), B)
   foldB(t, 0) -> t
   g(C) -> A
   g(B) -> B
   g(A) -> A
   g(C) -> B
   g(B) -> A
   g(C) -> C


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(g(x_1)) = x_1
POL(f''(x_1)) = x_1
POL(s(x_1)) = 1 + x_1
POL(B) = 0
POL(F'(x_1, x_2)) = x_1
POL(F(x_1, x_2)) = x_1
POL(f(x_1, x_2)) = x_1 + x_2
POL(f'(x_1, x_2)) = x_1 + x_2
POL(foldB(x_1, x_2)) = x_1
POL(0) = 0
POL(C) = 1
POL(F''(x_1)) = x_1
POL(triple(x_1, x_2, x_3)) = x_3
POL(FOLDB(x_1, x_2)) = x_1
POL(foldC(x_1, x_2)) = x_1 + x_2
POL(A) = 0
POL(FOLDC(x_1, x_2)) = x_1 + x_2

 resulting in one subcycle.


SCC1.MRR1.MRR1.Polo1:

FOLDB(t, s(n)) -> F(foldB(t, n), B)
F'(triple(a, b, c), A) -> FOLDB(triple(s(a), 0, c), b)
F(t, x) -> F'(t, g(x))
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   f''(triple(a, b, c)) -> foldC(triple(a, b, 0), c)
   foldC(t, s(n)) -> f(foldC(t, n), C)
   foldC(t, 0) -> t
   f(t, x) -> f'(t, g(x))
   f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
   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))
   foldB(t, s(n)) -> f(foldB(t, n), B)
   foldB(t, 0) -> t


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(g(x_1)) = 0
POL(f''(x_1)) = x_1
POL(s(x_1)) = 1
POL(B) = 0
POL(F'(x_1, x_2)) = x_1
POL(F(x_1, x_2)) = x_1
POL(f(x_1, x_2)) = x_1
POL(f'(x_1, x_2)) = x_1
POL(foldB(x_1, x_2)) = x_1
POL(0) = 0
POL(C) = 0
POL(triple(x_1, x_2, x_3)) = x_2
POL(FOLDB(x_1, x_2)) = x_1 + x_2
POL(foldC(x_1, x_2)) = x_1
POL(A) = 0

 resulting in one subcycle.


SCC1.MRR1.MRR1.Polo1.Polo1:

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

On this Scc, a Narrowing SCC transformation can be performed.
 
As a result of transforming the rule 

   F(t, x) -> F'(t, g(x))
six new Dependency Pairs
are created:


   F(t, C) -> F'(t, A)
   F(t, B) -> F'(t, B)
   F(t, A) -> F'(t, A)
   F(t, C) -> F'(t, B)
   F(t, B) -> F'(t, A)
   F(t, C) -> F'(t, C)

The transformation is resulting in no subcycles.


SCC2:

FOLD(t, x, s(n)) -> FOLD(t, x, n)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(FOLD(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3

The following Dependency Pairs can be deleted:

   FOLD(t, x, s(n)) -> FOLD(t, x, n)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 2.959 seconds.