YES Termination w.r.t. Q proof of Secret_06_TRS_gen-1.ari

(0) Obligation:

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

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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:

F(c(a, z, x)) → B(a, z)
B(x, b(z, y)) → F(b(f(f(z)), c(x, z, y)))
B(x, b(z, y)) → B(f(f(z)), c(x, z, y))
B(x, b(z, y)) → F(f(z))
B(x, b(z, y)) → F(z)

The TRS R consists of the following rules:

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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 1 SCC with 1 less node.

(4) Obligation:

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

B(x, b(z, y)) → F(b(f(f(z)), c(x, z, y)))
F(c(a, z, x)) → B(a, z)
B(x, b(z, y)) → F(f(z))
B(x, b(z, y)) → F(z)

The TRS R consists of the following rules:

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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

(5) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule B(x, b(z, y)) → F(b(f(f(z)), c(x, z, y))) we obtained the following new rules [LPAR04]:

B(a, b(x1, x2)) → F(b(f(f(x1)), c(a, x1, x2))) → B(a, b(x1, x2)) → F(b(f(f(x1)), c(a, x1, x2)))

(6) Obligation:

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

F(c(a, z, x)) → B(a, z)
B(x, b(z, y)) → F(f(z))
B(x, b(z, y)) → F(z)
B(a, b(x1, x2)) → F(b(f(f(x1)), c(a, x1, x2)))

The TRS R consists of the following rules:

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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

(7) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule B(x, b(z, y)) → F(f(z)) we obtained the following new rules [LPAR04]:

B(a, b(x1, x2)) → F(f(x1)) → B(a, b(x1, x2)) → F(f(x1))

(8) Obligation:

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

F(c(a, z, x)) → B(a, z)
B(x, b(z, y)) → F(z)
B(a, b(x1, x2)) → F(b(f(f(x1)), c(a, x1, x2)))
B(a, b(x1, x2)) → F(f(x1))

The TRS R consists of the following rules:

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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

(9) TransformationProof (EQUIVALENT transformation)

By instantiating [LPAR04] the rule B(x, b(z, y)) → F(z) we obtained the following new rules [LPAR04]:

B(a, b(x1, x2)) → F(x1) → B(a, b(x1, x2)) → F(x1)

(10) Obligation:

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

F(c(a, z, x)) → B(a, z)
B(a, b(x1, x2)) → F(b(f(f(x1)), c(a, x1, x2)))
B(a, b(x1, x2)) → F(f(x1))
B(a, b(x1, x2)) → F(x1)

The TRS R consists of the following rules:

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


B(a, b(x1, x2)) → F(f(x1))
B(a, b(x1, x2)) → F(x1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(F(x1)) = 2A + 0A·x1

POL(c(x1, x2, x3)) = -I + -I·x1 + 1A·x2 + 1A·x3

POL(a) = 1A

POL(B(x1, x2)) = 0A + -I·x1 + 1A·x2

POL(b(x1, x2)) = 4A + 1A·x1 + 1A·x2

POL(f(x1)) = 4A + 0A·x1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
f(c(a, z, x)) → b(a, z)
b(y, z) → z

(12) Obligation:

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

F(c(a, z, x)) → B(a, z)
B(a, b(x1, x2)) → F(b(f(f(x1)), c(a, x1, x2)))

The TRS R consists of the following rules:

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


F(c(a, z, x)) → B(a, z)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:

POL(B(x1, x2)) = [1] + [4]x1 + [4]x2   
POL(F(x1)) = [1] + x1   
POL(a) = 0   
POL(b(x1, x2)) = [2] + [2]x1 + x2   
POL(c(x1, x2, x3)) = [1] + [4]x2   
POL(f(x1)) = [2] + [1/4]x1   
The value of delta used in the strict ordering is 1.
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
f(c(a, z, x)) → b(a, z)
b(y, z) → z

(14) Obligation:

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

B(a, b(x1, x2)) → F(b(f(f(x1)), c(a, x1, x2)))

The TRS R consists of the following rules:

f(c(a, z, x)) → b(a, z)
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y)))
b(y, z) → z

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

(15) DependencyGraphProof (EQUIVALENT transformation)

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

(16) TRUE