0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 QDPSizeChangeProof (⇔)
↳9 TRUE
↳10 QDP
↳11 UsableRulesProof (⇔)
↳12 QDP
↳13 QDPSizeChangeProof (⇔)
↳14 TRUE
*(x, 1) → x
*(1, y) → y
*(i(x), x) → 1
*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)
i(1) → 1
*(*(x, y), i(y)) → x
*(*(x, i(y)), y) → x
i(i(x)) → x
i(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1
k(x, x) → 1
*(k(x, y), k(y, x)) → 1
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1
*1(x, *(y, z)) → *1(*(x, y), z)
*1(x, *(y, z)) → *1(x, y)
I(*(x, y)) → *1(i(y), i(x))
I(*(x, y)) → I(y)
I(*(x, y)) → I(x)
*1(*(i(x), k(y, z)), x) → K(*(*(i(x), y), x), *(*(i(x), z), x))
*1(*(i(x), k(y, z)), x) → *1(*(i(x), y), x)
*1(*(i(x), k(y, z)), x) → *1(i(x), y)
*1(*(i(x), k(y, z)), x) → *1(*(i(x), z), x)
*1(*(i(x), k(y, z)), x) → *1(i(x), z)
*(x, 1) → x
*(1, y) → y
*(i(x), x) → 1
*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)
i(1) → 1
*(*(x, y), i(y)) → x
*(*(x, i(y)), y) → x
i(i(x)) → x
i(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1
k(x, x) → 1
*(k(x, y), k(y, x)) → 1
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1
*1(x, *(y, z)) → *1(x, y)
*1(x, *(y, z)) → *1(*(x, y), z)
*1(*(i(x), k(y, z)), x) → *1(*(i(x), y), x)
*1(*(i(x), k(y, z)), x) → *1(i(x), y)
*1(*(i(x), k(y, z)), x) → *1(*(i(x), z), x)
*1(*(i(x), k(y, z)), x) → *1(i(x), z)
*(x, 1) → x
*(1, y) → y
*(i(x), x) → 1
*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)
i(1) → 1
*(*(x, y), i(y)) → x
*(*(x, i(y)), y) → x
i(i(x)) → x
i(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1
k(x, x) → 1
*(k(x, y), k(y, x)) → 1
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(*(i(x), k(y, z)), x) → *1(*(i(x), y), x)
*1(*(i(x), k(y, z)), x) → *1(i(x), y)
*1(*(i(x), k(y, z)), x) → *1(*(i(x), z), x)
*1(*(i(x), k(y, z)), x) → *1(i(x), z)
POL(*(x1, x2)) = x1 + x1·x2 + x2
POL(*1(x1, x2)) = x1 + x1·x2 + x2
POL(1) = 0
POL(i(x1)) = x1
POL(k(x1, x2)) = 1 + x1 + x2
i(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1
*(*(x, i(y)), y) → x
i(i(x)) → x
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1
k(x, x) → 1
*(k(x, y), k(y, x)) → 1
*(i(x), x) → 1
*(1, y) → y
*(x, 1) → x
*(*(x, y), i(y)) → x
i(1) → 1
*(x, *(y, z)) → *(*(x, y), z)
*(x, i(x)) → 1
*1(x, *(y, z)) → *1(x, y)
*1(x, *(y, z)) → *1(*(x, y), z)
*(x, 1) → x
*(1, y) → y
*(i(x), x) → 1
*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)
i(1) → 1
*(*(x, y), i(y)) → x
*(*(x, i(y)), y) → x
i(i(x)) → x
i(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1
k(x, x) → 1
*(k(x, y), k(y, x)) → 1
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1
From the DPs we obtained the following set of size-change graphs:
I(*(x, y)) → I(x)
I(*(x, y)) → I(y)
*(x, 1) → x
*(1, y) → y
*(i(x), x) → 1
*(x, i(x)) → 1
*(x, *(y, z)) → *(*(x, y), z)
i(1) → 1
*(*(x, y), i(y)) → x
*(*(x, i(y)), y) → x
i(i(x)) → x
i(*(x, y)) → *(i(y), i(x))
k(x, 1) → 1
k(x, x) → 1
*(k(x, y), k(y, x)) → 1
*(*(i(x), k(y, z)), x) → k(*(*(i(x), y), x), *(*(i(x), z), x))
k(*(x, i(y)), *(y, i(x))) → 1
I(*(x, y)) → I(x)
I(*(x, y)) → I(y)
From the DPs we obtained the following set of size-change graphs: