YES(O(1), O(1)) 0.00/0.53 YES(O(1), O(1)) 0.00/0.54 0.00/0.54 0.00/0.54
0.00/0.54 0.00/0.540 CpxTRS0.00/0.54
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.54
↳2 CdtProblem0.00/0.54
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.54
↳4 CdtProblem0.00/0.54
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.54
↳6 CdtProblem0.00/0.54
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.54
↳8 BOUNDS(O(1), O(1))0.00/0.54
d(x) → e(u(x)) 0.00/0.54
d(u(x)) → c(x) 0.00/0.54
c(u(x)) → b(x) 0.00/0.54
v(e(x)) → x 0.00/0.54
b(u(x)) → a(e(x))
Tuples:
d(z0) → e(u(z0)) 0.00/0.54
d(u(z0)) → c(z0) 0.00/0.54
c(u(z0)) → b(z0) 0.00/0.54
v(e(z0)) → z0 0.00/0.54
b(u(z0)) → a(e(z0))
S tuples:
D(u(z0)) → c2(C(z0)) 0.00/0.54
C(u(z0)) → c3(B(z0))
K tuples:none
D(u(z0)) → c2(C(z0)) 0.00/0.54
C(u(z0)) → c3(B(z0))
d, c, v, b
D, C
c2, c3
Tuples:
d(z0) → e(u(z0)) 0.00/0.54
d(u(z0)) → c(z0) 0.00/0.54
c(u(z0)) → b(z0) 0.00/0.54
v(e(z0)) → z0 0.00/0.54
b(u(z0)) → a(e(z0))
S tuples:
D(u(z0)) → c2(C(z0)) 0.00/0.54
C(u(z0)) → c3
K tuples:none
D(u(z0)) → c2(C(z0)) 0.00/0.54
C(u(z0)) → c3
d, c, v, b
D, C
c2, c3
C(u(z0)) → c3 0.00/0.54
D(u(z0)) → c2(C(z0))
Tuples:none
d(z0) → e(u(z0)) 0.00/0.54
d(u(z0)) → c(z0) 0.00/0.54
c(u(z0)) → b(z0) 0.00/0.54
v(e(z0)) → z0 0.00/0.54
b(u(z0)) → a(e(z0))
d, c, v, b