16.56/4.70 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

16.56/4.70

16.56/4.70
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxRelTRS

16.56/4.70

↳1 CpxRelTrsToCDT (UPPER BOUND (ID))

16.56/4.70

↳2 CdtProblem

16.56/4.70

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

16.56/4.70

↳4 CdtProblem

16.56/4.70

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

16.56/4.70

↳6 CdtProblem

16.56/4.70

↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

16.56/4.70

↳8 CdtProblem

16.56/4.70

↳9 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

16.56/4.70

↳10 CdtProblem

16.56/4.70

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

16.56/4.70

↳12 CdtProblem

16.56/4.70

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

16.56/4.70

↳14 CdtProblem

16.56/4.70

↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

16.56/4.70

↳16 CdtProblem

16.56/4.70

↳17 CdtKnowledgeProof (⇔)

16.56/4.70

↳18 BOUNDS(O(1), O(1))

16.56/4.70

16.56/4.70 16.56/4.70

16.56/4.70

(0) Obligation:

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

*(@x, @y) → #mult(@x, @y) 16.56/4.70
+(@x, @y) → #add(@x, @y) 16.56/4.70
computeLine(@line, @m, @acc) → computeLine#1(@line, @acc, @m) 16.56/4.70
computeLine#1(::(@x, @xs), @acc, @m) → computeLine#2(@m, @acc, @x, @xs) 16.56/4.70
computeLine#1(nil, @acc, @m) → @acc 16.56/4.70
computeLine#2(::(@l, @ls), @acc, @x, @xs) → computeLine(@xs, @ls, lineMult(@x, @l, @acc)) 16.56/4.70
computeLine#2(nil, @acc, @x, @xs) → nil 16.56/4.70
lineMult(@n, @l1, @l2) → lineMult#1(@l1, @l2, @n) 16.56/4.70
lineMult#1(::(@x, @xs), @l2, @n) → lineMult#2(@l2, @n, @x, @xs) 16.56/4.70
lineMult#1(nil, @l2, @n) → nil 16.56/4.70
lineMult#2(::(@y, @ys), @n, @x, @xs) → ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) 16.56/4.70
lineMult#2(nil, @n, @x, @xs) → ::(*(@x, @n), lineMult(@n, @xs, nil)) 16.56/4.70
matrixMult(@m1, @m2) → matrixMult#1(@m1, @m2) 16.56/4.70
matrixMult#1(::(@l, @ls), @m2) → ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) 16.56/4.70
matrixMult#1(nil, @m2) → nil

The (relative) TRS S consists of the following rules:

#add(#0, @y) → @y 16.56/4.70
#add(#neg(#s(#0)), @y) → #pred(@y) 16.56/4.70
#add(#neg(#s(#s(@x))), @y) → #pred(#add(#pos(#s(@x)), @y)) 16.56/4.70
#add(#pos(#s(#0)), @y) → #succ(@y) 16.56/4.70
#add(#pos(#s(#s(@x))), @y) → #succ(#add(#pos(#s(@x)), @y)) 16.56/4.70
#mult(#0, #0) → #0 16.56/4.70
#mult(#0, #neg(@y)) → #0 16.56/4.70
#mult(#0, #pos(@y)) → #0 16.56/4.70
#mult(#neg(@x), #0) → #0 16.56/4.70
#mult(#neg(@x), #neg(@y)) → #pos(#natmult(@x, @y)) 16.56/4.70
#mult(#neg(@x), #pos(@y)) → #neg(#natmult(@x, @y)) 16.56/4.70
#mult(#pos(@x), #0) → #0 16.56/4.70
#mult(#pos(@x), #neg(@y)) → #neg(#natmult(@x, @y)) 16.56/4.70
#mult(#pos(@x), #pos(@y)) → #pos(#natmult(@x, @y)) 16.56/4.70
#natmult(#0, @y) → #0 16.56/4.70
#natmult(#s(@x), @y) → #add(#pos(@y), #natmult(@x, @y)) 16.56/4.70
#pred(#0) → #neg(#s(#0)) 16.56/4.70
#pred(#neg(#s(@x))) → #neg(#s(#s(@x))) 16.56/4.70
#pred(#pos(#s(#0))) → #0 16.56/4.70
#pred(#pos(#s(#s(@x)))) → #pos(#s(@x)) 16.56/4.70
#succ(#0) → #pos(#s(#0)) 16.56/4.70
#succ(#neg(#s(#0))) → #0 16.56/4.70
#succ(#neg(#s(#s(@x)))) → #neg(#s(@x)) 16.56/4.70
#succ(#pos(#s(@x))) → #pos(#s(#s(@x)))

Rewrite Strategy: INNERMOST

16.56/4.70

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.

16.56/4.70

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 16.56/4.70
#add(#neg(#s(#0)), z0) → #pred(z0) 16.56/4.70
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 16.56/4.70
#add(#pos(#s(#0)), z0) → #succ(z0) 16.56/4.70
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 16.56/4.70
#mult(#0, #0) → #0 16.56/4.70
#mult(#0, #neg(z0)) → #0 16.56/4.70
#mult(#0, #pos(z0)) → #0 16.56/4.70
#mult(#neg(z0), #0) → #0 16.56/4.70
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 16.56/4.70
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 16.56/4.70
#mult(#pos(z0), #0) → #0 16.56/4.70
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 16.56/4.70
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 16.56/4.70
#natmult(#0, z0) → #0 16.56/4.70
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 16.56/4.70
#pred(#0) → #neg(#s(#0)) 16.56/4.70
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 16.56/4.70
#pred(#pos(#s(#0))) → #0 16.56/4.70
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 16.56/4.70
#succ(#0) → #pos(#s(#0)) 16.56/4.70
#succ(#neg(#s(#0))) → #0 16.56/4.70
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 16.56/4.70
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 16.56/4.70
*(z0, z1) → #mult(z0, z1) 16.56/4.70
+(z0, z1) → #add(z0, z1) 16.56/4.70
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 16.56/4.70
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 16.56/4.70
computeLine#1(nil, z0, z1) → z0 16.56/4.70
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 16.56/4.70
computeLine#2(nil, z0, z1, z2) → nil 16.56/4.70
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 16.56/4.70
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 16.56/4.70
lineMult#1(nil, z0, z1) → nil 16.56/4.70
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 16.56/4.70
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 16.56/4.70
matrixMult(z0, z1) → matrixMult#1(z0, z1) 16.56/4.70
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 16.56/4.70
matrixMult#1(nil, z0) → nil

Tuples:

#ADD(#neg(#s(#0)), z0) → c1(#PRED(z0)) 16.56/4.70
#ADD(#neg(#s(#s(z0))), z1) → c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) 16.56/4.70
#ADD(#pos(#s(#0)), z0) → c3(#SUCC(z0)) 16.56/4.70
#ADD(#pos(#s(#s(z0))), z1) → c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) 16.56/4.70
#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 16.56/4.70
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 16.56/4.70
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 16.56/4.70
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 16.56/4.70
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 16.56/4.70
*'(z0, z1) → c24(#MULT(z0, z1)) 16.56/4.70
+'(z0, z1) → c25(#ADD(z0, z1)) 16.56/4.70
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 16.56/4.70
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 16.56/4.70
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 16.56/4.70
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 16.56/4.70
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 16.56/4.70
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 16.56/4.70
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 16.56/4.70
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 16.56/4.70
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 16.56/4.70
+'(z0, z1) → c25(#ADD(z0, z1)) 16.56/4.70
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 16.56/4.70
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 16.56/4.70
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 16.56/4.70
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 16.56/4.70
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 16.56/4.70
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 16.56/4.70
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 16.56/4.70
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 16.56/4.70
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

K tuples:none
Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#ADD, #MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1

Compound Symbols:

c1, c2, c3, c4, c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37

16.56/4.70

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

Removed 4 trailing tuple parts

16.56/4.70

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 16.56/4.70
#add(#neg(#s(#0)), z0) → #pred(z0) 16.56/4.70
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 16.56/4.70
#add(#pos(#s(#0)), z0) → #succ(z0) 16.56/4.70
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 16.56/4.70
#mult(#0, #0) → #0 16.56/4.70
#mult(#0, #neg(z0)) → #0 16.56/4.70
#mult(#0, #pos(z0)) → #0 16.56/4.70
#mult(#neg(z0), #0) → #0 16.56/4.70
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 16.56/4.70
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 16.56/4.70
#mult(#pos(z0), #0) → #0 16.56/4.70
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 16.56/4.70
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 16.56/4.70
#natmult(#0, z0) → #0 16.56/4.70
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 16.56/4.70
#pred(#0) → #neg(#s(#0)) 16.56/4.70
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 16.56/4.70
#pred(#pos(#s(#0))) → #0 16.56/4.70
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 16.56/4.70
#succ(#0) → #pos(#s(#0)) 16.56/4.70
#succ(#neg(#s(#0))) → #0 16.56/4.70
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 16.56/4.70
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 16.56/4.70
*(z0, z1) → #mult(z0, z1) 16.56/4.70
+(z0, z1) → #add(z0, z1) 16.56/4.70
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 16.56/4.70
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 16.56/4.70
computeLine#1(nil, z0, z1) → z0 16.56/4.70
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 16.56/4.70
computeLine#2(nil, z0, z1, z2) → nil 16.56/4.70
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 16.56/4.70
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 16.56/4.70
lineMult#1(nil, z0, z1) → nil 16.56/4.70
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 16.56/4.70
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 16.56/4.70
matrixMult(z0, z1) → matrixMult#1(z0, z1) 16.56/4.70
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 16.56/4.70
matrixMult#1(nil, z0) → nil

Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 16.56/4.70
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 16.56/4.70
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 16.56/4.70
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 16.56/4.70
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 16.56/4.70
*'(z0, z1) → c24(#MULT(z0, z1)) 16.56/4.70
+'(z0, z1) → c25(#ADD(z0, z1)) 16.56/4.70
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 16.56/4.70
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 16.56/4.70
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 16.56/4.70
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 16.56/4.70
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 16.56/4.70
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 16.56/4.70
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 16.56/4.70
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 16.56/4.70
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.35/4.89
#ADD(#neg(#s(#0)), z0) → c1 17.35/4.89
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.35/4.89
#ADD(#pos(#s(#0)), z0) → c3 17.35/4.89
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 17.35/4.89
+'(z0, z1) → c25(#ADD(z0, z1)) 17.35/4.89
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.35/4.89
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.35/4.89
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.35/4.89
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.35/4.89
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.35/4.89
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.35/4.89
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.35/4.89
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.35/4.89
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

K tuples:none
Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37, c1, c2, c3, c4

17.35/4.89

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

Removed 2 trailing nodes:

#ADD(#pos(#s(#0)), z0) → c3 17.35/4.89
#ADD(#neg(#s(#0)), z0) → c1

17.35/4.89

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 17.35/4.89
#add(#neg(#s(#0)), z0) → #pred(z0) 17.35/4.89
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.35/4.89
#add(#pos(#s(#0)), z0) → #succ(z0) 17.35/4.89
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.35/4.89
#mult(#0, #0) → #0 17.35/4.89
#mult(#0, #neg(z0)) → #0 17.35/4.89
#mult(#0, #pos(z0)) → #0 17.35/4.89
#mult(#neg(z0), #0) → #0 17.35/4.89
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.35/4.89
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.35/4.89
#mult(#pos(z0), #0) → #0 17.35/4.89
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.35/4.89
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.35/4.89
#natmult(#0, z0) → #0 17.35/4.89
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.35/4.89
#pred(#0) → #neg(#s(#0)) 17.35/4.89
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.35/4.89
#pred(#pos(#s(#0))) → #0 17.35/4.89
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 17.35/4.89
#succ(#0) → #pos(#s(#0)) 17.35/4.89
#succ(#neg(#s(#0))) → #0 17.35/4.89
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.35/4.89
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.35/4.89
*(z0, z1) → #mult(z0, z1) 17.35/4.89
+(z0, z1) → #add(z0, z1) 17.35/4.89
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 17.35/4.89
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 17.35/4.89
computeLine#1(nil, z0, z1) → z0 17.35/4.89
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 17.35/4.89
computeLine#2(nil, z0, z1, z2) → nil 17.35/4.89
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.35/4.89
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.35/4.89
lineMult#1(nil, z0, z1) → nil 17.35/4.89
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.35/4.89
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.35/4.89
matrixMult(z0, z1) → matrixMult#1(z0, z1) 17.35/4.89
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 17.35/4.89
matrixMult#1(nil, z0) → nil

Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.35/4.89
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.35/4.89
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.35/4.89
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.35/4.89
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.35/4.89
*'(z0, z1) → c24(#MULT(z0, z1)) 17.35/4.89
+'(z0, z1) → c25(#ADD(z0, z1)) 17.35/4.89
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.35/4.89
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.35/4.89
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.35/4.89
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.35/4.89
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.35/4.89
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.91
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.91
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.91
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.91
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.91
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.91
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.91
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.91
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.91
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.91
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.91
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.91
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.91
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.91
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.91
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.91
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.91
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

K tuples:none
Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37, c1, c2, c3, c4

17.71/4.91

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

MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

We considered the (Usable) Rules:

*(z0, z1) → #mult(z0, z1) 17.71/4.91
#mult(#0, #0) → #0 17.71/4.91
#mult(#0, #neg(z0)) → #0 17.71/4.91
#mult(#0, #pos(z0)) → #0 17.71/4.91
#mult(#neg(z0), #0) → #0 17.71/4.91
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.91
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.91
#mult(#pos(z0), #0) → #0 17.71/4.91
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.91
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.91
#natmult(#0, z0) → #0 17.71/4.91
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.91
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.91
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.91
#add(#0, z0) → z0 17.71/4.91
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.91
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.91
#succ(#0) → #pos(#s(#0)) 17.71/4.91
#succ(#neg(#s(#0))) → #0 17.71/4.91
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.91
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.91
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.91
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.91
lineMult#1(nil, z0, z1) → nil 17.71/4.91
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.93
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.93
+(z0, z1) → #add(z0, z1) 17.71/4.93
#pred(#0) → #neg(#s(#0)) 17.71/4.93
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.93
#pred(#pos(#s(#0))) → #0 17.71/4.93
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

And the Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.93
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.93
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.93
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.93
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.93
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.93
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.93
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.93
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.93
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.93
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.93
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.93
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.93
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.93
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.93
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.93
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 17.71/4.93

POL(#0) = 0 17.71/4.93
POL(#ADD(x₁, x₂)) = 0 17.71/4.93
POL(#MULT(x₁, x₂)) = 0 17.71/4.93
POL(#NATMULT(x₁, x₂)) = 0 17.71/4.93
POL(#add(x₁, x₂)) = [1] + x₁ + x₂ 17.71/4.93
POL(#mult(x₁, x₂)) = 0 17.71/4.93
POL(#natmult(x₁, x₂)) = 0 17.71/4.93
POL(#neg(x₁)) = 0 17.71/4.93
POL(#pos(x₁)) = 0 17.71/4.93
POL(#pred(x₁)) = [3] 17.71/4.93
POL(#s(x₁)) = 0 17.71/4.93
POL(#succ(x₁)) = [3] 17.71/4.93
POL(*(x₁, x₂)) = [4] + [2]x₁ 17.71/4.93
POL(*'(x₁, x₂)) = 0 17.71/4.93
POL(+(x₁, x₂)) = [3] + [3]x₂ 17.71/4.93
POL(+'(x₁, x₂)) = 0 17.71/4.93
POL(::(x₁, x₂)) = [4] + x₂ 17.71/4.93
POL(COMPUTELINE(x₁, x₂, x₃)) = [3] 17.71/4.93
POL(COMPUTELINE#1(x₁, x₂, x₃)) = [3] 17.71/4.93
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = [3] 17.71/4.93
POL(LINEMULT(x₁, x₂, x₃)) = 0 17.71/4.93
POL(LINEMULT#1(x₁, x₂, x₃)) = 0 17.71/4.93
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = 0 17.71/4.93
POL(MATRIXMULT(x₁, x₂)) = [2]x₁ + x₂ 17.71/4.93
POL(MATRIXMULT#1(x₁, x₂)) = [2]x₁ + x₂ 17.71/4.93
POL(c1) = 0 17.71/4.93
POL(c10(x₁)) = x₁ 17.71/4.93
POL(c12(x₁)) = x₁ 17.71/4.93
POL(c13(x₁)) = x₁ 17.71/4.93
POL(c15(x₁, x₂)) = x₁ + x₂ 17.71/4.93
POL(c2(x₁)) = x₁ 17.71/4.93
POL(c24(x₁)) = x₁ 17.71/4.93
POL(c25(x₁)) = x₁ 17.71/4.93
POL(c26(x₁)) = x₁ 17.71/4.93
POL(c27(x₁)) = x₁ 17.71/4.93
POL(c29(x₁, x₂)) = x₁ + x₂ 17.71/4.93
POL(c3) = 0 17.71/4.93
POL(c31(x₁)) = x₁ 17.71/4.93
POL(c32(x₁)) = x₁ 17.71/4.93
POL(c34(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 17.71/4.93
POL(c35(x₁, x₂)) = x₁ + x₂ 17.71/4.93
POL(c36(x₁)) = x₁ 17.71/4.93
POL(c37(x₁, x₂)) = x₁ + x₂ 17.71/4.93
POL(c4(x₁)) = x₁ 17.71/4.93
POL(c9(x₁)) = x₁ 17.71/4.93
POL(lineMult(x₁, x₂, x₃)) = 0 17.71/4.93
POL(lineMult#1(x₁, x₂, x₃)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 17.71/4.93
POL(lineMult#2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ + [3]x₄ 17.71/4.93
POL(nil) = 0

17.71/4.93

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 17.71/4.93
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.93
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.93
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.93
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.93
#mult(#0, #0) → #0 17.71/4.93
#mult(#0, #neg(z0)) → #0 17.71/4.93
#mult(#0, #pos(z0)) → #0 17.71/4.93
#mult(#neg(z0), #0) → #0 17.71/4.93
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.93
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.93
#mult(#pos(z0), #0) → #0 17.71/4.93
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.93
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.93
#natmult(#0, z0) → #0 17.71/4.93
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.93
#pred(#0) → #neg(#s(#0)) 17.71/4.93
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.93
#pred(#pos(#s(#0))) → #0 17.71/4.93
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 17.71/4.93
#succ(#0) → #pos(#s(#0)) 17.71/4.93
#succ(#neg(#s(#0))) → #0 17.71/4.93
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.93
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.93
*(z0, z1) → #mult(z0, z1) 17.71/4.93
+(z0, z1) → #add(z0, z1) 17.71/4.93
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 17.71/4.93
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 17.71/4.93
computeLine#1(nil, z0, z1) → z0 17.71/4.93
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 17.71/4.93
computeLine#2(nil, z0, z1, z2) → nil 17.71/4.93
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.93
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.93
lineMult#1(nil, z0, z1) → nil 17.71/4.93
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.93
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.93
matrixMult(z0, z1) → matrixMult#1(z0, z1) 17.71/4.93
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 17.71/4.93
matrixMult#1(nil, z0) → nil

Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.93
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.93
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.93
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.93
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.93
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.93
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.93
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.93
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.93
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.93
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.93
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.93
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.93
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.93
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.93
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.93
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.93
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.93
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.93
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.93
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.93
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.93
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.93
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.93
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.93
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1))

K tuples:

MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37, c1, c2, c3, c4

17.71/4.93

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

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

MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.93
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2))

17.71/4.93

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 17.71/4.93
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.93
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.93
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.93
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.93
#mult(#0, #0) → #0 17.71/4.93
#mult(#0, #neg(z0)) → #0 17.71/4.93
#mult(#0, #pos(z0)) → #0 17.71/4.93
#mult(#neg(z0), #0) → #0 17.71/4.93
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.93
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.93
#mult(#pos(z0), #0) → #0 17.71/4.93
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.93
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.93
#natmult(#0, z0) → #0 17.71/4.93
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.93
#pred(#0) → #neg(#s(#0)) 17.71/4.93
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.93
#pred(#pos(#s(#0))) → #0 17.71/4.93
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 17.71/4.93
#succ(#0) → #pos(#s(#0)) 17.71/4.93
#succ(#neg(#s(#0))) → #0 17.71/4.93
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.93
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.93
*(z0, z1) → #mult(z0, z1) 17.71/4.93
+(z0, z1) → #add(z0, z1) 17.71/4.93
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 17.71/4.93
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 17.71/4.93
computeLine#1(nil, z0, z1) → z0 17.71/4.93
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 17.71/4.93
computeLine#2(nil, z0, z1, z2) → nil 17.71/4.93
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.93
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.93
lineMult#1(nil, z0, z1) → nil 17.71/4.93
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.93
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.93
matrixMult(z0, z1) → matrixMult#1(z0, z1) 17.71/4.93
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 17.71/4.93
matrixMult#1(nil, z0) → nil

Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.93
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.93
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.93
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.93
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.93
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.93
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.93
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.93
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.93
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.93
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.93
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.93
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.93
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.93
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.93
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.93
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.93
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.93
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.93
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.93
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.93
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.93
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.93
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.94
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.94
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil))

K tuples:

MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.94
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1))

Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37, c1, c2, c3, c4

17.71/4.94

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

COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1))

We considered the (Usable) Rules:

*(z0, z1) → #mult(z0, z1) 17.71/4.94
#mult(#0, #0) → #0 17.71/4.94
#mult(#0, #neg(z0)) → #0 17.71/4.94
#mult(#0, #pos(z0)) → #0 17.71/4.94
#mult(#neg(z0), #0) → #0 17.71/4.94
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.94
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.94
#mult(#pos(z0), #0) → #0 17.71/4.94
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.94
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.94
#natmult(#0, z0) → #0 17.71/4.94
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.94
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.94
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.94
#add(#0, z0) → z0 17.71/4.94
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.94
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.94
#succ(#0) → #pos(#s(#0)) 17.71/4.94
#succ(#neg(#s(#0))) → #0 17.71/4.94
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.94
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.94
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.94
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.94
lineMult#1(nil, z0, z1) → nil 17.71/4.94
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.94
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.94
+(z0, z1) → #add(z0, z1) 17.71/4.94
#pred(#0) → #neg(#s(#0)) 17.71/4.94
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.94
#pred(#pos(#s(#0))) → #0 17.71/4.94
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

And the Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.94
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.94
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.94
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.94
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.94
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.94
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.94
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.94
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.94
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.94
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.94
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.94
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.94
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.94
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.94
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.94
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.94
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.94
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.94
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 17.71/4.94

POL(#0) = 0 17.71/4.94
POL(#ADD(x₁, x₂)) = 0 17.71/4.94
POL(#MULT(x₁, x₂)) = 0 17.71/4.94
POL(#NATMULT(x₁, x₂)) = 0 17.71/4.94
POL(#add(x₁, x₂)) = 0 17.71/4.94
POL(#mult(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ 17.71/4.94
POL(#natmult(x₁, x₂)) = [1] 17.71/4.94
POL(#neg(x₁)) = 0 17.71/4.94
POL(#pos(x₁)) = 0 17.71/4.94
POL(#pred(x₁)) = [3] 17.71/4.94
POL(#s(x₁)) = 0 17.71/4.94
POL(#succ(x₁)) = [3] 17.71/4.94
POL(*(x₁, x₂)) = 0 17.71/4.94
POL(*'(x₁, x₂)) = 0 17.71/4.94
POL(+(x₁, x₂)) = [5] + [3]x₂ 17.71/4.94
POL(+'(x₁, x₂)) = 0 17.71/4.94
POL(::(x₁, x₂)) = [1] + x₁ + x₂ 17.71/4.94
POL(COMPUTELINE(x₁, x₂, x₃)) = [1] + x₁ 17.71/4.94
POL(COMPUTELINE#1(x₁, x₂, x₃)) = x₁ 17.71/4.94
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = [1] + x₄ 17.71/4.94
POL(LINEMULT(x₁, x₂, x₃)) = 0 17.71/4.94
POL(LINEMULT#1(x₁, x₂, x₃)) = 0 17.71/4.94
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = 0 17.71/4.94
POL(MATRIXMULT(x₁, x₂)) = [2] + [2]x₁ 17.71/4.94
POL(MATRIXMULT#1(x₁, x₂)) = [1] + [2]x₁ 17.71/4.94
POL(c1) = 0 17.71/4.94
POL(c10(x₁)) = x₁ 17.71/4.94
POL(c12(x₁)) = x₁ 17.71/4.94
POL(c13(x₁)) = x₁ 17.71/4.94
POL(c15(x₁, x₂)) = x₁ + x₂ 17.71/4.94
POL(c2(x₁)) = x₁ 17.71/4.94
POL(c24(x₁)) = x₁ 17.71/4.94
POL(c25(x₁)) = x₁ 17.71/4.94
POL(c26(x₁)) = x₁ 17.71/4.94
POL(c27(x₁)) = x₁ 17.71/4.94
POL(c29(x₁, x₂)) = x₁ + x₂ 17.71/4.94
POL(c3) = 0 17.71/4.94
POL(c31(x₁)) = x₁ 17.71/4.94
POL(c32(x₁)) = x₁ 17.71/4.94
POL(c34(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 17.71/4.94
POL(c35(x₁, x₂)) = x₁ + x₂ 17.71/4.94
POL(c36(x₁)) = x₁ 17.71/4.94
POL(c37(x₁, x₂)) = x₁ + x₂ 17.71/4.94
POL(c4(x₁)) = x₁ 17.71/4.94
POL(c9(x₁)) = x₁ 17.71/4.94
POL(lineMult(x₁, x₂, x₃)) = 0 17.71/4.94
POL(lineMult#1(x₁, x₂, x₃)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ 17.71/4.94
POL(lineMult#2(x₁, x₂, x₃, x₄)) = [3] + [3]x₁ + [3]x₂ + [3]x₃ + [3]x₄ 17.71/4.94
POL(nil) = 0

17.71/4.94

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 17.71/4.94
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.94
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.94
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.94
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.94
#mult(#0, #0) → #0 17.71/4.94
#mult(#0, #neg(z0)) → #0 17.71/4.94
#mult(#0, #pos(z0)) → #0 17.71/4.94
#mult(#neg(z0), #0) → #0 17.71/4.94
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.94
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.94
#mult(#pos(z0), #0) → #0 17.71/4.94
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.94
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.94
#natmult(#0, z0) → #0 17.71/4.94
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.94
#pred(#0) → #neg(#s(#0)) 17.71/4.94
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.94
#pred(#pos(#s(#0))) → #0 17.71/4.94
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 17.71/4.94
#succ(#0) → #pos(#s(#0)) 17.71/4.94
#succ(#neg(#s(#0))) → #0 17.71/4.94
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.94
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.94
*(z0, z1) → #mult(z0, z1) 17.71/4.94
+(z0, z1) → #add(z0, z1) 17.71/4.94
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 17.71/4.94
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 17.71/4.94
computeLine#1(nil, z0, z1) → z0 17.71/4.94
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 17.71/4.94
computeLine#2(nil, z0, z1, z2) → nil 17.71/4.94
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.94
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.94
lineMult#1(nil, z0, z1) → nil 17.71/4.94
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.94
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.94
matrixMult(z0, z1) → matrixMult#1(z0, z1) 17.71/4.94
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 17.71/4.94
matrixMult#1(nil, z0) → nil

Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.94
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.94
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.94
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.94
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.94
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.94
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.94
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.94
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.94
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.94
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.94
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.94
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.94
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.94
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.94
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.95
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.95
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.95
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.95
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.95
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.95
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.95
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil))

K tuples:

MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.95
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.95
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1))

Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37, c1, c2, c3, c4

17.71/4.95

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

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

COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.95
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1))

17.71/4.95

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 17.71/4.95
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.95
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.95
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.95
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.95
#mult(#0, #0) → #0 17.71/4.95
#mult(#0, #neg(z0)) → #0 17.71/4.95
#mult(#0, #pos(z0)) → #0 17.71/4.95
#mult(#neg(z0), #0) → #0 17.71/4.95
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.95
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.95
#mult(#pos(z0), #0) → #0 17.71/4.95
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.95
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.95
#natmult(#0, z0) → #0 17.71/4.95
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.95
#pred(#0) → #neg(#s(#0)) 17.71/4.95
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.95
#pred(#pos(#s(#0))) → #0 17.71/4.95
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 17.71/4.95
#succ(#0) → #pos(#s(#0)) 17.71/4.95
#succ(#neg(#s(#0))) → #0 17.71/4.95
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.95
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.95
*(z0, z1) → #mult(z0, z1) 17.71/4.95
+(z0, z1) → #add(z0, z1) 17.71/4.95
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 17.71/4.95
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 17.71/4.95
computeLine#1(nil, z0, z1) → z0 17.71/4.95
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 17.71/4.95
computeLine#2(nil, z0, z1, z2) → nil 17.71/4.95
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.95
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.95
lineMult#1(nil, z0, z1) → nil 17.71/4.95
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.95
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.95
matrixMult(z0, z1) → matrixMult#1(z0, z1) 17.71/4.95
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 17.71/4.95
matrixMult#1(nil, z0) → nil

Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.95
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.95
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.95
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.95
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.95
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.95
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.95
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.95
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.95
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.95
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.95
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.95
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.95
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.95
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil))

K tuples:

MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.95
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.95
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.95
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2))

Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37, c1, c2, c3, c4

17.71/4.95

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1))

We considered the (Usable) Rules:

*(z0, z1) → #mult(z0, z1) 17.71/4.95
#mult(#0, #0) → #0 17.71/4.95
#mult(#0, #neg(z0)) → #0 17.71/4.95
#mult(#0, #pos(z0)) → #0 17.71/4.95
#mult(#neg(z0), #0) → #0 17.71/4.95
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.95
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.95
#mult(#pos(z0), #0) → #0 17.71/4.95
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.95
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.95
#natmult(#0, z0) → #0 17.71/4.95
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.95
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.95
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.95
#add(#0, z0) → z0 17.71/4.95
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.95
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.95
#succ(#0) → #pos(#s(#0)) 17.71/4.95
#succ(#neg(#s(#0))) → #0 17.71/4.95
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.95
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.95
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.95
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.95
lineMult#1(nil, z0, z1) → nil 17.71/4.95
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.95
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.95
+(z0, z1) → #add(z0, z1) 17.71/4.95
#pred(#0) → #neg(#s(#0)) 17.71/4.95
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.95
#pred(#pos(#s(#0))) → #0 17.71/4.95
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0))

And the Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.95
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.95
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.95
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.95
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.95
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.95
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.95
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.95
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.95
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.95
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.95
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.95
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 17.71/4.95

POL(#0) = 0 17.71/4.95
POL(#ADD(x₁, x₂)) = 0 17.71/4.95
POL(#MULT(x₁, x₂)) = 0 17.71/4.95
POL(#NATMULT(x₁, x₂)) = 0 17.71/4.95
POL(#add(x₁, x₂)) = x₁ + x₂ 17.71/4.95
POL(#mult(x₁, x₂)) = [3] 17.71/4.95
POL(#natmult(x₁, x₂)) = 0 17.71/4.95
POL(#neg(x₁)) = x₁ 17.71/4.95
POL(#pos(x₁)) = 0 17.71/4.95
POL(#pred(x₁)) = x₁ 17.71/4.95
POL(#s(x₁)) = x₁ 17.71/4.95
POL(#succ(x₁)) = [3] 17.71/4.95
POL(*(x₁, x₂)) = [3]x₁² 17.71/4.95
POL(*'(x₁, x₂)) = 0 17.71/4.95
POL(+(x₁, x₂)) = [3] + [2]x₁ + [3]x₂ + [3]x₂² 17.71/4.95
POL(+'(x₁, x₂)) = 0 17.71/4.95
POL(::(x₁, x₂)) = [1] + x₁ + x₂ 17.71/4.95
POL(COMPUTELINE(x₁, x₂, x₃)) = [2]x₁·x₂ 17.71/4.95
POL(COMPUTELINE#1(x₁, x₂, x₃)) = [2]x₁·x₃ 17.71/4.95
POL(COMPUTELINE#2(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₁·x₄ + [2]x₁·x₃ 17.71/4.95
POL(LINEMULT(x₁, x₂, x₃)) = [2]x₂ 17.71/4.95
POL(LINEMULT#1(x₁, x₂, x₃)) = [2]x₁ 17.71/4.95
POL(LINEMULT#2(x₁, x₂, x₃, x₄)) = [2]x₃ + [2]x₄ 17.71/4.95
POL(MATRIXMULT(x₁, x₂)) = [3]x₂² + [2]x₁·x₂ 17.71/4.95
POL(MATRIXMULT#1(x₁, x₂)) = [3]x₂² + [2]x₁·x₂ 17.71/4.95
POL(c1) = 0 17.71/4.95
POL(c10(x₁)) = x₁ 17.71/4.95
POL(c12(x₁)) = x₁ 17.71/4.95
POL(c13(x₁)) = x₁ 17.71/4.95
POL(c15(x₁, x₂)) = x₁ + x₂ 17.71/4.95
POL(c2(x₁)) = x₁ 17.71/4.95
POL(c24(x₁)) = x₁ 17.71/4.95
POL(c25(x₁)) = x₁ 17.71/4.95
POL(c26(x₁)) = x₁ 17.71/4.95
POL(c27(x₁)) = x₁ 17.71/4.95
POL(c29(x₁, x₂)) = x₁ + x₂ 17.71/4.95
POL(c3) = 0 17.71/4.95
POL(c31(x₁)) = x₁ 17.71/4.95
POL(c32(x₁)) = x₁ 17.71/4.95
POL(c34(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 17.71/4.95
POL(c35(x₁, x₂)) = x₁ + x₂ 17.71/4.95
POL(c36(x₁)) = x₁ 17.71/4.95
POL(c37(x₁, x₂)) = x₁ + x₂ 17.71/4.95
POL(c4(x₁)) = x₁ 17.71/4.95
POL(c9(x₁)) = x₁ 17.71/4.95
POL(lineMult(x₁, x₂, x₃)) = 0 17.71/4.95
POL(lineMult#1(x₁, x₂, x₃)) = [3] + [3]x₂ + [3]x₃ + [3]x₃² + [3]x₂·x₃ + [3]x₂² 17.71/4.95
POL(lineMult#2(x₁, x₂, x₃, x₄)) = [3] + [3]x₂ + [3]x₃ + [3]x₄ + [3]x₄² + [3]x₃·x₄ + [3]x₂·x₄ + [3]x₃² + [3]x₂·x₃ + [3]x₂² 17.71/4.95
POL(nil) = 0

17.71/4.95

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

#add(#0, z0) → z0 17.71/4.95
#add(#neg(#s(#0)), z0) → #pred(z0) 17.71/4.95
#add(#neg(#s(#s(z0))), z1) → #pred(#add(#pos(#s(z0)), z1)) 17.71/4.95
#add(#pos(#s(#0)), z0) → #succ(z0) 17.71/4.95
#add(#pos(#s(#s(z0))), z1) → #succ(#add(#pos(#s(z0)), z1)) 17.71/4.95
#mult(#0, #0) → #0 17.71/4.95
#mult(#0, #neg(z0)) → #0 17.71/4.95
#mult(#0, #pos(z0)) → #0 17.71/4.95
#mult(#neg(z0), #0) → #0 17.71/4.95
#mult(#neg(z0), #neg(z1)) → #pos(#natmult(z0, z1)) 17.71/4.95
#mult(#neg(z0), #pos(z1)) → #neg(#natmult(z0, z1)) 17.71/4.95
#mult(#pos(z0), #0) → #0 17.71/4.95
#mult(#pos(z0), #neg(z1)) → #neg(#natmult(z0, z1)) 17.71/4.95
#mult(#pos(z0), #pos(z1)) → #pos(#natmult(z0, z1)) 17.71/4.95
#natmult(#0, z0) → #0 17.71/4.95
#natmult(#s(z0), z1) → #add(#pos(z1), #natmult(z0, z1)) 17.71/4.95
#pred(#0) → #neg(#s(#0)) 17.71/4.95
#pred(#neg(#s(z0))) → #neg(#s(#s(z0))) 17.71/4.95
#pred(#pos(#s(#0))) → #0 17.71/4.95
#pred(#pos(#s(#s(z0)))) → #pos(#s(z0)) 17.71/4.95
#succ(#0) → #pos(#s(#0)) 17.71/4.95
#succ(#neg(#s(#0))) → #0 17.71/4.95
#succ(#neg(#s(#s(z0)))) → #neg(#s(z0)) 17.71/4.95
#succ(#pos(#s(z0))) → #pos(#s(#s(z0))) 17.71/4.95
*(z0, z1) → #mult(z0, z1) 17.71/4.95
+(z0, z1) → #add(z0, z1) 17.71/4.95
computeLine(z0, z1, z2) → computeLine#1(z0, z2, z1) 17.71/4.95
computeLine#1(::(z0, z1), z2, z3) → computeLine#2(z3, z2, z0, z1) 17.71/4.95
computeLine#1(nil, z0, z1) → z0 17.71/4.95
computeLine#2(::(z0, z1), z2, z3, z4) → computeLine(z4, z1, lineMult(z3, z0, z2)) 17.71/4.95
computeLine#2(nil, z0, z1, z2) → nil 17.71/4.95
lineMult(z0, z1, z2) → lineMult#1(z1, z2, z0) 17.71/4.95
lineMult#1(::(z0, z1), z2, z3) → lineMult#2(z2, z3, z0, z1) 17.71/4.95
lineMult#1(nil, z0, z1) → nil 17.71/4.95
lineMult#2(::(z0, z1), z2, z3, z4) → ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) 17.71/4.95
lineMult#2(nil, z0, z1, z2) → ::(*(z1, z0), lineMult(z0, z2, nil)) 17.71/4.95
matrixMult(z0, z1) → matrixMult#1(z0, z1) 17.71/4.95
matrixMult#1(::(z0, z1), z2) → ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) 17.71/4.95
matrixMult#1(nil, z0) → nil

Tuples:

#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.95
#NATMULT(#s(z0), z1) → c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) 17.71/4.95
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.95
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.95
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1)) 17.71/4.95
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.95
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.95
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.95
MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.95
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.95
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.95
#ADD(#pos(#s(#0)), z0) → c3 17.71/4.95
#ADD(#pos(#s(#s(z0))), z1) → c4(#ADD(#pos(#s(z0)), z1))

S tuples:

*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.95
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil))

K tuples:

MATRIXMULT#1(::(z0, z1), z2) → c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) 17.71/4.95
MATRIXMULT(z0, z1) → c36(MATRIXMULT#1(z0, z1)) 17.71/4.95
COMPUTELINE(z0, z1, z2) → c26(COMPUTELINE#1(z0, z2, z1)) 17.71/4.95
COMPUTELINE#1(::(z0, z1), z2, z3) → c27(COMPUTELINE#2(z3, z2, z0, z1)) 17.71/4.95
COMPUTELINE#2(::(z0, z1), z2, z3, z4) → c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) 17.71/4.95
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1))

Defined Rule Symbols:

*, +, computeLine, computeLine#1, computeLine#2, lineMult, lineMult#1, lineMult#2, matrixMult, matrixMult#1, #add, #mult, #natmult, #pred, #succ

Defined Pair Symbols:

#MULT, #NATMULT, *', +', COMPUTELINE, COMPUTELINE#1, COMPUTELINE#2, LINEMULT, LINEMULT#1, LINEMULT#2, MATRIXMULT, MATRIXMULT#1, #ADD

Compound Symbols:

c9, c10, c12, c13, c15, c24, c25, c26, c27, c29, c31, c32, c34, c35, c36, c37, c1, c2, c3, c4

17.71/4.95

(17) CdtKnowledgeProof (EQUIVALENT transformation)

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

LINEMULT#2(::(z0, z1), z2, z3, z4) → c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) 17.71/4.95
LINEMULT#2(nil, z0, z1, z2) → c35(*'(z1, z0), LINEMULT(z0, z2, nil)) 17.71/4.95
+'(z0, z1) → c25(#ADD(z0, z1)) 17.71/4.95
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
*'(z0, z1) → c24(#MULT(z0, z1)) 17.71/4.95
LINEMULT(z0, z1, z2) → c31(LINEMULT#1(z1, z2, z0)) 17.71/4.95
#ADD(#neg(#s(#0)), z0) → c1 17.71/4.95
#ADD(#neg(#s(#s(z0))), z1) → c2(#ADD(#pos(#s(z0)), z1)) 17.71/4.95
#MULT(#neg(z0), #neg(z1)) → c9(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#neg(z0), #pos(z1)) → c10(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #neg(z1)) → c12(#NATMULT(z0, z1)) 17.71/4.95
#MULT(#pos(z0), #pos(z1)) → c13(#NATMULT(z0, z1)) 17.71/4.95
LINEMULT#1(::(z0, z1), z2, z3) → c32(LINEMULT#2(z2, z3, z0, z1))

Now S is empty

17.71/4.95

(18) BOUNDS(O(1), O(1))

17.71/4.95