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

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

(0) Obligation:

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

merge(nil, y) → y 18.11/6.63
merge(x, nil) → x 18.11/6.63
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))) 18.11/6.63
++(nil, y) → y 18.11/6.63
++(.(x, y), z) → .(x, ++(y, z)) 18.11/6.63
if(true, x, y) → x 18.11/6.63
if(false, x, y) → x

Rewrite Strategy: INNERMOST
18.11/6.63
18.11/6.63

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

Converted CpxTRS to CDT
18.11/6.63
18.11/6.63

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.63
merge(z0, nil) → z0 18.11/6.63
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.63
++(nil, z0) → z0 18.11/6.63
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.63
if(true, z0, z1) → z0 18.11/6.63
if(false, z0, z1) → z0
Tuples:

MERGE(.(z0, z1), .(z2, z3)) → c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3)) 18.11/6.63
++'(.(z0, z1), z2) → c4(++'(z1, z2))
S tuples:

MERGE(.(z0, z1), .(z2, z3)) → c2(IF(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))), MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3)) 18.11/6.63
++'(.(z0, z1), z2) → c4(++'(z1, z2))
K tuples:none
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

MERGE, ++'

Compound Symbols:

c2, c4

18.11/6.63
18.11/6.63

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
18.11/6.63
18.11/6.63

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.63
merge(z0, nil) → z0 18.11/6.63
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.63
++(nil, z0) → z0 18.11/6.63
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.63
if(true, z0, z1) → z0 18.11/6.63
if(false, z0, z1) → z0
Tuples:

++'(.(z0, z1), z2) → c4(++'(z1, z2)) 18.11/6.63
MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3))
S tuples:

++'(.(z0, z1), z2) → c4(++'(z1, z2)) 18.11/6.63
MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3))
K tuples:none
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

++', MERGE

Compound Symbols:

c4, c2

18.11/6.63
18.11/6.63

(5) 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) → c4(++'(z1, z2))
We considered the (Usable) Rules:none
And the Tuples:

++'(.(z0, z1), z2) → c4(++'(z1, z2)) 18.11/6.63
MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 18.11/6.63

POL(++'(x1, x2)) = [3]x1    18.11/6.63
POL(.(x1, x2)) = [1] + x2    18.11/6.63
POL(MERGE(x1, x2)) = 0    18.11/6.63
POL(c2(x1, x2)) = x1 + x2    18.11/6.63
POL(c4(x1)) = x1   
18.11/6.63
18.11/6.63

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.63
merge(z0, nil) → z0 18.11/6.63
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.63
++(nil, z0) → z0 18.11/6.64
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.64
if(true, z0, z1) → z0 18.11/6.64
if(false, z0, z1) → z0
Tuples:

++'(.(z0, z1), z2) → c4(++'(z1, z2)) 18.11/6.64
MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3))
S tuples:

MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3))
K tuples:

++'(.(z0, z1), z2) → c4(++'(z1, z2))
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

++', MERGE

Compound Symbols:

c4, c2

18.11/6.64
18.11/6.64

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

Use forward instantiation to replace ++'(.(z0, z1), z2) → c4(++'(z1, z2)) by

++'(.(z0, .(y0, y1)), z2) → c4(++'(.(y0, y1), z2))
18.11/6.64
18.11/6.64

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.64
merge(z0, nil) → z0 18.11/6.64
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.64
++(nil, z0) → z0 18.11/6.64
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.64
if(true, z0, z1) → z0 18.11/6.64
if(false, z0, z1) → z0
Tuples:

MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3)) 18.11/6.64
++'(.(z0, .(y0, y1)), z2) → c4(++'(.(y0, y1), z2))
S tuples:

MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3))
K tuples:

++'(.(z0, .(y0, y1)), z2) → c4(++'(.(y0, y1), z2))
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

MERGE, ++'

Compound Symbols:

c2, c4

18.11/6.64
18.11/6.64

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

Use forward instantiation to replace MERGE(.(z0, z1), .(z2, z3)) → c2(MERGE(z1, .(z2, z3)), MERGE(.(z0, z1), z3)) by

MERGE(.(z0, .(y0, y1)), .(z2, z3)) → c2(MERGE(.(y0, y1), .(z2, z3)), MERGE(.(z0, .(y0, y1)), z3)) 18.11/6.64
MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3)))
18.11/6.64
18.11/6.64

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.64
merge(z0, nil) → z0 18.11/6.64
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.64
++(nil, z0) → z0 18.11/6.64
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.64
if(true, z0, z1) → z0 18.11/6.64
if(false, z0, z1) → z0
Tuples:

++'(.(z0, .(y0, y1)), z2) → c4(++'(.(y0, y1), z2)) 18.11/6.64
MERGE(.(z0, .(y0, y1)), .(z2, z3)) → c2(MERGE(.(y0, y1), .(z2, z3)), MERGE(.(z0, .(y0, y1)), z3)) 18.11/6.64
MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3)))
S tuples:

MERGE(.(z0, .(y0, y1)), .(z2, z3)) → c2(MERGE(.(y0, y1), .(z2, z3)), MERGE(.(z0, .(y0, y1)), z3)) 18.11/6.64
MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3)))
K tuples:

++'(.(z0, .(y0, y1)), z2) → c4(++'(.(y0, y1), z2))
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

++', MERGE

Compound Symbols:

c4, c2

18.11/6.64
18.11/6.64

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

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

++'(.(z0, .(z1, .(y1, y2))), z3) → c4(++'(.(z1, .(y1, y2)), z3))
18.11/6.64
18.11/6.64

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.64
merge(z0, nil) → z0 18.11/6.64
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.64
++(nil, z0) → z0 18.11/6.64
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.64
if(true, z0, z1) → z0 18.11/6.64
if(false, z0, z1) → z0
Tuples:

MERGE(.(z0, .(y0, y1)), .(z2, z3)) → c2(MERGE(.(y0, y1), .(z2, z3)), MERGE(.(z0, .(y0, y1)), z3)) 18.11/6.64
MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3))) 18.11/6.64
++'(.(z0, .(z1, .(y1, y2))), z3) → c4(++'(.(z1, .(y1, y2)), z3))
S tuples:

MERGE(.(z0, .(y0, y1)), .(z2, z3)) → c2(MERGE(.(y0, y1), .(z2, z3)), MERGE(.(z0, .(y0, y1)), z3)) 18.11/6.64
MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3)))
K tuples:

++'(.(z0, .(z1, .(y1, y2))), z3) → c4(++'(.(z1, .(y1, y2)), z3))
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

MERGE, ++'

Compound Symbols:

c2, c4

18.11/6.64
18.11/6.64

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

Use forward instantiation to replace MERGE(.(z0, .(y0, y1)), .(z2, z3)) → c2(MERGE(.(y0, y1), .(z2, z3)), MERGE(.(z0, .(y0, y1)), z3)) by

MERGE(.(z0, .(z1, .(y1, y2))), .(z3, z4)) → c2(MERGE(.(z1, .(y1, y2)), .(z3, z4)), MERGE(.(z0, .(z1, .(y1, y2))), z4)) 18.11/6.64
MERGE(.(z0, .(z1, z2)), .(z3, .(y3, y4))) → c2(MERGE(.(z1, z2), .(z3, .(y3, y4))), MERGE(.(z0, .(z1, z2)), .(y3, y4))) 18.11/6.64
MERGE(.(z0, .(z1, z2)), .(z3, .(y2, .(y3, y4)))) → c2(MERGE(.(z1, z2), .(z3, .(y2, .(y3, y4)))), MERGE(.(z0, .(z1, z2)), .(y2, .(y3, y4))))
18.11/6.64
18.11/6.64

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.64
merge(z0, nil) → z0 18.11/6.64
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.64
++(nil, z0) → z0 18.11/6.64
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.64
if(true, z0, z1) → z0 18.11/6.64
if(false, z0, z1) → z0
Tuples:

MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3))) 18.11/6.64
++'(.(z0, .(z1, .(y1, y2))), z3) → c4(++'(.(z1, .(y1, y2)), z3)) 18.11/6.64
MERGE(.(z0, .(z1, .(y1, y2))), .(z3, z4)) → c2(MERGE(.(z1, .(y1, y2)), .(z3, z4)), MERGE(.(z0, .(z1, .(y1, y2))), z4)) 18.11/6.64
MERGE(.(z0, .(z1, z2)), .(z3, .(y3, y4))) → c2(MERGE(.(z1, z2), .(z3, .(y3, y4))), MERGE(.(z0, .(z1, z2)), .(y3, y4))) 18.11/6.64
MERGE(.(z0, .(z1, z2)), .(z3, .(y2, .(y3, y4)))) → c2(MERGE(.(z1, z2), .(z3, .(y2, .(y3, y4)))), MERGE(.(z0, .(z1, z2)), .(y2, .(y3, y4))))
S tuples:

MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3))) 18.11/6.64
MERGE(.(z0, .(z1, .(y1, y2))), .(z3, z4)) → c2(MERGE(.(z1, .(y1, y2)), .(z3, z4)), MERGE(.(z0, .(z1, .(y1, y2))), z4)) 18.11/6.65
MERGE(.(z0, .(z1, z2)), .(z3, .(y3, y4))) → c2(MERGE(.(z1, z2), .(z3, .(y3, y4))), MERGE(.(z0, .(z1, z2)), .(y3, y4))) 18.11/6.65
MERGE(.(z0, .(z1, z2)), .(z3, .(y2, .(y3, y4)))) → c2(MERGE(.(z1, z2), .(z3, .(y2, .(y3, y4)))), MERGE(.(z0, .(z1, z2)), .(y2, .(y3, y4))))
K tuples:

++'(.(z0, .(z1, .(y1, y2))), z3) → c4(++'(.(z1, .(y1, y2)), z3))
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

MERGE, ++'

Compound Symbols:

c2, c4

18.11/6.65
18.11/6.65

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

Use forward instantiation to replace MERGE(.(z0, z1), .(z2, .(y2, y3))) → c2(MERGE(z1, .(z2, .(y2, y3))), MERGE(.(z0, z1), .(y2, y3))) by

MERGE(.(z0, .(y0, y1)), .(z2, .(z3, z4))) → c2(MERGE(.(y0, y1), .(z2, .(z3, z4))), MERGE(.(z0, .(y0, y1)), .(z3, z4))) 18.11/6.65
MERGE(.(z0, z1), .(z2, .(z3, .(y3, y4)))) → c2(MERGE(z1, .(z2, .(z3, .(y3, y4)))), MERGE(.(z0, z1), .(z3, .(y3, y4)))) 18.11/6.65
MERGE(.(z0, .(y0, .(y1, .(y2, y3)))), .(z2, .(z3, z4))) → c2(MERGE(.(y0, .(y1, .(y2, y3))), .(z2, .(z3, z4))), MERGE(.(z0, .(y0, .(y1, .(y2, y3)))), .(z3, z4))) 18.11/6.65
MERGE(.(z0, .(y1, .(y2, y3))), .(z2, .(z3, z4))) → c2(MERGE(.(y1, .(y2, y3)), .(z2, .(z3, z4))), MERGE(.(z0, .(y1, .(y2, y3))), .(z3, z4))) 18.11/6.65
MERGE(.(z0, .(y1, y2)), .(z2, .(z3, .(y4, y5)))) → c2(MERGE(.(y1, y2), .(z2, .(z3, .(y4, y5)))), MERGE(.(z0, .(y1, y2)), .(z3, .(y4, y5)))) 18.11/6.65
MERGE(.(z0, .(y0, .(y1, y2))), .(z2, .(z3, .(y5, y6)))) → c2(MERGE(.(y0, .(y1, y2)), .(z2, .(z3, .(y5, y6)))), MERGE(.(z0, .(y0, .(y1, y2))), .(z3, .(y5, y6)))) 18.11/6.65
MERGE(.(z0, .(y1, y2)), .(z2, .(z3, .(y4, .(y5, y6))))) → c2(MERGE(.(y1, y2), .(z2, .(z3, .(y4, .(y5, y6))))), MERGE(.(z0, .(y1, y2)), .(z3, .(y4, .(y5, y6)))))
18.11/6.65
18.11/6.65

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

merge(nil, z0) → z0 18.11/6.65
merge(z0, nil) → z0 18.11/6.65
merge(.(z0, z1), .(z2, z3)) → if(<(z0, z2), .(z0, merge(z1, .(z2, z3))), .(z2, merge(.(z0, z1), z3))) 18.11/6.65
++(nil, z0) → z0 18.11/6.65
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 18.11/6.65
if(true, z0, z1) → z0 18.11/6.65
if(false, z0, z1) → z0
Tuples:

++'(.(z0, .(z1, .(y1, y2))), z3) → c4(++'(.(z1, .(y1, y2)), z3)) 18.11/6.65
MERGE(.(z0, .(z1, .(y1, y2))), .(z3, z4)) → c2(MERGE(.(z1, .(y1, y2)), .(z3, z4)), MERGE(.(z0, .(z1, .(y1, y2))), z4)) 18.11/6.65
MERGE(.(z0, .(z1, z2)), .(z3, .(y3, y4))) → c2(MERGE(.(z1, z2), .(z3, .(y3, y4))), MERGE(.(z0, .(z1, z2)), .(y3, y4))) 18.11/6.65
MERGE(.(z0, .(z1, z2)), .(z3, .(y2, .(y3, y4)))) → c2(MERGE(.(z1, z2), .(z3, .(y2, .(y3, y4)))), MERGE(.(z0, .(z1, z2)), .(y2, .(y3, y4)))) 18.11/6.65
MERGE(.(z0, z1), .(z2, .(z3, .(y3, y4)))) → c2(MERGE(z1, .(z2, .(z3, .(y3, y4)))), MERGE(.(z0, z1), .(z3, .(y3, y4)))) 18.11/6.65
MERGE(.(z0, .(y0, .(y1, .(y2, y3)))), .(z2, .(z3, z4))) → c2(MERGE(.(y0, .(y1, .(y2, y3))), .(z2, .(z3, z4))), MERGE(.(z0, .(y0, .(y1, .(y2, y3)))), .(z3, z4))) 18.11/6.65
MERGE(.(z0, .(y1, .(y2, y3))), .(z2, .(z3, z4))) → c2(MERGE(.(y1, .(y2, y3)), .(z2, .(z3, z4))), MERGE(.(z0, .(y1, .(y2, y3))), .(z3, z4))) 18.11/6.65
MERGE(.(z0, .(y0, .(y1, y2))), .(z2, .(z3, .(y5, y6)))) → c2(MERGE(.(y0, .(y1, y2)), .(z2, .(z3, .(y5, y6)))), MERGE(.(z0, .(y0, .(y1, y2))), .(z3, .(y5, y6)))) 18.11/6.65
MERGE(.(z0, .(y1, y2)), .(z2, .(z3, .(y4, .(y5, y6))))) → c2(MERGE(.(y1, y2), .(z2, .(z3, .(y4, .(y5, y6))))), MERGE(.(z0, .(y1, y2)), .(z3, .(y4, .(y5, y6)))))
S tuples:

MERGE(.(z0, .(z1, .(y1, y2))), .(z3, z4)) → c2(MERGE(.(z1, .(y1, y2)), .(z3, z4)), MERGE(.(z0, .(z1, .(y1, y2))), z4)) 18.11/6.65
MERGE(.(z0, .(z1, z2)), .(z3, .(y3, y4))) → c2(MERGE(.(z1, z2), .(z3, .(y3, y4))), MERGE(.(z0, .(z1, z2)), .(y3, y4))) 18.11/6.65
MERGE(.(z0, .(z1, z2)), .(z3, .(y2, .(y3, y4)))) → c2(MERGE(.(z1, z2), .(z3, .(y2, .(y3, y4)))), MERGE(.(z0, .(z1, z2)), .(y2, .(y3, y4)))) 18.11/6.65
MERGE(.(z0, z1), .(z2, .(z3, .(y3, y4)))) → c2(MERGE(z1, .(z2, .(z3, .(y3, y4)))), MERGE(.(z0, z1), .(z3, .(y3, y4)))) 18.11/6.65
MERGE(.(z0, .(y0, .(y1, .(y2, y3)))), .(z2, .(z3, z4))) → c2(MERGE(.(y0, .(y1, .(y2, y3))), .(z2, .(z3, z4))), MERGE(.(z0, .(y0, .(y1, .(y2, y3)))), .(z3, z4))) 18.11/6.65
MERGE(.(z0, .(y1, .(y2, y3))), .(z2, .(z3, z4))) → c2(MERGE(.(y1, .(y2, y3)), .(z2, .(z3, z4))), MERGE(.(z0, .(y1, .(y2, y3))), .(z3, z4))) 18.11/6.65
MERGE(.(z0, .(y0, .(y1, y2))), .(z2, .(z3, .(y5, y6)))) → c2(MERGE(.(y0, .(y1, y2)), .(z2, .(z3, .(y5, y6)))), MERGE(.(z0, .(y0, .(y1, y2))), .(z3, .(y5, y6)))) 18.11/6.65
MERGE(.(z0, .(y1, y2)), .(z2, .(z3, .(y4, .(y5, y6))))) → c2(MERGE(.(y1, y2), .(z2, .(z3, .(y4, .(y5, y6))))), MERGE(.(z0, .(y1, y2)), .(z3, .(y4, .(y5, y6)))))
K tuples:

++'(.(z0, .(z1, .(y1, y2))), z3) → c4(++'(.(z1, .(y1, y2)), z3))
Defined Rule Symbols:

merge, ++, if

Defined Pair Symbols:

++', MERGE

Compound Symbols:

c4, c2

18.11/6.65
18.11/6.65
18.11/6.68 EOF