(5) UsableRulesReductionPairsProof (EQUIVALENT transformation)
First, we A-transformed [FROCOS05] 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(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(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 [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] 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 [POLO]:
POL(a(x1)) = x1
POL(a1(x1)) = 2·x1
POL(b(x1)) = x1
(7) RFCMatchBoundsDPProof (EQUIVALENT transformation)
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(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(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(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(b(x)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
9566745, 9566746, 9566750, 9566751, 9566752, 9566749, 9566748, 9566747, 9566757, 9566758, 9566754, 9566755, 9566753, 9566760, 9566756, 9566759, 9566768, 9566765, 9566766, 9566762, 9566763, 9566764, 9566761, 9566767, 9566773, 9566774, 9566771, 9566772, 9566769, 9566775, 9566770, 9566776, 9566778, 9566779, 9566780, 9566783, 9566784, 9566782, 9566781, 9566777, 9566787, 9566788, 9566785, 9566786, 9566789, 9566790, 9566792, 9566791, 9566797, 9566798, 9566800, 9566794, 9566795, 9566799, 9566793, 9566796
Node 9566745 is start node and node 9566746 is final node.
Those nodes are connect through the following edges:
- 9566745 to 9566747 labelled a1_1(0)
- 9566745 to 9566751 labelled a1_1(0)
- 9566745 to 9566750 labelled a1_1(0)
- 9566745 to 9566755 labelled a1_1(1)
- 9566745 to 9566759 labelled a1_1(1)
- 9566745 to 9566758 labelled a1_1(1)
- 9566745 to 9566763 labelled a1_1(1)
- 9566745 to 9566767 labelled a1_1(1)
- 9566745 to 9566766 labelled a1_1(1)
- 9566745 to 9566771 labelled a1_1(2)
- 9566745 to 9566775 labelled a1_1(2)
- 9566745 to 9566774 labelled a1_1(2)
- 9566745 to 9566779 labelled a1_1(2)
- 9566745 to 9566783 labelled a1_1(2)
- 9566745 to 9566782 labelled a1_1(2)
- 9566745 to 9566787 labelled a1_1(2)
- 9566745 to 9566791 labelled a1_1(2)
- 9566745 to 9566790 labelled a1_1(2)
- 9566745 to 9566795 labelled a1_1(3)
- 9566745 to 9566799 labelled a1_1(3)
- 9566745 to 9566798 labelled a1_1(3)
- 9566746 to 9566746 labelled #_1(0)
- 9566750 to 9566751 labelled a_1(0)
- 9566750 to 9566753 labelled a_1(1)
- 9566751 to 9566752 labelled a_1(0)
- 9566752 to 9566746 labelled b_1(0)
- 9566749 to 9566750 labelled a_1(0)
- 9566749 to 9566761 labelled a_1(1)
- 9566749 to 9566753 labelled a_1(1)
- 9566748 to 9566749 labelled b_1(0)
- 9566747 to 9566748 labelled a_1(0)
- 9566757 to 9566758 labelled a_1(1)
- 9566757 to 9566769 labelled a_1(2)
- 9566758 to 9566759 labelled a_1(1)
- 9566758 to 9566753 labelled a_1(1)
- 9566754 to 9566755 labelled a_1(1)
- 9566754 to 9566777 labelled a_1(2)
- 9566755 to 9566756 labelled a_1(1)
- 9566753 to 9566754 labelled b_1(1)
- 9566760 to 9566746 labelled b_1(1)
- 9566760 to 9566755 labelled b_1(1)
- 9566760 to 9566769 labelled b_1(1)
- 9566760 to 9566777 labelled b_1(1)
- 9566756 to 9566757 labelled b_1(1)
- 9566759 to 9566760 labelled a_1(1)
- 9566768 to 9566758 labelled b_1(1)
- 9566765 to 9566766 labelled a_1(1)
- 9566765 to 9566769 labelled a_1(2)
- 9566766 to 9566767 labelled a_1(1)
- 9566766 to 9566753 labelled a_1(1)
- 9566766 to 9566785 labelled a_1(2)
- 9566762 to 9566763 labelled a_1(1)
- 9566762 to 9566777 labelled a_1(2)
- 9566763 to 9566764 labelled a_1(1)
- 9566764 to 9566765 labelled b_1(1)
- 9566761 to 9566762 labelled b_1(1)
- 9566767 to 9566768 labelled a_1(1)
- 9566773 to 9566774 labelled a_1(2)
- 9566773 to 9566769 labelled a_1(2)
- 9566773 to 9566793 labelled a_1(3)
- 9566774 to 9566775 labelled a_1(2)
- 9566774 to 9566753 labelled a_1(1)
- 9566774 to 9566785 labelled a_1(2)
- 9566771 to 9566772 labelled a_1(2)
- 9566772 to 9566773 labelled b_1(2)
- 9566769 to 9566770 labelled b_1(2)
- 9566775 to 9566776 labelled a_1(2)
- 9566770 to 9566771 labelled a_1(2)
- 9566770 to 9566777 labelled a_1(2)
- 9566770 to 9566793 labelled a_1(3)
- 9566776 to 9566758 labelled b_1(2)
- 9566776 to 9566790 labelled b_1(2)
- 9566776 to 9566769 labelled b_1(2)
- 9566778 to 9566779 labelled a_1(2)
- 9566779 to 9566780 labelled a_1(2)
- 9566780 to 9566781 labelled b_1(2)
- 9566783 to 9566784 labelled a_1(2)
- 9566784 to 9566755 labelled b_1(2)
- 9566784 to 9566787 labelled b_1(2)
- 9566784 to 9566777 labelled b_1(2)
- 9566782 to 9566783 labelled a_1(2)
- 9566781 to 9566782 labelled a_1(2)
- 9566777 to 9566778 labelled b_1(2)
- 9566787 to 9566788 labelled a_1(2)
- 9566788 to 9566789 labelled b_1(2)
- 9566785 to 9566786 labelled b_1(2)
- 9566786 to 9566787 labelled a_1(2)
- 9566789 to 9566790 labelled a_1(2)
- 9566790 to 9566791 labelled a_1(2)
- 9566792 to 9566756 labelled b_1(2)
- 9566791 to 9566792 labelled a_1(2)
- 9566797 to 9566798 labelled a_1(3)
- 9566798 to 9566799 labelled a_1(3)
- 9566800 to 9566790 labelled b_1(3)
- 9566800 to 9566787 labelled b_1(3)
- 9566794 to 9566795 labelled a_1(3)
- 9566795 to 9566796 labelled a_1(3)
- 9566799 to 9566800 labelled a_1(3)
- 9566793 to 9566794 labelled b_1(3)
- 9566796 to 9566797 labelled b_1(3)