MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: #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)) - Weak TRS: #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() #abs(#0()) -> #0() #abs(#neg(z0)) -> #pos(z0) #abs(#pos(z0)) -> #pos(z0) #abs(#s(z0)) -> #pos(#s(z0)) #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) 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)) - Signature: {#ABS/1,#ADD/2,#MULT/2,#NATMULT/2,#PRED/1,#SUCC/1,#abs/1,#add/2,#mult/2,#natmult/2,#pred/1,#succ/1,*/2,*'/2 ,+/2,+'/2,ATTACH/2,ATTACH#1/2,ATTACH#2/3,LINEMULT/2,LINEMULT#1/2,M1/1,M2/1,M3/1,M4/1,MAKEBASE/1,MAKEBASE#1/1 ,MATRIXMULT/2,MATRIXMULT'/2,MATRIXMULT'#1/2,MATRIXMULT3/3,MATRIXMULTLIST/2,MATRIXMULTLIST#1/2 ,MATRIXMULTOLD/2,MKBASE/1,MKBASE#1/1,MULT/2,MULT#1/2,MULT#2/3,SPLIT/1,SPLIT#1/1,SPLIT#2/2,SPLIT#3/3 ,TRANSACC/2,TRANSACC#1/2,TRANSPOSE/1,TRANSPOSE#1/2,TRANSPOSE#2/1,TRANSPOSE#3/2,TRANSPOSE'/1,attach/2 ,attach#1/2,attach#2/3,lineMult/2,lineMult#1/2,m1/1,m2/1,m3/1,m4/1,makeBase/1,makeBase#1/1,matrixMult/2 ,matrixMult'/2,matrixMult'#1/2,matrixMult3/3,matrixMultList/2,matrixMultList#1/2,matrixMultOld/2,mkBase/1 ,mkBase#1/1,mult/2,mult#1/2,mult#2/3,split/1,split#1/1,split#2/2,split#3/3,transAcc/2,transAcc#1/2 ,transpose/1,transpose#1/2,transpose#2/1,transpose#3/2,transpose'/1} / {#0/0,#neg/1,#pos/1,#s/1,::/2,c/0 ,c1/1,c10/1,c100/2,c11/0,c12/1,c13/1,c14/0,c15/2,c16/0,c17/0,c18/0,c19/0,c2/2,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/1,c29/1,c3/1,c30/1,c31/1,c32/0,c33/1,c34/0,c35/1,c36/1,c37/1,c38/0,c39/1,c4/2,c40/1 ,c41/1,c42/1,c43/1,c44/1,c45/1,c46/1,c47/1,c48/1,c49/1,c5/0,c50/1,c51/1,c52/1,c53/1,c54/1,c55/1,c56/1,c57/1 ,c58/1,c59/1,c6/0,c60/1,c61/1,c62/1,c63/1,c64/1,c65/0,c66/3,c67/1,c68/1,c69/1,c7/0,c70/0,c71/2,c72/1,c73/2 ,c74/0,c75/2,c76/1,c77/1,c78/0,c79/1,c8/0,c80/1,c81/1,c82/2,c83/2,c84/1,c85/1,c86/1,c87/0,c88/2,c89/0,c9/1 ,c90/0,c91/1,c92/2,c93/0,c94/1,c95/2,c96/0,c97/1,c98/1,c99/0,nil/0,tuple#2/2} - Obligation: innermost runtime complexity wrt. defined symbols {#ABS,#ADD,#MULT,#NATMULT,#PRED,#SUCC,#abs,#add,#mult ,#natmult,#pred,#succ,*,*',+,+',ATTACH,ATTACH#1,ATTACH#2,LINEMULT,LINEMULT#1,M1,M2,M3,M4,MAKEBASE,MAKEBASE#1 ,MATRIXMULT,MATRIXMULT',MATRIXMULT'#1,MATRIXMULT3,MATRIXMULTLIST,MATRIXMULTLIST#1,MATRIXMULTOLD,MKBASE ,MKBASE#1,MULT,MULT#1,MULT#2,SPLIT,SPLIT#1,SPLIT#2,SPLIT#3,TRANSACC,TRANSACC#1,TRANSPOSE,TRANSPOSE#1 ,TRANSPOSE#2,TRANSPOSE#3,TRANSPOSE',attach,attach#1,attach#2,lineMult,lineMult#1,m1,m2,m3,m4,makeBase ,makeBase#1,matrixMult,matrixMult',matrixMult'#1,matrixMult3,matrixMultList,matrixMultList#1,matrixMultOld ,mkBase,mkBase#1,mult,mult#1,mult#2,split,split#1,split#2,split#3,transAcc,transAcc#1,transpose,transpose#1 ,transpose#2,transpose#3,transpose'} and constructors {#0,#neg,#pos,#s,::,c,c1,c10,c100,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4 ,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c6,c60,c61,c62,c63,c64 ,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83,c84,c85,c86,c87,c88,c89 ,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,nil,tuple#2} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: None MAYBE