YES
Termination w.r.t. Q proof of ../tpdb/TRS/Zantema/z30.trs
Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(a, f(b, x))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, x)
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(a, f(b, x)))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, x))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))
The TRS R consists of the following rules:
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(a, f(b, x))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, x)
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(a, f(b, x)))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, x))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))
The TRS R consists of the following rules:
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
Q DP problem:
The TRS P consists of the following rules:
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))
The TRS R consists of the following rules:
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
First, we A-transformed [17] the QDP-Problem.
Then we obtain the following A-transformed DP problem.
The pairs P are:
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
and the Q and R are:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))
Q is empty.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
No dependency pairs are removed.
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [25]:
POL(a(x1)) = x1
POL(a1(x1)) = x1
POL(b(x1)) = x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ RFCMatchBoundsDPProof
Q DP problem:
The TRS P consists of the following rules:
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
The TRS R consists of the following rules:
a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 3.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
To find matches we regarded all rules of R and P:
a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
44, 45, 51, 47, 48, 50, 49, 46, 59, 55, 56, 52, 53, 58, 57, 54, 67, 63, 64, 60, 61, 66, 65, 62, 68, 72, 73, 71, 70, 69, 80, 81, 79, 78, 76, 77, 75, 74, 88, 89, 87, 86, 84, 85, 83, 82, 96, 97, 95, 94, 92, 93, 91, 90, 104, 105, 103, 102, 100, 101, 99, 98, 112, 113, 111, 110, 108, 109, 107, 106, 121, 117, 118, 114, 115, 120, 119, 116, 129, 125, 126, 122, 123, 128, 127, 124, 136, 137, 135, 134, 132, 133, 131, 130
Node 44 is start node and node 45 is final node.
Those nodes are connect through the following edges:
- 44 to 46 labelled a1_1(0)
- 44 to 49 labelled a1_1(0)
- 44 to 50 labelled a1_1(0)
- 44 to 54 labelled a1_1(1)
- 44 to 57 labelled a1_1(1)
- 44 to 58 labelled a1_1(1)
- 44 to 62 labelled a1_1(1)
- 44 to 65 labelled a1_1(1)
- 44 to 66 labelled a1_1(1)
- 44 to 68 labelled a1_1(2)
- 44 to 71 labelled a1_1(2)
- 44 to 72 labelled a1_1(2)
- 44 to 76 labelled a1_1(2)
- 44 to 100 labelled a1_1(2)
- 44 to 103 labelled a1_1(2)
- 44 to 104 labelled a1_1(2)
- 44 to 84 labelled a1_1(2)
- 44 to 92 labelled a1_1(2)
- 44 to 95 labelled a1_1(2)
- 44 to 116 labelled a1_1(3)
- 44 to 119 labelled a1_1(3)
- 44 to 120 labelled a1_1(3)
- 44 to 124 labelled a1_1(3)
- 44 to 127 labelled a1_1(3)
- 44 to 128 labelled a1_1(3)
- 44 to 132 labelled a1_1(2)
- 44 to 135 labelled a1_1(2)
- 44 to 136 labelled a1_1(2)
- 45 to 45 labelled #_1(0)
- 51 to 45 labelled b_1(0)
- 47 to 48 labelled b_1(0)
- 48 to 49 labelled a_1(0)
- 48 to 60 labelled a_1(1)
- 50 to 51 labelled a_1(0)
- 49 to 50 labelled a_1(0)
- 49 to 52 labelled a_1(1)
- 46 to 47 labelled a_1(0)
- 59 to 45 labelled b_1(1)
- 59 to 54 labelled b_1(1)
- 59 to 74 labelled b_1(1)
- 55 to 56 labelled b_1(1)
- 56 to 57 labelled a_1(1)
- 56 to 90 labelled a_1(2)
- 56 to 98 labelled a_1(2)
- 56 to 130 labelled a_1(2)
- 52 to 53 labelled b_1(1)
- 53 to 54 labelled a_1(1)
- 53 to 74 labelled a_1(2)
- 58 to 59 labelled a_1(1)
- 57 to 58 labelled a_1(1)
- 57 to 52 labelled a_1(1)
- 54 to 55 labelled a_1(1)
- 67 to 57 labelled b_1(1)
- 67 to 90 labelled b_1(1)
- 67 to 98 labelled b_1(1)
- 67 to 130 labelled b_1(1)
- 63 to 64 labelled b_1(1)
- 64 to 65 labelled a_1(1)
- 64 to 98 labelled a_1(2)
- 64 to 90 labelled a_1(2)
- 64 to 130 labelled a_1(2)
- 60 to 61 labelled b_1(1)
- 61 to 62 labelled a_1(1)
- 61 to 106 labelled a_1(2)
- 61 to 74 labelled a_1(2)
- 66 to 67 labelled a_1(1)
- 65 to 66 labelled a_1(1)
- 65 to 52 labelled a_1(1)
- 65 to 82 labelled a_1(2)
- 62 to 63 labelled a_1(1)
- 68 to 69 labelled a_1(2)
- 72 to 73 labelled a_1(2)
- 73 to 54 labelled b_1(2)
- 73 to 55 labelled b_1(2)
- 73 to 57 labelled b_1(2)
- 73 to 87 labelled b_1(2)
- 73 to 84 labelled b_1(2)
- 73 to 74 labelled b_1(2)
- 73 to 90 labelled b_1(2)
- 71 to 72 labelled a_1(2)
- 71 to 52 labelled a_1(1)
- 71 to 82 labelled a_1(2)
- 70 to 71 labelled a_1(2)
- 70 to 122 labelled a_1(3)
- 70 to 130 labelled a_1(2)
- 70 to 98 labelled a_1(2)
- 70 to 90 labelled a_1(2)
- 69 to 70 labelled b_1(2)
- 80 to 81 labelled a_1(2)
- 81 to 54 labelled b_1(2)
- 81 to 74 labelled b_1(2)
- 79 to 80 labelled a_1(2)
- 78 to 79 labelled a_1(2)
- 76 to 77 labelled a_1(2)
- 77 to 78 labelled b_1(2)
- 75 to 76 labelled a_1(2)
- 74 to 75 labelled b_1(2)
- 88 to 89 labelled a_1(2)
- 89 to 55 labelled b_1(2)
- 87 to 88 labelled a_1(2)
- 86 to 87 labelled a_1(2)
- 84 to 85 labelled a_1(2)
- 85 to 86 labelled b_1(2)
- 83 to 84 labelled a_1(2)
- 82 to 83 labelled b_1(2)
- 96 to 97 labelled a_1(2)
- 97 to 57 labelled b_1(2)
- 95 to 96 labelled a_1(2)
- 95 to 52 labelled a_1(1)
- 95 to 82 labelled a_1(2)
- 94 to 95 labelled a_1(2)
- 94 to 122 labelled a_1(3)
- 94 to 130 labelled a_1(2)
- 94 to 98 labelled a_1(2)
- 94 to 90 labelled a_1(2)
- 92 to 93 labelled a_1(2)
- 93 to 94 labelled b_1(2)
- 91 to 92 labelled a_1(2)
- 91 to 114 labelled a_1(3)
- 91 to 74 labelled a_1(2)
- 90 to 91 labelled b_1(2)
- 104 to 105 labelled a_1(2)
- 105 to 87 labelled b_1(2)
- 105 to 90 labelled b_1(2)
- 103 to 104 labelled a_1(2)
- 102 to 103 labelled a_1(2)
- 100 to 101 labelled a_1(2)
- 101 to 102 labelled b_1(2)
- 99 to 100 labelled a_1(2)
- 98 to 99 labelled b_1(2)
- 112 to 113 labelled a_1(2)
- 113 to 84 labelled b_1(2)
- 111 to 112 labelled a_1(2)
- 110 to 111 labelled a_1(2)
- 108 to 109 labelled a_1(2)
- 109 to 110 labelled b_1(2)
- 107 to 108 labelled a_1(2)
- 106 to 107 labelled b_1(2)
- 121 to 84 labelled b_1(3)
- 117 to 118 labelled b_1(3)
- 118 to 119 labelled a_1(3)
- 114 to 115 labelled b_1(3)
- 115 to 116 labelled a_1(3)
- 120 to 121 labelled a_1(3)
- 119 to 120 labelled a_1(3)
- 116 to 117 labelled a_1(3)
- 129 to 87 labelled b_1(3)
- 125 to 126 labelled b_1(3)
- 126 to 127 labelled a_1(3)
- 122 to 123 labelled b_1(3)
- 123 to 124 labelled a_1(3)
- 128 to 129 labelled a_1(3)
- 127 to 128 labelled a_1(3)
- 124 to 125 labelled a_1(3)
- 136 to 137 labelled a_1(2)
- 137 to 98 labelled b_1(2)
- 137 to 130 labelled b_1(2)
- 135 to 136 labelled a_1(2)
- 134 to 135 labelled a_1(2)
- 132 to 133 labelled a_1(2)
- 133 to 134 labelled b_1(2)
- 131 to 132 labelled a_1(2)
- 130 to 131 labelled b_1(2)