MAYBE 407.94/225.61 MAYBE 407.94/225.64 407.94/225.64 407.94/225.64 407.94/225.64 407.94/225.64 407.94/225.64 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 407.94/225.64 407.94/225.64 407.94/225.64
407.94/225.64
407.94/225.64
407.94/225.64
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
407.94/225.64 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
407.94/225.64 
↳2 CdtProblem
407.94/225.64 
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
407.94/225.64 
↳4 CdtProblem
407.94/225.64 
↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
407.94/225.64 
↳6 CdtProblem
407.94/225.64 
↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
407.94/225.64 
↳8 CdtProblem
407.94/225.64 
↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
407.94/225.64 
↳10 CdtProblem
407.94/225.64 
↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
407.94/225.64 
↳12 CdtProblem
407.94/225.64 
↳13 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
407.94/225.64 
↳14 CdtProblem
407.94/225.64
407.94/225.64 407.94/225.64
407.94/225.64
407.94/225.64

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

*(*(x, y), z) → *(x, *(y, z)) 407.94/225.64
*(+(x, y), z) → +(*(x, z), *(y, z)) 407.94/225.64
*(x, +(y, f(z))) → *(g(x, z), +(y, y))

Rewrite Strategy: INNERMOST
407.94/225.64
407.94/225.64

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
407.94/225.64
407.94/225.64

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 407.94/225.64
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 407.94/225.64
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.64
*'(+(z0, z1), z2) → c1(*'(z0, z2), *'(z1, z2)) 407.94/225.64
*'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1)))
S tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.64
*'(+(z0, z1), z2) → c1(*'(z0, z2), *'(z1, z2)) 407.94/225.64
*'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1)))
K tuples:none
Defined Rule Symbols:

*

Defined Pair Symbols:

*'

Compound Symbols:

c, c1, c2

407.94/225.64
407.94/225.64

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.64
*'(+(z0, z1), z2) → c1(*'(z0, z2), *'(z1, z2))
We considered the (Usable) Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 407.94/225.64
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 407.94/225.64
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
And the Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.64
*'(+(z0, z1), z2) → c1(*'(z0, z2), *'(z1, z2)) 407.94/225.64
*'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1)))
The order we found is given by the following interpretation:
Polynomial interpretation : 407.94/225.64

POL(*(x1, x2)) = [4] + [4]x1 + [2]x2    407.94/225.64
POL(*'(x1, x2)) = [2] + [4]x1    407.94/225.64
POL(+(x1, x2)) = [2] + x1 + x2    407.94/225.64
POL(c(x1, x2)) = x1 + x2    407.94/225.64
POL(c1(x1, x2)) = x1 + x2    407.94/225.64
POL(c2(x1)) = x1    407.94/225.64
POL(f(x1)) = 0    407.94/225.64
POL(g(x1, x2)) = x1   
407.94/225.64
407.94/225.64

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 407.94/225.64
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 407.94/225.64
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.64
*'(+(z0, z1), z2) → c1(*'(z0, z2), *'(z1, z2)) 407.94/225.64
*'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1)))
S tuples:

*'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1)))
K tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.67
*'(+(z0, z1), z2) → c1(*'(z0, z2), *'(z1, z2))
Defined Rule Symbols:

*

Defined Pair Symbols:

*'

Compound Symbols:

c, c1, c2

407.94/225.67
407.94/225.67

(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace *'(+(z0, z1), z2) → c1(*'(z0, z2), *'(z1, z2)) by

*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 407.94/225.67
*'(+(+(y0, y1), z1), z2) → c1(*'(+(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) 407.94/225.67
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2))))
407.94/225.67
407.94/225.67

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 407.94/225.67
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 407.94/225.67
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.67
*'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1))) 407.94/225.67
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 407.94/225.67
*'(+(+(y0, y1), z1), z2) → c1(*'(+(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) 407.94/225.67
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2))))
S tuples:

*'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1)))
K tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.67
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 407.94/225.67
*'(+(+(y0, y1), z1), z2) → c1(*'(+(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) 407.94/225.67
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2))))
Defined Rule Symbols:

*

Defined Pair Symbols:

*'

Compound Symbols:

c, c2, c1

407.94/225.67
407.94/225.67

(7) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace *'(z0, +(z1, f(z2))) → c2(*'(g(z0, z2), +(z1, z1))) by

*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2))))
407.94/225.67
407.94/225.67

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 407.94/225.67
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 407.94/225.67
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.67
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 407.94/225.67
*'(+(+(y0, y1), z1), z2) → c1(*'(+(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) 407.94/225.67
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2)))) 407.94/225.67
*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2))))
S tuples:

*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2))))
K tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 407.94/225.67
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 407.94/225.67
*'(+(+(y0, y1), z1), z2) → c1(*'(+(y0, y1), z2), *'(z1, z2)) 407.94/225.67
*'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) 407.94/225.67
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2))))
Defined Rule Symbols:

*

Defined Pair Symbols:

*'

Compound Symbols:

c, c1, c2

408.27/225.71
408.27/225.71

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace *'(+(+(y0, y1), z1), z2) → c1(*'(+(y0, y1), z2), *'(z1, z2)) by

*'(+(+(z0, z1), *(y0, y1)), z3) → c1(*'(+(z0, z1), z3), *'(*(y0, y1), z3)) 408.27/225.71
*'(+(+(*(y0, y1), z1), z2), z3) → c1(*'(+(*(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(*(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(*(y0, y1), y2), z3)) 408.27/225.71
*'(+(+(z0, *(y1, y2)), z2), z3) → c1(*'(+(z0, *(y1, y2)), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(y0, *(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, *(y1, y2)), z3)) 408.27/225.71
*'(+(+(+(y0, y1), z1), z2), z3) → c1(*'(+(+(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(+(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(+(y0, y1), y2), z3)) 408.27/225.71
*'(+(+(z0, +(y1, y2)), z2), z3) → c1(*'(+(z0, +(y1, y2)), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(y0, +(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, +(y1, y2)), z3)) 408.27/225.71
*'(+(+(z0, z1), z2), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(z2, +(y2, f(y3)))) 408.27/225.71
*'(+(+(z0, z1), +(y0, y1)), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(+(y0, y1), +(y2, f(y3)))) 408.27/225.71
*'(+(+(z0, z1), z2), +(f(y1), f(y2))) → c1(*'(+(z0, z1), +(f(y1), f(y2))), *'(z2, +(f(y1), f(y2))))
408.27/225.71
408.27/225.71

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 408.27/225.71
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 408.27/225.71
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 408.27/225.71
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 408.27/225.71
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 408.27/225.71
*'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) 408.27/225.71
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2)))) 408.27/225.71
*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2)))) 408.27/225.71
*'(+(+(z0, z1), *(y0, y1)), z3) → c1(*'(+(z0, z1), z3), *'(*(y0, y1), z3)) 408.27/225.71
*'(+(+(*(y0, y1), z1), z2), z3) → c1(*'(+(*(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(*(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(*(y0, y1), y2), z3)) 408.27/225.71
*'(+(+(z0, *(y1, y2)), z2), z3) → c1(*'(+(z0, *(y1, y2)), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(y0, *(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, *(y1, y2)), z3)) 408.27/225.71
*'(+(+(+(y0, y1), z1), z2), z3) → c1(*'(+(+(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(+(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(+(y0, y1), y2), z3)) 408.27/225.71
*'(+(+(z0, +(y1, y2)), z2), z3) → c1(*'(+(z0, +(y1, y2)), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(y0, +(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, +(y1, y2)), z3)) 408.27/225.71
*'(+(+(z0, z1), z2), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(z2, +(y2, f(y3)))) 408.27/225.71
*'(+(+(z0, z1), +(y0, y1)), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(+(y0, y1), +(y2, f(y3)))) 408.27/225.71
*'(+(+(z0, z1), z2), +(f(y1), f(y2))) → c1(*'(+(z0, z1), +(f(y1), f(y2))), *'(z2, +(f(y1), f(y2))))
S tuples:

*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2))))
K tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 408.27/225.71
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 408.27/225.71
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 408.27/225.71
*'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) 408.27/225.71
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2)))) 408.27/225.71
*'(+(+(z0, z1), *(y0, y1)), z3) → c1(*'(+(z0, z1), z3), *'(*(y0, y1), z3)) 408.27/225.71
*'(+(+(*(y0, y1), z1), z2), z3) → c1(*'(+(*(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(*(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(*(y0, y1), y2), z3)) 408.27/225.71
*'(+(+(z0, *(y1, y2)), z2), z3) → c1(*'(+(z0, *(y1, y2)), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(y0, *(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, *(y1, y2)), z3)) 408.27/225.71
*'(+(+(+(y0, y1), z1), z2), z3) → c1(*'(+(+(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(+(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(+(y0, y1), y2), z3)) 408.27/225.71
*'(+(+(z0, +(y1, y2)), z2), z3) → c1(*'(+(z0, +(y1, y2)), z3), *'(z2, z3)) 408.27/225.71
*'(+(+(z0, z1), +(y0, +(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, +(y1, y2)), z3)) 408.27/225.71
*'(+(+(z0, z1), z2), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(z2, +(y2, f(y3)))) 408.27/225.71
*'(+(+(z0, z1), +(y0, y1)), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(+(y0, y1), +(y2, f(y3)))) 408.27/225.71
*'(+(+(z0, z1), z2), +(f(y1), f(y2))) → c1(*'(+(z0, z1), +(f(y1), f(y2))), *'(z2, +(f(y1), f(y2))))
Defined Rule Symbols:

*

Defined Pair Symbols:

*'

Compound Symbols:

c, c1, c2

408.27/225.71
408.27/225.71

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace *'(+(z0, +(y0, y1)), z2) → c1(*'(z0, z2), *'(+(y0, y1), z2)) by

*'(+(*(y0, y1), +(z1, z2)), z3) → c1(*'(*(y0, y1), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(+(*(y0, y1), y2), +(z1, z2)), z3) → c1(*'(+(*(y0, y1), y2), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(*(y0, y1), z2)), z3) → c1(*'(z0, z3), *'(+(*(y0, y1), z2), z3)) 408.27/225.71
*'(+(+(y0, *(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, *(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(z1, *(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, *(y1, y2)), z3)) 408.27/225.71
*'(+(+(y0, +(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, +(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(z1, +(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, +(y1, y2)), z3)) 408.27/225.71
*'(+(+(y0, y1), +(z1, z2)), +(y2, f(y3))) → c1(*'(+(y0, y1), +(y2, f(y3))), *'(+(z1, z2), +(y2, f(y3)))) 408.27/225.71
*'(+(z0, +(z1, z2)), +(y2, f(y3))) → c1(*'(z0, +(y2, f(y3))), *'(+(z1, z2), +(y2, f(y3)))) 408.27/225.71
*'(+(z0, +(z1, z2)), +(f(y1), f(y2))) → c1(*'(z0, +(f(y1), f(y2))), *'(+(z1, z2), +(f(y1), f(y2)))) 408.27/225.71
*'(+(+(+(y0, y1), *(y2, y3)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), *(y2, y3)), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(+(y0, y1), *(y2, y3))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), *(y2, y3)), z3)) 408.27/225.71
*'(+(+(+(*(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(*(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(+(*(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(*(y0, y1), y2), z2), z3)) 408.27/225.71
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(*(y2, y3), y4)), z3)) 408.27/225.71
*'(+(+(+(y0, *(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, *(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(+(y0, *(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, *(y1, y2)), z2), z3)) 408.27/225.71
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, *(y3, y4))), z3)) 408.27/225.71
*'(+(+(+(+(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(+(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.71
*'(+(z0, +(+(+(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(+(y0, y1), y2), z2), z3)) 408.27/225.71
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(+(y2, y3), y4)), z3)) 408.27/225.73
*'(+(+(+(y0, +(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, +(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, +(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, +(y1, y2)), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, +(y3, y4))), z3)) 408.27/225.73
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(y3, f(y4))) → c1(*'(+(+(y0, y1), y2), +(y3, f(y4))), *'(+(z1, z2), +(y3, f(y4)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), z2)), +(y3, f(y4))) → c1(*'(z0, +(y3, f(y4))), *'(+(+(y0, y1), z2), +(y3, f(y4)))) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, y3)), +(z1, z2)), +(y4, f(y5))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5))), *'(+(z1, z2), +(y4, f(y5)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, y3))), +(y4, f(y5))) → c1(*'(z0, +(y4, f(y5))), *'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5)))) 408.27/225.73
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(f(y3), f(y4))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(y4))), *'(+(z1, z2), +(f(y3), f(y4)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), z2)), +(f(y3), f(y4))) → c1(*'(z0, +(f(y3), f(y4))), *'(+(+(y0, y1), z2), +(f(y3), f(y4))))
408.27/225.73
408.27/225.73

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 408.27/225.73
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 408.27/225.73
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 408.27/225.73
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 408.27/225.73
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 408.27/225.73
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2)))) 408.27/225.73
*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2)))) 408.27/225.73
*'(+(+(z0, z1), *(y0, y1)), z3) → c1(*'(+(z0, z1), z3), *'(*(y0, y1), z3)) 408.27/225.73
*'(+(+(*(y0, y1), z1), z2), z3) → c1(*'(+(*(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(*(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(*(y0, y1), y2), z3)) 408.27/225.73
*'(+(+(z0, *(y1, y2)), z2), z3) → c1(*'(+(z0, *(y1, y2)), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(y0, *(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, *(y1, y2)), z3)) 408.27/225.73
*'(+(+(+(y0, y1), z1), z2), z3) → c1(*'(+(+(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(+(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(+(y0, y1), y2), z3)) 408.27/225.73
*'(+(+(z0, +(y1, y2)), z2), z3) → c1(*'(+(z0, +(y1, y2)), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(y0, +(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, +(y1, y2)), z3)) 408.27/225.73
*'(+(+(z0, z1), z2), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(z2, +(y2, f(y3)))) 408.27/225.73
*'(+(+(z0, z1), +(y0, y1)), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(+(y0, y1), +(y2, f(y3)))) 408.27/225.73
*'(+(+(z0, z1), z2), +(f(y1), f(y2))) → c1(*'(+(z0, z1), +(f(y1), f(y2))), *'(z2, +(f(y1), f(y2)))) 408.27/225.73
*'(+(*(y0, y1), +(z1, z2)), z3) → c1(*'(*(y0, y1), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(+(*(y0, y1), y2), +(z1, z2)), z3) → c1(*'(+(*(y0, y1), y2), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(*(y0, y1), z2)), z3) → c1(*'(z0, z3), *'(+(*(y0, y1), z2), z3)) 408.27/225.73
*'(+(+(y0, *(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, *(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(z1, *(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, *(y1, y2)), z3)) 408.27/225.73
*'(+(+(y0, +(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, +(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(z1, +(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, +(y1, y2)), z3)) 408.27/225.73
*'(+(z0, +(z1, z2)), +(y2, f(y3))) → c1(*'(z0, +(y2, f(y3))), *'(+(z1, z2), +(y2, f(y3)))) 408.27/225.73
*'(+(z0, +(z1, z2)), +(f(y1), f(y2))) → c1(*'(z0, +(f(y1), f(y2))), *'(+(z1, z2), +(f(y1), f(y2)))) 408.27/225.73
*'(+(+(+(y0, y1), *(y2, y3)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), *(y2, y3)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), *(y2, y3))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), *(y2, y3)), z3)) 408.27/225.73
*'(+(+(+(*(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(*(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(*(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(*(y0, y1), y2), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(*(y2, y3), y4)), z3)) 408.27/225.73
*'(+(+(+(y0, *(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, *(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, *(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, *(y1, y2)), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, *(y3, y4))), z3)) 408.27/225.73
*'(+(+(+(+(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(+(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(+(y0, y1), y2), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(+(y2, y3), y4)), z3)) 408.27/225.73
*'(+(+(+(y0, +(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, +(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, +(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, +(y1, y2)), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, +(y3, y4))), z3)) 408.27/225.73
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(y3, f(y4))) → c1(*'(+(+(y0, y1), y2), +(y3, f(y4))), *'(+(z1, z2), +(y3, f(y4)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), z2)), +(y3, f(y4))) → c1(*'(z0, +(y3, f(y4))), *'(+(+(y0, y1), z2), +(y3, f(y4)))) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, y3)), +(z1, z2)), +(y4, f(y5))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5))), *'(+(z1, z2), +(y4, f(y5)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, y3))), +(y4, f(y5))) → c1(*'(z0, +(y4, f(y5))), *'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5)))) 408.27/225.73
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(f(y3), f(y4))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(y4))), *'(+(z1, z2), +(f(y3), f(y4)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), z2)), +(f(y3), f(y4))) → c1(*'(z0, +(f(y3), f(y4))), *'(+(+(y0, y1), z2), +(f(y3), f(y4))))
S tuples:

*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2))))
K tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 408.27/225.73
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 408.27/225.73
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 408.27/225.73
*'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2)))) 408.27/225.73
*'(+(+(z0, z1), *(y0, y1)), z3) → c1(*'(+(z0, z1), z3), *'(*(y0, y1), z3)) 408.27/225.73
*'(+(+(*(y0, y1), z1), z2), z3) → c1(*'(+(*(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(*(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(*(y0, y1), y2), z3)) 408.27/225.73
*'(+(+(z0, *(y1, y2)), z2), z3) → c1(*'(+(z0, *(y1, y2)), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(y0, *(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, *(y1, y2)), z3)) 408.27/225.73
*'(+(+(+(y0, y1), z1), z2), z3) → c1(*'(+(+(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(+(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(+(y0, y1), y2), z3)) 408.27/225.73
*'(+(+(z0, +(y1, y2)), z2), z3) → c1(*'(+(z0, +(y1, y2)), z3), *'(z2, z3)) 408.27/225.73
*'(+(+(z0, z1), +(y0, +(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, +(y1, y2)), z3)) 408.27/225.73
*'(+(+(z0, z1), z2), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(z2, +(y2, f(y3)))) 408.27/225.73
*'(+(+(z0, z1), +(y0, y1)), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(+(y0, y1), +(y2, f(y3)))) 408.27/225.73
*'(+(+(z0, z1), z2), +(f(y1), f(y2))) → c1(*'(+(z0, z1), +(f(y1), f(y2))), *'(z2, +(f(y1), f(y2)))) 408.27/225.73
*'(+(*(y0, y1), +(z1, z2)), z3) → c1(*'(*(y0, y1), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(+(*(y0, y1), y2), +(z1, z2)), z3) → c1(*'(+(*(y0, y1), y2), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(*(y0, y1), z2)), z3) → c1(*'(z0, z3), *'(+(*(y0, y1), z2), z3)) 408.27/225.73
*'(+(+(y0, *(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, *(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(z1, *(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, *(y1, y2)), z3)) 408.27/225.73
*'(+(+(y0, +(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, +(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(z1, +(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, +(y1, y2)), z3)) 408.27/225.73
*'(+(z0, +(z1, z2)), +(y2, f(y3))) → c1(*'(z0, +(y2, f(y3))), *'(+(z1, z2), +(y2, f(y3)))) 408.27/225.73
*'(+(z0, +(z1, z2)), +(f(y1), f(y2))) → c1(*'(z0, +(f(y1), f(y2))), *'(+(z1, z2), +(f(y1), f(y2)))) 408.27/225.73
*'(+(+(+(y0, y1), *(y2, y3)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), *(y2, y3)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), *(y2, y3))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), *(y2, y3)), z3)) 408.27/225.73
*'(+(+(+(*(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(*(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(*(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(*(y0, y1), y2), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(*(y2, y3), y4)), z3)) 408.27/225.73
*'(+(+(+(y0, *(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, *(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, *(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, *(y1, y2)), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, *(y3, y4))), z3)) 408.27/225.73
*'(+(+(+(+(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(+(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(+(y0, y1), y2), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(+(y2, y3), y4)), z3)) 408.27/225.73
*'(+(+(+(y0, +(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, +(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, +(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, +(y1, y2)), z2), z3)) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, +(y3, y4))), z3)) 408.27/225.73
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(y3, f(y4))) → c1(*'(+(+(y0, y1), y2), +(y3, f(y4))), *'(+(z1, z2), +(y3, f(y4)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), z2)), +(y3, f(y4))) → c1(*'(z0, +(y3, f(y4))), *'(+(+(y0, y1), z2), +(y3, f(y4)))) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, y3)), +(z1, z2)), +(y4, f(y5))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5))), *'(+(z1, z2), +(y4, f(y5)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, y3))), +(y4, f(y5))) → c1(*'(z0, +(y4, f(y5))), *'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5)))) 408.27/225.73
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(f(y3), f(y4))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(y4))), *'(+(z1, z2), +(f(y3), f(y4)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), z2)), +(f(y3), f(y4))) → c1(*'(z0, +(f(y3), f(y4))), *'(+(+(y0, y1), z2), +(f(y3), f(y4))))
Defined Rule Symbols:

*

Defined Pair Symbols:

*'

Compound Symbols:

c, c1, c2

408.27/225.73
408.27/225.73

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace *'(+(z0, z1), +(y1, f(y2))) → c1(*'(z0, +(y1, f(y2))), *'(z1, +(y1, f(y2)))) by

*'(+(*(y0, y1), z1), +(z2, f(z3))) → c1(*'(*(y0, y1), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, *(y0, y1)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(*(y0, y1), +(z2, f(z3)))) 408.27/225.73
*'(+(+(*(y0, y1), y2), z1), +(z2, f(z3))) → c1(*'(+(*(y0, y1), y2), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(*(y0, y1), y2)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(*(y0, y1), y2), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, *(y1, y2)), z1), +(z2, f(z3))) → c1(*'(+(y0, *(y1, y2)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, *(y1, y2))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, *(y1, y2)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, y1), z1), +(z2, f(z3))) → c1(*'(+(y0, y1), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, y1)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, y1), +(z2, f(z3)))) 408.27/225.73
*'(+(z0, z1), +(f(y1), f(z3))) → c1(*'(z0, +(f(y1), f(z3))), *'(z1, +(f(y1), f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), *(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), *(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), *(y2, y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), *(y2, y3)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(*(y0, y1), y2), y3), z1), +(z2, f(z3))) → c1(*'(+(+(*(y0, y1), y2), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(*(y0, y1), y2), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(*(y0, y1), y2), y3), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(*(y2, y3), y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, *(y1, y2)), y3), z1), +(z2, f(z3))) → c1(*'(+(+(y0, *(y1, y2)), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, *(y1, y2)), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, *(y1, y2)), y3), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(y2, *(y3, y4))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, y1), y2), y3), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), y2), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), y2), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), y2), y3), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(+(y2, y3), y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, +(y1, y2)), y3), z1), +(z2, f(z3))) → c1(*'(+(+(y0, +(y1, y2)), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, +(y1, y2)), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, +(y1, y2)), y3), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(y2, +(y3, y4))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), y2), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), y2), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), y2)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), y2), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), +(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), +(y2, y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(y2, y3)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, y1), y2), z1), +(f(y3), f(z3))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(z3))), *'(z1, +(f(y3), f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, y1), y2)), +(f(y3), f(z3))) → c1(*'(z0, +(f(y3), f(z3))), *'(+(+(y0, y1), y2), +(f(y3), f(z3)))) 408.27/225.73
*'(+(+(*(y0, y1), +(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(*(y0, y1), +(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(*(y0, y1), +(y2, y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(*(y0, y1), +(y2, y3)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(*(y0, y1), y2), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(*(y0, y1), y2), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(*(y0, y1), y2), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(*(y0, y1), y2), +(y3, y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(*(y1, y2), y3)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(*(y1, y2), y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(*(y1, y2), y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(*(y1, y2), y3)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, *(y1, y2)), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, *(y1, y2)), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, *(y1, y2)), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, *(y1, y2)), +(y3, y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(y1, *(y2, y3))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, *(y2, y3))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(y1, *(y2, y3)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, *(y2, y3))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(y0, +(y1, y2)), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, +(y1, y2)), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(y0, +(y1, y2)), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, +(y1, y2)), +(y3, y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(y1, +(y2, y3))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, +(y2, y3))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(y1, +(y2, y3)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, +(y2, y3))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(y1, y2)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, y2)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(y1, y2))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, y2)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(y1, y2)), z1), +(f(y3), f(z3))) → c1(*'(+(y0, +(y1, y2)), +(f(y3), f(z3))), *'(z1, +(f(y3), f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(y1, y2))), +(f(y3), f(z3))) → c1(*'(z0, +(f(y3), f(z3))), *'(+(y0, +(y1, y2)), +(f(y3), f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), *(y2, y3)), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, y2), *(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), *(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, y2), *(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), *(y3, y4))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(*(y0, y1), y2), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(*(y1, y2), y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(*(y1, y2), y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(*(y1, y2), y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(*(y1, y2), y3), y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, y2), +(*(y3, y4), y5)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, *(y1, y2)), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, *(y2, y3)), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, *(y2, y3)), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, *(y2, y3)), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, *(y2, y3)), y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, y2), +(y3, *(y4, y5))))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(+(y0, y1), y2), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(+(y1, y2), y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(+(y1, y2), y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(+(y1, y2), y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(+(y1, y2), y3), y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, y2), +(+(y3, y4), y5)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, +(y1, y2)), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, +(y2, y3)), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, +(y2, y3)), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, +(y2, y3)), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, +(y2, y3)), y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, y2), +(y3, +(y4, y5))))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), +(z2, f(z3)))) 408.27/225.73
*'(+(+(+(+(y0, y1), y2), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), y2), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(+(+(y0, y1), y2), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), y2), +(y3, y4)), +(z2, f(z3)))) 408.27/225.73
*'(+(+(y0, +(+(y1, y2), y3)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.73
*'(+(z0, +(y0, +(+(y1, y2), y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(y2, y3)), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), +(y3, y4)), z1), +(f(y5), f(z3))) → c1(*'(+(+(+(y0, y1), y2), +(y3, y4)), +(f(y5), f(z3))), *'(z1, +(f(y5), f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), +(y3, y4))), +(f(y5), f(z3))) → c1(*'(z0, +(f(y5), f(z3))), *'(+(+(+(y0, y1), y2), +(y3, y4)), +(f(y5), f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), y3)), z1), +(f(y4), f(z3))) → c1(*'(+(y0, +(+(y1, y2), y3)), +(f(y4), f(z3))), *'(z1, +(f(y4), f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), y3))), +(f(y4), f(z3))) → c1(*'(z0, +(f(y4), f(z3))), *'(+(y0, +(+(y1, y2), y3)), +(f(y4), f(z3))))
408.27/225.77
408.27/225.77

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

*(*(z0, z1), z2) → *(z0, *(z1, z2)) 408.27/225.77
*(+(z0, z1), z2) → +(*(z0, z2), *(z1, z2)) 408.27/225.77
*(z0, +(z1, f(z2))) → *(g(z0, z2), +(z1, z1))
Tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 408.27/225.77
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 408.27/225.77
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 408.27/225.77
*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2)))) 408.27/225.77
*'(+(+(z0, z1), *(y0, y1)), z3) → c1(*'(+(z0, z1), z3), *'(*(y0, y1), z3)) 408.27/225.77
*'(+(+(*(y0, y1), z1), z2), z3) → c1(*'(+(*(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(*(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(*(y0, y1), y2), z3)) 408.27/225.77
*'(+(+(z0, *(y1, y2)), z2), z3) → c1(*'(+(z0, *(y1, y2)), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(y0, *(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, *(y1, y2)), z3)) 408.27/225.77
*'(+(+(+(y0, y1), z1), z2), z3) → c1(*'(+(+(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(+(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(+(y0, y1), y2), z3)) 408.27/225.77
*'(+(+(z0, +(y1, y2)), z2), z3) → c1(*'(+(z0, +(y1, y2)), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(y0, +(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, +(y1, y2)), z3)) 408.27/225.77
*'(+(+(z0, z1), z2), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(z2, +(y2, f(y3)))) 408.27/225.77
*'(+(+(z0, z1), +(y0, y1)), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(+(y0, y1), +(y2, f(y3)))) 408.27/225.77
*'(+(+(z0, z1), z2), +(f(y1), f(y2))) → c1(*'(+(z0, z1), +(f(y1), f(y2))), *'(z2, +(f(y1), f(y2)))) 408.27/225.77
*'(+(*(y0, y1), +(z1, z2)), z3) → c1(*'(*(y0, y1), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(+(*(y0, y1), y2), +(z1, z2)), z3) → c1(*'(+(*(y0, y1), y2), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(*(y0, y1), z2)), z3) → c1(*'(z0, z3), *'(+(*(y0, y1), z2), z3)) 408.27/225.77
*'(+(+(y0, *(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, *(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(z1, *(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, *(y1, y2)), z3)) 408.27/225.77
*'(+(+(y0, +(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, +(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(z1, +(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, +(y1, y2)), z3)) 408.27/225.77
*'(+(z0, +(z1, z2)), +(y2, f(y3))) → c1(*'(z0, +(y2, f(y3))), *'(+(z1, z2), +(y2, f(y3)))) 408.27/225.77
*'(+(z0, +(z1, z2)), +(f(y1), f(y2))) → c1(*'(z0, +(f(y1), f(y2))), *'(+(z1, z2), +(f(y1), f(y2)))) 408.27/225.77
*'(+(+(+(y0, y1), *(y2, y3)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), *(y2, y3)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), *(y2, y3))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), *(y2, y3)), z3)) 408.27/225.77
*'(+(+(+(*(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(*(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(*(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(*(y0, y1), y2), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(*(y2, y3), y4)), z3)) 408.27/225.77
*'(+(+(+(y0, *(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, *(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, *(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, *(y1, y2)), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, *(y3, y4))), z3)) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(+(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(+(y0, y1), y2), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(+(y2, y3), y4)), z3)) 408.27/225.77
*'(+(+(+(y0, +(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, +(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, +(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, +(y1, y2)), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, +(y3, y4))), z3)) 408.27/225.77
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(y3, f(y4))) → c1(*'(+(+(y0, y1), y2), +(y3, f(y4))), *'(+(z1, z2), +(y3, f(y4)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), z2)), +(y3, f(y4))) → c1(*'(z0, +(y3, f(y4))), *'(+(+(y0, y1), z2), +(y3, f(y4)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, y3)), +(z1, z2)), +(y4, f(y5))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5))), *'(+(z1, z2), +(y4, f(y5)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, y3))), +(y4, f(y5))) → c1(*'(z0, +(y4, f(y5))), *'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5)))) 408.27/225.77
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(f(y3), f(y4))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(y4))), *'(+(z1, z2), +(f(y3), f(y4)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), z2)), +(f(y3), f(y4))) → c1(*'(z0, +(f(y3), f(y4))), *'(+(+(y0, y1), z2), +(f(y3), f(y4)))) 408.27/225.77
*'(+(*(y0, y1), z1), +(z2, f(z3))) → c1(*'(*(y0, y1), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, *(y0, y1)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(*(y0, y1), +(z2, f(z3)))) 408.27/225.77
*'(+(+(*(y0, y1), y2), z1), +(z2, f(z3))) → c1(*'(+(*(y0, y1), y2), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(*(y0, y1), y2)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(*(y0, y1), y2), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, *(y1, y2)), z1), +(z2, f(z3))) → c1(*'(+(y0, *(y1, y2)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, *(y1, y2))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, *(y1, y2)), +(z2, f(z3)))) 408.27/225.77
*'(+(z0, z1), +(f(y1), f(z3))) → c1(*'(z0, +(f(y1), f(z3))), *'(z1, +(f(y1), f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), *(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), *(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), *(y2, y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), *(y2, y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(*(y0, y1), y2), y3), z1), +(z2, f(z3))) → c1(*'(+(+(*(y0, y1), y2), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(*(y0, y1), y2), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(*(y0, y1), y2), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(*(y2, y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, *(y1, y2)), y3), z1), +(z2, f(z3))) → c1(*'(+(+(y0, *(y1, y2)), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, *(y1, y2)), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, *(y1, y2)), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(y2, *(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), y3), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), y2), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), y2), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(+(y2, y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, +(y1, y2)), y3), z1), +(z2, f(z3))) → c1(*'(+(+(y0, +(y1, y2)), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, +(y1, y2)), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, +(y1, y2)), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(y2, +(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), y2), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), y2), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), y2), z1), +(f(y3), f(z3))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(z3))), *'(z1, +(f(y3), f(z3)))) 408.27/225.77
*'(+(+(*(y0, y1), +(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(*(y0, y1), +(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(*(y0, y1), +(y2, y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(*(y0, y1), +(y2, y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(*(y0, y1), y2), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(*(y0, y1), y2), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(*(y0, y1), y2), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(*(y0, y1), y2), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(*(y1, y2), y3)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(*(y1, y2), y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(*(y1, y2), y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(*(y1, y2), y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, *(y1, y2)), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, *(y1, y2)), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, *(y1, y2)), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, *(y1, y2)), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, *(y2, y3))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, *(y2, y3))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, *(y2, y3)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, *(y2, y3))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, +(y1, y2)), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, +(y1, y2)), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, +(y1, y2)), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, +(y1, y2)), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, +(y2, y3))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, +(y2, y3))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, +(y2, y3)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, +(y2, y3))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, y2)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, y2)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, y2))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, y2)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, y2)), z1), +(f(y3), f(z3))) → c1(*'(+(y0, +(y1, y2)), +(f(y3), f(z3))), *'(z1, +(f(y3), f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, y2))), +(f(y3), f(z3))) → c1(*'(z0, +(f(y3), f(z3))), *'(+(y0, +(y1, y2)), +(f(y3), f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), *(y2, y3)), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), *(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), *(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), *(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), *(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(*(y0, y1), y2), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(*(y1, y2), y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(*(y1, y2), y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(*(y1, y2), y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(*(y1, y2), y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(*(y3, y4), y5)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, *(y1, y2)), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, *(y2, y3)), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, *(y2, y3)), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, *(y2, y3)), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, *(y2, y3)), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(y3, *(y4, y5))))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(+(y0, y1), y2), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(+(y1, y2), y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(+(y1, y2), y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(+(y1, y2), y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(+(y1, y2), y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(+(y3, y4), y5)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, +(y1, y2)), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, +(y2, y3)), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, +(y2, y3)), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, +(y2, y3)), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, +(y2, y3)), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(y3, +(y4, y5))))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), y2), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), y2), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), y3)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(y2, y3)), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), +(y3, y4)), z1), +(f(y5), f(z3))) → c1(*'(+(+(+(y0, y1), y2), +(y3, y4)), +(f(y5), f(z3))), *'(z1, +(f(y5), f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), +(y3, y4))), +(f(y5), f(z3))) → c1(*'(z0, +(f(y5), f(z3))), *'(+(+(+(y0, y1), y2), +(y3, y4)), +(f(y5), f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), y3)), z1), +(f(y4), f(z3))) → c1(*'(+(y0, +(+(y1, y2), y3)), +(f(y4), f(z3))), *'(z1, +(f(y4), f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), y3))), +(f(y4), f(z3))) → c1(*'(z0, +(f(y4), f(z3))), *'(+(y0, +(+(y1, y2), y3)), +(f(y4), f(z3))))
S tuples:

*'(z0, +(f(y2), f(z2))) → c2(*'(g(z0, z2), +(f(y2), f(y2))))
K tuples:

*'(*(z0, z1), z2) → c(*'(z0, *(z1, z2)), *'(z1, z2)) 408.27/225.77
*'(+(*(y0, y1), z1), z2) → c1(*'(*(y0, y1), z2), *'(z1, z2)) 408.27/225.77
*'(+(z0, *(y0, y1)), z2) → c1(*'(z0, z2), *'(*(y0, y1), z2)) 408.27/225.77
*'(+(+(z0, z1), *(y0, y1)), z3) → c1(*'(+(z0, z1), z3), *'(*(y0, y1), z3)) 408.27/225.77
*'(+(+(*(y0, y1), z1), z2), z3) → c1(*'(+(*(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(*(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(*(y0, y1), y2), z3)) 408.27/225.77
*'(+(+(z0, *(y1, y2)), z2), z3) → c1(*'(+(z0, *(y1, y2)), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(y0, *(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, *(y1, y2)), z3)) 408.27/225.77
*'(+(+(+(y0, y1), z1), z2), z3) → c1(*'(+(+(y0, y1), z1), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(+(y0, y1), y2)), z3) → c1(*'(+(z0, z1), z3), *'(+(+(y0, y1), y2), z3)) 408.27/225.77
*'(+(+(z0, +(y1, y2)), z2), z3) → c1(*'(+(z0, +(y1, y2)), z3), *'(z2, z3)) 408.27/225.77
*'(+(+(z0, z1), +(y0, +(y1, y2))), z3) → c1(*'(+(z0, z1), z3), *'(+(y0, +(y1, y2)), z3)) 408.27/225.77
*'(+(+(z0, z1), z2), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(z2, +(y2, f(y3)))) 408.27/225.77
*'(+(+(z0, z1), +(y0, y1)), +(y2, f(y3))) → c1(*'(+(z0, z1), +(y2, f(y3))), *'(+(y0, y1), +(y2, f(y3)))) 408.27/225.77
*'(+(+(z0, z1), z2), +(f(y1), f(y2))) → c1(*'(+(z0, z1), +(f(y1), f(y2))), *'(z2, +(f(y1), f(y2)))) 408.27/225.77
*'(+(*(y0, y1), +(z1, z2)), z3) → c1(*'(*(y0, y1), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(+(*(y0, y1), y2), +(z1, z2)), z3) → c1(*'(+(*(y0, y1), y2), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(*(y0, y1), z2)), z3) → c1(*'(z0, z3), *'(+(*(y0, y1), z2), z3)) 408.27/225.77
*'(+(+(y0, *(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, *(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(z1, *(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, *(y1, y2)), z3)) 408.27/225.77
*'(+(+(y0, +(y1, y2)), +(z1, z2)), z3) → c1(*'(+(y0, +(y1, y2)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(z1, +(y1, y2))), z3) → c1(*'(z0, z3), *'(+(z1, +(y1, y2)), z3)) 408.27/225.77
*'(+(z0, +(z1, z2)), +(y2, f(y3))) → c1(*'(z0, +(y2, f(y3))), *'(+(z1, z2), +(y2, f(y3)))) 408.27/225.77
*'(+(z0, +(z1, z2)), +(f(y1), f(y2))) → c1(*'(z0, +(f(y1), f(y2))), *'(+(z1, z2), +(f(y1), f(y2)))) 408.27/225.77
*'(+(+(+(y0, y1), *(y2, y3)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), *(y2, y3)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), *(y2, y3))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), *(y2, y3)), z3)) 408.27/225.77
*'(+(+(+(*(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(*(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(*(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(*(y0, y1), y2), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(*(y2, y3), y4)), z3)) 408.27/225.77
*'(+(+(+(y0, *(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, *(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, *(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, *(y1, y2)), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, *(y3, y4))), z3)) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), y3), +(z1, z2)), z3) → c1(*'(+(+(+(y0, y1), y2), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), z2)), z3) → c1(*'(z0, z3), *'(+(+(+(y0, y1), y2), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(+(y2, y3), y4)), z3)) 408.27/225.77
*'(+(+(+(y0, +(y1, y2)), y3), +(z1, z2)), z3) → c1(*'(+(+(y0, +(y1, y2)), y3), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, +(y1, y2)), z2)), z3) → c1(*'(z0, z3), *'(+(+(y0, +(y1, y2)), z2), z3)) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(z1, z2)), z3) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), z3), *'(+(z1, z2), z3)) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), z3) → c1(*'(z0, z3), *'(+(+(y0, y1), +(y2, +(y3, y4))), z3)) 408.27/225.77
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(y3, f(y4))) → c1(*'(+(+(y0, y1), y2), +(y3, f(y4))), *'(+(z1, z2), +(y3, f(y4)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), z2)), +(y3, f(y4))) → c1(*'(z0, +(y3, f(y4))), *'(+(+(y0, y1), z2), +(y3, f(y4)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, y3)), +(z1, z2)), +(y4, f(y5))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5))), *'(+(z1, z2), +(y4, f(y5)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, y3))), +(y4, f(y5))) → c1(*'(z0, +(y4, f(y5))), *'(+(+(y0, y1), +(y2, y3)), +(y4, f(y5)))) 408.27/225.77
*'(+(+(+(y0, y1), y2), +(z1, z2)), +(f(y3), f(y4))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(y4))), *'(+(z1, z2), +(f(y3), f(y4)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), z2)), +(f(y3), f(y4))) → c1(*'(z0, +(f(y3), f(y4))), *'(+(+(y0, y1), z2), +(f(y3), f(y4)))) 408.27/225.77
*'(+(*(y0, y1), z1), +(z2, f(z3))) → c1(*'(*(y0, y1), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, *(y0, y1)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(*(y0, y1), +(z2, f(z3)))) 408.27/225.77
*'(+(+(*(y0, y1), y2), z1), +(z2, f(z3))) → c1(*'(+(*(y0, y1), y2), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(*(y0, y1), y2)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(*(y0, y1), y2), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, *(y1, y2)), z1), +(z2, f(z3))) → c1(*'(+(y0, *(y1, y2)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, *(y1, y2))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, *(y1, y2)), +(z2, f(z3)))) 408.27/225.77
*'(+(z0, z1), +(f(y1), f(z3))) → c1(*'(z0, +(f(y1), f(z3))), *'(z1, +(f(y1), f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), *(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), *(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), *(y2, y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), *(y2, y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(*(y0, y1), y2), y3), z1), +(z2, f(z3))) → c1(*'(+(+(*(y0, y1), y2), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(*(y0, y1), y2), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(*(y0, y1), y2), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(*(y2, y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(*(y2, y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(*(y2, y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(*(y2, y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, *(y1, y2)), y3), z1), +(z2, f(z3))) → c1(*'(+(+(y0, *(y1, y2)), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, *(y1, y2)), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, *(y1, y2)), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, *(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, *(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, *(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(y2, *(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), y3), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), y2), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), y2), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(+(y2, y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(+(y2, y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(+(y2, y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(+(y2, y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, +(y1, y2)), y3), z1), +(z2, f(z3))) → c1(*'(+(+(y0, +(y1, y2)), y3), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, +(y1, y2)), y3)), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, +(y1, y2)), y3), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, +(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, +(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, y1), +(y2, +(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, y1), +(y2, +(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), y2), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), y2), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), +(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, y1), +(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, y1), y2), z1), +(f(y3), f(z3))) → c1(*'(+(+(y0, y1), y2), +(f(y3), f(z3))), *'(z1, +(f(y3), f(z3)))) 408.27/225.77
*'(+(+(*(y0, y1), +(y2, y3)), z1), +(z2, f(z3))) → c1(*'(+(*(y0, y1), +(y2, y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(*(y0, y1), +(y2, y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(*(y0, y1), +(y2, y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(*(y0, y1), y2), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(*(y0, y1), y2), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(*(y0, y1), y2), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(*(y0, y1), y2), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(*(y1, y2), y3)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(*(y1, y2), y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(*(y1, y2), y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(*(y1, y2), y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, *(y1, y2)), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, *(y1, y2)), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, *(y1, y2)), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, *(y1, y2)), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, *(y2, y3))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, *(y2, y3))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, *(y2, y3)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, *(y2, y3))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(y0, +(y1, y2)), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(y0, +(y1, y2)), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(y0, +(y1, y2)), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(y0, +(y1, y2)), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, +(y2, y3))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, +(y2, y3))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, +(y2, y3)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, +(y2, y3))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, y2)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(y1, y2)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, y2))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(y1, y2)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(y1, y2)), z1), +(f(y3), f(z3))) → c1(*'(+(y0, +(y1, y2)), +(f(y3), f(z3))), *'(z1, +(f(y3), f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(y1, y2))), +(f(y3), f(z3))) → c1(*'(z0, +(f(y3), f(z3))), *'(+(y0, +(y1, y2)), +(f(y3), f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), *(y2, y3)), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), *(y2, y3)), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), *(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), *(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), *(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), *(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(*(y0, y1), y2), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(*(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(*(y1, y2), y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(*(y1, y2), y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(*(y1, y2), y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(*(y1, y2), y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(*(y2, y3), y4)), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(*(y3, y4), y5)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(*(y3, y4), y5))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, *(y1, y2)), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, *(y1, y2)), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, *(y2, y3)), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, *(y2, y3)), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, *(y2, y3)), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, *(y2, y3)), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, *(y3, y4))), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(y3, *(y4, y5))))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, *(y4, y5)))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(+(y0, y1), y2), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(+(y0, y1), y2), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(+(y1, y2), y3), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(+(y1, y2), y3), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(+(y1, y2), y3), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(+(y1, y2), y3), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(+(y2, y3), y4)), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(+(y3, y4), y5)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(+(y3, y4), y5))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, +(y1, y2)), y3), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, +(y1, y2)), y3), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, +(y2, y3)), y4)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, +(y2, y3)), y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, +(y2, y3)), y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, +(y2, y3)), y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, +(y3, y4))), +(y5, y6)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(y3, +(y4, y5))))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, +(y4, y5)))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), +(y3, y4)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), y2), +(y3, y4)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), +(y3, y4))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), y2), +(y3, y4)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), y3)), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), y3)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), y3))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), y3)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), z1), +(z2, f(z3))) → c1(*'(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), +(y2, y3)), +(y4, y5))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(+(+(y0, y1), +(y2, y3)), +(y4, y5)), +(z2, f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), +(y3, y4))), z1), +(z2, f(z3))) → c1(*'(+(y0, +(+(y1, y2), +(y3, y4))), +(z2, f(z3))), *'(z1, +(z2, f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), +(y3, y4)))), +(z2, f(z3))) → c1(*'(z0, +(z2, f(z3))), *'(+(y0, +(+(y1, y2), +(y3, y4))), +(z2, f(z3)))) 408.27/225.77
*'(+(+(+(+(y0, y1), y2), +(y3, y4)), z1), +(f(y5), f(z3))) → c1(*'(+(+(+(y0, y1), y2), +(y3, y4)), +(f(y5), f(z3))), *'(z1, +(f(y5), f(z3)))) 408.27/225.77
*'(+(z0, +(+(+(y0, y1), y2), +(y3, y4))), +(f(y5), f(z3))) → c1(*'(z0, +(f(y5), f(z3))), *'(+(+(+(y0, y1), y2), +(y3, y4)), +(f(y5), f(z3)))) 408.27/225.77
*'(+(+(y0, +(+(y1, y2), y3)), z1), +(f(y4), f(z3))) → c1(*'(+(y0, +(+(y1, y2), y3)), +(f(y4), f(z3))), *'(z1, +(f(y4), f(z3)))) 408.27/225.77
*'(+(z0, +(y0, +(+(y1, y2), y3))), +(f(y4), f(z3))) → c1(*'(z0, +(f(y4), f(z3))), *'(+(y0, +(+(y1, y2), y3)), +(f(y4), f(z3))))
Defined Rule Symbols:

*

Defined Pair Symbols:

*'

Compound Symbols:

c, c1, c2

408.27/225.77
408.27/225.77
408.57/225.84 EOF