(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:
786808, 786809, 786812, 786813, 786814, 786810, 786811, 786819, 786817, 786818, 786816, 786815, 786822, 786823, 786820, 786821, 786824, 786825, 786827, 786828, 786829, 786826, 786834, 786832, 786833, 786830, 786831, 786835, 786837, 786838, 786839, 786836, 786840, 786842, 786843, 786844, 786841, 786848, 786849, 786847, 786845, 786846
Node 786808 is start node and node 786809 is final node.
Those nodes are connect through the following edges:
- 786808 to 786810 labelled s0_1(0)
- 786809 to 786809 labelled #_1(0)
- 786812 to 786813 labelled s1_1(0)
- 786812 to 786820 labelled s0_1(1)
- 786813 to 786814 labelled s1_1(0)
- 786813 to 786815 labelled s0_1(1)
- 786814 to 786809 labelled s1_1(0)
- 786814 to 786815 labelled s0_1(1)
- 786810 to 786811 labelled s0_1(0)
- 786811 to 786812 labelled s0_1(0)
- 786819 to 786809 labelled s1_1(1)
- 786819 to 786815 labelled s0_1(1)
- 786817 to 786818 labelled s1_1(1)
- 786817 to 786825 labelled s0_1(2)
- 786818 to 786819 labelled s1_1(1)
- 786818 to 786815 labelled s0_1(1)
- 786816 to 786817 labelled s0_1(1)
- 786815 to 786816 labelled s0_1(1)
- 786822 to 786823 labelled s1_1(1)
- 786823 to 786824 labelled s1_1(1)
- 786823 to 786830 labelled s0_1(2)
- 786820 to 786821 labelled s0_1(1)
- 786821 to 786822 labelled s0_1(1)
- 786824 to 786816 labelled s1_1(1)
- 786825 to 786826 labelled s0_1(2)
- 786827 to 786828 labelled s1_1(2)
- 786828 to 786829 labelled s1_1(2)
- 786828 to 786830 labelled s0_1(2)
- 786829 to 786816 labelled s1_1(2)
- 786826 to 786827 labelled s0_1(2)
- 786834 to 786825 labelled s1_1(2)
- 786832 to 786833 labelled s1_1(2)
- 786833 to 786834 labelled s1_1(2)
- 786833 to 786835 labelled s0_1(3)
- 786830 to 786831 labelled s0_1(2)
- 786831 to 786832 labelled s0_1(2)
- 786835 to 786836 labelled s0_1(3)
- 786837 to 786838 labelled s1_1(3)
- 786837 to 786845 labelled s0_1(4)
- 786838 to 786839 labelled s1_1(3)
- 786839 to 786827 labelled s1_1(3)
- 786839 to 786840 labelled s0_1(3)
- 786836 to 786837 labelled s0_1(3)
- 786840 to 786841 labelled s0_1(3)
- 786842 to 786843 labelled s1_1(3)
- 786843 to 786844 labelled s1_1(3)
- 786844 to 786831 labelled s1_1(3)
- 786841 to 786842 labelled s0_1(3)
- 786848 to 786849 labelled s1_1(4)
- 786849 to 786841 labelled s1_1(4)
- 786847 to 786848 labelled s1_1(4)
- 786845 to 786846 labelled s0_1(4)
- 786846 to 786847 labelled s0_1(4)