WORST_CASE(Omega(n^1),O(n^1)) 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^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 1169 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 20 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 1 ms] (8) CdtProblem (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 243 ms] (14) CdtProblem (15) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 133 ms] (18) CdtProblem (19) CdtKnowledgeProof [FINISHED, 0 ms] (20) BOUNDS(1, 1) (21) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (22) TRS for Loop Detection (23) DecreasingLoopProof [LOWER BOUND(ID), 97 ms] (24) BEST (25) proven lower bound (26) LowerBoundPropagationProof [FINISHED, 0 ms] (27) BOUNDS(n^1, INF) (28) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 The (relative) TRS S consists of the following rules: #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 #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 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^1). The TRS R consists of the following rules: *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 The (relative) TRS S consists of the following rules: #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 #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 Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: #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 #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 *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 Tuples: #ADD'(#0, z0) -> c42 #ADD'(#neg(#s(#0)), z0) -> c43(#PRED'(z0)) #ADD'(#neg(#s(#s(z0))), z1) -> c44(#PRED'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD'(#pos(#s(#0)), z0) -> c45(#SUCC'(z0)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#SUCC'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #MULT'(#0, #0) -> c47 #MULT'(#0, #neg(z0)) -> c48 #MULT'(#0, #pos(z0)) -> c49 #MULT'(#neg(z0), #0) -> c50 #MULT'(#neg(z0), #neg(z1)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #0) -> c53 #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#0, z0) -> c56 #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #PRED'(#0) -> c58 #PRED'(#neg(#s(z0))) -> c59 #PRED'(#pos(#s(#0))) -> c60 #PRED'(#pos(#s(#s(z0)))) -> c61 #SUCC'(#0) -> c62 #SUCC'(#neg(#s(#0))) -> c63 #SUCC'(#neg(#s(#s(z0)))) -> c64 #SUCC'(#pos(#s(z0))) -> c65 #ADD''(#0, z0) -> c66 #ADD''(#neg(#s(#0)), z0) -> c67(#PRED''(z0)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#PRED''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#0)), z0) -> c69(#SUCC''(z0)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#SUCC''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #MULT''(#0, #0) -> c71 #MULT''(#0, #neg(z0)) -> c72 #MULT''(#0, #pos(z0)) -> c73 #MULT''(#neg(z0), #0) -> c74 #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #0) -> c77 #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#0, z0) -> c80 #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) #PRED''(#0) -> c82 #PRED''(#neg(#s(z0))) -> c83 #PRED''(#pos(#s(#0))) -> c84 #PRED''(#pos(#s(#s(z0)))) -> c85 #SUCC''(#0) -> c86 #SUCC''(#neg(#s(#0))) -> c87 #SUCC''(#neg(#s(#s(z0)))) -> c88 #SUCC''(#pos(#s(z0))) -> c89 *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#1'(nil, z0, z1) -> c94 COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) COMPUTELINE#2'(nil, z0, z1, z2) -> c96 LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#1'(nil, z0, z1) -> c99 LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) MATRIXMULT#1'(nil, z0) -> c104 *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#1''(nil, z0, z1) -> c109 COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) COMPUTELINE#2''(nil, z0, z1, z2) -> c111 LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#1''(nil, z0, z1) -> c114 LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c115(+'''(*(z3, z2), z0), *''(z3, z2), *'''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) MATRIXMULT#1''(nil, z0) -> c122 S tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#1''(nil, z0, z1) -> c109 COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) COMPUTELINE#2''(nil, z0, z1, z2) -> c111 LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#1''(nil, z0, z1) -> c114 LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c115(+'''(*(z3, z2), z0), *''(z3, z2), *'''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) MATRIXMULT#1''(nil, z0) -> c122 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, #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 Defined Pair Symbols: #ADD'_2, #MULT'_2, #NATMULT'_2, #PRED'_1, #SUCC'_1, #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, *'''_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: c42, c43_1, c44_3, c45_1, c46_3, c47, c48, c49, c50, c51_1, c52_1, c53, c54_1, c55_1, c56, c57_3, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67_1, c68_2, c69_1, c70_2, c71, c72, c73, c74, c75_1, c76_1, c77, c78_1, c79_1, c80, c81_2, c82, c83, c84, c85, c86, c87, c88, c89, c90_1, c91_1, c92_1, c93_1, c94, c95_2, c96, c97_1, c98_1, c99, c100_3, c101_2, c102_1, c103_2, c104, c105_1, c106_1, c107_1, c108_1, c109, c110_3, c111, c112_1, c113_1, c114, c115_3, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1, c122 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 42 trailing nodes: #MULT'(#neg(z0), #0) -> c50 #SUCC'(#neg(#s(#0))) -> c63 #ADD''(#0, z0) -> c66 #PRED''(#pos(#s(#s(z0)))) -> c85 #MULT'(#0, #0) -> c47 #PRED''(#pos(#s(#0))) -> c84 #MULT'(#pos(z0), #0) -> c53 #NATMULT''(#0, z0) -> c80 #MULT''(#0, #neg(z0)) -> c72 COMPUTELINE#1'(nil, z0, z1) -> c94 #SUCC''(#neg(#s(#0))) -> c87 #SUCC'(#pos(#s(z0))) -> c65 #SUCC''(#pos(#s(z0))) -> c89 #PRED'(#pos(#s(#0))) -> c60 #NATMULT'(#0, z0) -> c56 #SUCC'(#neg(#s(#s(z0)))) -> c64 #PRED''(#0) -> c82 #ADD''(#pos(#s(#0)), z0) -> c69(#SUCC''(z0)) #MULT''(#neg(z0), #0) -> c74 #PRED''(#neg(#s(z0))) -> c83 #PRED'(#pos(#s(#s(z0)))) -> c61 #MULT'(#0, #neg(z0)) -> c48 MATRIXMULT#1''(nil, z0) -> c122 #MULT''(#0, #0) -> c71 LINEMULT#1''(nil, z0, z1) -> c114 #ADD''(#neg(#s(#0)), z0) -> c67(#PRED''(z0)) #ADD'(#neg(#s(#0)), z0) -> c43(#PRED'(z0)) COMPUTELINE#1''(nil, z0, z1) -> c109 #PRED'(#0) -> c58 #ADD'(#0, z0) -> c42 #SUCC''(#0) -> c86 #MULT''(#0, #pos(z0)) -> c73 COMPUTELINE#2''(nil, z0, z1, z2) -> c111 LINEMULT#1'(nil, z0, z1) -> c99 #MULT''(#pos(z0), #0) -> c77 #SUCC''(#neg(#s(#s(z0)))) -> c88 #SUCC'(#0) -> c62 #ADD'(#pos(#s(#0)), z0) -> c45(#SUCC'(z0)) COMPUTELINE#2'(nil, z0, z1, z2) -> c96 #PRED'(#neg(#s(z0))) -> c59 MATRIXMULT#1'(nil, z0) -> c104 #MULT'(#0, #pos(z0)) -> c49 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: #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 #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 *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 Tuples: #ADD'(#neg(#s(#s(z0))), z1) -> c44(#PRED'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#SUCC'(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #MULT'(#neg(z0), #neg(z1)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#PRED''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#SUCC''(#add(#pos(#s(z0)), z1)), #ADD''(#pos(#s(z0)), z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c115(+'''(*(z3, z2), z0), *''(z3, z2), *'''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) S tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c115(+'''(*(z3, z2), z0), *''(z3, z2), *'''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(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, #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 Defined Pair Symbols: #ADD'_2, #MULT'_2, #NATMULT'_2, #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, *'''_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: c44_3, c46_3, c51_1, c52_1, c54_1, c55_1, c57_3, c68_2, c70_2, c75_1, c76_1, c78_1, c79_1, c81_2, c90_1, c91_1, c92_1, c93_1, c95_2, c97_1, c98_1, c100_3, c101_2, c102_1, c103_2, c105_1, c106_1, c107_1, c108_1, c110_3, c112_1, c113_1, c115_3, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: #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 #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 *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 Tuples: #MULT'(#neg(z0), #neg(z1)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c115(+'''(*(z3, z2), z0), *''(z3, z2), *'''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c44(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) S tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c115(+'''(*(z3, z2), z0), *''(z3, z2), *'''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(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, #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 Defined Pair Symbols: #MULT'_2, #NATMULT'_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, *'''_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, #ADD''_2 Compound Symbols: c51_1, c52_1, c54_1, c55_1, c57_3, c75_1, c76_1, c78_1, c79_1, c81_2, c90_1, c91_1, c92_1, c93_1, c95_2, c97_1, c98_1, c100_3, c101_2, c102_1, c103_2, c105_1, c106_1, c107_1, c108_1, c110_3, c112_1, c113_1, c115_3, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1, c44_2, c46_2, c68_1, c70_1 ---------------------------------------- (9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: #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 #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 *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 Tuples: #MULT'(#neg(z0), #neg(z1)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD'(#pos(#s(z0)), z1)) S tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, 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, #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 Defined Pair Symbols: #MULT'_2, #NATMULT'_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, *'''_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, #ADD''_2 Compound Symbols: c51_1, c52_1, c54_1, c55_1, c57_3, c75_1, c76_1, c78_1, c79_1, c81_2, c90_1, c91_1, c92_1, c93_1, c95_2, c97_1, c98_1, c100_3, c101_2, c102_1, c103_2, c105_1, c106_1, c107_1, c108_1, c110_3, c112_1, c113_1, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1, c46_2, c68_1, c70_1, c42_1 ---------------------------------------- (11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: #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 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 *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 ---------------------------------------- (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)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD'(#pos(#s(z0)), z1)) S tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, 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, #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, *'''_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, #ADD''_2 Compound Symbols: c51_1, c52_1, c54_1, c55_1, c57_3, c75_1, c76_1, c78_1, c79_1, c81_2, c90_1, c91_1, c92_1, c93_1, c95_2, c97_1, c98_1, c100_3, c101_2, c102_1, c103_2, c105_1, c106_1, c107_1, c108_1, c110_3, c112_1, c113_1, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1, c46_2, c68_1, c70_1, c42_1 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) We considered the (Usable) Rules:none And the Tuples: #MULT'(#neg(z0), #neg(z1)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#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(#ADD''(x_1, x_2)) = 0 POL(#MULT'(x_1, x_2)) = x_1 POL(#MULT''(x_1, x_2)) = 0 POL(#NATMULT'(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)) = [1] + 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)) = x_1 + x_2 POL(*''(x_1, x_2)) = 0 POL(*'''(x_1, x_2)) = [1] + x_1 POL(+(x_1, x_2)) = [1] + x_1 + x_2 POL(+''(x_1, x_2)) = 0 POL(+'''(x_1, x_2)) = [1] POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(COMPUTELINE#1'(x_1, x_2, x_3)) = x_1 POL(COMPUTELINE#1''(x_1, x_2, x_3)) = x_3 POL(COMPUTELINE#2'(x_1, x_2, x_3, x_4)) = [1] + x_3 + x_4 POL(COMPUTELINE#2''(x_1, x_2, x_3, x_4)) = x_1 POL(COMPUTELINE'(x_1, x_2, x_3)) = [1] + x_1 POL(COMPUTELINE''(x_1, x_2, x_3)) = x_2 POL(LINEMULT#1'(x_1, x_2, x_3)) = 0 POL(LINEMULT#1''(x_1, x_2, x_3)) = x_1 POL(LINEMULT#2'(x_1, x_2, x_3, x_4)) = 0 POL(LINEMULT#2''(x_1, x_2, x_3, x_4)) = [1] + x_3 + x_4 POL(LINEMULT'(x_1, x_2, x_3)) = 0 POL(LINEMULT''(x_1, x_2, x_3)) = x_2 POL(MATRIXMULT#1'(x_1, x_2)) = [1] + x_1 + x_2 POL(MATRIXMULT#1''(x_1, x_2)) = [1] + x_2 POL(MATRIXMULT'(x_1, x_2)) = [1] + x_1 + x_2 POL(MATRIXMULT''(x_1, x_2)) = [1] + x_2 POL(c100(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c101(x_1, x_2)) = x_1 + x_2 POL(c102(x_1)) = x_1 POL(c103(x_1, x_2)) = x_1 + x_2 POL(c105(x_1)) = x_1 POL(c106(x_1)) = x_1 POL(c107(x_1)) = x_1 POL(c108(x_1)) = x_1 POL(c110(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c112(x_1)) = x_1 POL(c113(x_1)) = x_1 POL(c116(x_1)) = x_1 POL(c117(x_1)) = x_1 POL(c118(x_1)) = x_1 POL(c119(x_1)) = x_1 POL(c120(x_1)) = x_1 POL(c121(x_1)) = x_1 POL(c42(x_1)) = x_1 POL(c46(x_1, x_2)) = x_1 + x_2 POL(c51(x_1)) = x_1 POL(c52(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c57(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c68(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1, x_2)) = x_1 + x_2 POL(c90(x_1)) = x_1 POL(c91(x_1)) = x_1 POL(c92(x_1)) = x_1 POL(c93(x_1)) = x_1 POL(c95(x_1, x_2)) = x_1 + x_2 POL(c97(x_1)) = x_1 POL(c98(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_2 + x_3 POL(lineMult#2(x_1, x_2, x_3, x_4)) = [1] + x_2 + x_3 + x_4 POL(nil) = 0 ---------------------------------------- (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)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD'(#pos(#s(z0)), z1)) S tuples: COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) K tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, 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, #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, *'''_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, #ADD''_2 Compound Symbols: c51_1, c52_1, c54_1, c55_1, c57_3, c75_1, c76_1, c78_1, c79_1, c81_2, c90_1, c91_1, c92_1, c93_1, c95_2, c97_1, c98_1, c100_3, c101_2, c102_1, c103_2, c105_1, c106_1, c107_1, c108_1, c110_3, c112_1, c113_1, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1, c46_2, c68_1, c70_1, c42_1 ---------------------------------------- (15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) ---------------------------------------- (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)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD'(#pos(#s(z0)), z1)) S tuples: MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) K tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, 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, #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, *'''_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, #ADD''_2 Compound Symbols: c51_1, c52_1, c54_1, c55_1, c57_3, c75_1, c76_1, c78_1, c79_1, c81_2, c90_1, c91_1, c92_1, c93_1, c95_2, c97_1, c98_1, c100_3, c101_2, c102_1, c103_2, c105_1, c106_1, c107_1, c108_1, c110_3, c112_1, c113_1, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1, c46_2, c68_1, c70_1, c42_1 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) We considered the (Usable) Rules:none And the Tuples: #MULT'(#neg(z0), #neg(z1)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#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(#ADD''(x_1, x_2)) = 0 POL(#MULT'(x_1, x_2)) = [1] + x_1 + x_2 POL(#MULT''(x_1, x_2)) = 0 POL(#NATMULT'(x_1, x_2)) = [1] 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)) = [1] + x_2 POL(#neg(x_1)) = [1] 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)) = x_1 POL(*''(x_1, x_2)) = 0 POL(*'''(x_1, x_2)) = [1] + x_1 + x_2 POL(+(x_1, x_2)) = [1] + x_1 + x_2 POL(+''(x_1, x_2)) = 0 POL(+'''(x_1, x_2)) = 0 POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(COMPUTELINE#1'(x_1, x_2, x_3)) = [1] + x_1 POL(COMPUTELINE#1''(x_1, x_2, x_3)) = x_1 + x_3 POL(COMPUTELINE#2'(x_1, x_2, x_3, x_4)) = [1] + x_3 + x_4 POL(COMPUTELINE#2''(x_1, x_2, x_3, x_4)) = [1] + x_1 + x_3 + x_4 POL(COMPUTELINE'(x_1, x_2, x_3)) = [1] + x_1 POL(COMPUTELINE''(x_1, x_2, x_3)) = [1] + x_1 + x_2 POL(LINEMULT#1'(x_1, x_2, x_3)) = 0 POL(LINEMULT#1''(x_1, x_2, x_3)) = x_1 + x_3 POL(LINEMULT#2'(x_1, x_2, x_3, x_4)) = 0 POL(LINEMULT#2''(x_1, x_2, x_3, x_4)) = [1] + x_2 + x_3 + x_4 POL(LINEMULT'(x_1, x_2, x_3)) = 0 POL(LINEMULT''(x_1, x_2, x_3)) = [1] + x_1 + x_2 POL(MATRIXMULT#1'(x_1, x_2)) = [1] + x_1 + x_2 POL(MATRIXMULT#1''(x_1, x_2)) = [1] + x_1 + x_2 POL(MATRIXMULT'(x_1, x_2)) = [1] + x_1 + x_2 POL(MATRIXMULT''(x_1, x_2)) = [1] + x_1 + x_2 POL(c100(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c101(x_1, x_2)) = x_1 + x_2 POL(c102(x_1)) = x_1 POL(c103(x_1, x_2)) = x_1 + x_2 POL(c105(x_1)) = x_1 POL(c106(x_1)) = x_1 POL(c107(x_1)) = x_1 POL(c108(x_1)) = x_1 POL(c110(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c112(x_1)) = x_1 POL(c113(x_1)) = x_1 POL(c116(x_1)) = x_1 POL(c117(x_1)) = x_1 POL(c118(x_1)) = x_1 POL(c119(x_1)) = x_1 POL(c120(x_1)) = x_1 POL(c121(x_1)) = x_1 POL(c42(x_1)) = x_1 POL(c46(x_1, x_2)) = x_1 + x_2 POL(c51(x_1)) = x_1 POL(c52(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1)) = x_1 POL(c57(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c68(x_1)) = x_1 POL(c70(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1)) = x_1 POL(c78(x_1)) = x_1 POL(c79(x_1)) = x_1 POL(c81(x_1, x_2)) = x_1 + x_2 POL(c90(x_1)) = x_1 POL(c91(x_1)) = x_1 POL(c92(x_1)) = x_1 POL(c93(x_1)) = x_1 POL(c95(x_1, x_2)) = x_1 + x_2 POL(c97(x_1)) = x_1 POL(c98(x_1)) = x_1 POL(lineMult(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(lineMult#1(x_1, x_2, x_3)) = 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) = [1] ---------------------------------------- (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)) -> c51(#NATMULT'(z0, z1)) #MULT'(#neg(z0), #pos(z1)) -> c52(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #neg(z1)) -> c54(#NATMULT'(z0, z1)) #MULT'(#pos(z0), #pos(z1)) -> c55(#NATMULT'(z0, z1)) #NATMULT'(#s(z0), z1) -> c57(#ADD'(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1), #NATMULT'(z0, z1)) #MULT''(#neg(z0), #neg(z1)) -> c75(#NATMULT''(z0, z1)) #MULT''(#neg(z0), #pos(z1)) -> c76(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #neg(z1)) -> c78(#NATMULT''(z0, z1)) #MULT''(#pos(z0), #pos(z1)) -> c79(#NATMULT''(z0, z1)) #NATMULT''(#s(z0), z1) -> c81(#ADD''(#pos(z1), #natmult(z0, z1)), #NATMULT''(z0, z1)) *''(z0, z1) -> c90(#MULT''(z0, z1)) +''(z0, z1) -> c91(#ADD''(z0, z1)) COMPUTELINE'(z0, z1, z2) -> c92(COMPUTELINE#1'(z0, z2, z1)) COMPUTELINE#1'(::(z0, z1), z2, z3) -> c93(COMPUTELINE#2'(z3, z2, z0, z1)) COMPUTELINE#2'(::(z0, z1), z2, z3, z4) -> c95(COMPUTELINE'(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2)) LINEMULT'(z0, z1, z2) -> c97(LINEMULT#1'(z1, z2, z0)) LINEMULT#1'(::(z0, z1), z2, z3) -> c98(LINEMULT#2'(z2, z3, z0, z1)) LINEMULT#2'(::(z0, z1), z2, z3, z4) -> c100(+''(*(z3, z2), z0), *''(z3, z2), LINEMULT'(z2, z4, z1)) LINEMULT#2'(nil, z0, z1, z2) -> c101(*''(z1, z0), LINEMULT'(z0, z2, nil)) MATRIXMULT'(z0, z1) -> c102(MATRIXMULT#1'(z0, z1)) MATRIXMULT#1'(::(z0, z1), z2) -> c103(COMPUTELINE'(z0, z2, nil), MATRIXMULT'(z1, z2)) *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) #ADD'(#pos(#s(#s(z0))), z1) -> c46(#ADD''(#pos(#s(z0)), z1), #ADD'(#pos(#s(z0)), z1)) #ADD''(#neg(#s(#s(z0))), z1) -> c68(#ADD''(#pos(#s(z0)), z1)) #ADD''(#pos(#s(#s(z0))), z1) -> c70(#ADD''(#pos(#s(z0)), z1)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD''(#pos(#s(z0)), z1)) #ADD'(#neg(#s(#s(z0))), z1) -> c42(#ADD'(#pos(#s(z0)), z1)) S tuples: MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) K tuples: *'''(z0, z1) -> c105(#MULT'(z0, z1)) +'''(z0, z1) -> c106(#ADD'(z0, z1)) COMPUTELINE#2''(::(z0, z1), z2, z3, z4) -> c110(COMPUTELINE''(z4, z1, lineMult(z3, z0, z2)), LINEMULT'(z3, z0, z2), LINEMULT''(z3, z0, z2)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c116(LINEMULT''(z2, z4, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c118(LINEMULT''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*''(z3, z2)) COMPUTELINE''(z0, z1, z2) -> c107(COMPUTELINE#1''(z0, z2, z1)) COMPUTELINE#1''(::(z0, z1), z2, z3) -> c108(COMPUTELINE#2''(z3, z2, z0, z1)) LINEMULT''(z0, z1, z2) -> c112(LINEMULT#1''(z1, z2, z0)) LINEMULT#1''(::(z0, z1), z2, z3) -> c113(LINEMULT#2''(z2, z3, z0, z1)) LINEMULT#2''(nil, z0, z1, z2) -> c117(*'''(z1, z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(+'''(*(z3, z2), z0)) LINEMULT#2''(::(z0, z1), z2, z3, z4) -> c42(*'''(z3, z2)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(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, #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, *'''_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, #ADD''_2 Compound Symbols: c51_1, c52_1, c54_1, c55_1, c57_3, c75_1, c76_1, c78_1, c79_1, c81_2, c90_1, c91_1, c92_1, c93_1, c95_2, c97_1, c98_1, c100_3, c101_2, c102_1, c103_2, c105_1, c106_1, c107_1, c108_1, c110_3, c112_1, c113_1, c116_1, c117_1, c118_1, c119_1, c120_1, c121_1, c46_2, c68_1, c70_1, c42_1 ---------------------------------------- (19) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: MATRIXMULT''(z0, z1) -> c119(MATRIXMULT#1''(z0, z1)) MATRIXMULT#1''(::(z0, z1), z2) -> c120(COMPUTELINE''(z0, z2, nil)) MATRIXMULT#1''(::(z0, z1), z2) -> c121(MATRIXMULT''(z1, z2)) Now S is empty ---------------------------------------- (20) BOUNDS(1, 1) ---------------------------------------- (21) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (22) 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^1). The TRS R consists of the following rules: *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 The (relative) TRS S consists of the following rules: #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 #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 Rewrite Strategy: INNERMOST ---------------------------------------- (23) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence MATRIXMULT(::(z01_2, z12_2), z1) ->^+ c38(c40(MATRIXMULT(z12_2, z1))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0]. The pumping substitution is [z12_2 / ::(z01_2, z12_2)]. The result substitution is [ ]. ---------------------------------------- (24) Complex Obligation (BEST) ---------------------------------------- (25) 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^1). The TRS R consists of the following rules: *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 The (relative) TRS S consists of the following rules: #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 #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 Rewrite Strategy: INNERMOST ---------------------------------------- (26) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (27) BOUNDS(n^1, INF) ---------------------------------------- (28) 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^1). The TRS R consists of the following rules: *'(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#2(::(z0, z1), z2, z3, z4) -> c35(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c36(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c37(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c38(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c39(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c40(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c41 The (relative) TRS S consists of the following rules: #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 #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 Rewrite Strategy: INNERMOST