YES(O(1), O(n^1)) 3.95/1.47 YES(O(1), O(n^1)) 4.36/1.51 4.36/1.51 4.36/1.51 4.36/1.51 4.36/1.51 4.36/1.51 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 4.36/1.51 4.36/1.51 4.36/1.51
4.36/1.51
4.36/1.51
4.36/1.51
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
4.36/1.51 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
4.36/1.51 
↳2 CdtProblem
4.36/1.51 
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
4.36/1.51 
↳4 CdtProblem
4.36/1.51 
↳5 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
4.36/1.51 
↳6 CdtProblem
4.36/1.51 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
4.36/1.51 
↳8 CdtProblem
4.36/1.51 
↳9 CdtKnowledgeProof (⇔)
4.36/1.51 
↳10 BOUNDS(O(1), O(1))
4.36/1.51
4.36/1.51 4.36/1.51
4.36/1.51
4.36/1.51

(0) Obligation:

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

append(@l1, @l2) → append#1(@l1, @l2) 4.36/1.51
append#1(::(@x, @xs), @l2) → ::(@x, append(@xs, @l2)) 4.36/1.51
append#1(nil, @l2) → @l2 4.36/1.51
appendAll(@l) → appendAll#1(@l) 4.36/1.51
appendAll#1(::(@l1, @ls)) → append(@l1, appendAll(@ls)) 4.36/1.51
appendAll#1(nil) → nil 4.36/1.51
appendAll2(@l) → appendAll2#1(@l) 4.36/1.51
appendAll2#1(::(@l1, @ls)) → append(appendAll(@l1), appendAll2(@ls)) 4.36/1.51
appendAll2#1(nil) → nil 4.36/1.51
appendAll3(@l) → appendAll3#1(@l) 4.36/1.51
appendAll3#1(::(@l1, @ls)) → append(appendAll2(@l1), appendAll3(@ls)) 4.36/1.51
appendAll3#1(nil) → nil

Rewrite Strategy: INNERMOST
4.36/1.51
4.36/1.51

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

Converted CpxTRS to CDT
4.36/1.51
4.36/1.51

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1) 4.36/1.51
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 4.36/1.51
append#1(nil, z0) → z0 4.36/1.51
appendAll(z0) → appendAll#1(z0) 4.36/1.51
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1)) 4.36/1.51
appendAll#1(nil) → nil 4.36/1.51
appendAll2(z0) → appendAll2#1(z0) 4.36/1.51
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1)) 4.36/1.51
appendAll2#1(nil) → nil 4.36/1.51
appendAll3(z0) → appendAll3#1(z0) 4.36/1.51
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1)) 4.36/1.51
appendAll3#1(nil) → nil
Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.51
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.51
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.51
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.51
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.51
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.51
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.51
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.51
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.51
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.51
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.51
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.51
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.51
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.51
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
K tuples:none
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

4.36/1.51
4.36/1.51

(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.

APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.51
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.51
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
We considered the (Usable) Rules:

appendAll2(z0) → appendAll2#1(z0) 4.36/1.51
appendAll3(z0) → appendAll3#1(z0) 4.36/1.51
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1)) 4.36/1.51
appendAll3#1(nil) → nil 4.36/1.51
append(z0, z1) → append#1(z0, z1) 4.36/1.51
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 4.36/1.51
append#1(nil, z0) → z0 4.36/1.51
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1)) 4.36/1.51
appendAll2#1(nil) → nil 4.36/1.51
appendAll(z0) → appendAll#1(z0) 4.36/1.51
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1)) 4.36/1.51
appendAll#1(nil) → nil
And the Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.51
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.51
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.51
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.51
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.51
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.51
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.51
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.36/1.51

POL(::(x1, x2)) = [3] + x1 + x2    4.36/1.51
POL(APPEND(x1, x2)) = 0    4.36/1.51
POL(APPEND#1(x1, x2)) = 0    4.36/1.51
POL(APPENDALL(x1)) = [4] + [2]x1    4.36/1.51
POL(APPENDALL#1(x1)) = [4] + [2]x1    4.36/1.51
POL(APPENDALL2(x1)) = [4] + [2]x1    4.36/1.51
POL(APPENDALL2#1(x1)) = [2] + [2]x1    4.36/1.51
POL(APPENDALL3(x1)) = [4] + [2]x1    4.36/1.51
POL(APPENDALL3#1(x1)) = [4] + [2]x1    4.36/1.51
POL(append(x1, x2)) = x2    4.36/1.51
POL(append#1(x1, x2)) = [3] + [3]x2    4.36/1.51
POL(appendAll(x1)) = [1]    4.36/1.51
POL(appendAll#1(x1)) = [1]    4.36/1.51
POL(appendAll2(x1)) = 0    4.36/1.51
POL(appendAll2#1(x1)) = [3] + [3]x1    4.36/1.51
POL(appendAll3(x1)) = 0    4.36/1.51
POL(appendAll3#1(x1)) = [3] + [3]x1    4.36/1.51
POL(c(x1)) = x1    4.36/1.51
POL(c1(x1)) = x1    4.36/1.51
POL(c10(x1, x2, x3)) = x1 + x2 + x3    4.36/1.51
POL(c3(x1)) = x1    4.36/1.51
POL(c4(x1, x2)) = x1 + x2    4.36/1.51
POL(c6(x1)) = x1    4.36/1.51
POL(c7(x1, x2, x3)) = x1 + x2 + x3    4.36/1.51
POL(c9(x1)) = x1    4.36/1.51
POL(nil) = 0   
4.36/1.51
4.36/1.52

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1) 4.36/1.52
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 4.36/1.52
append#1(nil, z0) → z0 4.36/1.52
appendAll(z0) → appendAll#1(z0) 4.36/1.52
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1)) 4.36/1.52
appendAll#1(nil) → nil 4.36/1.52
appendAll2(z0) → appendAll2#1(z0) 4.36/1.52
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1)) 4.36/1.52
appendAll2#1(nil) → nil 4.36/1.52
appendAll3(z0) → appendAll3#1(z0) 4.36/1.52
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1)) 4.36/1.52
appendAll3#1(nil) → nil
Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.52
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.52
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0))
K tuples:

APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

4.36/1.52
4.36/1.52

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

The following tuples could be moved from S to K by knowledge propagation:

APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) 4.36/1.52
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1))
4.36/1.52
4.36/1.52

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1) 4.36/1.52
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 4.36/1.52
append#1(nil, z0) → z0 4.36/1.52
appendAll(z0) → appendAll#1(z0) 4.36/1.52
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1)) 4.36/1.52
appendAll#1(nil) → nil 4.36/1.52
appendAll2(z0) → appendAll2#1(z0) 4.36/1.52
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1)) 4.36/1.52
appendAll2#1(nil) → nil 4.36/1.52
appendAll3(z0) → appendAll3#1(z0) 4.36/1.52
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1)) 4.36/1.52
appendAll3#1(nil) → nil
Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.52
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
K tuples:

APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) 4.36/1.52
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0))
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

4.36/1.52
4.36/1.52

(7) 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.

APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
We considered the (Usable) Rules:

appendAll2(z0) → appendAll2#1(z0) 4.36/1.52
appendAll3(z0) → appendAll3#1(z0) 4.36/1.52
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1)) 4.36/1.52
appendAll3#1(nil) → nil 4.36/1.52
append(z0, z1) → append#1(z0, z1) 4.36/1.52
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 4.36/1.52
append#1(nil, z0) → z0 4.36/1.52
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1)) 4.36/1.52
appendAll2#1(nil) → nil 4.36/1.52
appendAll(z0) → appendAll#1(z0) 4.36/1.52
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1)) 4.36/1.52
appendAll#1(nil) → nil
And the Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.52
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 4.36/1.52

POL(::(x1, x2)) = [1] + x1 + x2    4.36/1.52
POL(APPEND(x1, x2)) = x1    4.36/1.52
POL(APPEND#1(x1, x2)) = x1    4.36/1.52
POL(APPENDALL(x1)) = [2]x1    4.36/1.52
POL(APPENDALL#1(x1)) = [2]x1    4.36/1.52
POL(APPENDALL2(x1)) = [2] + [3]x1    4.36/1.52
POL(APPENDALL2#1(x1)) = [2] + [3]x1    4.36/1.52
POL(APPENDALL3(x1)) = [4]x1    4.36/1.52
POL(APPENDALL3#1(x1)) = [4]x1    4.36/1.52
POL(append(x1, x2)) = x1 + x2    4.36/1.52
POL(append#1(x1, x2)) = x1 + x2    4.36/1.52
POL(appendAll(x1)) = x1    4.36/1.52
POL(appendAll#1(x1)) = x1    4.36/1.52
POL(appendAll2(x1)) = x1    4.36/1.52
POL(appendAll2#1(x1)) = x1    4.36/1.52
POL(appendAll3(x1)) = [2]x1    4.36/1.52
POL(appendAll3#1(x1)) = [2]x1    4.36/1.52
POL(c(x1)) = x1    4.36/1.52
POL(c1(x1)) = x1    4.36/1.52
POL(c10(x1, x2, x3)) = x1 + x2 + x3    4.36/1.52
POL(c3(x1)) = x1    4.36/1.52
POL(c4(x1, x2)) = x1 + x2    4.36/1.52
POL(c6(x1)) = x1    4.36/1.52
POL(c7(x1, x2, x3)) = x1 + x2 + x3    4.36/1.52
POL(c9(x1)) = x1    4.36/1.52
POL(nil) = 0   
4.36/1.52
4.36/1.52

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

append(z0, z1) → append#1(z0, z1) 4.36/1.52
append#1(::(z0, z1), z2) → ::(z0, append(z1, z2)) 4.36/1.52
append#1(nil, z0) → z0 4.36/1.52
appendAll(z0) → appendAll#1(z0) 4.36/1.52
appendAll#1(::(z0, z1)) → append(z0, appendAll(z1)) 4.36/1.52
appendAll#1(nil) → nil 4.36/1.52
appendAll2(z0) → appendAll2#1(z0) 4.36/1.52
appendAll2#1(::(z0, z1)) → append(appendAll(z0), appendAll2(z1)) 4.36/1.52
appendAll2#1(nil) → nil 4.36/1.52
appendAll3(z0) → appendAll3#1(z0) 4.36/1.52
appendAll3#1(::(z0, z1)) → append(appendAll2(z0), appendAll3(z1)) 4.36/1.52
appendAll3#1(nil) → nil
Tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.52
APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1))
S tuples:

APPEND(z0, z1) → c(APPEND#1(z0, z1))
K tuples:

APPENDALL#1(::(z0, z1)) → c4(APPEND(z0, appendAll(z1)), APPENDALL(z1)) 4.36/1.52
APPENDALL2(z0) → c6(APPENDALL2#1(z0)) 4.36/1.52
APPENDALL3#1(::(z0, z1)) → c10(APPEND(appendAll2(z0), appendAll3(z1)), APPENDALL2(z0), APPENDALL3(z1)) 4.36/1.52
APPENDALL2#1(::(z0, z1)) → c7(APPEND(appendAll(z0), appendAll2(z1)), APPENDALL(z0), APPENDALL2(z1)) 4.36/1.52
APPENDALL3(z0) → c9(APPENDALL3#1(z0)) 4.36/1.52
APPENDALL(z0) → c3(APPENDALL#1(z0)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
Defined Rule Symbols:

append, append#1, appendAll, appendAll#1, appendAll2, appendAll2#1, appendAll3, appendAll3#1

Defined Pair Symbols:

APPEND, APPEND#1, APPENDALL, APPENDALL#1, APPENDALL2, APPENDALL2#1, APPENDALL3, APPENDALL3#1

Compound Symbols:

c, c1, c3, c4, c6, c7, c9, c10

4.36/1.52
4.36/1.52

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

APPEND(z0, z1) → c(APPEND#1(z0, z1)) 4.36/1.52
APPEND#1(::(z0, z1), z2) → c1(APPEND(z1, z2))
Now S is empty
4.36/1.52
4.36/1.52

(10) BOUNDS(O(1), O(1))

4.36/1.52
4.36/1.52
4.36/1.59 EOF