WORST_CASE(Omega(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, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 2862 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 187 ms] (6) BEST (7) proven lower bound (8) LowerBoundPropagationProof [FINISHED, 0 ms] (9) BOUNDS(n^1, INF) (10) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) APPENDREVERSE(z0, z1) -> c26(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c27(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c28 BFTMULT(z0, z1) -> c29(BFTMULT'(tuple#2(::(z0, nil), nil), z1)) BFTMULT'(z0, z1) -> c30(BFTMULT'#1(bftMult'#2(z0), z1), BFTMULT'#2(z0)) BFTMULT'#1(tuple#2(z0, z1), z2) -> c31(BFTMULT'#3(z0, z2, z1)) BFTMULT'#2(tuple#2(z0, z1)) -> c32(DEQUEUE(z0, z1)) BFTMULT'#3(::(z0, z1), z2, z3) -> c33(BFTMULT'#4(z0, z2, z3)) BFTMULT'#3(nil, z0, z1) -> c34 BFTMULT'#4(leaf, z0, z1) -> c35(BFTMULT'(z1, z0)) BFTMULT'#4(node(z0, z1, z2), z3, z4) -> c36(BFTMULT'#5(enqueue(z2, enqueue(z1, z4)), z3, z0), ENQUEUE(z2, enqueue(z1, z4)), ENQUEUE(z1, z4)) BFTMULT'#5(z0, z1, z2) -> c37(BFTMULT'(z0, matrixMult(z1, z2)), MATRIXMULT(z1, z2)) COMPUTELINE(z0, z1, z2) -> c38(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c39(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#1(nil, z0, z1) -> c40 COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c41(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE#2(nil, z0, z1, z2) -> c42 DEQUEUE(z0, z1) -> c43(DEQUEUE#1(z0, z1)) DEQUEUE#1(::(z0, z1), z2) -> c44 DEQUEUE#1(nil, z0) -> c45(DEQUEUE#2(reverse(z0)), REVERSE(z0)) DEQUEUE#2(::(z0, z1)) -> c46 DEQUEUE#2(nil) -> c47 ENQUEUE(z0, z1) -> c48(ENQUEUE#1(z1, z0)) ENQUEUE#1(tuple#2(z0, z1), z2) -> c49 LINEMULT(z0, z1, z2) -> c50(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c51(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#1(nil, z0, z1) -> c52 LINEMULT#2(::(z0, z1), z2, z3, z4) -> c53(+'(*(z3, z2), z0), *'(z3, z2)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c54(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c55(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c56(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c57(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c58(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c59(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c60 REVERSE(z0) -> c61(APPENDREVERSE(z0, nil)) 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) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bftMult(z0, z1) -> bftMult'(tuple#2(::(z0, nil), nil), z1) bftMult'(z0, z1) -> bftMult'#1(bftMult'#2(z0), z1) bftMult'#1(tuple#2(z0, z1), z2) -> bftMult'#3(z0, z2, z1) bftMult'#2(tuple#2(z0, z1)) -> dequeue(z0, z1) bftMult'#3(::(z0, z1), z2, z3) -> bftMult'#4(z0, z2, z3) bftMult'#3(nil, z0, z1) -> z0 bftMult'#4(leaf, z0, z1) -> bftMult'(z1, z0) bftMult'#4(node(z0, z1, z2), z3, z4) -> bftMult'#5(enqueue(z2, enqueue(z1, z4)), z3, z0) bftMult'#5(z0, z1, z2) -> bftMult'(z0, matrixMult(z1, z2)) 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 dequeue(z0, z1) -> dequeue#1(z0, z1) dequeue#1(::(z0, z1), z2) -> tuple#2(::(z0, nil), tuple#2(z1, z2)) dequeue#1(nil, z0) -> dequeue#2(reverse(z0)) dequeue#2(::(z0, z1)) -> tuple#2(::(z0, nil), tuple#2(z1, nil)) dequeue#2(nil) -> tuple#2(nil, tuple#2(nil, nil)) enqueue(z0, z1) -> enqueue#1(z1, z0) enqueue#1(tuple#2(z0, z1), z2) -> tuple#2(z0, ::(z2, z1)) 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 reverse(z0) -> appendreverse(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, INF). The TRS R consists of the following rules: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) APPENDREVERSE(z0, z1) -> c26(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c27(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c28 BFTMULT(z0, z1) -> c29(BFTMULT'(tuple#2(::(z0, nil), nil), z1)) BFTMULT'(z0, z1) -> c30(BFTMULT'#1(bftMult'#2(z0), z1), BFTMULT'#2(z0)) BFTMULT'#1(tuple#2(z0, z1), z2) -> c31(BFTMULT'#3(z0, z2, z1)) BFTMULT'#2(tuple#2(z0, z1)) -> c32(DEQUEUE(z0, z1)) BFTMULT'#3(::(z0, z1), z2, z3) -> c33(BFTMULT'#4(z0, z2, z3)) BFTMULT'#3(nil, z0, z1) -> c34 BFTMULT'#4(leaf, z0, z1) -> c35(BFTMULT'(z1, z0)) BFTMULT'#4(node(z0, z1, z2), z3, z4) -> c36(BFTMULT'#5(enqueue(z2, enqueue(z1, z4)), z3, z0), ENQUEUE(z2, enqueue(z1, z4)), ENQUEUE(z1, z4)) BFTMULT'#5(z0, z1, z2) -> c37(BFTMULT'(z0, matrixMult(z1, z2)), MATRIXMULT(z1, z2)) COMPUTELINE(z0, z1, z2) -> c38(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c39(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#1(nil, z0, z1) -> c40 COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c41(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE#2(nil, z0, z1, z2) -> c42 DEQUEUE(z0, z1) -> c43(DEQUEUE#1(z0, z1)) DEQUEUE#1(::(z0, z1), z2) -> c44 DEQUEUE#1(nil, z0) -> c45(DEQUEUE#2(reverse(z0)), REVERSE(z0)) DEQUEUE#2(::(z0, z1)) -> c46 DEQUEUE#2(nil) -> c47 ENQUEUE(z0, z1) -> c48(ENQUEUE#1(z1, z0)) ENQUEUE#1(tuple#2(z0, z1), z2) -> c49 LINEMULT(z0, z1, z2) -> c50(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c51(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#1(nil, z0, z1) -> c52 LINEMULT#2(::(z0, z1), z2, z3, z4) -> c53(+'(*(z3, z2), z0), *'(z3, z2)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c54(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c55(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c56(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c57(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c58(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c59(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c60 REVERSE(z0) -> c61(APPENDREVERSE(z0, nil)) 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) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bftMult(z0, z1) -> bftMult'(tuple#2(::(z0, nil), nil), z1) bftMult'(z0, z1) -> bftMult'#1(bftMult'#2(z0), z1) bftMult'#1(tuple#2(z0, z1), z2) -> bftMult'#3(z0, z2, z1) bftMult'#2(tuple#2(z0, z1)) -> dequeue(z0, z1) bftMult'#3(::(z0, z1), z2, z3) -> bftMult'#4(z0, z2, z3) bftMult'#3(nil, z0, z1) -> z0 bftMult'#4(leaf, z0, z1) -> bftMult'(z1, z0) bftMult'#4(node(z0, z1, z2), z3, z4) -> bftMult'#5(enqueue(z2, enqueue(z1, z4)), z3, z0) bftMult'#5(z0, z1, z2) -> bftMult'(z0, matrixMult(z1, z2)) 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 dequeue(z0, z1) -> dequeue#1(z0, z1) dequeue#1(::(z0, z1), z2) -> tuple#2(::(z0, nil), tuple#2(z1, z2)) dequeue#1(nil, z0) -> dequeue#2(reverse(z0)) dequeue#2(::(z0, z1)) -> tuple#2(::(z0, nil), tuple#2(z1, nil)) dequeue#2(nil) -> tuple#2(nil, tuple#2(nil, nil)) enqueue(z0, z1) -> enqueue#1(z1, z0) enqueue#1(tuple#2(z0, z1), z2) -> tuple#2(z0, ::(z2, z1)) 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 reverse(z0) -> appendreverse(z0, nil) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (4) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) APPENDREVERSE(z0, z1) -> c26(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c27(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c28 BFTMULT(z0, z1) -> c29(BFTMULT'(tuple#2(::(z0, nil), nil), z1)) BFTMULT'(z0, z1) -> c30(BFTMULT'#1(bftMult'#2(z0), z1), BFTMULT'#2(z0)) BFTMULT'#1(tuple#2(z0, z1), z2) -> c31(BFTMULT'#3(z0, z2, z1)) BFTMULT'#2(tuple#2(z0, z1)) -> c32(DEQUEUE(z0, z1)) BFTMULT'#3(::(z0, z1), z2, z3) -> c33(BFTMULT'#4(z0, z2, z3)) BFTMULT'#3(nil, z0, z1) -> c34 BFTMULT'#4(leaf, z0, z1) -> c35(BFTMULT'(z1, z0)) BFTMULT'#4(node(z0, z1, z2), z3, z4) -> c36(BFTMULT'#5(enqueue(z2, enqueue(z1, z4)), z3, z0), ENQUEUE(z2, enqueue(z1, z4)), ENQUEUE(z1, z4)) BFTMULT'#5(z0, z1, z2) -> c37(BFTMULT'(z0, matrixMult(z1, z2)), MATRIXMULT(z1, z2)) COMPUTELINE(z0, z1, z2) -> c38(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c39(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#1(nil, z0, z1) -> c40 COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c41(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE#2(nil, z0, z1, z2) -> c42 DEQUEUE(z0, z1) -> c43(DEQUEUE#1(z0, z1)) DEQUEUE#1(::(z0, z1), z2) -> c44 DEQUEUE#1(nil, z0) -> c45(DEQUEUE#2(reverse(z0)), REVERSE(z0)) DEQUEUE#2(::(z0, z1)) -> c46 DEQUEUE#2(nil) -> c47 ENQUEUE(z0, z1) -> c48(ENQUEUE#1(z1, z0)) ENQUEUE#1(tuple#2(z0, z1), z2) -> c49 LINEMULT(z0, z1, z2) -> c50(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c51(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#1(nil, z0, z1) -> c52 LINEMULT#2(::(z0, z1), z2, z3, z4) -> c53(+'(*(z3, z2), z0), *'(z3, z2)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c54(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c55(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c56(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c57(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c58(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c59(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c60 REVERSE(z0) -> c61(APPENDREVERSE(z0, nil)) 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) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bftMult(z0, z1) -> bftMult'(tuple#2(::(z0, nil), nil), z1) bftMult'(z0, z1) -> bftMult'#1(bftMult'#2(z0), z1) bftMult'#1(tuple#2(z0, z1), z2) -> bftMult'#3(z0, z2, z1) bftMult'#2(tuple#2(z0, z1)) -> dequeue(z0, z1) bftMult'#3(::(z0, z1), z2, z3) -> bftMult'#4(z0, z2, z3) bftMult'#3(nil, z0, z1) -> z0 bftMult'#4(leaf, z0, z1) -> bftMult'(z1, z0) bftMult'#4(node(z0, z1, z2), z3, z4) -> bftMult'#5(enqueue(z2, enqueue(z1, z4)), z3, z0) bftMult'#5(z0, z1, z2) -> bftMult'(z0, matrixMult(z1, z2)) 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 dequeue(z0, z1) -> dequeue#1(z0, z1) dequeue#1(::(z0, z1), z2) -> tuple#2(::(z0, nil), tuple#2(z1, z2)) dequeue#1(nil, z0) -> dequeue#2(reverse(z0)) dequeue#2(::(z0, z1)) -> tuple#2(::(z0, nil), tuple#2(z1, nil)) dequeue#2(nil) -> tuple#2(nil, tuple#2(nil, nil)) enqueue(z0, z1) -> enqueue#1(z1, z0) enqueue#1(tuple#2(z0, z1), z2) -> tuple#2(z0, ::(z2, z1)) 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 reverse(z0) -> appendreverse(z0, nil) Rewrite Strategy: INNERMOST ---------------------------------------- (5) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence APPENDREVERSE(::(z01_2, z12_2), z1) ->^+ c26(c27(APPENDREVERSE(z12_2, ::(z01_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 [z1 / ::(z01_2, z1)]. ---------------------------------------- (6) Complex Obligation (BEST) ---------------------------------------- (7) 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, INF). The TRS R consists of the following rules: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) APPENDREVERSE(z0, z1) -> c26(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c27(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c28 BFTMULT(z0, z1) -> c29(BFTMULT'(tuple#2(::(z0, nil), nil), z1)) BFTMULT'(z0, z1) -> c30(BFTMULT'#1(bftMult'#2(z0), z1), BFTMULT'#2(z0)) BFTMULT'#1(tuple#2(z0, z1), z2) -> c31(BFTMULT'#3(z0, z2, z1)) BFTMULT'#2(tuple#2(z0, z1)) -> c32(DEQUEUE(z0, z1)) BFTMULT'#3(::(z0, z1), z2, z3) -> c33(BFTMULT'#4(z0, z2, z3)) BFTMULT'#3(nil, z0, z1) -> c34 BFTMULT'#4(leaf, z0, z1) -> c35(BFTMULT'(z1, z0)) BFTMULT'#4(node(z0, z1, z2), z3, z4) -> c36(BFTMULT'#5(enqueue(z2, enqueue(z1, z4)), z3, z0), ENQUEUE(z2, enqueue(z1, z4)), ENQUEUE(z1, z4)) BFTMULT'#5(z0, z1, z2) -> c37(BFTMULT'(z0, matrixMult(z1, z2)), MATRIXMULT(z1, z2)) COMPUTELINE(z0, z1, z2) -> c38(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c39(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#1(nil, z0, z1) -> c40 COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c41(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE#2(nil, z0, z1, z2) -> c42 DEQUEUE(z0, z1) -> c43(DEQUEUE#1(z0, z1)) DEQUEUE#1(::(z0, z1), z2) -> c44 DEQUEUE#1(nil, z0) -> c45(DEQUEUE#2(reverse(z0)), REVERSE(z0)) DEQUEUE#2(::(z0, z1)) -> c46 DEQUEUE#2(nil) -> c47 ENQUEUE(z0, z1) -> c48(ENQUEUE#1(z1, z0)) ENQUEUE#1(tuple#2(z0, z1), z2) -> c49 LINEMULT(z0, z1, z2) -> c50(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c51(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#1(nil, z0, z1) -> c52 LINEMULT#2(::(z0, z1), z2, z3, z4) -> c53(+'(*(z3, z2), z0), *'(z3, z2)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c54(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c55(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c56(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c57(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c58(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c59(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c60 REVERSE(z0) -> c61(APPENDREVERSE(z0, nil)) 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) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bftMult(z0, z1) -> bftMult'(tuple#2(::(z0, nil), nil), z1) bftMult'(z0, z1) -> bftMult'#1(bftMult'#2(z0), z1) bftMult'#1(tuple#2(z0, z1), z2) -> bftMult'#3(z0, z2, z1) bftMult'#2(tuple#2(z0, z1)) -> dequeue(z0, z1) bftMult'#3(::(z0, z1), z2, z3) -> bftMult'#4(z0, z2, z3) bftMult'#3(nil, z0, z1) -> z0 bftMult'#4(leaf, z0, z1) -> bftMult'(z1, z0) bftMult'#4(node(z0, z1, z2), z3, z4) -> bftMult'#5(enqueue(z2, enqueue(z1, z4)), z3, z0) bftMult'#5(z0, z1, z2) -> bftMult'(z0, matrixMult(z1, z2)) 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 dequeue(z0, z1) -> dequeue#1(z0, z1) dequeue#1(::(z0, z1), z2) -> tuple#2(::(z0, nil), tuple#2(z1, z2)) dequeue#1(nil, z0) -> dequeue#2(reverse(z0)) dequeue#2(::(z0, z1)) -> tuple#2(::(z0, nil), tuple#2(z1, nil)) dequeue#2(nil) -> tuple#2(nil, tuple#2(nil, nil)) enqueue(z0, z1) -> enqueue#1(z1, z0) enqueue#1(tuple#2(z0, z1), z2) -> tuple#2(z0, ::(z2, z1)) 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 reverse(z0) -> appendreverse(z0, nil) Rewrite Strategy: INNERMOST ---------------------------------------- (8) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (9) BOUNDS(n^1, INF) ---------------------------------------- (10) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: *'(z0, z1) -> c24(#MULT(z0, z1)) +'(z0, z1) -> c25(#ADD(z0, z1)) APPENDREVERSE(z0, z1) -> c26(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c27(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c28 BFTMULT(z0, z1) -> c29(BFTMULT'(tuple#2(::(z0, nil), nil), z1)) BFTMULT'(z0, z1) -> c30(BFTMULT'#1(bftMult'#2(z0), z1), BFTMULT'#2(z0)) BFTMULT'#1(tuple#2(z0, z1), z2) -> c31(BFTMULT'#3(z0, z2, z1)) BFTMULT'#2(tuple#2(z0, z1)) -> c32(DEQUEUE(z0, z1)) BFTMULT'#3(::(z0, z1), z2, z3) -> c33(BFTMULT'#4(z0, z2, z3)) BFTMULT'#3(nil, z0, z1) -> c34 BFTMULT'#4(leaf, z0, z1) -> c35(BFTMULT'(z1, z0)) BFTMULT'#4(node(z0, z1, z2), z3, z4) -> c36(BFTMULT'#5(enqueue(z2, enqueue(z1, z4)), z3, z0), ENQUEUE(z2, enqueue(z1, z4)), ENQUEUE(z1, z4)) BFTMULT'#5(z0, z1, z2) -> c37(BFTMULT'(z0, matrixMult(z1, z2)), MATRIXMULT(z1, z2)) COMPUTELINE(z0, z1, z2) -> c38(COMPUTELINE#1(z0, z2, z1)) COMPUTELINE#1(::(z0, z1), z2, z3) -> c39(COMPUTELINE#2(z3, z2, z0, z1)) COMPUTELINE#1(nil, z0, z1) -> c40 COMPUTELINE#2(::(z0, z1), z2, z3, z4) -> c41(COMPUTELINE(z4, z1, lineMult(z3, z0, z2)), LINEMULT(z3, z0, z2)) COMPUTELINE#2(nil, z0, z1, z2) -> c42 DEQUEUE(z0, z1) -> c43(DEQUEUE#1(z0, z1)) DEQUEUE#1(::(z0, z1), z2) -> c44 DEQUEUE#1(nil, z0) -> c45(DEQUEUE#2(reverse(z0)), REVERSE(z0)) DEQUEUE#2(::(z0, z1)) -> c46 DEQUEUE#2(nil) -> c47 ENQUEUE(z0, z1) -> c48(ENQUEUE#1(z1, z0)) ENQUEUE#1(tuple#2(z0, z1), z2) -> c49 LINEMULT(z0, z1, z2) -> c50(LINEMULT#1(z1, z2, z0)) LINEMULT#1(::(z0, z1), z2, z3) -> c51(LINEMULT#2(z2, z3, z0, z1)) LINEMULT#1(nil, z0, z1) -> c52 LINEMULT#2(::(z0, z1), z2, z3, z4) -> c53(+'(*(z3, z2), z0), *'(z3, z2)) LINEMULT#2(::(z0, z1), z2, z3, z4) -> c54(LINEMULT(z2, z4, z1)) LINEMULT#2(nil, z0, z1, z2) -> c55(*'(z1, z0)) LINEMULT#2(nil, z0, z1, z2) -> c56(LINEMULT(z0, z2, nil)) MATRIXMULT(z0, z1) -> c57(MATRIXMULT#1(z0, z1)) MATRIXMULT#1(::(z0, z1), z2) -> c58(COMPUTELINE(z0, z2, nil)) MATRIXMULT#1(::(z0, z1), z2) -> c59(MATRIXMULT(z1, z2)) MATRIXMULT#1(nil, z0) -> c60 REVERSE(z0) -> c61(APPENDREVERSE(z0, nil)) 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) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bftMult(z0, z1) -> bftMult'(tuple#2(::(z0, nil), nil), z1) bftMult'(z0, z1) -> bftMult'#1(bftMult'#2(z0), z1) bftMult'#1(tuple#2(z0, z1), z2) -> bftMult'#3(z0, z2, z1) bftMult'#2(tuple#2(z0, z1)) -> dequeue(z0, z1) bftMult'#3(::(z0, z1), z2, z3) -> bftMult'#4(z0, z2, z3) bftMult'#3(nil, z0, z1) -> z0 bftMult'#4(leaf, z0, z1) -> bftMult'(z1, z0) bftMult'#4(node(z0, z1, z2), z3, z4) -> bftMult'#5(enqueue(z2, enqueue(z1, z4)), z3, z0) bftMult'#5(z0, z1, z2) -> bftMult'(z0, matrixMult(z1, z2)) 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 dequeue(z0, z1) -> dequeue#1(z0, z1) dequeue#1(::(z0, z1), z2) -> tuple#2(::(z0, nil), tuple#2(z1, z2)) dequeue#1(nil, z0) -> dequeue#2(reverse(z0)) dequeue#2(::(z0, z1)) -> tuple#2(::(z0, nil), tuple#2(z1, nil)) dequeue#2(nil) -> tuple#2(nil, tuple#2(nil, nil)) enqueue(z0, z1) -> enqueue#1(z1, z0) enqueue#1(tuple#2(z0, z1), z2) -> tuple#2(z0, ::(z2, z1)) 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 reverse(z0) -> appendreverse(z0, nil) Rewrite Strategy: INNERMOST