WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 427 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 175 ms] (12) CdtProblem (13) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 88 ms] (16) CdtProblem (17) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 594 ms] (20) CdtProblem (21) CdtKnowledgeProof [FINISHED, 0 ms] (22) BOUNDS(1, 1) (23) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (24) TRS for Loop Detection (25) DecreasingLoopProof [LOWER BOUND(ID), 72 ms] (26) BEST (27) proven lower bound (28) LowerBoundPropagationProof [FINISHED, 0 ms] (29) BOUNDS(n^1, INF) (30) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: *(@x, @y) -> #mult(@x, @y) +(@x, @y) -> #add(@x, @y) computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) computeLine#1(nil, @acc, @m) -> @acc computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) computeLine#2(nil, @acc, @x, @xs) -> nil lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) lineMult#1(nil, @l2, @n) -> nil lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) lineMult#2(nil, @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil)) matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) matrixMult#1(nil, @m2) -> nil The (relative) TRS S consists of the following rules: #add(#0, @y) -> @y #add(#neg(#s(#0)), @y) -> #pred(@y) #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) #add(#pos(#s(#0)), @y) -> #succ(@y) #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) #mult(#0, #0) -> #0 #mult(#0, #neg(@y)) -> #0 #mult(#0, #pos(@y)) -> #0 #mult(#neg(@x), #0) -> #0 #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #0) -> #0 #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) #natmult(#0, @y) -> #0 #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: *(@x, @y) -> #mult(@x, @y) +(@x, @y) -> #add(@x, @y) computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) computeLine#1(nil, @acc, @m) -> @acc computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) computeLine#2(nil, @acc, @x, @xs) -> nil lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) lineMult#1(nil, @l2, @n) -> nil lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) lineMult#2(nil, @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil)) matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) matrixMult#1(nil, @m2) -> nil The (relative) TRS S consists of the following rules: #add(#0, @y) -> @y #add(#neg(#s(#0)), @y) -> #pred(@y) #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) #add(#pos(#s(#0)), @y) -> #succ(@y) #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) #mult(#0, #0) -> #0 #mult(#0, #neg(@y)) -> #0 #mult(#0, #pos(@y)) -> #0 #mult(#neg(@x), #0) -> #0 #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #0) -> #0 #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) #natmult(#0, @y) -> #0 #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) computeLine(z0, z1, z2) -> computeLine#1(z0, z2, z1) computeLine#1(::(z0, z1), z2, z3) -> computeLine#2(z3, z2, z0, z1) computeLine#1(nil, z0, z1) -> z0 computeLine#2(::(z0, z1), z2, z3, z4) -> computeLine(z4, z1, lineMult(z3, z0, z2)) computeLine#2(nil, z0, z1, z2) -> nil lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) matrixMult(z0, z1) -> matrixMult#1(z0, z1) matrixMult#1(::(z0, z1), z2) -> ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) matrixMult#1(nil, z0) -> nil Tuples: #ADD(#0, z0) -> c #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#0, #0) -> c5 #MULT(#0, #neg(z0)) -> c6 #MULT(#0, #pos(z0)) -> c7 #MULT(#neg(z0), #0) -> c8 #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #0) -> c11 #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#0, z0) -> c14 #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) #PRED(#0) -> c16 #PRED(#neg(#s(z0))) -> c17 #PRED(#pos(#s(#0))) -> c18 #PRED(#pos(#s(#s(z0)))) -> c19 #SUCC(#0) -> c20 #SUCC(#neg(#s(#0))) -> c21 #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#pos(#s(z0))) -> c23 *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#1(nil, z0, z1) -> c28 COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE#2(nil, z0, z1, z2) -> c30 LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#1(nil, z0, z1) -> c33 LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c38 S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#1(nil, z0, z1) -> c28 COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE#2(nil, z0, z1, z2) -> c30 LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#1(nil, z0, z1) -> c33 LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c38 K tuples:none Defined Rule Symbols: *_2, +_2, computeLine_3, computeLine#1_3, computeLine#2_4, lineMult_3, lineMult#1_3, lineMult#2_4, matrixMult_2, matrixMult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1 Defined Pair Symbols: #ADD_2, #MULT_2, #NATMULT_2, #PRED_1, #SUCC_1, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2 Compound Symbols: c, c1_1, c2_2, c3_1, c4_2, c5, c6, c7, c8, c9_1, c10_1, c11, c12_1, c13_1, c14, c15_2, c16, c17, c18, c19, c20, c21, c22, c23, c24_1, c25_1, c26_1, c27_1, c28, c29_2, c30, c31_1, c32_1, c33, c34_3, c35_2, c36_1, c37_2, c38 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 21 trailing nodes: LINEMULT#1(nil, z0, z1) -> c33 #PRED(#neg(#s(z0))) -> c17 #ADD(#neg(#s(#0)), z0) -> c1(#PRED(z0)) COMPUTELINE#2(nil, z0, z1, z2) -> c30 COMPUTELINE#1(nil, z0, z1) -> c28 #SUCC(#neg(#s(#0))) -> c21 #NATMULT(#0, z0) -> c14 #PRED(#0) -> c16 MATRIXMULT#1(nil, z0) -> c38 #PRED(#pos(#s(#s(z0)))) -> c19 #ADD(#0, z0) -> c #PRED(#pos(#s(#0))) -> c18 #SUCC(#pos(#s(z0))) -> c23 #MULT(#0, #0) -> c5 #MULT(#neg(z0), #0) -> c8 #MULT(#pos(z0), #0) -> c11 #MULT(#0, #neg(z0)) -> c6 #ADD(#pos(#s(#0)), z0) -> c3(#SUCC(z0)) #SUCC(#neg(#s(#s(z0)))) -> c22 #SUCC(#0) -> c20 #MULT(#0, #pos(z0)) -> c7 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) computeLine(z0, z1, z2) -> computeLine#1(z0, z2, z1) computeLine#1(::(z0, z1), z2, z3) -> computeLine#2(z3, z2, z0, z1) computeLine#1(nil, z0, z1) -> z0 computeLine#2(::(z0, z1), z2, z3, z4) -> computeLine(z4, z1, lineMult(z3, z0, z2)) computeLine#2(nil, z0, z1, z2) -> nil lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) matrixMult(z0, z1) -> matrixMult#1(z0, z1) matrixMult#1(::(z0, z1), z2) -> ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) matrixMult#1(nil, z0) -> nil Tuples: #ADD(#neg(#s(#s(z0))), z1) -> c2(#PRED(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#SUCC(#add(#pos(#s(z0)), z1)), #ADD(#pos(#s(z0)), z1)) #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) K tuples:none Defined Rule Symbols: *_2, +_2, computeLine_3, computeLine#1_3, computeLine#2_4, lineMult_3, lineMult#1_3, lineMult#2_4, matrixMult_2, matrixMult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1 Defined Pair Symbols: #ADD_2, #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2 Compound Symbols: c2_2, c4_2, c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) computeLine(z0, z1, z2) -> computeLine#1(z0, z2, z1) computeLine#1(::(z0, z1), z2, z3) -> computeLine#2(z3, z2, z0, z1) computeLine#1(nil, z0, z1) -> z0 computeLine#2(::(z0, z1), z2, z3, z4) -> computeLine(z4, z1, lineMult(z3, z0, z2)) computeLine#2(nil, z0, z1, z2) -> nil lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) matrixMult(z0, z1) -> matrixMult#1(z0, z1) matrixMult#1(::(z0, z1), z2) -> ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) matrixMult#1(nil, z0) -> nil Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) K tuples:none Defined Rule Symbols: *_2, +_2, computeLine_3, computeLine#1_3, computeLine#2_4, lineMult_3, lineMult#1_3, lineMult#2_4, matrixMult_2, matrixMult#1_2, #add_2, #mult_2, #natmult_2, #pred_1, #succ_1 Defined Pair Symbols: #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2, #ADD_2 Compound Symbols: c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2, c2_1, c4_1 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: computeLine(z0, z1, z2) -> computeLine#1(z0, z2, z1) computeLine#1(::(z0, z1), z2, z3) -> computeLine#2(z3, z2, z0, z1) computeLine#1(nil, z0, z1) -> z0 computeLine#2(::(z0, z1), z2, z3, z4) -> computeLine(z4, z1, lineMult(z3, z0, z2)) computeLine#2(nil, z0, z1, z2) -> nil matrixMult(z0, z1) -> matrixMult#1(z0, z1) matrixMult#1(::(z0, z1), z2) -> ::(computeLine(z0, z2, nil), matrixMult(z1, z2)) matrixMult#1(nil, z0) -> nil ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) +(z0, z1) -> #add(z0, z1) *(z0, z1) -> #mult(z0, z1) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) K tuples:none Defined Rule Symbols: #natmult_2, #add_2, #succ_1, lineMult_3, lineMult#1_3, lineMult#2_4, +_2, *_2, #mult_2, #pred_1 Defined Pair Symbols: #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2, #ADD_2 Compound Symbols: c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2, c2_1, c4_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) We considered the (Usable) Rules:none And the Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(#0) = 0 POL(#ADD(x_1, x_2)) = 0 POL(#MULT(x_1, x_2)) = 0 POL(#NATMULT(x_1, x_2)) = 0 POL(#add(x_1, x_2)) = 0 POL(#mult(x_1, x_2)) = [3] + [3]x_1 + [3]x_2 POL(#natmult(x_1, x_2)) = x_1 POL(#neg(x_1)) = 0 POL(#pos(x_1)) = 0 POL(#pred(x_1)) = [3] + [3]x_1 POL(#s(x_1)) = [1] POL(#succ(x_1)) = [3] POL(*(x_1, x_2)) = [3]x_1 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = [3] + [3]x_1 + [3]x_2 POL(+'(x_1, x_2)) = 0 POL(::(x_1, x_2)) = [2] + x_2 POL(COMPUTELINE(x_1, x_2, x_3)) = [2] POL(COMPUTELINE#1(x_1, x_2, x_3)) = [2] POL(COMPUTELINE#2(x_1, x_2, x_3, x_4)) = [2] POL(LINEMULT(x_1, x_2, x_3)) = 0 POL(LINEMULT#1(x_1, x_2, x_3)) = 0 POL(LINEMULT#2(x_1, x_2, x_3, x_4)) = 0 POL(MATRIXMULT(x_1, x_2)) = [2] + [2]x_1 + [3]x_2 POL(MATRIXMULT#1(x_1, x_2)) = [2]x_1 + [3]x_2 POL(c10(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c15(x_1, x_2)) = x_1 + x_2 POL(c2(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1, x_2)) = x_1 + x_2 POL(c31(x_1)) = x_1 POL(c32(x_1)) = x_1 POL(c34(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c4(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(lineMult(x_1, x_2, x_3)) = [3]x_1 + [3]x_2 + [2]x_3 POL(lineMult#1(x_1, x_2, x_3)) = [3] + [3]x_1 + [3]x_2 + [3]x_3 POL(lineMult#2(x_1, x_2, x_3, x_4)) = [3] + [3]x_1 + [3]x_2 + [3]x_3 + [3]x_4 POL(nil) = 0 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) +(z0, z1) -> #add(z0, z1) *(z0, z1) -> #mult(z0, z1) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) K tuples: MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) Defined Rule Symbols: #natmult_2, #add_2, #succ_1, lineMult_3, lineMult#1_3, lineMult#2_4, +_2, *_2, #mult_2, #pred_1 Defined Pair Symbols: #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2, #ADD_2 Compound Symbols: c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2, c2_1, c4_1 ---------------------------------------- (13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) +(z0, z1) -> #add(z0, z1) *(z0, z1) -> #mult(z0, z1) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) K tuples: MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) Defined Rule Symbols: #natmult_2, #add_2, #succ_1, lineMult_3, lineMult#1_3, lineMult#2_4, +_2, *_2, #mult_2, #pred_1 Defined Pair Symbols: #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2, #ADD_2 Compound Symbols: c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2, c2_1, c4_1 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) We considered the (Usable) Rules:none And the Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(#0) = 0 POL(#ADD(x_1, x_2)) = 0 POL(#MULT(x_1, x_2)) = 0 POL(#NATMULT(x_1, x_2)) = 0 POL(#add(x_1, x_2)) = 0 POL(#mult(x_1, x_2)) = [1] + x_1 + x_2 POL(#natmult(x_1, x_2)) = [1] + x_1 + x_2 POL(#neg(x_1)) = 0 POL(#pos(x_1)) = 0 POL(#pred(x_1)) = [1] + x_1 POL(#s(x_1)) = 0 POL(#succ(x_1)) = [1] + x_1 POL(*(x_1, x_2)) = x_1 + x_2 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = [1] + x_1 + x_2 POL(+'(x_1, x_2)) = 0 POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(COMPUTELINE(x_1, x_2, x_3)) = x_1 POL(COMPUTELINE#1(x_1, x_2, x_3)) = x_1 POL(COMPUTELINE#2(x_1, x_2, x_3, x_4)) = x_3 + x_4 POL(LINEMULT(x_1, x_2, x_3)) = x_1 POL(LINEMULT#1(x_1, x_2, x_3)) = x_3 POL(LINEMULT#2(x_1, x_2, x_3, x_4)) = x_2 POL(MATRIXMULT(x_1, x_2)) = [1] + x_1 + x_2 POL(MATRIXMULT#1(x_1, x_2)) = [1] + x_1 + x_2 POL(c10(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c15(x_1, x_2)) = x_1 + x_2 POL(c2(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1, x_2)) = x_1 + x_2 POL(c31(x_1)) = x_1 POL(c32(x_1)) = x_1 POL(c34(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c4(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(lineMult(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(lineMult#1(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(lineMult#2(x_1, x_2, x_3, x_4)) = [1] + x_1 + x_2 + x_3 + x_4 POL(nil) = 0 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) +(z0, z1) -> #add(z0, z1) *(z0, z1) -> #mult(z0, z1) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) K tuples: MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) Defined Rule Symbols: #natmult_2, #add_2, #succ_1, lineMult_3, lineMult#1_3, lineMult#2_4, +_2, *_2, #mult_2, #pred_1 Defined Pair Symbols: #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2, #ADD_2 Compound Symbols: c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2, c2_1, c4_1 ---------------------------------------- (17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) +(z0, z1) -> #add(z0, z1) *(z0, z1) -> #mult(z0, z1) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) K tuples: MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) Defined Rule Symbols: #natmult_2, #add_2, #succ_1, lineMult_3, lineMult#1_3, lineMult#2_4, +_2, *_2, #mult_2, #pred_1 Defined Pair Symbols: #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2, #ADD_2 Compound Symbols: c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2, c2_1, c4_1 ---------------------------------------- (19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) 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:none And the Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(#0) = 0 POL(#ADD(x_1, x_2)) = 0 POL(#MULT(x_1, x_2)) = 0 POL(#NATMULT(x_1, x_2)) = 0 POL(#add(x_1, x_2)) = 0 POL(#mult(x_1, x_2)) = [1] POL(#natmult(x_1, x_2)) = [2]x_2 POL(#neg(x_1)) = 0 POL(#pos(x_1)) = 0 POL(#pred(x_1)) = [1] POL(#s(x_1)) = 0 POL(#succ(x_1)) = [1] POL(*(x_1, x_2)) = 0 POL(*'(x_1, x_2)) = 0 POL(+(x_1, x_2)) = [2] + x_1 + x_2 + [2]x_2^2 + x_1*x_2 + [2]x_1^2 POL(+'(x_1, x_2)) = 0 POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(COMPUTELINE(x_1, x_2, x_3)) = x_2 POL(COMPUTELINE#1(x_1, x_2, x_3)) = x_3 POL(COMPUTELINE#2(x_1, x_2, x_3, x_4)) = x_1 POL(LINEMULT(x_1, x_2, x_3)) = x_2 POL(LINEMULT#1(x_1, x_2, x_3)) = x_1 POL(LINEMULT#2(x_1, x_2, x_3, x_4)) = x_4 POL(MATRIXMULT(x_1, x_2)) = [2]x_2^2 + [2]x_1*x_2 POL(MATRIXMULT#1(x_1, x_2)) = [2]x_2^2 + [2]x_1*x_2 POL(c10(x_1)) = x_1 POL(c12(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c15(x_1, x_2)) = x_1 + x_2 POL(c2(x_1)) = x_1 POL(c24(x_1)) = x_1 POL(c25(x_1)) = x_1 POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c29(x_1, x_2)) = x_1 + x_2 POL(c31(x_1)) = x_1 POL(c32(x_1)) = x_1 POL(c34(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c35(x_1, x_2)) = x_1 + x_2 POL(c36(x_1)) = x_1 POL(c37(x_1, x_2)) = x_1 + x_2 POL(c4(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(lineMult(x_1, x_2, x_3)) = 0 POL(lineMult#1(x_1, x_2, x_3)) = [1] + x_2 + x_3 + x_3^2 + x_2*x_3 + x_2^2 POL(lineMult#2(x_1, x_2, x_3, x_4)) = [1] + x_2 + x_3 + x_4 + x_4^2 + x_3*x_4 + x_2*x_4 + x_3^2 + x_2*x_3 + x_2^2 POL(nil) = 0 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: #natmult(#0, z0) -> #0 #natmult(#s(z0), z1) -> #add(#pos(z1), #natmult(z0, z1)) #add(#pos(#s(#0)), z0) -> #succ(z0) #add(#pos(#s(#s(z0))), z1) -> #succ(#add(#pos(#s(z0)), z1)) #add(#0, z0) -> z0 #add(#neg(#s(#0)), z0) -> #pred(z0) #add(#neg(#s(#s(z0))), z1) -> #pred(#add(#pos(#s(z0)), z1)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(z0)))) -> #neg(#s(z0)) #succ(#pos(#s(z0))) -> #pos(#s(#s(z0))) lineMult(z0, z1, z2) -> lineMult#1(z1, z2, z0) lineMult#1(::(z0, z1), z2, z3) -> lineMult#2(z2, z3, z0, z1) lineMult#1(nil, z0, z1) -> nil lineMult#2(::(z0, z1), z2, z3, z4) -> ::(+(*(z3, z2), z0), lineMult(z2, z4, z1)) lineMult#2(nil, z0, z1, z2) -> ::(*(z1, z0), lineMult(z0, z2, nil)) +(z0, z1) -> #add(z0, z1) *(z0, z1) -> #mult(z0, z1) #mult(#0, #0) -> #0 #mult(#0, #neg(z0)) -> #0 #mult(#0, #pos(z0)) -> #0 #mult(#neg(z0), #0) -> #0 #mult(#neg(z0), #neg(z1)) -> #pos(#natmult(z0, z1)) #mult(#neg(z0), #pos(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #0) -> #0 #mult(#pos(z0), #neg(z1)) -> #neg(#natmult(z0, z1)) #mult(#pos(z0), #pos(z1)) -> #pos(#natmult(z0, z1)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(z0))) -> #neg(#s(#s(z0))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(z0)))) -> #pos(#s(z0)) Tuples: #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) #NATMULT(#s(z0), z1) -> c15(#ADD(#pos(z1), #natmult(z0, z1)), #NATMULT(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #ADD(#pos(#s(#s(z0))), z1) -> c4(#ADD(#pos(#s(z0)), z1)) S tuples: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c34(+'(*(z3, z2), z0), *'(z3, z2), LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) K tuples: MATRIXMULT(z0, z1) -> c36(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c37(COMPUTELINE(z0, z2, nil), MATRIXMULT(z1, z2)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c27(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c29(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE(z0, z1, z2) -> c26(COMPUTELINE#1(z0, z2, z1)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) Defined Rule Symbols: #natmult_2, #add_2, #succ_1, lineMult_3, lineMult#1_3, lineMult#2_4, +_2, *_2, #mult_2, #pred_1 Defined Pair Symbols: #MULT_2, #NATMULT_2, *'_2, +'_2, COMPUTELINE_3, COMPUTELINE#1_3, COMPUTELINE#2_4, LINEMULT_3, LINEMULT#1_3, LINEMULT#2_4, MATRIXMULT_2, MATRIXMULT#1_2, #ADD_2 Compound Symbols: c9_1, c10_1, c12_1, c13_1, c15_2, c24_1, c25_1, c26_1, c27_1, c29_2, c31_1, c32_1, c34_3, c35_2, c36_1, c37_2, c2_1, c4_1 ---------------------------------------- (21) CdtKnowledgeProof (FINISHED) 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)) LINEMULT#2(nil, z0, z1, z2) -> c35(*'(z1, z0), LINEMULT(z0, z2, nil)) +'(z0, z1) -> c25(#ADD(z0, z1)) *'(z0, z1) -> c24(#MULT(z0, z1)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) *'(z0, z1) -> c24(#MULT(z0, z1)) LINEMULT(z0, z1, z2) -> c31(LINEMULT#1(z1, z2, z0)) #ADD(#neg(#s(#s(z0))), z1) -> c2(#ADD(#pos(#s(z0)), z1)) #MULT(#neg(z0), #neg(z1)) -> c9(#NATMULT(z0, z1)) #MULT(#neg(z0), #pos(z1)) -> c10(#NATMULT(z0, z1)) #MULT(#pos(z0), #neg(z1)) -> c12(#NATMULT(z0, z1)) #MULT(#pos(z0), #pos(z1)) -> c13(#NATMULT(z0, z1)) LINEMULT#1(::(z0, z1), z2, z3) -> c32(LINEMULT#2(z2, z3, z0, z1)) Now S is empty ---------------------------------------- (22) BOUNDS(1, 1) ---------------------------------------- (23) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (24) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: *(@x, @y) -> #mult(@x, @y) +(@x, @y) -> #add(@x, @y) computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) computeLine#1(nil, @acc, @m) -> @acc computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) computeLine#2(nil, @acc, @x, @xs) -> nil lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) lineMult#1(nil, @l2, @n) -> nil lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) lineMult#2(nil, @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil)) matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) matrixMult#1(nil, @m2) -> nil The (relative) TRS S consists of the following rules: #add(#0, @y) -> @y #add(#neg(#s(#0)), @y) -> #pred(@y) #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) #add(#pos(#s(#0)), @y) -> #succ(@y) #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) #mult(#0, #0) -> #0 #mult(#0, #neg(@y)) -> #0 #mult(#0, #pos(@y)) -> #0 #mult(#neg(@x), #0) -> #0 #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #0) -> #0 #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) #natmult(#0, @y) -> #0 #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) Rewrite Strategy: INNERMOST ---------------------------------------- (25) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence matrixMult#1(::(@l, @ls), @m2) ->^+ ::(computeLine(@l, @m2, nil), matrixMult#1(@ls, @m2)) gives rise to a decreasing loop by considering the right hand sides subterm at position [1]. The pumping substitution is [@ls / ::(@l, @ls)]. The result substitution is [ ]. ---------------------------------------- (26) Complex Obligation (BEST) ---------------------------------------- (27) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: *(@x, @y) -> #mult(@x, @y) +(@x, @y) -> #add(@x, @y) computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) computeLine#1(nil, @acc, @m) -> @acc computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) computeLine#2(nil, @acc, @x, @xs) -> nil lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) lineMult#1(nil, @l2, @n) -> nil lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) lineMult#2(nil, @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil)) matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) matrixMult#1(nil, @m2) -> nil The (relative) TRS S consists of the following rules: #add(#0, @y) -> @y #add(#neg(#s(#0)), @y) -> #pred(@y) #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) #add(#pos(#s(#0)), @y) -> #succ(@y) #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) #mult(#0, #0) -> #0 #mult(#0, #neg(@y)) -> #0 #mult(#0, #pos(@y)) -> #0 #mult(#neg(@x), #0) -> #0 #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #0) -> #0 #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) #natmult(#0, @y) -> #0 #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) Rewrite Strategy: INNERMOST ---------------------------------------- (28) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (29) BOUNDS(n^1, INF) ---------------------------------------- (30) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: *(@x, @y) -> #mult(@x, @y) +(@x, @y) -> #add(@x, @y) computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) computeLine#1(nil, @acc, @m) -> @acc computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) computeLine#2(nil, @acc, @x, @xs) -> nil lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) lineMult#1(nil, @l2, @n) -> nil lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) lineMult#2(nil, @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil)) matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil), matrixMult(@ls, @m2)) matrixMult#1(nil, @m2) -> nil The (relative) TRS S consists of the following rules: #add(#0, @y) -> @y #add(#neg(#s(#0)), @y) -> #pred(@y) #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) #add(#pos(#s(#0)), @y) -> #succ(@y) #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) #mult(#0, #0) -> #0 #mult(#0, #neg(@y)) -> #0 #mult(#0, #pos(@y)) -> #0 #mult(#neg(@x), #0) -> #0 #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #0) -> #0 #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) #natmult(#0, @y) -> #0 #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y)) #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) Rewrite Strategy: INNERMOST