(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:
s1(s1(s0(s0(x)))) → s0(s0(s0(s1(s1(s1(x))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
2682805, 2682806, 2682807, 2682811, 2682809, 2682810, 2682808, 2682814, 2682815, 2682816, 2682813, 2682812, 2682818, 2682819, 2682817, 2682821, 2682820, 2682824, 2682825, 2682822, 2682823, 2682826, 2682829, 2682830, 2682831, 2682827, 2682828, 2682832, 2682834, 2682835, 2682836, 2682833, 2682837, 2682839, 2682840, 2682838, 2682841, 2682844, 2682845, 2682842, 2682843, 2682846
Node 2682805 is start node and node 2682806 is final node.
Those nodes are connect through the following edges:
- 2682805 to 2682807 labelled s0_1(0)
- 2682806 to 2682806 labelled #_1(0)
- 2682807 to 2682808 labelled s0_1(0)
- 2682811 to 2682806 labelled s1_1(0)
- 2682811 to 2682812 labelled s0_1(1)
- 2682809 to 2682810 labelled s1_1(0)
- 2682809 to 2682817 labelled s0_1(1)
- 2682810 to 2682811 labelled s1_1(0)
- 2682810 to 2682812 labelled s0_1(1)
- 2682808 to 2682809 labelled s0_1(0)
- 2682814 to 2682815 labelled s1_1(1)
- 2682814 to 2682822 labelled s0_1(2)
- 2682815 to 2682816 labelled s1_1(1)
- 2682815 to 2682812 labelled s0_1(1)
- 2682816 to 2682806 labelled s1_1(1)
- 2682816 to 2682812 labelled s0_1(1)
- 2682813 to 2682814 labelled s0_1(1)
- 2682812 to 2682813 labelled s0_1(1)
- 2682818 to 2682819 labelled s0_1(1)
- 2682819 to 2682820 labelled s1_1(1)
- 2682817 to 2682818 labelled s0_1(1)
- 2682821 to 2682813 labelled s1_1(1)
- 2682820 to 2682821 labelled s1_1(1)
- 2682820 to 2682827 labelled s0_1(2)
- 2682824 to 2682825 labelled s1_1(2)
- 2682825 to 2682826 labelled s1_1(2)
- 2682825 to 2682827 labelled s0_1(2)
- 2682822 to 2682823 labelled s0_1(2)
- 2682823 to 2682824 labelled s0_1(2)
- 2682826 to 2682813 labelled s1_1(2)
- 2682829 to 2682830 labelled s1_1(2)
- 2682830 to 2682831 labelled s1_1(2)
- 2682830 to 2682832 labelled s0_1(3)
- 2682831 to 2682822 labelled s1_1(2)
- 2682827 to 2682828 labelled s0_1(2)
- 2682828 to 2682829 labelled s0_1(2)
- 2682832 to 2682833 labelled s0_1(3)
- 2682834 to 2682835 labelled s1_1(3)
- 2682834 to 2682842 labelled s0_1(4)
- 2682835 to 2682836 labelled s1_1(3)
- 2682836 to 2682824 labelled s1_1(3)
- 2682836 to 2682837 labelled s0_1(3)
- 2682833 to 2682834 labelled s0_1(3)
- 2682837 to 2682838 labelled s0_1(3)
- 2682839 to 2682840 labelled s1_1(3)
- 2682840 to 2682841 labelled s1_1(3)
- 2682838 to 2682839 labelled s0_1(3)
- 2682841 to 2682828 labelled s1_1(3)
- 2682844 to 2682845 labelled s1_1(4)
- 2682845 to 2682846 labelled s1_1(4)
- 2682842 to 2682843 labelled s0_1(4)
- 2682843 to 2682844 labelled s0_1(4)
- 2682846 to 2682838 labelled s1_1(4)