YES(O(1), O(n^1)) 0.00/0.88 YES(O(1), O(n^1)) 0.00/0.91 0.00/0.91 0.00/0.91
0.00/0.91 0.00/0.910 CpxTRS0.00/0.91
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.91
↳2 CdtProblem0.00/0.91
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.91
↳4 CdtProblem0.00/0.91
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.91
↳6 CdtProblem0.00/0.91
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.91
↳8 CdtProblem0.00/0.91
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.91
↳10 BOUNDS(O(1), O(1))0.00/0.91
:(:(x, y), z) → :(x, :(y, z)) 0.00/0.91
:(+(x, y), z) → +(:(x, z), :(y, z)) 0.00/0.91
:(z, +(x, f(y))) → :(g(z, y), +(x, a))
Tuples:
:(:(z0, z1), z2) → :(z0, :(z1, z2)) 0.00/0.91
:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2)) 0.00/0.91
:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))
S tuples:
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2(:'(g(z0, z2), +(z1, a)))
K tuples:none
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2(:'(g(z0, z2), +(z1, a)))
:
:'
c, c1, c2
Tuples:
:(:(z0, z1), z2) → :(z0, :(z1, z2)) 0.00/0.91
:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2)) 0.00/0.91
:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))
S tuples:
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
K tuples:none
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
:
:'
c, c1, c2
:'(z0, +(z1, f(z2))) → c2
Tuples:
:(:(z0, z1), z2) → :(z0, :(z1, z2)) 0.00/0.91
:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2)) 0.00/0.91
:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))
S tuples:
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
K tuples:none
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
:
:'
c, c1, c2
We considered the (Usable) Rules:
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
And the Tuples:
:(:(z0, z1), z2) → :(z0, :(z1, z2)) 0.00/0.91
:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2)) 0.00/0.91
:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))
The order we found is given by the following interpretation:
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
POL(+(x1, x2)) = [4] + x1 + x2 0.00/0.91
POL(:(x1, x2)) = [4] + [4]x1 + x2 0.00/0.91
POL(:'(x1, x2)) = [4] + [4]x1 0.00/0.91
POL(a) = [3] 0.00/0.91
POL(c(x1, x2)) = x1 + x2 0.00/0.91
POL(c1(x1, x2)) = x1 + x2 0.00/0.91
POL(c2) = 0 0.00/0.91
POL(f(x1)) = [3] + x1 0.00/0.91
POL(g(x1, x2)) = [3] + x1 + x2
Tuples:
:(:(z0, z1), z2) → :(z0, :(z1, z2)) 0.00/0.91
:(+(z0, z1), z2) → +(:(z0, z2), :(z1, z2)) 0.00/0.91
:(z0, +(z1, f(z2))) → :(g(z0, z2), +(z1, a))
S tuples:none
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
Defined Rule Symbols:
:'(:(z0, z1), z2) → c(:'(z0, :(z1, z2)), :'(z1, z2)) 0.00/0.91
:'(+(z0, z1), z2) → c1(:'(z0, z2), :'(z1, z2)) 0.00/0.91
:'(z0, +(z1, f(z2))) → c2
:
:'
c, c1, c2