YES(O(1), O(1)) 0.00/0.54 YES(O(1), O(1)) 0.00/0.56 0.00/0.56 0.00/0.56
0.00/0.56 0.00/0.560 CpxTRS0.00/0.56
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳2 CdtProblem0.00/0.56
↳3 CdtUnreachableProof (⇔)0.00/0.56
↳4 CdtProblem0.00/0.56
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳6 CdtProblem0.00/0.56
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳8 CdtProblem0.00/0.56
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳10 BOUNDS(O(1), O(1))0.00/0.56
f(c(a, z, x)) → b(a, z) 0.00/0.56
b(x, b(z, y)) → f(b(f(f(z)), c(x, z, y))) 0.00/0.56
b(y, z) → z
Tuples:
f(c(a, z0, z1)) → b(a, z0) 0.00/0.56
b(z0, b(z1, z2)) → f(b(f(f(z1)), c(z0, z1, z2))) 0.00/0.56
b(z0, z1) → z1
S tuples:
F(c(a, z0, z1)) → c1(B(a, z0)) 0.00/0.56
B(z0, b(z1, z2)) → c2(F(b(f(f(z1)), c(z0, z1, z2))), B(f(f(z1)), c(z0, z1, z2)), F(f(z1)), F(z1))
K tuples:none
F(c(a, z0, z1)) → c1(B(a, z0)) 0.00/0.56
B(z0, b(z1, z2)) → c2(F(b(f(f(z1)), c(z0, z1, z2))), B(f(f(z1)), c(z0, z1, z2)), F(f(z1)), F(z1))
f, b
F, B
c1, c2
B(z0, b(z1, z2)) → c2(F(b(f(f(z1)), c(z0, z1, z2))), B(f(f(z1)), c(z0, z1, z2)), F(f(z1)), F(z1))
Tuples:
f(c(a, z0, z1)) → b(a, z0) 0.00/0.56
b(z0, b(z1, z2)) → f(b(f(f(z1)), c(z0, z1, z2))) 0.00/0.56
b(z0, z1) → z1
S tuples:
F(c(a, z0, z1)) → c1(B(a, z0))
K tuples:none
F(c(a, z0, z1)) → c1(B(a, z0))
f, b
F
c1
Tuples:
f(c(a, z0, z1)) → b(a, z0) 0.00/0.56
b(z0, b(z1, z2)) → f(b(f(f(z1)), c(z0, z1, z2))) 0.00/0.56
b(z0, z1) → z1
S tuples:
F(c(a, z0, z1)) → c1
K tuples:none
F(c(a, z0, z1)) → c1
f, b
F
c1
F(c(a, z0, z1)) → c1
Tuples:none
f(c(a, z0, z1)) → b(a, z0) 0.00/0.56
b(z0, b(z1, z2)) → f(b(f(f(z1)), c(z0, z1, z2))) 0.00/0.56
b(z0, z1) → z1
f, b