1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))
↳ QTRS
↳ DependencyPairsProof
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))
01(2(0(x1))) → 11(x1)
01(2(R(x1))) → 11(R(x1))
L1(2(0(x1))) → L1(1(0(1(x1))))
L1(2(0(x1))) → 11(x1)
01(2(1(x1))) → 11(0(2(x1)))
L1(2(1(x1))) → 01(2(x1))
01(2(R(x1))) → 11(0(1(R(x1))))
11(2(1(x1))) → 01(2(x1))
L1(2(1(x1))) → L1(1(0(2(x1))))
01(2(0(x1))) → 11(0(1(x1)))
01(2(0(x1))) → 01(1(x1))
01(2(R(x1))) → 01(1(R(x1)))
L1(2(0(x1))) → 11(0(1(x1)))
11(2(0(x1))) → 01(1(x1))
11(2(0(x1))) → 11(x1)
L1(2(1(x1))) → 11(0(2(x1)))
11(2(R(x1))) → 11(R(x1))
L1(2(0(x1))) → 01(1(x1))
11(2(R(x1))) → 01(1(R(x1)))
01(2(1(x1))) → 01(2(x1))
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
01(2(0(x1))) → 11(x1)
01(2(R(x1))) → 11(R(x1))
L1(2(0(x1))) → L1(1(0(1(x1))))
L1(2(0(x1))) → 11(x1)
01(2(1(x1))) → 11(0(2(x1)))
L1(2(1(x1))) → 01(2(x1))
01(2(R(x1))) → 11(0(1(R(x1))))
11(2(1(x1))) → 01(2(x1))
L1(2(1(x1))) → L1(1(0(2(x1))))
01(2(0(x1))) → 11(0(1(x1)))
01(2(0(x1))) → 01(1(x1))
01(2(R(x1))) → 01(1(R(x1)))
L1(2(0(x1))) → 11(0(1(x1)))
11(2(0(x1))) → 01(1(x1))
11(2(0(x1))) → 11(x1)
L1(2(1(x1))) → 11(0(2(x1)))
11(2(R(x1))) → 11(R(x1))
L1(2(0(x1))) → 01(1(x1))
11(2(R(x1))) → 01(1(R(x1)))
01(2(1(x1))) → 01(2(x1))
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
01(2(0(x1))) → 11(x1)
11(2(0(x1))) → 01(1(x1))
11(2(0(x1))) → 11(x1)
01(2(1(x1))) → 11(0(2(x1)))
11(2(1(x1))) → 01(2(x1))
01(2(0(x1))) → 01(1(x1))
01(2(0(x1))) → 11(0(1(x1)))
01(2(1(x1))) → 01(2(x1))
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
01(2(0(x1))) → 11(x1)
11(2(0(x1))) → 01(1(x1))
11(2(0(x1))) → 11(x1)
01(2(1(x1))) → 11(0(2(x1)))
11(2(1(x1))) → 01(2(x1))
01(2(0(x1))) → 01(1(x1))
01(2(0(x1))) → 11(0(1(x1)))
01(2(1(x1))) → 01(2(x1))
The value of delta used in the strict ordering is 5.
POL(11(x1)) = 4 + (4)x_1
POL(1(x1)) = 1 + (2)x_1
POL(01(x1)) = 1 + (4)x_1
POL(2(x1)) = 3 + (4)x_1
POL(0(x1)) = x_1
POL(R(x1)) = 0
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
1(2(0(x1))) → 2(0(1(x1)))
0(2(0(x1))) → 1(0(1(x1)))
0(2(R(x1))) → 1(0(1(R(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
L1(2(0(x1))) → L1(1(0(1(x1))))
L1(2(1(x1))) → L1(1(0(2(x1))))
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
L1(2(0(x1))) → L1(1(0(1(x1))))
L1(2(1(x1))) → L1(1(0(2(x1))))
The value of delta used in the strict ordering is 12.
POL(1(x1)) = (4)x_1
POL(L1(x1)) = (3)x_1
POL(2(x1)) = 4 + (4)x_1
POL(0(x1)) = 0
POL(R(x1)) = 0
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
1(2(0(x1))) → 2(0(1(x1)))
0(2(0(x1))) → 1(0(1(x1)))
0(2(R(x1))) → 1(0(1(R(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
1(2(1(x1))) → 2(0(2(x1)))
0(2(1(x1))) → 1(0(2(x1)))
L(2(1(x1))) → L(1(0(2(x1))))
1(2(0(x1))) → 2(0(1(x1)))
1(2(R(x1))) → 2(0(1(R(x1))))
0(2(0(x1))) → 1(0(1(x1)))
L(2(0(x1))) → L(1(0(1(x1))))
0(2(R(x1))) → 1(0(1(R(x1))))