Termination w.r.t. Q proof of /tmp/tmpOWPPAi/filliatre3.xml

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

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 AND

    ↳5 QDP

        ↳6 QDPOrderProof (⇔)

        ↳7 QDP

        ↳8 QDPOrderProof (⇔)

        ↳9 QDP

        ↳10 DependencyGraphProof (⇔)

        ↳11 QDP

        ↳12 QDPOrderProof (⇔)

        ↳13 QDP

        ↳14 QDPOrderProof (⇔)

        ↳15 QDP

        ↳16 PisEmptyProof (⇔)

        ↳17 TRUE

    ↳18 QDP

        ↳19 QDPOrderProof (⇔)

        ↳20 QDP

        ↳21 PisEmptyProof (⇔)

        ↳22 TRUE

(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) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
F(x0, x1, x2) = F(x0)
F'(x0, x1, x2) = F'(x1, x2)
F''(x0, x1) = F''(x1)
FOLDC(x0, x1, x2) = FOLDC(x0, x1, x2)
FOLDB(x0, x1, x2) = FOLDB(x0, x1, x2)

Tags:
F has argument tags [0,8,15] and root tag 0
F' has argument tags [15,0,0] and root tag 0
F'' has argument tags [3,0] and root tag 0
FOLDC has argument tags [0,0,3] and root tag 0
FOLDB has argument tags [0,0,15] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(0) = 0
POL(A) = 0
POL(B) = 1
POL(C) = 1
POL(F(x₁, x₂)) = x₁ + x₂
POL(F'(x₁, x₂)) = 0
POL(F''(x₁)) = 1
POL(FOLDB(x₁, x₂)) = x₁ + x₂
POL(FOLDC(x₁, x₂)) = x₁ + x₂
POL(f(x₁, x₂)) = x₁ + x₂
POL(f'(x₁, x₂)) = 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₃)) = 1 + x₂ + x₃

The following usable rules [FROCOS05] were oriented:

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), 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), C) → triple(a, b, s(c))

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

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.

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

F'(triple(a, b, c), A) → F''(foldB(triple(s(a), 0, c), b))
FOLDC(t, s(n)) → F(foldC(t, n), C)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
F(x0, x1, x2) = F(x0, x2)
F'(x0, x1, x2) = F'(x0)
F''(x0, x1) = F''(x0)
FOLDC(x0, x1, x2) = FOLDC(x0, x1)
FOLDB(x0, x1, x2) = FOLDB(x1)

Tags:
F has argument tags [8,1,2] and root tag 0
F' has argument tags [8,0,9] and root tag 0
F'' has argument tags [2,8] and root tag 2
FOLDC has argument tags [2,2,0] and root tag 2
FOLDB has argument tags [0,8,0] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented:

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), 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), C) → triple(a, b, s(c))

(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)) → FOLDC(triple(a, b, 0), 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:

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.

(10) DependencyGraphProof (EQUIVALENT transformation)

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

(11) 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))
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:

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.

(12) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

F'(triple(a, b, c), A) → FOLDB(triple(s(a), 0, c), b)
FOLDB(t, s(n)) → F(foldB(t, n), B)

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
F'(x0, x1, x2) = F'(x1)
F(x0, x1, x2) = F(x0, x1)
FOLDB(x0, x1, x2) = FOLDB(x0, x2)

Tags:
F' has argument tags [0,1,0] and root tag 2
F has argument tags [0,1,2] and root tag 2
FOLDB has argument tags [1,12,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented:

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

(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:

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.

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
F'(x0, x1, x2) = F'(x1, x2)
F(x0, x1, x2) = F(x0, x1, x2)

Tags:
F' has argument tags [4,0,0] and root tag 0
F has argument tags [7,0,1] and root tag 1

Comparison: MS
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

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

The following usable rules [FROCOS05] were oriented: none

(15) Obligation:

Q DP problem:
P is empty.
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.

(16) PisEmptyProof (EQUIVALENT transformation)

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

(17) TRUE

(18) 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.

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
FOLD(x0, x1, x2, x3) = FOLD(x3)

Tags:
FOLD has argument tags [0,0,0,1] and root tag 0

Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Polynomial interpretation [POLO]:

POL(FOLD(x₁, x₂, x₃)) = 1 + x₁ + x₂
POL(s(x₁)) = 1 + x₁

The following usable rules [FROCOS05] were oriented: none

(20) Obligation:

Q DP problem:
P is empty.
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) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) DependencyPairsProof (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) QDPOrderProof (EQUIVALENT transformation)

(7) Obligation:

(8) QDPOrderProof (EQUIVALENT transformation)

(9) Obligation:

(10) DependencyGraphProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPOrderProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPOrderProof (EQUIVALENT transformation)

(15) Obligation:

(16) PisEmptyProof (EQUIVALENT transformation)

(17) TRUE

(18) Obligation:

(19) QDPOrderProof (EQUIVALENT transformation)

(20) Obligation:

(21) PisEmptyProof (EQUIVALENT transformation)

(22) TRUE