(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:
f(f(x)) → f(c(f(x)))
f(f(x)) → f(d(f(x)))
g(c(x)) → x
g(d(x)) → x
g(c(0)) → g(d(1))
g(c(1)) → g(d(0))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
1072800, 1072801, 1072802, 1072803, 1072805, 1072804, 1072807, 1072806, 1072808, 1072809, 1072810, 1072811, 1072813, 1072812
Node 1072800 is start node and node 1072801 is final node.
Those nodes are connect through the following edges:
- 1072800 to 1072801 labelled f_1(0), 1(0), c_1(0), g_1(0), 0(0), d_1(0), f_1(1), 1(1), c_1(1), g_1(1), 0(1), d_1(1), 0(2), 1(2)
- 1072800 to 1072802 labelled g_1(0)
- 1072800 to 1072804 labelled f_1(0)
- 1072800 to 1072806 labelled f_1(0)
- 1072800 to 1072812 labelled g_1(1)
- 1072800 to 1072808 labelled f_1(1)
- 1072800 to 1072810 labelled f_1(1)
- 1072801 to 1072801 labelled #_1(0)
- 1072802 to 1072803 labelled d_1(0)
- 1072803 to 1072801 labelled 0(0), 1(0)
- 1072805 to 1072801 labelled f_1(0)
- 1072805 to 1072808 labelled f_1(1)
- 1072805 to 1072810 labelled f_1(1)
- 1072804 to 1072805 labelled c_1(0)
- 1072807 to 1072801 labelled f_1(0)
- 1072807 to 1072808 labelled f_1(1)
- 1072807 to 1072810 labelled f_1(1)
- 1072806 to 1072807 labelled d_1(0)
- 1072808 to 1072809 labelled c_1(1)
- 1072809 to 1072801 labelled f_1(1)
- 1072809 to 1072808 labelled f_1(1)
- 1072809 to 1072810 labelled f_1(1)
- 1072810 to 1072811 labelled d_1(1)
- 1072811 to 1072801 labelled f_1(1)
- 1072811 to 1072808 labelled f_1(1)
- 1072811 to 1072810 labelled f_1(1)
- 1072813 to 1072801 labelled 0(1), 1(1)
- 1072812 to 1072813 labelled d_1(1)