Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema

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

0 QTRS

↳1 QTRS Reverse (⇔, 0 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 QDP

↳5 QDPOrderProof (⇔, 25 ms)

↳6 QDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 QDP

↳9 QDPOrderProof (⇔, 47 ms)

↳10 QDP

↳11 QDPOrderProof (⇔, 673 ms)

↳12 QDP

↳13 DependencyGraphProof (⇔, 0 ms)

↳14 TRUE

(0) Obligation:

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

d(a(x)) → b(d(x))
b(x) → a(a(a(x)))
c(d(c(x))) → a(d(x))
b(d(d(x))) → c(c(d(d(c(x)))))

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

a(d(x)) → d(b(x))
b(x) → a(a(a(x)))
c(d(c(x))) → d(a(x))
d(d(b(x))) → c(d(d(c(c(x)))))

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

A(d(x)) → D(b(x))
A(d(x)) → B(x)
B(x) → A(a(a(x)))
B(x) → A(a(x))
B(x) → A(x)
C(d(c(x))) → D(a(x))
C(d(c(x))) → A(x)
D(d(b(x))) → C(d(d(c(c(x)))))
D(d(b(x))) → D(d(c(c(x))))
D(d(b(x))) → D(c(c(x)))
D(d(b(x))) → C(c(x))
D(d(b(x))) → C(x)

The TRS R consists of the following rules:

a(d(x)) → d(b(x))
b(x) → a(a(a(x)))
c(d(c(x))) → d(a(x))
d(d(b(x))) → c(d(d(c(c(x)))))

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

(5) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

A(d(x)) → B(x)
C(d(c(x))) → A(x)
D(d(b(x))) → D(c(c(x)))
D(d(b(x))) → C(c(x))
D(d(b(x))) → C(x)

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

POL(A(x₁)) = x₁
POL(B(x₁)) = x₁
POL(C(x₁)) = x₁
POL(D(x₁)) = 1 + x₁
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(c(x₁)) = x₁
POL(d(x₁)) = 1 + x₁

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

b(x) → a(a(a(x)))
a(d(x)) → d(b(x))
d(d(b(x))) → c(d(d(c(c(x)))))
c(d(c(x))) → d(a(x))

(6) Obligation:

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

A(d(x)) → D(b(x))
B(x) → A(a(a(x)))
B(x) → A(a(x))
B(x) → A(x)
C(d(c(x))) → D(a(x))
D(d(b(x))) → C(d(d(c(c(x)))))
D(d(b(x))) → D(d(c(c(x))))

The TRS R consists of the following rules:

a(d(x)) → d(b(x))
b(x) → a(a(a(x)))
c(d(c(x))) → d(a(x))
d(d(b(x))) → c(d(d(c(c(x)))))

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

D(d(b(x))) → C(d(d(c(c(x)))))
C(d(c(x))) → D(a(x))
D(d(b(x))) → D(d(c(c(x))))

The TRS R consists of the following rules:

a(d(x)) → d(b(x))
b(x) → a(a(a(x)))
c(d(c(x))) → d(a(x))
d(d(b(x))) → c(d(d(c(c(x)))))

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

(9) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

D(d(b(x))) → D(d(c(c(x))))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( C(x₁) ) = 1

POL( D(x₁) ) = max{0, 2x₁ - 1}

POL( d(x₁) ) = max{0, x₁ - 1}

POL( b(x₁) ) = 2

POL( c(x₁) ) = max{0, -2}

POL( a(x₁) ) = 1

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

d(d(b(x))) → c(d(d(c(c(x)))))
c(d(c(x))) → d(a(x))
a(d(x)) → d(b(x))
b(x) → a(a(a(x)))

(10) Obligation:

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

D(d(b(x))) → C(d(d(c(c(x)))))
C(d(c(x))) → D(a(x))

The TRS R consists of the following rules:

a(d(x)) → d(b(x))
b(x) → a(a(a(x)))
c(d(c(x))) → d(a(x))
d(d(b(x))) → c(d(d(c(c(x)))))

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.

C(d(c(x))) → D(a(x))

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

POL(D(x₁)) = 0A +
[ -I, -I, 0A ]

· x₁

POL(d(x₁)) =
/ 0A \

| 0A |

\ 1A /

+
/ -I 0A 0A \

| 1A -I 0A |

\ 0A 0A 1A /

· x₁

POL(b(x₁)) =
/ 1A \

| 1A |

\ 0A /

+
/ 0A 0A 1A \

| 0A 0A 1A |

\ -I -I 0A /

· x₁

POL(C(x₁)) = 0A +
[ -I, 0A, -I ]

· x₁

POL(c(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ 0A 0A 0A \

| -I -I 0A |

\ -I -I 0A /

· x₁

POL(a(x₁)) =
/ 0A \

| 0A |

\ 0A /

+
/ -I -I 0A \

| 0A 0A 1A |

\ -I -I 0A /

· x₁

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

d(d(b(x))) → c(d(d(c(c(x)))))
c(d(c(x))) → d(a(x))
a(d(x)) → d(b(x))
b(x) → a(a(a(x)))

(12) Obligation:

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

D(d(b(x))) → C(d(d(c(c(x)))))

The TRS R consists of the following rules:

a(d(x)) → d(b(x))
b(x) → a(a(a(x)))
c(d(c(x))) → d(a(x))
d(d(b(x))) → c(d(d(c(c(x)))))

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

(13) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) QTRS Reverse (EQUIVALENT transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) QDPOrderProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Obligation:

(9) QDPOrderProof (EQUIVALENT transformation)

(10) Obligation:

(11) QDPOrderProof (EQUIVALENT transformation)

(12) Obligation:

(13) DependencyGraphProof (EQUIVALENT transformation)

(14) TRUE