0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
↳ QTRS
↳ DependencyPairsProof
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
01(0(*(*(x1)))) → 11(1(x1))
11(1(*(*(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(0(#(#(x1))))
#1(#(1(1(x1)))) → #1(x1)
11(1(*(*(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(1(#(#(x1))))
11(1(*(*(x1)))) → 01(0(#(#(x1))))
11(1(*(*(x1)))) → #1(x1)
#1(#(1(1(x1)))) → #1(#(x1))
#1(#(0(0(x1)))) → #1(x1)
#1(#(0(0(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(#(#(x1)))
01(0(*(*(x1)))) → 11(x1)
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
01(0(*(*(x1)))) → 11(1(x1))
11(1(*(*(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(0(#(#(x1))))
#1(#(1(1(x1)))) → #1(x1)
11(1(*(*(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(1(#(#(x1))))
11(1(*(*(x1)))) → 01(0(#(#(x1))))
11(1(*(*(x1)))) → #1(x1)
#1(#(1(1(x1)))) → #1(#(x1))
#1(#(0(0(x1)))) → #1(x1)
#1(#(0(0(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(#(#(x1)))
01(0(*(*(x1)))) → 11(x1)
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
01(0(*(*(x1)))) → 11(1(x1))
11(1(*(*(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(#(#(x1)))
#1(#(0(0(x1)))) → 01(0(#(#(x1))))
#1(#(1(1(x1)))) → #1(x1)
11(1(*(*(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(1(#(#(x1))))
11(1(*(*(x1)))) → 01(0(#(#(x1))))
11(1(*(*(x1)))) → #1(x1)
#1(#(1(1(x1)))) → #1(#(x1))
#1(#(0(0(x1)))) → #1(x1)
#1(#(0(0(x1)))) → #1(#(x1))
#1(#(1(1(x1)))) → 11(#(#(x1)))
01(0(*(*(x1)))) → 11(x1)
The value of delta used in the strict ordering is 38.
POL(*(x1)) = 2 + (4)x_1
POL(11(x1)) = (2)x_1
POL(1(x1)) = 2 + (4)x_1
POL(01(x1)) = x_1
POL(#1(x1)) = (4)x_1
POL(0(x1)) = 2 + (4)x_1
POL(#(x1)) = 2 + (4)x_1
POL($(x1)) = 0
0(0(*(*(x1)))) → *(*(1(1(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#(*(*(x1)))) → *(*(x1))
#(#(#(#(x1)))) → #(#(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
0(0(*(*(x1)))) → *(*(1(1(x1))))
1(1(*(*(x1)))) → 0(0(#(#(x1))))
#(#(0(0(x1)))) → 0(0(#(#(x1))))
#(#(1(1(x1)))) → 1(1(#(#(x1))))
#(#($($(x1)))) → *(*($($(x1))))
#(#(#(#(x1)))) → #(#(x1))
#(#(*(*(x1)))) → *(*(x1))