Termination w.r.t. Q proof of Secret_07_TRS

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

0 QTRS

↳1 DependencyPairsProof (⇔, 0 ms)

↳2 QDP

↳3 DependencyGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 QDP

        ↳6 UsableRulesProof (⇔, 0 ms)

        ↳7 QDP

        ↳8 QDPOrderProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 PisEmptyProof (⇔, 0 ms)

        ↳11 YES

    ↳12 QDP

        ↳13 UsableRulesProof (⇔, 0 ms)

        ↳14 QDP

        ↳15 TransformationProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 QDPBoundsTAProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QDPBoundsTAProof (⇔, 0 ms)

        ↳20 QDP

        ↳21 PisEmptyProof (⇔, 0 ms)

        ↳22 YES

    ↳23 QDP

        ↳24 QDPOrderProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 TransformationProof (⇔, 0 ms)

        ↳27 QDP

        ↳28 QDPOrderProof (⇔, 467 ms)

        ↳29 QDP

        ↳30 PisEmptyProof (⇔, 0 ms)

        ↳31 YES

(0) Obligation:

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

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, 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:

H(x, x) → H(a, b)
G(g(x, a), y) → G(g(a, y), g(a, x))
G(g(x, a), y) → G(a, y)
G(g(x, a), y) → G(a, x)
F(g(x, y)) → G(g(f(f(y)), h(a, a)), x)
F(g(x, y)) → G(f(f(y)), h(a, a))
F(g(x, y)) → F(f(y))
F(g(x, y)) → F(y)
F(g(x, y)) → H(a, a)
H(h(f(f(x)), y), h(z, v)) → H(h(f(z), f(f(f(y)))), h(v, x))
H(h(f(f(x)), y), h(z, v)) → H(f(z), f(f(f(y))))
H(h(f(f(x)), y), h(z, v)) → F(z)
H(h(f(f(x)), y), h(z, v)) → F(f(f(y)))
H(h(f(f(x)), y), h(z, v)) → F(f(y))
H(h(f(f(x)), y), h(z, v)) → F(y)
H(h(f(f(x)), y), h(z, v)) → H(v, x)

The TRS R consists of the following rules:

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, 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 3 SCCs with 11 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

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

G(g(x, a), y) → G(g(a, y), g(a, x))

The TRS R consists of the following rules:

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, 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:

G(g(x, a), y) → G(g(a, y), g(a, x))

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

(8) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

G(g(x, a), y) → G(g(a, y), g(a, x))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:

POL(G(x₁, x₂)) = [4]x₁ + [2]x₂
POL(a) = [1/2]
POL(g(x₁, x₂)) = [1/4]x₁ + [1/2]x₂

The value of delta used in the strict ordering is 1/4.
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(9) Obligation:

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

(10) PisEmptyProof (EQUIVALENT transformation)

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

(11) YES

(12) Obligation:

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

F(g(x, y)) → F(y)
F(g(x, y)) → F(f(y))

The TRS R consists of the following rules:

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))

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

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

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

F(g(x, y)) → F(y)
F(g(x, y)) → F(f(y))

The TRS R consists of the following rules:

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))

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

(15) TransformationProof (EQUIVALENT transformation)

By narrowing [LPAR04] the rule F(g(x, y)) → F(f(y)) at position [0] we obtained the following new rules [LPAR04]:

F(g(y0, g(x0, x1))) → F(g(g(f(f(x1)), h(a, a)), x0)) → F(g(y0, g(x0, x1))) → F(g(g(f(f(x1)), h(a, a)), x0))

(16) Obligation:

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

F(g(x, y)) → F(y)
F(g(y0, g(x0, x1))) → F(g(g(f(f(x1)), h(a, a)), x0))

The TRS R consists of the following rules:

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))

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

(17) QDPBoundsTAProof (EQUIVALENT transformation)

The DP-Problem (P, R) could be shown to be Match-(raise-)DP-Bounded [TAB_NONLEFTLINEAR] by 1 for the Rule:

F(g(x, y)) → F(y)

by considering the usable rules:

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))

The compatible tree automaton used to show the Match-(raise-)DP-Boundedness is represented by:
final states : [0]
transitions:
#0() → 13
F0(1) → 0
f0(6) → 5
f0(5) → 4
a0() → 14
h0(8, 9) → 7
g0(4, 7) → 3
g0(3, 10) → 15
F0(2) → 0
b0() → 11
h0(8, 11) → 7
F0(10) → 0
f0(10) → 12
f0(12) → 4
g0(3, 3) → 4
F0(15) → 0
f0(13) → 16
f0(15) → 4
h0(14, 9) → 7
h0(14, 11) → 7
h0(8, 14) → 7
h0(14, 14) → 7
g0(3, 13) → 15
f0(16) → 4
F1(13) → 0
F0(13) → 0

(18) Obligation:

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

F(g(y0, g(x0, x1))) → F(g(g(f(f(x1)), h(a, a)), x0))

The TRS R consists of the following rules:

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))

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

(19) QDPBoundsTAProof (EQUIVALENT transformation)

The DP-Problem (P, R) could be shown to be Match-(raise-)DP-Bounded [TAB_NONLEFTLINEAR] by 0 for the Rule:

F(g(y0, g(x0, x1))) → F(g(g(f(f(x1)), h(a, a)), x0))

by considering the usable rules:

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))

The compatible tree automaton used to show the Match-(raise-)DP-Boundedness is represented by:
final states : [0]
transitions:
#0() → 12
f0(5) → 4
f0(4) → 3
a0() → 13
h0(7, 8) → 6
g0(3, 6) → 2
g0(2, 9) → 14
F0(1) → 0
b0() → 10
h0(7, 10) → 6
f0(9) → 11
f0(11) → 3
g0(2, 2) → 3
f0(12) → 15
f0(14) → 3
h0(13, 8) → 6
h0(13, 10) → 6
h0(7, 13) → 6
h0(13, 13) → 6
g0(2, 12) → 14
F0(14) → 0
f0(15) → 3

(20) Obligation:

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

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, 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.

(22) YES

(23) Obligation:

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

H(h(f(f(x)), y), h(z, v)) → H(v, x)
H(h(f(f(x)), y), h(z, v)) → H(h(f(z), f(f(f(y)))), h(v, x))

The TRS R consists of the following rules:

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))

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

(24) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

H(h(f(f(x)), y), h(z, v)) → H(v, x)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(H(x₁, x₂)) = x₁ + x₂
POL(a) = 0
POL(b) = 0
POL(f(x₁)) = x₁
POL(g(x₁, x₂)) = 0
POL(h(x₁, x₂)) = 1 + x₁ + x₂

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

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))
g(g(x, a), y) → g(g(a, y), g(a, x))

(25) Obligation:

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

H(h(f(f(x)), y), h(z, v)) → H(h(f(z), f(f(f(y)))), h(v, x))

The TRS R consists of the following rules:

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))

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

(26) TransformationProof (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule H(h(f(f(x)), y), h(z, v)) → H(h(f(z), f(f(f(y)))), h(v, x)) we obtained the following new rules [LPAR04]:

H(h(f(f(x0)), x1), h(f(y_0), x3)) → H(h(f(f(y_0)), f(f(f(x1)))), h(x3, x0)) → H(h(f(f(x0)), x1), h(f(y_0), x3)) → H(h(f(f(y_0)), f(f(f(x1)))), h(x3, x0))

(27) Obligation:

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

H(h(f(f(x0)), x1), h(f(y_0), x3)) → H(h(f(f(y_0)), f(f(f(x1)))), h(x3, x0))

The TRS R consists of the following rules:

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))

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

(28) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

H(h(f(f(x0)), x1), h(f(y_0), x3)) → H(h(f(f(y_0)), f(f(f(x1)))), h(x3, x0))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(H(x₁, x₂)) = 0A +
[ 1A, -I, -I ]

· x₁ +
[ -I, 3A, 2A ]

· x₂

POL(h(x₁, x₂)) =
/ 2A \

| 3A |

\ 3A /

+
/ 0A -I -I \

| 2A -I 2A |

\ -I -I -I /

· x₁ +
/ -I 3A -I \

| 3A 3A 3A |

\ -I -I -I /

· x₂

POL(f(x₁)) =
/ 3A \

| 1A |

\ 0A /

+
/ 3A -I 3A \

| -I -I -I |

\ -I 3A 0A /

· x₁

POL(g(x₁, x₂)) =
/ 0A \

| 0A |

\ 1A /

+
/ -I 1A -I \

| -I 0A -I |

\ 1A 2A -I /

· x₁ +
/ -I -I -I \

| -I -I -I |

\ -I 1A -I /

· x₂

POL(a) =
/ 1A \

| 0A |

\ 0A /

POL(b) =
/ 0A \

| -I |

\ 0A /

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

f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(x, x) → h(a, b)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))
g(g(x, a), y) → g(g(a, y), g(a, x))

(29) Obligation:

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

h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))

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

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

(7) Obligation:

(8) QDPOrderProof (EQUIVALENT transformation)

(9) Obligation:

(10) PisEmptyProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

(15) TransformationProof (EQUIVALENT transformation)

(16) Obligation:

(17) QDPBoundsTAProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPBoundsTAProof (EQUIVALENT transformation)

(20) Obligation:

(21) PisEmptyProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) QDPOrderProof (EQUIVALENT transformation)

(25) Obligation:

(26) TransformationProof (EQUIVALENT transformation)

(27) Obligation:

(28) QDPOrderProof (EQUIVALENT transformation)

(29) Obligation:

(30) PisEmptyProof (EQUIVALENT transformation)

(31) YES