YES(O(1), O(n^1)) 2.42/1.07 YES(O(1), O(n^1)) 2.81/1.12 2.81/1.12 2.81/1.12
2.81/1.12 2.81/1.120 CpxTRS2.81/1.12
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))2.81/1.12
↳2 CdtProblem2.81/1.12
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))2.81/1.12
↳4 CdtProblem2.81/1.12
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))2.81/1.12
↳6 CdtProblem2.81/1.12
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.81/1.12
↳8 CdtProblem2.81/1.12
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.81/1.12
↳10 CdtProblem2.81/1.12
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))2.81/1.12
↳12 BOUNDS(O(1), O(1))2.81/1.12
del(.(x, .(y, z))) → f(=(x, y), x, y, z) 2.81/1.12
f(true, x, y, z) → del(.(y, z)) 2.81/1.12
f(false, x, y, z) → .(x, del(.(y, z))) 2.81/1.12
=(nil, nil) → true 2.81/1.12
=(.(x, y), nil) → false 2.81/1.12
=(nil, .(y, z)) → false 2.81/1.12
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))
Tuples:
del(.(z0, .(z1, z2))) → f(=(z0, z1), z0, z1, z2) 2.81/1.12
f(true, z0, z1, z2) → del(.(z1, z2)) 2.81/1.12
f(false, z0, z1, z2) → .(z0, del(.(z1, z2))) 2.81/1.12
=(nil, nil) → true 2.81/1.12
=(.(z0, z1), nil) → false 2.81/1.12
=(nil, .(z0, z1)) → false 2.81/1.12
=(.(z0, z1), .(u, v)) → and(=(z0, u), =(z1, v))
S tuples:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6(='(z0, u), ='(z1, v))
K tuples:none
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6(='(z0, u), ='(z1, v))
del, f, =
DEL, F, ='
c, c1, c2, c6
Tuples:
del(.(z0, .(z1, z2))) → f(=(z0, z1), z0, z1, z2) 2.81/1.12
f(true, z0, z1, z2) → del(.(z1, z2)) 2.81/1.12
f(false, z0, z1, z2) → .(z0, del(.(z1, z2))) 2.81/1.12
=(nil, nil) → true 2.81/1.12
=(.(z0, z1), nil) → false 2.81/1.12
=(nil, .(z0, z1)) → false 2.81/1.12
=(.(z0, z1), .(u, v)) → and(=(z0, u), =(z1, v))
S tuples:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
K tuples:none
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
del, f, =
DEL, F, ='
c, c1, c2, c6
='(.(z0, z1), .(u, v)) → c6
Tuples:
del(.(z0, .(z1, z2))) → f(=(z0, z1), z0, z1, z2) 2.81/1.12
f(true, z0, z1, z2) → del(.(z1, z2)) 2.81/1.12
f(false, z0, z1, z2) → .(z0, del(.(z1, z2))) 2.81/1.12
=(nil, nil) → true 2.81/1.12
=(.(z0, z1), nil) → false 2.81/1.12
=(nil, .(z0, z1)) → false 2.81/1.12
=(.(z0, z1), .(u, v)) → and(=(z0, u), =(z1, v))
S tuples:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
K tuples:none
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
del, f, =
DEL, F, ='
c, c1, c2, c6
We considered the (Usable) Rules:
='(.(z0, z1), .(u, v)) → c6
And the Tuples:
=(nil, nil) → true 2.81/1.12
=(.(z0, z1), nil) → false 2.81/1.12
=(nil, .(z0, z1)) → false 2.81/1.12
=(.(z0, z1), .(u, v)) → and(=(z0, u), =(z1, v))
The order we found is given by the following interpretation:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
POL(.(x1, x2)) = [2] + x2 2.81/1.12
POL(=(x1, x2)) = 0 2.81/1.12
POL(='(x1, x2)) = [2] 2.81/1.12
POL(DEL(x1)) = [2] + x1 2.81/1.12
POL(F(x1, x2, x3, x4)) = [4] + x4 2.81/1.12
POL(and(x1, x2)) = [3] 2.81/1.12
POL(c(x1, x2)) = x1 + x2 2.81/1.12
POL(c1(x1)) = x1 2.81/1.12
POL(c2(x1)) = x1 2.81/1.12
POL(c6) = 0 2.81/1.12
POL(false) = 0 2.81/1.12
POL(nil) = [3] 2.81/1.12
POL(true) = 0 2.81/1.12
POL(u) = 0 2.81/1.12
POL(v) = 0
Tuples:
del(.(z0, .(z1, z2))) → f(=(z0, z1), z0, z1, z2) 2.81/1.12
f(true, z0, z1, z2) → del(.(z1, z2)) 2.81/1.12
f(false, z0, z1, z2) → .(z0, del(.(z1, z2))) 2.81/1.12
=(nil, nil) → true 2.81/1.12
=(.(z0, z1), nil) → false 2.81/1.12
=(nil, .(z0, z1)) → false 2.81/1.12
=(.(z0, z1), .(u, v)) → and(=(z0, u), =(z1, v))
S tuples:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
K tuples:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2)))
Defined Rule Symbols:
='(.(z0, z1), .(u, v)) → c6
del, f, =
DEL, F, ='
c, c1, c2, c6
We considered the (Usable) Rules:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2)))
And the Tuples:
=(nil, nil) → true 2.81/1.12
=(.(z0, z1), nil) → false 2.81/1.12
=(nil, .(z0, z1)) → false 2.81/1.12
=(.(z0, z1), .(u, v)) → and(=(z0, u), =(z1, v))
The order we found is given by the following interpretation:
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
POL(.(x1, x2)) = [2] + x1 + x2 2.81/1.12
POL(=(x1, x2)) = [5] + [3]x1 + [5]x2 2.81/1.12
POL(='(x1, x2)) = x1 2.81/1.12
POL(DEL(x1)) = [2]x1 2.81/1.12
POL(F(x1, x2, x3, x4)) = [5] + [2]x3 + [2]x4 2.81/1.12
POL(and(x1, x2)) = [5] + x1 + x2 2.81/1.12
POL(c(x1, x2)) = x1 + x2 2.81/1.12
POL(c1(x1)) = x1 2.81/1.12
POL(c2(x1)) = x1 2.81/1.12
POL(c6) = 0 2.81/1.12
POL(false) = 0 2.81/1.12
POL(nil) = [1] 2.81/1.12
POL(true) = 0 2.81/1.12
POL(u) = [4] 2.81/1.12
POL(v) = [5]
Tuples:
del(.(z0, .(z1, z2))) → f(=(z0, z1), z0, z1, z2) 2.81/1.12
f(true, z0, z1, z2) → del(.(z1, z2)) 2.81/1.12
f(false, z0, z1, z2) → .(z0, del(.(z1, z2))) 2.81/1.12
=(nil, nil) → true 2.81/1.12
=(.(z0, z1), nil) → false 2.81/1.12
=(nil, .(z0, z1)) → false 2.81/1.12
=(.(z0, z1), .(u, v)) → and(=(z0, u), =(z1, v))
S tuples:none
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2))) 2.81/1.12
='(.(z0, z1), .(u, v)) → c6
Defined Rule Symbols:
='(.(z0, z1), .(u, v)) → c6 2.81/1.12
DEL(.(z0, .(z1, z2))) → c(F(=(z0, z1), z0, z1, z2), ='(z0, z1)) 2.81/1.12
F(true, z0, z1, z2) → c1(DEL(.(z1, z2))) 2.81/1.12
F(false, z0, z1, z2) → c2(DEL(.(z1, z2)))
del, f, =
DEL, F, ='
c, c1, c2, c6