g(A) -> A

g(B) -> A

g(B) -> B

g(C) -> A

g(C) -> B

g(C) -> C

foldB(

foldB(

foldC(

foldC(

f(

f'(triple(

f'(triple(

f'(triple(

f''(triple(

R

↳Dependency Pair Analysis

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)

Furthermore,

R

↳DPs

→DP Problem 1

↳Polynomial Ordering

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

The following dependency pairs can be strictly oriented:

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

FOLDB(t, s(n)) -> F(foldB(t,n), B)

Additionally, the following usable rules w.r.t. to the implicit AFS can be oriented:

foldB(t, 0) ->t

foldB(t, s(n)) -> f(foldB(t,n), B)

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(t,x) -> f'(t, g(x))

foldC(t, 0) ->t

foldC(t, s(n)) -> f(foldC(t,n), C)

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(foldB(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(FOLDC(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(triple(x)_{1}, x_{2}, x_{3})= x _{2}_{ }^{ }_{ }^{ }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(foldC(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(FOLDB(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F''(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(C)= 0 _{ }^{ }_{ }^{ }POL(B)= 0 _{ }^{ }_{ }^{ }POL(g(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(F'(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(f''(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(A)= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Dependency Graph

**F'(triple( a, b, c), A) -> FOLDB(triple(s(a), 0, c), 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)

Using the Dependency Graph the DP problem was split into 1 DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳DGraph

...

→DP Problem 3

↳Polynomial Ordering

**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 dependency pairs can be strictly oriented:

FOLDC(t, s(n)) -> F(foldC(t,n), C)

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

Additionally, the following usable rules w.r.t. to the implicit AFS can be oriented:

foldB(t, 0) ->t

foldB(t, s(n)) -> f(foldB(t,n), B)

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(t,x) -> f'(t, g(x))

foldC(t, 0) ->t

foldC(t, s(n)) -> f(foldC(t,n), C)

g(A) -> A

g(B) -> A

g(B) -> B

g(C) -> A

g(C) -> B

g(C) -> C

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(foldB(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(FOLDC(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(triple(x)_{1}, x_{2}, x_{3})= x _{3}_{ }^{ }_{ }^{ }POL(f'(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(foldC(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F''(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(C)= 1 _{ }^{ }_{ }^{ }POL(B)= 0 _{ }^{ }_{ }^{ }POL(g(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F'(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(f''(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(A)= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳DGraph

...

→DP Problem 4

↳Dependency Graph

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

Using the Dependency Graph the DP problem was split into 1 DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳DGraph

...

→DP Problem 5

↳Narrowing Transformation

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

On this DP problem, a Narrowing SCC transformation can be performed.

As a result of transforming the rule

six new Dependency Pairs are created:

F(t,x) -> F'(t, g(x))

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

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

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

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

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

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

The transformation is resulting in no new DP problems.

Duration:

0:01 minutes