YES(O(1), O(n^1)) 0.00/0.71 YES(O(1), O(n^1)) 0.00/0.73 0.00/0.73 0.00/0.73
0.00/0.73 0.00/0.730 CpxTRS0.00/0.73
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.73
↳2 CdtProblem0.00/0.73
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.73
↳4 CdtProblem0.00/0.73
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.73
↳6 CdtProblem0.00/0.73
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.73
↳8 BOUNDS(O(1), O(1))0.00/0.73
or(true, y) → true 0.00/0.73
or(x, true) → true 0.00/0.73
or(false, false) → false 0.00/0.73
mem(x, nil) → false 0.00/0.73
mem(x, set(y)) → =(x, y) 0.00/0.73
mem(x, union(y, z)) → or(mem(x, y), mem(x, z))
Tuples:
or(true, z0) → true 0.00/0.73
or(z0, true) → true 0.00/0.73
or(false, false) → false 0.00/0.73
mem(z0, nil) → false 0.00/0.73
mem(z0, set(z1)) → =(z0, z1) 0.00/0.73
mem(z0, union(z1, z2)) → or(mem(z0, z1), mem(z0, z2))
S tuples:
MEM(z0, union(z1, z2)) → c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1), MEM(z0, z2))
K tuples:none
MEM(z0, union(z1, z2)) → c5(OR(mem(z0, z1), mem(z0, z2)), MEM(z0, z1), MEM(z0, z2))
or, mem
MEM
c5
Tuples:
or(true, z0) → true 0.00/0.73
or(z0, true) → true 0.00/0.73
or(false, false) → false 0.00/0.73
mem(z0, nil) → false 0.00/0.73
mem(z0, set(z1)) → =(z0, z1) 0.00/0.73
mem(z0, union(z1, z2)) → or(mem(z0, z1), mem(z0, z2))
S tuples:
MEM(z0, union(z1, z2)) → c5(MEM(z0, z1), MEM(z0, z2))
K tuples:none
MEM(z0, union(z1, z2)) → c5(MEM(z0, z1), MEM(z0, z2))
or, mem
MEM
c5
We considered the (Usable) Rules:none
MEM(z0, union(z1, z2)) → c5(MEM(z0, z1), MEM(z0, z2))
The order we found is given by the following interpretation:
MEM(z0, union(z1, z2)) → c5(MEM(z0, z1), MEM(z0, z2))
POL(MEM(x1, x2)) = x2 0.00/0.73
POL(c5(x1, x2)) = x1 + x2 0.00/0.73
POL(union(x1, x2)) = [1] + x1 + x2
Tuples:
or(true, z0) → true 0.00/0.73
or(z0, true) → true 0.00/0.73
or(false, false) → false 0.00/0.73
mem(z0, nil) → false 0.00/0.73
mem(z0, set(z1)) → =(z0, z1) 0.00/0.73
mem(z0, union(z1, z2)) → or(mem(z0, z1), mem(z0, z2))
S tuples:none
MEM(z0, union(z1, z2)) → c5(MEM(z0, z1), MEM(z0, z2))
Defined Rule Symbols:
MEM(z0, union(z1, z2)) → c5(MEM(z0, z1), MEM(z0, z2))
or, mem
MEM
c5