b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS Reverse
↳ QTRS Reverse
b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
Used ordering:
b(a(c(x1))) → b(c(x1))
POL(a(x1)) = 1 + x1
POL(b(x1)) = 1 + x1
POL(c(x1)) = 1 + x1
POL(d(x1)) = x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS Reverse
b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
B(b(b(x1))) → B(c(x1))
D(c(x1)) → B(d(x1))
B(b(b(x1))) → A(b(c(x1)))
D(a(c(x1))) → B(x1)
A(d(x1)) → D(c(x1))
D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)
D(a(c(x1))) → B(b(x1))
b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
↳ QTRS Reverse
B(b(b(x1))) → B(c(x1))
D(c(x1)) → B(d(x1))
B(b(b(x1))) → A(b(c(x1)))
D(a(c(x1))) → B(x1)
A(d(x1)) → D(c(x1))
D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)
D(a(c(x1))) → B(b(x1))
b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QTRS Reverse
↳ QTRS Reverse
D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)
b(d(b(x1))) → c(d(b(x1)))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesProof
↳ QTRS Reverse
↳ QTRS Reverse
D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ RuleRemovalProof
↳ QTRS Reverse
↳ QTRS Reverse
D(c(x1)) → D(b(d(x1)))
D(c(x1)) → D(x1)
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
D(c(x1)) → D(x1)
POL(D(x1)) = x1
POL(a(x1)) = 2 + x1
POL(b(x1)) = 2 + x1
POL(c(x1)) = 2 + x1
POL(d(x1)) = x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QTRS Reverse
↳ QTRS Reverse
D(c(x1)) → D(b(d(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
D(c(a(c(x0)))) → D(b(b(b(x0))))
D(c(b(x0))) → D(c(d(b(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(c(x0))) → D(b(b(d(x0))))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QTRS Reverse
↳ QTRS Reverse
D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(a(c(x0)))) → D(b(b(b(x0))))
D(c(b(x0))) → D(c(d(b(x0))))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
D(c(a(c(b(b(x0)))))) → D(b(b(a(b(c(x0))))))
D(c(a(c(d(b(x0)))))) → D(b(b(c(d(b(x0))))))
D(c(a(c(b(x0))))) → D(b(a(b(c(x0)))))
D(c(a(c(x0)))) → D(a(b(c(x0))))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
↳ QTRS Reverse
D(c(a(c(b(x0))))) → D(b(a(b(c(x0)))))
D(c(a(c(b(b(x0)))))) → D(b(b(a(b(c(x0))))))
D(c(a(c(x0)))) → D(a(b(c(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(c(x0))) → D(b(b(d(x0))))
D(c(a(c(d(b(x0)))))) → D(b(b(c(d(b(x0))))))
D(c(b(x0))) → D(c(d(b(x0))))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPToSRSProof
↳ QTRS Reverse
↳ QTRS Reverse
D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(b(x0))) → D(c(d(b(x0))))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS Reverse
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(b(x0))) → D(c(d(b(x0))))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x1))) → c(d(b(x1)))
b(b(b(x1))) → a(b(c(x1)))
D(c(c(x0))) → D(b(b(d(x0))))
D(c(c(x0))) → D(b(d(b(d(x0)))))
D(c(b(x0))) → D(c(d(b(x0))))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
b(d(b(x))) → b(d(c(x)))
b(b(b(x))) → c(b(a(x)))
c(c(D(x))) → d(b(b(D(x))))
c(c(D(x))) → d(b(d(b(D(x)))))
b(c(D(x))) → b(d(c(D(x))))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPToSRSProof
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ RFCMatchBoundsTRSProof
↳ QTRS Reverse
↳ QTRS Reverse
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
b(d(b(x))) → b(d(c(x)))
b(b(b(x))) → c(b(a(x)))
c(c(D(x))) → d(b(b(D(x))))
c(c(D(x))) → d(b(d(b(D(x)))))
b(c(D(x))) → b(d(c(D(x))))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
b(d(b(x))) → b(d(c(x)))
b(b(b(x))) → c(b(a(x)))
c(c(D(x))) → d(b(b(D(x))))
c(c(D(x))) → d(b(d(b(D(x)))))
b(c(D(x))) → b(d(c(D(x))))
The certificate consists of the following enumerated nodes:
1421, 1422, 1423, 1424, 1425, 1427, 1428, 1426, 1429, 1430, 1433, 1434, 1431, 1432, 1435, 1436, 1437, 1438, 1439, 1441, 1442, 1440, 1443, 1446, 1447, 1444, 1445, 1448, 1449, 1450, 1451, 1452, 1453, 1454, 1455
Node 1421 is start node and node 1422 is final node.
Those nodes are connect through the following edges:
b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
b(d(b(x1))) → c(d(b(x1)))
b(a(c(x1))) → b(c(x1))
a(d(x1)) → d(c(x1))
b(b(b(x1))) → a(b(c(x1)))
d(c(x1)) → b(d(x1))
d(c(x1)) → d(b(d(x1)))
d(a(c(x1))) → b(b(x1))
b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
b(d(b(x))) → b(d(c(x)))
c(a(b(x))) → c(b(x))
d(a(x)) → c(d(x))
b(b(b(x))) → c(b(a(x)))
c(d(x)) → d(b(x))
c(d(x)) → d(b(d(x)))
c(a(d(x))) → b(b(x))