WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox2/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), 1819 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 756 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: #ABS(#0) -> c24 #ABS(#neg(z0)) -> c25 #ABS(#pos(z0)) -> c26 #ABS(#s(z0)) -> c27 *'(z0, z1) -> c28(#MULT(z0, z1)) +'(z0, z1) -> c29(#ADD(z0, z1)) ATTACH(z0, z1) -> c30(ATTACH#1(z0, z1)) ATTACH#1(::(z0, z1), z2) -> c31(ATTACH#2(z2, z0, z1)) ATTACH#1(nil, z0) -> c32 ATTACH#2(::(z0, z1), z2, z3) -> c33(ATTACH(z3, z1)) ATTACH#2(nil, z0, z1) -> c34 LINEMULT(z0, z1) -> c35(LINEMULT#1(z1, z0)) LINEMULT#1(::(z0, z1), z2) -> c36(MULT(z2, z0)) LINEMULT#1(::(z0, z1), z2) -> c37(LINEMULT(z2, z1)) LINEMULT#1(nil, z0) -> c38 M1(z0) -> c39(#ABS(#pos(#s(#0)))) M1(z0) -> c40(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c41(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c42(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c43(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c44(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c45(#ABS(#pos(#s(#0)))) M2(z0) -> c46(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c47(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c48(#ABS(#pos(#s(#s(#s(#0)))))) M2(z0) -> c49(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c50(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c51(#ABS(#pos(#s(#0)))) M3(z0) -> c52(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c53(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c54(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c55(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c56(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c57(#ABS(#pos(#s(#s(#s(#s(#0))))))) M3(z0) -> c58(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M4(z0) -> c59(#ABS(#pos(#s(#0)))) M4(z0) -> c60(#ABS(#pos(#s(#s(#0))))) M4(z0) -> c61(#ABS(#pos(#s(#s(#s(#0)))))) M4(z0) -> c62(#ABS(#pos(#s(#s(#s(#s(#0))))))) MAKEBASE(z0) -> c63(MAKEBASE#1(z0)) MAKEBASE#1(::(z0, z1)) -> c64(MKBASE(z0)) MAKEBASE#1(nil) -> c65 MATRIXMULT(z0, z1) -> c66(MATRIXMULT'(z0, transAcc(z1, makeBase(z1))), TRANSACC(z1, makeBase(z1)), MAKEBASE(z1)) MATRIXMULT'(z0, z1) -> c67(MATRIXMULT'#1(z0, z1)) MATRIXMULT'#1(::(z0, z1), z2) -> c68(LINEMULT(z0, z2)) MATRIXMULT'#1(::(z0, z1), z2) -> c69(MATRIXMULT'(z1, z2)) MATRIXMULT'#1(nil, z0) -> c70 MATRIXMULT3(z0, z1, z2) -> c71(MATRIXMULT(matrixMult(z0, z1), z2), MATRIXMULT(z0, z1)) MATRIXMULTLIST(z0, z1) -> c72(MATRIXMULTLIST#1(z1, z0)) MATRIXMULTLIST#1(::(z0, z1), z2) -> c73(MATRIXMULTLIST(matrixMult(z2, z0), z1), MATRIXMULT(z2, z0)) MATRIXMULTLIST#1(nil, z0) -> c74 MATRIXMULTOLD(z0, z1) -> c75(MATRIXMULT'(z0, transpose(z1)), TRANSPOSE(z1)) MKBASE(z0) -> c76(MKBASE#1(z0)) MKBASE#1(::(z0, z1)) -> c77(MKBASE(z1)) MKBASE#1(nil) -> c78 MULT(z0, z1) -> c79(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c80(MULT#2(z2, z0, z1)) MULT#1(nil, z0) -> c81(#ABS(#0)) MULT#2(::(z0, z1), z2, z3) -> c82(+'(*(z2, z0), mult(z3, z1)), *'(z2, z0)) MULT#2(::(z0, z1), z2, z3) -> c83(+'(*(z2, z0), mult(z3, z1)), MULT(z3, z1)) MULT#2(nil, z0, z1) -> c84(#ABS(#0)) SPLIT(z0) -> c85(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c86(SPLIT#2(z0, z1)) SPLIT#1(nil) -> c87 SPLIT#2(::(z0, z1), z2) -> c88(SPLIT#3(split(z2), z0, z1), SPLIT(z2)) SPLIT#2(nil, z0) -> c89 SPLIT#3(tuple#2(z0, z1), z2, z3) -> c90 TRANSACC(z0, z1) -> c91(TRANSACC#1(z0, z1)) TRANSACC#1(::(z0, z1), z2) -> c92(ATTACH(z0, transAcc(z1, z2)), TRANSACC(z1, z2)) TRANSACC#1(nil, z0) -> c93 TRANSPOSE(z0) -> c94(TRANSPOSE#1(z0, z0)) TRANSPOSE#1(::(z0, z1), z2) -> c95(TRANSPOSE#2(split(z2)), SPLIT(z2)) TRANSPOSE#1(nil, z0) -> c96 TRANSPOSE#2(tuple#2(z0, z1)) -> c97(TRANSPOSE#3(z1, z0)) TRANSPOSE#3(::(z0, z1), z2) -> c98(TRANSPOSE(::(z0, z1))) TRANSPOSE#3(nil, z0) -> c99 TRANSPOSE'(z0) -> c100(TRANSACC(z0, makeBase(z0)), MAKEBASE(z0)) 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))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) attach(z0, z1) -> attach#1(z0, z1) attach#1(::(z0, z1), z2) -> attach#2(z2, z0, z1) attach#1(nil, z0) -> nil attach#2(::(z0, z1), z2, z3) -> ::(::(z2, z0), attach(z3, z1)) attach#2(nil, z0, z1) -> nil lineMult(z0, z1) -> lineMult#1(z1, z0) lineMult#1(::(z0, z1), z2) -> ::(mult(z2, z0), lineMult(z2, z1)) lineMult#1(nil, z0) -> nil m1(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil)) m2(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil))) m3(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil)) m4(z0) -> ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil)))) makeBase(z0) -> makeBase#1(z0) makeBase#1(::(z0, z1)) -> mkBase(z0) makeBase#1(nil) -> nil matrixMult(z0, z1) -> matrixMult'(z0, transAcc(z1, makeBase(z1))) matrixMult'(z0, z1) -> matrixMult'#1(z0, z1) matrixMult'#1(::(z0, z1), z2) -> ::(lineMult(z0, z2), matrixMult'(z1, z2)) matrixMult'#1(nil, z0) -> nil matrixMult3(z0, z1, z2) -> matrixMult(matrixMult(z0, z1), z2) matrixMultList(z0, z1) -> matrixMultList#1(z1, z0) matrixMultList#1(::(z0, z1), z2) -> matrixMultList(matrixMult(z2, z0), z1) matrixMultList#1(nil, z0) -> z0 matrixMultOld(z0, z1) -> matrixMult'(z0, transpose(z1)) mkBase(z0) -> mkBase#1(z0) mkBase#1(::(z0, z1)) -> ::(nil, mkBase(z1)) mkBase#1(nil) -> nil mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(z2, z0, z1) mult#1(nil, z0) -> #abs(#0) mult#2(::(z0, z1), z2, z3) -> +(*(z2, z0), mult(z3, z1)) mult#2(nil, z0, z1) -> #abs(#0) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> split#2(z0, z1) split#1(nil) -> tuple#2(nil, nil) split#2(::(z0, z1), z2) -> split#3(split(z2), z0, z1) split#2(nil, z0) -> tuple#2(nil, nil) split#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1)) transAcc(z0, z1) -> transAcc#1(z0, z1) transAcc#1(::(z0, z1), z2) -> attach(z0, transAcc(z1, z2)) transAcc#1(nil, z0) -> z0 transpose(z0) -> transpose#1(z0, z0) transpose#1(::(z0, z1), z2) -> transpose#2(split(z2)) transpose#1(nil, z0) -> nil transpose#2(tuple#2(z0, z1)) -> transpose#3(z1, z0) transpose#3(::(z0, z1), z2) -> ::(z2, transpose(::(z0, z1))) transpose#3(nil, z0) -> nil transpose'(z0) -> transAcc(z0, makeBase(z0)) 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: #ABS(#0) -> c24 #ABS(#neg(z0)) -> c25 #ABS(#pos(z0)) -> c26 #ABS(#s(z0)) -> c27 *'(z0, z1) -> c28(#MULT(z0, z1)) +'(z0, z1) -> c29(#ADD(z0, z1)) ATTACH(z0, z1) -> c30(ATTACH#1(z0, z1)) ATTACH#1(::(z0, z1), z2) -> c31(ATTACH#2(z2, z0, z1)) ATTACH#1(nil, z0) -> c32 ATTACH#2(::(z0, z1), z2, z3) -> c33(ATTACH(z3, z1)) ATTACH#2(nil, z0, z1) -> c34 LINEMULT(z0, z1) -> c35(LINEMULT#1(z1, z0)) LINEMULT#1(::(z0, z1), z2) -> c36(MULT(z2, z0)) LINEMULT#1(::(z0, z1), z2) -> c37(LINEMULT(z2, z1)) LINEMULT#1(nil, z0) -> c38 M1(z0) -> c39(#ABS(#pos(#s(#0)))) M1(z0) -> c40(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c41(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c42(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c43(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c44(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c45(#ABS(#pos(#s(#0)))) M2(z0) -> c46(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c47(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c48(#ABS(#pos(#s(#s(#s(#0)))))) M2(z0) -> c49(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c50(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c51(#ABS(#pos(#s(#0)))) M3(z0) -> c52(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c53(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c54(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c55(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c56(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c57(#ABS(#pos(#s(#s(#s(#s(#0))))))) M3(z0) -> c58(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M4(z0) -> c59(#ABS(#pos(#s(#0)))) M4(z0) -> c60(#ABS(#pos(#s(#s(#0))))) M4(z0) -> c61(#ABS(#pos(#s(#s(#s(#0)))))) M4(z0) -> c62(#ABS(#pos(#s(#s(#s(#s(#0))))))) MAKEBASE(z0) -> c63(MAKEBASE#1(z0)) MAKEBASE#1(::(z0, z1)) -> c64(MKBASE(z0)) MAKEBASE#1(nil) -> c65 MATRIXMULT(z0, z1) -> c66(MATRIXMULT'(z0, transAcc(z1, makeBase(z1))), TRANSACC(z1, makeBase(z1)), MAKEBASE(z1)) MATRIXMULT'(z0, z1) -> c67(MATRIXMULT'#1(z0, z1)) MATRIXMULT'#1(::(z0, z1), z2) -> c68(LINEMULT(z0, z2)) MATRIXMULT'#1(::(z0, z1), z2) -> c69(MATRIXMULT'(z1, z2)) MATRIXMULT'#1(nil, z0) -> c70 MATRIXMULT3(z0, z1, z2) -> c71(MATRIXMULT(matrixMult(z0, z1), z2), MATRIXMULT(z0, z1)) MATRIXMULTLIST(z0, z1) -> c72(MATRIXMULTLIST#1(z1, z0)) MATRIXMULTLIST#1(::(z0, z1), z2) -> c73(MATRIXMULTLIST(matrixMult(z2, z0), z1), MATRIXMULT(z2, z0)) MATRIXMULTLIST#1(nil, z0) -> c74 MATRIXMULTOLD(z0, z1) -> c75(MATRIXMULT'(z0, transpose(z1)), TRANSPOSE(z1)) MKBASE(z0) -> c76(MKBASE#1(z0)) MKBASE#1(::(z0, z1)) -> c77(MKBASE(z1)) MKBASE#1(nil) -> c78 MULT(z0, z1) -> c79(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c80(MULT#2(z2, z0, z1)) MULT#1(nil, z0) -> c81(#ABS(#0)) MULT#2(::(z0, z1), z2, z3) -> c82(+'(*(z2, z0), mult(z3, z1)), *'(z2, z0)) MULT#2(::(z0, z1), z2, z3) -> c83(+'(*(z2, z0), mult(z3, z1)), MULT(z3, z1)) MULT#2(nil, z0, z1) -> c84(#ABS(#0)) SPLIT(z0) -> c85(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c86(SPLIT#2(z0, z1)) SPLIT#1(nil) -> c87 SPLIT#2(::(z0, z1), z2) -> c88(SPLIT#3(split(z2), z0, z1), SPLIT(z2)) SPLIT#2(nil, z0) -> c89 SPLIT#3(tuple#2(z0, z1), z2, z3) -> c90 TRANSACC(z0, z1) -> c91(TRANSACC#1(z0, z1)) TRANSACC#1(::(z0, z1), z2) -> c92(ATTACH(z0, transAcc(z1, z2)), TRANSACC(z1, z2)) TRANSACC#1(nil, z0) -> c93 TRANSPOSE(z0) -> c94(TRANSPOSE#1(z0, z0)) TRANSPOSE#1(::(z0, z1), z2) -> c95(TRANSPOSE#2(split(z2)), SPLIT(z2)) TRANSPOSE#1(nil, z0) -> c96 TRANSPOSE#2(tuple#2(z0, z1)) -> c97(TRANSPOSE#3(z1, z0)) TRANSPOSE#3(::(z0, z1), z2) -> c98(TRANSPOSE(::(z0, z1))) TRANSPOSE#3(nil, z0) -> c99 TRANSPOSE'(z0) -> c100(TRANSACC(z0, makeBase(z0)), MAKEBASE(z0)) 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))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) attach(z0, z1) -> attach#1(z0, z1) attach#1(::(z0, z1), z2) -> attach#2(z2, z0, z1) attach#1(nil, z0) -> nil attach#2(::(z0, z1), z2, z3) -> ::(::(z2, z0), attach(z3, z1)) attach#2(nil, z0, z1) -> nil lineMult(z0, z1) -> lineMult#1(z1, z0) lineMult#1(::(z0, z1), z2) -> ::(mult(z2, z0), lineMult(z2, z1)) lineMult#1(nil, z0) -> nil m1(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil)) m2(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil))) m3(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil)) m4(z0) -> ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil)))) makeBase(z0) -> makeBase#1(z0) makeBase#1(::(z0, z1)) -> mkBase(z0) makeBase#1(nil) -> nil matrixMult(z0, z1) -> matrixMult'(z0, transAcc(z1, makeBase(z1))) matrixMult'(z0, z1) -> matrixMult'#1(z0, z1) matrixMult'#1(::(z0, z1), z2) -> ::(lineMult(z0, z2), matrixMult'(z1, z2)) matrixMult'#1(nil, z0) -> nil matrixMult3(z0, z1, z2) -> matrixMult(matrixMult(z0, z1), z2) matrixMultList(z0, z1) -> matrixMultList#1(z1, z0) matrixMultList#1(::(z0, z1), z2) -> matrixMultList(matrixMult(z2, z0), z1) matrixMultList#1(nil, z0) -> z0 matrixMultOld(z0, z1) -> matrixMult'(z0, transpose(z1)) mkBase(z0) -> mkBase#1(z0) mkBase#1(::(z0, z1)) -> ::(nil, mkBase(z1)) mkBase#1(nil) -> nil mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(z2, z0, z1) mult#1(nil, z0) -> #abs(#0) mult#2(::(z0, z1), z2, z3) -> +(*(z2, z0), mult(z3, z1)) mult#2(nil, z0, z1) -> #abs(#0) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> split#2(z0, z1) split#1(nil) -> tuple#2(nil, nil) split#2(::(z0, z1), z2) -> split#3(split(z2), z0, z1) split#2(nil, z0) -> tuple#2(nil, nil) split#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1)) transAcc(z0, z1) -> transAcc#1(z0, z1) transAcc#1(::(z0, z1), z2) -> attach(z0, transAcc(z1, z2)) transAcc#1(nil, z0) -> z0 transpose(z0) -> transpose#1(z0, z0) transpose#1(::(z0, z1), z2) -> transpose#2(split(z2)) transpose#1(nil, z0) -> nil transpose#2(tuple#2(z0, z1)) -> transpose#3(z1, z0) transpose#3(::(z0, z1), z2) -> ::(z2, transpose(::(z0, z1))) transpose#3(nil, z0) -> nil transpose'(z0) -> transAcc(z0, makeBase(z0)) 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: #ABS(#0) -> c24 #ABS(#neg(z0)) -> c25 #ABS(#pos(z0)) -> c26 #ABS(#s(z0)) -> c27 *'(z0, z1) -> c28(#MULT(z0, z1)) +'(z0, z1) -> c29(#ADD(z0, z1)) ATTACH(z0, z1) -> c30(ATTACH#1(z0, z1)) ATTACH#1(::(z0, z1), z2) -> c31(ATTACH#2(z2, z0, z1)) ATTACH#1(nil, z0) -> c32 ATTACH#2(::(z0, z1), z2, z3) -> c33(ATTACH(z3, z1)) ATTACH#2(nil, z0, z1) -> c34 LINEMULT(z0, z1) -> c35(LINEMULT#1(z1, z0)) LINEMULT#1(::(z0, z1), z2) -> c36(MULT(z2, z0)) LINEMULT#1(::(z0, z1), z2) -> c37(LINEMULT(z2, z1)) LINEMULT#1(nil, z0) -> c38 M1(z0) -> c39(#ABS(#pos(#s(#0)))) M1(z0) -> c40(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c41(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c42(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c43(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c44(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c45(#ABS(#pos(#s(#0)))) M2(z0) -> c46(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c47(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c48(#ABS(#pos(#s(#s(#s(#0)))))) M2(z0) -> c49(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c50(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c51(#ABS(#pos(#s(#0)))) M3(z0) -> c52(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c53(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c54(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c55(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c56(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c57(#ABS(#pos(#s(#s(#s(#s(#0))))))) M3(z0) -> c58(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M4(z0) -> c59(#ABS(#pos(#s(#0)))) M4(z0) -> c60(#ABS(#pos(#s(#s(#0))))) M4(z0) -> c61(#ABS(#pos(#s(#s(#s(#0)))))) M4(z0) -> c62(#ABS(#pos(#s(#s(#s(#s(#0))))))) MAKEBASE(z0) -> c63(MAKEBASE#1(z0)) MAKEBASE#1(::(z0, z1)) -> c64(MKBASE(z0)) MAKEBASE#1(nil) -> c65 MATRIXMULT(z0, z1) -> c66(MATRIXMULT'(z0, transAcc(z1, makeBase(z1))), TRANSACC(z1, makeBase(z1)), MAKEBASE(z1)) MATRIXMULT'(z0, z1) -> c67(MATRIXMULT'#1(z0, z1)) MATRIXMULT'#1(::(z0, z1), z2) -> c68(LINEMULT(z0, z2)) MATRIXMULT'#1(::(z0, z1), z2) -> c69(MATRIXMULT'(z1, z2)) MATRIXMULT'#1(nil, z0) -> c70 MATRIXMULT3(z0, z1, z2) -> c71(MATRIXMULT(matrixMult(z0, z1), z2), MATRIXMULT(z0, z1)) MATRIXMULTLIST(z0, z1) -> c72(MATRIXMULTLIST#1(z1, z0)) MATRIXMULTLIST#1(::(z0, z1), z2) -> c73(MATRIXMULTLIST(matrixMult(z2, z0), z1), MATRIXMULT(z2, z0)) MATRIXMULTLIST#1(nil, z0) -> c74 MATRIXMULTOLD(z0, z1) -> c75(MATRIXMULT'(z0, transpose(z1)), TRANSPOSE(z1)) MKBASE(z0) -> c76(MKBASE#1(z0)) MKBASE#1(::(z0, z1)) -> c77(MKBASE(z1)) MKBASE#1(nil) -> c78 MULT(z0, z1) -> c79(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c80(MULT#2(z2, z0, z1)) MULT#1(nil, z0) -> c81(#ABS(#0)) MULT#2(::(z0, z1), z2, z3) -> c82(+'(*(z2, z0), mult(z3, z1)), *'(z2, z0)) MULT#2(::(z0, z1), z2, z3) -> c83(+'(*(z2, z0), mult(z3, z1)), MULT(z3, z1)) MULT#2(nil, z0, z1) -> c84(#ABS(#0)) SPLIT(z0) -> c85(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c86(SPLIT#2(z0, z1)) SPLIT#1(nil) -> c87 SPLIT#2(::(z0, z1), z2) -> c88(SPLIT#3(split(z2), z0, z1), SPLIT(z2)) SPLIT#2(nil, z0) -> c89 SPLIT#3(tuple#2(z0, z1), z2, z3) -> c90 TRANSACC(z0, z1) -> c91(TRANSACC#1(z0, z1)) TRANSACC#1(::(z0, z1), z2) -> c92(ATTACH(z0, transAcc(z1, z2)), TRANSACC(z1, z2)) TRANSACC#1(nil, z0) -> c93 TRANSPOSE(z0) -> c94(TRANSPOSE#1(z0, z0)) TRANSPOSE#1(::(z0, z1), z2) -> c95(TRANSPOSE#2(split(z2)), SPLIT(z2)) TRANSPOSE#1(nil, z0) -> c96 TRANSPOSE#2(tuple#2(z0, z1)) -> c97(TRANSPOSE#3(z1, z0)) TRANSPOSE#3(::(z0, z1), z2) -> c98(TRANSPOSE(::(z0, z1))) TRANSPOSE#3(nil, z0) -> c99 TRANSPOSE'(z0) -> c100(TRANSACC(z0, makeBase(z0)), MAKEBASE(z0)) 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))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) attach(z0, z1) -> attach#1(z0, z1) attach#1(::(z0, z1), z2) -> attach#2(z2, z0, z1) attach#1(nil, z0) -> nil attach#2(::(z0, z1), z2, z3) -> ::(::(z2, z0), attach(z3, z1)) attach#2(nil, z0, z1) -> nil lineMult(z0, z1) -> lineMult#1(z1, z0) lineMult#1(::(z0, z1), z2) -> ::(mult(z2, z0), lineMult(z2, z1)) lineMult#1(nil, z0) -> nil m1(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil)) m2(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil))) m3(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil)) m4(z0) -> ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil)))) makeBase(z0) -> makeBase#1(z0) makeBase#1(::(z0, z1)) -> mkBase(z0) makeBase#1(nil) -> nil matrixMult(z0, z1) -> matrixMult'(z0, transAcc(z1, makeBase(z1))) matrixMult'(z0, z1) -> matrixMult'#1(z0, z1) matrixMult'#1(::(z0, z1), z2) -> ::(lineMult(z0, z2), matrixMult'(z1, z2)) matrixMult'#1(nil, z0) -> nil matrixMult3(z0, z1, z2) -> matrixMult(matrixMult(z0, z1), z2) matrixMultList(z0, z1) -> matrixMultList#1(z1, z0) matrixMultList#1(::(z0, z1), z2) -> matrixMultList(matrixMult(z2, z0), z1) matrixMultList#1(nil, z0) -> z0 matrixMultOld(z0, z1) -> matrixMult'(z0, transpose(z1)) mkBase(z0) -> mkBase#1(z0) mkBase#1(::(z0, z1)) -> ::(nil, mkBase(z1)) mkBase#1(nil) -> nil mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(z2, z0, z1) mult#1(nil, z0) -> #abs(#0) mult#2(::(z0, z1), z2, z3) -> +(*(z2, z0), mult(z3, z1)) mult#2(nil, z0, z1) -> #abs(#0) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> split#2(z0, z1) split#1(nil) -> tuple#2(nil, nil) split#2(::(z0, z1), z2) -> split#3(split(z2), z0, z1) split#2(nil, z0) -> tuple#2(nil, nil) split#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1)) transAcc(z0, z1) -> transAcc#1(z0, z1) transAcc#1(::(z0, z1), z2) -> attach(z0, transAcc(z1, z2)) transAcc#1(nil, z0) -> z0 transpose(z0) -> transpose#1(z0, z0) transpose#1(::(z0, z1), z2) -> transpose#2(split(z2)) transpose#1(nil, z0) -> nil transpose#2(tuple#2(z0, z1)) -> transpose#3(z1, z0) transpose#3(::(z0, z1), z2) -> ::(z2, transpose(::(z0, z1))) transpose#3(nil, z0) -> nil transpose'(z0) -> transAcc(z0, makeBase(z0)) 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 MKBASE#1(::(z0, z1)) ->^+ c77(c76(MKBASE#1(z1))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0]. The pumping substitution is [z1 / ::(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (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: #ABS(#0) -> c24 #ABS(#neg(z0)) -> c25 #ABS(#pos(z0)) -> c26 #ABS(#s(z0)) -> c27 *'(z0, z1) -> c28(#MULT(z0, z1)) +'(z0, z1) -> c29(#ADD(z0, z1)) ATTACH(z0, z1) -> c30(ATTACH#1(z0, z1)) ATTACH#1(::(z0, z1), z2) -> c31(ATTACH#2(z2, z0, z1)) ATTACH#1(nil, z0) -> c32 ATTACH#2(::(z0, z1), z2, z3) -> c33(ATTACH(z3, z1)) ATTACH#2(nil, z0, z1) -> c34 LINEMULT(z0, z1) -> c35(LINEMULT#1(z1, z0)) LINEMULT#1(::(z0, z1), z2) -> c36(MULT(z2, z0)) LINEMULT#1(::(z0, z1), z2) -> c37(LINEMULT(z2, z1)) LINEMULT#1(nil, z0) -> c38 M1(z0) -> c39(#ABS(#pos(#s(#0)))) M1(z0) -> c40(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c41(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c42(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c43(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c44(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c45(#ABS(#pos(#s(#0)))) M2(z0) -> c46(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c47(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c48(#ABS(#pos(#s(#s(#s(#0)))))) M2(z0) -> c49(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c50(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c51(#ABS(#pos(#s(#0)))) M3(z0) -> c52(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c53(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c54(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c55(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c56(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c57(#ABS(#pos(#s(#s(#s(#s(#0))))))) M3(z0) -> c58(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M4(z0) -> c59(#ABS(#pos(#s(#0)))) M4(z0) -> c60(#ABS(#pos(#s(#s(#0))))) M4(z0) -> c61(#ABS(#pos(#s(#s(#s(#0)))))) M4(z0) -> c62(#ABS(#pos(#s(#s(#s(#s(#0))))))) MAKEBASE(z0) -> c63(MAKEBASE#1(z0)) MAKEBASE#1(::(z0, z1)) -> c64(MKBASE(z0)) MAKEBASE#1(nil) -> c65 MATRIXMULT(z0, z1) -> c66(MATRIXMULT'(z0, transAcc(z1, makeBase(z1))), TRANSACC(z1, makeBase(z1)), MAKEBASE(z1)) MATRIXMULT'(z0, z1) -> c67(MATRIXMULT'#1(z0, z1)) MATRIXMULT'#1(::(z0, z1), z2) -> c68(LINEMULT(z0, z2)) MATRIXMULT'#1(::(z0, z1), z2) -> c69(MATRIXMULT'(z1, z2)) MATRIXMULT'#1(nil, z0) -> c70 MATRIXMULT3(z0, z1, z2) -> c71(MATRIXMULT(matrixMult(z0, z1), z2), MATRIXMULT(z0, z1)) MATRIXMULTLIST(z0, z1) -> c72(MATRIXMULTLIST#1(z1, z0)) MATRIXMULTLIST#1(::(z0, z1), z2) -> c73(MATRIXMULTLIST(matrixMult(z2, z0), z1), MATRIXMULT(z2, z0)) MATRIXMULTLIST#1(nil, z0) -> c74 MATRIXMULTOLD(z0, z1) -> c75(MATRIXMULT'(z0, transpose(z1)), TRANSPOSE(z1)) MKBASE(z0) -> c76(MKBASE#1(z0)) MKBASE#1(::(z0, z1)) -> c77(MKBASE(z1)) MKBASE#1(nil) -> c78 MULT(z0, z1) -> c79(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c80(MULT#2(z2, z0, z1)) MULT#1(nil, z0) -> c81(#ABS(#0)) MULT#2(::(z0, z1), z2, z3) -> c82(+'(*(z2, z0), mult(z3, z1)), *'(z2, z0)) MULT#2(::(z0, z1), z2, z3) -> c83(+'(*(z2, z0), mult(z3, z1)), MULT(z3, z1)) MULT#2(nil, z0, z1) -> c84(#ABS(#0)) SPLIT(z0) -> c85(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c86(SPLIT#2(z0, z1)) SPLIT#1(nil) -> c87 SPLIT#2(::(z0, z1), z2) -> c88(SPLIT#3(split(z2), z0, z1), SPLIT(z2)) SPLIT#2(nil, z0) -> c89 SPLIT#3(tuple#2(z0, z1), z2, z3) -> c90 TRANSACC(z0, z1) -> c91(TRANSACC#1(z0, z1)) TRANSACC#1(::(z0, z1), z2) -> c92(ATTACH(z0, transAcc(z1, z2)), TRANSACC(z1, z2)) TRANSACC#1(nil, z0) -> c93 TRANSPOSE(z0) -> c94(TRANSPOSE#1(z0, z0)) TRANSPOSE#1(::(z0, z1), z2) -> c95(TRANSPOSE#2(split(z2)), SPLIT(z2)) TRANSPOSE#1(nil, z0) -> c96 TRANSPOSE#2(tuple#2(z0, z1)) -> c97(TRANSPOSE#3(z1, z0)) TRANSPOSE#3(::(z0, z1), z2) -> c98(TRANSPOSE(::(z0, z1))) TRANSPOSE#3(nil, z0) -> c99 TRANSPOSE'(z0) -> c100(TRANSACC(z0, makeBase(z0)), MAKEBASE(z0)) 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))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) attach(z0, z1) -> attach#1(z0, z1) attach#1(::(z0, z1), z2) -> attach#2(z2, z0, z1) attach#1(nil, z0) -> nil attach#2(::(z0, z1), z2, z3) -> ::(::(z2, z0), attach(z3, z1)) attach#2(nil, z0, z1) -> nil lineMult(z0, z1) -> lineMult#1(z1, z0) lineMult#1(::(z0, z1), z2) -> ::(mult(z2, z0), lineMult(z2, z1)) lineMult#1(nil, z0) -> nil m1(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil)) m2(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil))) m3(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil)) m4(z0) -> ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil)))) makeBase(z0) -> makeBase#1(z0) makeBase#1(::(z0, z1)) -> mkBase(z0) makeBase#1(nil) -> nil matrixMult(z0, z1) -> matrixMult'(z0, transAcc(z1, makeBase(z1))) matrixMult'(z0, z1) -> matrixMult'#1(z0, z1) matrixMult'#1(::(z0, z1), z2) -> ::(lineMult(z0, z2), matrixMult'(z1, z2)) matrixMult'#1(nil, z0) -> nil matrixMult3(z0, z1, z2) -> matrixMult(matrixMult(z0, z1), z2) matrixMultList(z0, z1) -> matrixMultList#1(z1, z0) matrixMultList#1(::(z0, z1), z2) -> matrixMultList(matrixMult(z2, z0), z1) matrixMultList#1(nil, z0) -> z0 matrixMultOld(z0, z1) -> matrixMult'(z0, transpose(z1)) mkBase(z0) -> mkBase#1(z0) mkBase#1(::(z0, z1)) -> ::(nil, mkBase(z1)) mkBase#1(nil) -> nil mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(z2, z0, z1) mult#1(nil, z0) -> #abs(#0) mult#2(::(z0, z1), z2, z3) -> +(*(z2, z0), mult(z3, z1)) mult#2(nil, z0, z1) -> #abs(#0) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> split#2(z0, z1) split#1(nil) -> tuple#2(nil, nil) split#2(::(z0, z1), z2) -> split#3(split(z2), z0, z1) split#2(nil, z0) -> tuple#2(nil, nil) split#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1)) transAcc(z0, z1) -> transAcc#1(z0, z1) transAcc#1(::(z0, z1), z2) -> attach(z0, transAcc(z1, z2)) transAcc#1(nil, z0) -> z0 transpose(z0) -> transpose#1(z0, z0) transpose#1(::(z0, z1), z2) -> transpose#2(split(z2)) transpose#1(nil, z0) -> nil transpose#2(tuple#2(z0, z1)) -> transpose#3(z1, z0) transpose#3(::(z0, z1), z2) -> ::(z2, transpose(::(z0, z1))) transpose#3(nil, z0) -> nil transpose'(z0) -> transAcc(z0, makeBase(z0)) 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: #ABS(#0) -> c24 #ABS(#neg(z0)) -> c25 #ABS(#pos(z0)) -> c26 #ABS(#s(z0)) -> c27 *'(z0, z1) -> c28(#MULT(z0, z1)) +'(z0, z1) -> c29(#ADD(z0, z1)) ATTACH(z0, z1) -> c30(ATTACH#1(z0, z1)) ATTACH#1(::(z0, z1), z2) -> c31(ATTACH#2(z2, z0, z1)) ATTACH#1(nil, z0) -> c32 ATTACH#2(::(z0, z1), z2, z3) -> c33(ATTACH(z3, z1)) ATTACH#2(nil, z0, z1) -> c34 LINEMULT(z0, z1) -> c35(LINEMULT#1(z1, z0)) LINEMULT#1(::(z0, z1), z2) -> c36(MULT(z2, z0)) LINEMULT#1(::(z0, z1), z2) -> c37(LINEMULT(z2, z1)) LINEMULT#1(nil, z0) -> c38 M1(z0) -> c39(#ABS(#pos(#s(#0)))) M1(z0) -> c40(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c41(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c42(#ABS(#pos(#s(#s(#0))))) M1(z0) -> c43(#ABS(#pos(#s(#s(#s(#0)))))) M1(z0) -> c44(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c45(#ABS(#pos(#s(#0)))) M2(z0) -> c46(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c47(#ABS(#pos(#s(#s(#0))))) M2(z0) -> c48(#ABS(#pos(#s(#s(#s(#0)))))) M2(z0) -> c49(#ABS(#pos(#s(#s(#s(#s(#0))))))) M2(z0) -> c50(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c51(#ABS(#pos(#s(#0)))) M3(z0) -> c52(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c53(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c54(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M3(z0) -> c55(#ABS(#pos(#s(#s(#0))))) M3(z0) -> c56(#ABS(#pos(#s(#s(#s(#0)))))) M3(z0) -> c57(#ABS(#pos(#s(#s(#s(#s(#0))))))) M3(z0) -> c58(#ABS(#pos(#s(#s(#s(#s(#s(#0)))))))) M4(z0) -> c59(#ABS(#pos(#s(#0)))) M4(z0) -> c60(#ABS(#pos(#s(#s(#0))))) M4(z0) -> c61(#ABS(#pos(#s(#s(#s(#0)))))) M4(z0) -> c62(#ABS(#pos(#s(#s(#s(#s(#0))))))) MAKEBASE(z0) -> c63(MAKEBASE#1(z0)) MAKEBASE#1(::(z0, z1)) -> c64(MKBASE(z0)) MAKEBASE#1(nil) -> c65 MATRIXMULT(z0, z1) -> c66(MATRIXMULT'(z0, transAcc(z1, makeBase(z1))), TRANSACC(z1, makeBase(z1)), MAKEBASE(z1)) MATRIXMULT'(z0, z1) -> c67(MATRIXMULT'#1(z0, z1)) MATRIXMULT'#1(::(z0, z1), z2) -> c68(LINEMULT(z0, z2)) MATRIXMULT'#1(::(z0, z1), z2) -> c69(MATRIXMULT'(z1, z2)) MATRIXMULT'#1(nil, z0) -> c70 MATRIXMULT3(z0, z1, z2) -> c71(MATRIXMULT(matrixMult(z0, z1), z2), MATRIXMULT(z0, z1)) MATRIXMULTLIST(z0, z1) -> c72(MATRIXMULTLIST#1(z1, z0)) MATRIXMULTLIST#1(::(z0, z1), z2) -> c73(MATRIXMULTLIST(matrixMult(z2, z0), z1), MATRIXMULT(z2, z0)) MATRIXMULTLIST#1(nil, z0) -> c74 MATRIXMULTOLD(z0, z1) -> c75(MATRIXMULT'(z0, transpose(z1)), TRANSPOSE(z1)) MKBASE(z0) -> c76(MKBASE#1(z0)) MKBASE#1(::(z0, z1)) -> c77(MKBASE(z1)) MKBASE#1(nil) -> c78 MULT(z0, z1) -> c79(MULT#1(z0, z1)) MULT#1(::(z0, z1), z2) -> c80(MULT#2(z2, z0, z1)) MULT#1(nil, z0) -> c81(#ABS(#0)) MULT#2(::(z0, z1), z2, z3) -> c82(+'(*(z2, z0), mult(z3, z1)), *'(z2, z0)) MULT#2(::(z0, z1), z2, z3) -> c83(+'(*(z2, z0), mult(z3, z1)), MULT(z3, z1)) MULT#2(nil, z0, z1) -> c84(#ABS(#0)) SPLIT(z0) -> c85(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c86(SPLIT#2(z0, z1)) SPLIT#1(nil) -> c87 SPLIT#2(::(z0, z1), z2) -> c88(SPLIT#3(split(z2), z0, z1), SPLIT(z2)) SPLIT#2(nil, z0) -> c89 SPLIT#3(tuple#2(z0, z1), z2, z3) -> c90 TRANSACC(z0, z1) -> c91(TRANSACC#1(z0, z1)) TRANSACC#1(::(z0, z1), z2) -> c92(ATTACH(z0, transAcc(z1, z2)), TRANSACC(z1, z2)) TRANSACC#1(nil, z0) -> c93 TRANSPOSE(z0) -> c94(TRANSPOSE#1(z0, z0)) TRANSPOSE#1(::(z0, z1), z2) -> c95(TRANSPOSE#2(split(z2)), SPLIT(z2)) TRANSPOSE#1(nil, z0) -> c96 TRANSPOSE#2(tuple#2(z0, z1)) -> c97(TRANSPOSE#3(z1, z0)) TRANSPOSE#3(::(z0, z1), z2) -> c98(TRANSPOSE(::(z0, z1))) TRANSPOSE#3(nil, z0) -> c99 TRANSPOSE'(z0) -> c100(TRANSACC(z0, makeBase(z0)), MAKEBASE(z0)) 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))) #abs(#0) -> #0 #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) *(z0, z1) -> #mult(z0, z1) +(z0, z1) -> #add(z0, z1) attach(z0, z1) -> attach#1(z0, z1) attach#1(::(z0, z1), z2) -> attach#2(z2, z0, z1) attach#1(nil, z0) -> nil attach#2(::(z0, z1), z2, z3) -> ::(::(z2, z0), attach(z3, z1)) attach#2(nil, z0, z1) -> nil lineMult(z0, z1) -> lineMult#1(z1, z0) lineMult#1(::(z0, z1), z2) -> ::(mult(z2, z0), lineMult(z2, z1)) lineMult#1(nil, z0) -> nil m1(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil))), nil)) m2(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), nil)), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), nil)), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)), nil))) m3(z0) -> ::(::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), ::(::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#0))))), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), nil)))), nil)) m4(z0) -> ::(::(#abs(#pos(#s(#0))), nil), ::(::(#abs(#pos(#s(#s(#0)))), nil), ::(::(#abs(#pos(#s(#s(#s(#0))))), nil), ::(::(#abs(#pos(#s(#s(#s(#s(#0)))))), nil), nil)))) makeBase(z0) -> makeBase#1(z0) makeBase#1(::(z0, z1)) -> mkBase(z0) makeBase#1(nil) -> nil matrixMult(z0, z1) -> matrixMult'(z0, transAcc(z1, makeBase(z1))) matrixMult'(z0, z1) -> matrixMult'#1(z0, z1) matrixMult'#1(::(z0, z1), z2) -> ::(lineMult(z0, z2), matrixMult'(z1, z2)) matrixMult'#1(nil, z0) -> nil matrixMult3(z0, z1, z2) -> matrixMult(matrixMult(z0, z1), z2) matrixMultList(z0, z1) -> matrixMultList#1(z1, z0) matrixMultList#1(::(z0, z1), z2) -> matrixMultList(matrixMult(z2, z0), z1) matrixMultList#1(nil, z0) -> z0 matrixMultOld(z0, z1) -> matrixMult'(z0, transpose(z1)) mkBase(z0) -> mkBase#1(z0) mkBase#1(::(z0, z1)) -> ::(nil, mkBase(z1)) mkBase#1(nil) -> nil mult(z0, z1) -> mult#1(z0, z1) mult#1(::(z0, z1), z2) -> mult#2(z2, z0, z1) mult#1(nil, z0) -> #abs(#0) mult#2(::(z0, z1), z2, z3) -> +(*(z2, z0), mult(z3, z1)) mult#2(nil, z0, z1) -> #abs(#0) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> split#2(z0, z1) split#1(nil) -> tuple#2(nil, nil) split#2(::(z0, z1), z2) -> split#3(split(z2), z0, z1) split#2(nil, z0) -> tuple#2(nil, nil) split#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1)) transAcc(z0, z1) -> transAcc#1(z0, z1) transAcc#1(::(z0, z1), z2) -> attach(z0, transAcc(z1, z2)) transAcc#1(nil, z0) -> z0 transpose(z0) -> transpose#1(z0, z0) transpose#1(::(z0, z1), z2) -> transpose#2(split(z2)) transpose#1(nil, z0) -> nil transpose#2(tuple#2(z0, z1)) -> transpose#3(z1, z0) transpose#3(::(z0, z1), z2) -> ::(z2, transpose(::(z0, z1))) transpose#3(nil, z0) -> nil transpose'(z0) -> transAcc(z0, makeBase(z0)) Rewrite Strategy: INNERMOST