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