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 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳6 BOUNDS(O(1), O(1))0.00/0.55
+(x, 0) → x 0.00/0.55
+(x, i(x)) → 0 0.00/0.55
+(+(x, y), z) → +(x, +(y, z)) 0.00/0.55
*(x, +(y, z)) → +(*(x, y), *(x, z)) 0.00/0.55
*(+(x, y), z) → +(*(x, z), *(y, z))
Tuples:
+(z0, 0) → z0 0.00/0.55
+(z0, i(z0)) → 0 0.00/0.55
+(+(z0, z1), z2) → +(z0, +(z1, z2)) 0.00/0.55
*(z0, +(z1, z2)) → +(*(z0, z1), *(z0, z2)) 0.00/0.55
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2))
S tuples:
+'(+(z0, z1), z2) → c2(+'(z0, +(z1, z2)), +'(z1, z2)) 0.00/0.55
*'(z0, +(z1, z2)) → c3(+'(*(z0, z1), *(z0, z2)), *'(z0, z1), *'(z0, z2)) 0.00/0.55
*'(+(z0, z1), z2) → c4(+'(*(z0, z2), *(z1, z2)), *'(z0, z2), *'(z1, z2))
K tuples:none
+'(+(z0, z1), z2) → c2(+'(z0, +(z1, z2)), +'(z1, z2)) 0.00/0.55
*'(z0, +(z1, z2)) → c3(+'(*(z0, z1), *(z0, z2)), *'(z0, z1), *'(z0, z2)) 0.00/0.55
*'(+(z0, z1), z2) → c4(+'(*(z0, z2), *(z1, z2)), *'(z0, z2), *'(z1, z2))
+, *
+', *'
c2, c3, c4
+'(+(z0, z1), z2) → c2(+'(z0, +(z1, z2)), +'(z1, z2)) 0.00/0.55
*'(z0, +(z1, z2)) → c3(+'(*(z0, z1), *(z0, z2)), *'(z0, z1), *'(z0, z2)) 0.00/0.55
*'(+(z0, z1), z2) → c4(+'(*(z0, z2), *(z1, z2)), *'(z0, z2), *'(z1, z2))
Tuples:none
+(z0, 0) → z0 0.00/0.55
+(z0, i(z0)) → 0 0.00/0.55
+(+(z0, z1), z2) → +(z0, +(z1, z2)) 0.00/0.55
*(z0, +(z1, z2)) → +(*(z0, z1), *(z0, z2)) 0.00/0.55
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2))
+, *