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 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳4 CdtProblem0.00/0.56
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳6 CdtProblem0.00/0.56
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳8 BOUNDS(O(1), O(1))0.00/0.56
f(g(i(a, b, b'), c), d) → if(e, f(.(b, c), d'), f(.(b', c), d')) 0.00/0.56
f(g(h(a, b), c), d) → if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))
Tuples:
f(g(i(a, b, b'), c), d) → if(e, f(.(b, c), d'), f(.(b', c), d')) 0.00/0.56
f(g(h(a, b), c), d) → if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))
S tuples:
F(g(i(a, b, b'), c), d) → c1(F(.(b, c), d'), F(.(b', c), d')) 0.00/0.56
F(g(h(a, b), c), d) → c2(F(.(b, g(h(a, b), c)), d), F(c, d'))
K tuples:none
F(g(i(a, b, b'), c), d) → c1(F(.(b, c), d'), F(.(b', c), d')) 0.00/0.56
F(g(h(a, b), c), d) → c2(F(.(b, g(h(a, b), c)), d), F(c, d'))
f
F
c1, c2
Tuples:
f(g(i(a, b, b'), c), d) → if(e, f(.(b, c), d'), f(.(b', c), d')) 0.00/0.56
f(g(h(a, b), c), d) → if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))
S tuples:
F(g(i(a, b, b'), c), d) → c1 0.00/0.56
F(g(h(a, b), c), d) → c2
K tuples:none
F(g(i(a, b, b'), c), d) → c1 0.00/0.56
F(g(h(a, b), c), d) → c2
f
F
c1, c2
F(g(h(a, b), c), d) → c2 0.00/0.56
F(g(i(a, b, b'), c), d) → c1
Tuples:none
f(g(i(a, b, b'), c), d) → if(e, f(.(b, c), d'), f(.(b', c), d')) 0.00/0.56
f(g(h(a, b), c), d) → if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))
f