WORST_CASE(?,O(n^2)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (?,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (?,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (?,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 7. out1transAcc(A,B,C,D) -> out1transAcc(A,-1 + B,C,D) [B >= 1] (?,1) 8. out2transAcc(A,B,C,D) -> out2transAcc(A,-1 + B,C,D) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (?,1) 12. out1split(A,B,C,D) -> out1split(A,-1 + B,C,D) [B >= 1] (?,1) 13. out2split(A,B,C,D) -> out2split(A,-1 + B,C,D) [B >= 1] (?,1) 14. out3split(A,B,C,D) -> out3split(A,-1 + B,C,D) [B >= 1] (?,1) 15. split(A,B,C,D) -> split(A,-1 + B,C,D) [B >= 1] (?,1) 16. out1makeBase(A,B,C,D) -> outmkBase(A,D,C,D) [B = 0] (?,1) 17. outmkBase(A,B,C,D) -> outmkBase(A,-1 + B,C,D) [B >= 1] (?,1) 18. matrixmult3(A,B,C,D) -> matrixmult(A,B,C,D) True (?,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 26. transpose(A,B,C,D) -> split(A,B,C,D) [B >= 1 && D = 1] (?,1) 27. transpose0(A,B,C,D) -> split(A,B,C,D) True (?,1) 28. transpose1(A,B,C,D) -> transpose(A,B,C,-1 + D) True (?,1) 29. transpose(A,B,C,D) -> c2(transpose0(A,B,C,D),transpose1(A,B,C,D)) [B >= 1 && D >= 2] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},7->{7},8->{8},9->{9},10->{11},11->{11},12->{12} ,13->{13},14->{14},15->{15},16->{17},17->{17},18->{3},19->{24},20->{21},21->{19,20},22->{25},23->{24} ,24->{22,23},25->{25},26->{15},27->{15},28->{26,29},29->{27,28},30->{3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (?,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (?,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (?,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 7. out1transAcc(A,B,C,D) -> out1transAcc(A,-1 + B,C,D) [B >= 1] (?,1) 8. out2transAcc(A,B,C,D) -> out2transAcc(A,-1 + B,C,D) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (?,1) 12. out1split(A,B,C,D) -> out1split(A,-1 + B,C,D) [B >= 1] (?,1) 13. out2split(A,B,C,D) -> out2split(A,-1 + B,C,D) [B >= 1] (?,1) 14. out3split(A,B,C,D) -> out3split(A,-1 + B,C,D) [B >= 1] (?,1) 15. split(A,B,C,D) -> split(A,-1 + B,C,D) [B >= 1] (?,1) 16. out1makeBase(A,B,C,D) -> outmkBase(A,D,C,D) [B = 0] (1,1) 17. outmkBase(A,B,C,D) -> outmkBase(A,-1 + B,C,D) [B >= 1] (?,1) 18. matrixmult3(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 26. transpose(A,B,C,D) -> split(A,B,C,D) [B >= 1 && D = 1] (?,1) 27. transpose0(A,B,C,D) -> split(A,B,C,D) True (?,1) 28. transpose1(A,B,C,D) -> transpose(A,B,C,-1 + D) True (?,1) 29. transpose(A,B,C,D) -> c2(transpose0(A,B,C,D),transpose1(A,B,C,D)) [B >= 1 && D >= 2] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},7->{7},8->{8},9->{9},10->{11},11->{11},12->{12} ,13->{13},14->{14},15->{15},16->{17},17->{17},18->{3},19->{24},20->{21},21->{19,20},22->{25},23->{24} ,24->{22,23},25->{25},26->{15},27->{15},28->{26,29},29->{27,28},30->{3}] + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [7 ,8 ,12 ,13 ,14 ,15 ,16 ,17 ,18 ,26 ,27 ,28 ,29] * Step 3: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (?,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (?,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (?,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (?,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21} ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, B, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, 0, .= 0) (< 0,0,D>, D, .= 0) (< 1,0,A>, B, .= 0) (< 1,0,B>, A, .= 0) (< 1,0,C>, A + D, .* 0) (< 1,0,D>, C, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) (< 3,0,A>, B, .= 0) (< 3,0,B>, A, .= 0) (< 3,0,C>, D, .= 0) (< 3,0,D>, C, .= 0) (< 3,1,A>, B, .= 0) (< 3,1,B>, A, .= 0) (< 3,1,C>, D, .= 0) (< 3,1,D>, C, .= 0) (< 3,2,A>, B, .= 0) (< 3,2,B>, A, .= 0) (< 3,2,C>, D, .= 0) (< 3,2,D>, C, .= 0) (< 4,0,A>, 1 + A + D, .* 1) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, 1 + D, .+ 1) (< 5,0,A>, C, .= 0) (< 5,0,B>, 1 + D, .+ 1) (< 5,0,C>, A, .= 0) (< 5,0,D>, B, .= 0) (< 6,0,A>, C, .= 0) (< 6,0,B>, D, .= 0) (< 6,0,C>, A, .= 0) (< 6,0,D>, B, .= 0) (< 6,1,A>, C, .= 0) (< 6,1,B>, D, .= 0) (< 6,1,C>, A, .= 0) (< 6,1,D>, B, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>, C, .= 0) (< 9,0,D>, 1 + D, .+ 1) (<10,0,A>, A, .= 0) (<10,0,B>, D, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, 1 + B, .+ 1) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<19,0,A>, A, .= 0) (<19,0,B>, B, .= 0) (<19,0,C>, C, .= 0) (<19,0,D>, D, .= 0) (<20,0,A>, D, .= 0) (<20,0,B>, 1 + C, .+ 1) (<20,0,C>, A, .= 0) (<20,0,D>, B, .= 0) (<21,0,A>, C, .= 0) (<21,0,B>, D, .= 0) (<21,0,C>, B, .= 0) (<21,0,D>, A, .= 0) (<21,1,A>, C, .= 0) (<21,1,B>, D, .= 0) (<21,1,C>, B, .= 0) (<21,1,D>, A, .= 0) (<22,0,A>, A, .= 0) (<22,0,B>, B, .= 0) (<22,0,C>, C, .= 0) (<22,0,D>, D, .= 0) (<23,0,A>, D, .= 0) (<23,0,B>, B, .= 0) (<23,0,C>, C, .= 0) (<23,0,D>, 1 + A, .+ 1) (<24,0,A>, D, .= 0) (<24,0,B>, B, .= 0) (<24,0,C>, C, .= 0) (<24,0,D>, A, .= 0) (<24,1,A>, D, .= 0) (<24,1,B>, B, .= 0) (<24,1,C>, C, .= 0) (<24,1,D>, A, .= 0) (<25,0,A>, A, .= 0) (<25,0,B>, 1 + B, .+ 1) (<25,0,C>, C, .= 0) (<25,0,D>, 1 + D, .+ 1) (<30,0,A>, A, .= 0) (<30,0,B>, B, .= 0) (<30,0,C>, C, .= 0) (<30,0,D>, D, .= 0) * Step 4: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (?,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (?,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (?,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (?,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21} ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,1,A>, ?) (< 3,1,B>, ?) (< 3,1,C>, ?) (< 3,1,D>, ?) (< 3,2,A>, ?) (< 3,2,B>, ?) (< 3,2,C>, ?) (< 3,2,D>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,1,A>, ?) (< 6,1,B>, ?) (< 6,1,C>, ?) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<19,0,A>, ?) (<19,0,B>, ?) (<19,0,C>, ?) (<19,0,D>, ?) (<20,0,A>, ?) (<20,0,B>, ?) (<20,0,C>, ?) (<20,0,D>, ?) (<21,0,A>, ?) (<21,0,B>, ?) (<21,0,C>, ?) (<21,0,D>, ?) (<21,1,A>, ?) (<21,1,B>, ?) (<21,1,C>, ?) (<21,1,D>, ?) (<22,0,A>, ?) (<22,0,B>, ?) (<22,0,C>, ?) (<22,0,D>, ?) (<23,0,A>, ?) (<23,0,B>, ?) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, ?) (<24,0,C>, ?) (<24,0,D>, ?) (<24,1,A>, ?) (<24,1,B>, ?) (<24,1,C>, ?) (<24,1,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 2,0,A>, B) (< 2,0,B>, A) (< 2,0,C>, D) (< 2,0,D>, C) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<10,0,A>, B) (<10,0,B>, C) (<10,0,C>, D) (<10,0,D>, C) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) * Step 5: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (?,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (?,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (?,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (?,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21} ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 2,0,A>, B) (< 2,0,B>, A) (< 2,0,C>, D) (< 2,0,D>, C) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<10,0,A>, B) (<10,0,B>, C) (<10,0,C>, D) (<10,0,D>, C) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(attach) = 0 p(linemult) = 0 p(linemult0) = 0 p(linemult1) = 0 p(makeBase) = 1 p(matrixmult) = 2 p(matrixmult0) = 0 p(matrixmult1) = 1 p(matrixmult2) = 1 p(matrixmultp) = 1 p(matrixmultp0) = 0 p(matrixmultp1) = 1 p(mkBase) = 0 p(mult) = 0 p(start) = 2 p(transAcc) = 0 p(transAcc0) = 0 p(transAcc1) = 0 The following rules are strictly oriented: [B >= 1] ==> makeBase(A,B,C,D) = 1 > 0 = mkBase(A,D,C,D) The following rules are weakly oriented: True ==> matrixmult0(A,B,C,D) = 0 >= 0 = transAcc(B,B,0,D) True ==> matrixmult1(A,B,C,D) = 1 >= 1 = matrixmultp(B,A,A + D,C) True ==> matrixmult2(A,B,C,D) = 1 >= 1 = makeBase(A,B,C,D) [B >= 0 && D >= 0 && A >= 0 && C >= 0] ==> matrixmult(A,B,C,D) = 2 >= 2 = c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) True ==> transAcc0(A,B,C,D) = 0 >= 0 = attach(-1 + A + D,B,C,-1 + D) True ==> transAcc1(A,B,C,D) = 0 >= 0 = transAcc(C,-1 + D,A,B) [B >= 1] ==> transAcc(A,B,C,D) = 0 >= 0 = c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] ==> attach(A,B,C,D) = 0 >= 0 = attach(A,-1 + B,C,-1 + D) [B >= 1] ==> mkBase(A,B,C,D) = 0 >= 0 = mkBase(A,-1 + B,C,D) True ==> matrixmultp0(A,B,C,D) = 0 >= 0 = linemult(A,B,C,D) True ==> matrixmultp1(A,B,C,D) = 1 >= 1 = matrixmultp(D,-1 + C,A,B) [B >= 1] ==> matrixmultp(A,B,C,D) = 1 >= 1 = c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) True ==> linemult0(A,B,C,D) = 0 >= 0 = mult(A,B,C,D) True ==> linemult1(A,B,C,D) = 0 >= 0 = linemult(D,B,C,-1 + A) [D >= 1] ==> linemult(A,B,C,D) = 0 >= 0 = c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [B >= 1 && D >= 1] ==> mult(A,B,C,D) = 0 >= 0 = mult(A,-1 + B,C,-1 + D) True ==> start(A,B,C,D) = 2 >= 2 = matrixmult(A,B,C,D) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (?,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (?,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (?,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (?,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (2,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (?,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21} ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 2,0,A>, B) (< 2,0,B>, A) (< 2,0,C>, D) (< 2,0,D>, C) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<10,0,A>, B) (<10,0,B>, C) (<10,0,C>, D) (<10,0,D>, C) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 7: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (1,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (1,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (2,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (?,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21} ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 2,0,A>, B) (< 2,0,B>, A) (< 2,0,C>, D) (< 2,0,D>, C) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<10,0,A>, B) (<10,0,B>, C) (<10,0,C>, D) (<10,0,D>, C) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [11], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(mkBase) = x2 The following rules are strictly oriented: [B >= 1] ==> mkBase(A,B,C,D) = B > -1 + B = mkBase(A,-1 + B,C,D) The following rules are weakly oriented: We use the following global sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 2,0,A>, B) (< 2,0,B>, A) (< 2,0,C>, D) (< 2,0,D>, C) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<10,0,A>, B) (<10,0,B>, C) (<10,0,C>, D) (<10,0,D>, C) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) * Step 8: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (1,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 2. matrixmult2(A,B,C,D) -> makeBase(A,B,C,D) True (1,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (2,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},2->{10},3->{0,1,2},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21} ,21->{19,20},22->{25},23->{24},24->{22,23},25->{25},30->{3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 2,0,A>, B) (< 2,0,B>, A) (< 2,0,C>, D) (< 2,0,D>, C) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<10,0,A>, B) (<10,0,B>, C) (<10,0,C>, D) (<10,0,D>, C) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) + Applied Processor: ChainProcessor False [0,1,2,3,4,5,6,9,10,11,19,20,21,22,23,24,25,30] + Details: We chained rule 2 to obtain the rules [31] . * Step 9: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (1,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 10. makeBase(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (2,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},3->{0,1,31},4->{9},5->{6},6->{4,5},9->{9},10->{11},11->{11},19->{24},20->{21},21->{19,20} ,22->{25},23->{24},24->{22,23},25->{25},30->{3},31->{11}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<10,0,A>, B) (<10,0,B>, C) (<10,0,C>, D) (<10,0,D>, C) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [10] * Step 10: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (1,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 3. matrixmult(A,B,C,D) -> c3(matrixmult0(B,A,D,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},3->{0,1,31},4->{9},5->{6},6->{4,5},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25} ,23->{24},24->{22,23},25->{25},30->{3},31->{11}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 3,0,A>, B) (< 3,0,B>, A) (< 3,0,C>, D) (< 3,0,D>, C) (< 3,1,A>, B) (< 3,1,B>, A) (< 3,1,C>, D) (< 3,1,D>, C) (< 3,2,A>, B) (< 3,2,B>, A) (< 3,2,C>, D) (< 3,2,D>, C) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) + Applied Processor: ChainProcessor False [0,1,3,4,5,6,9,11,19,20,21,22,23,24,25,30,31] + Details: We chained rule 3 to obtain the rules [32] . * Step 11: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. matrixmult0(A,B,C,D) -> transAcc(B,B,0,D) True (1,1) 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [0->{6},1->{21},4->{9},5->{6},6->{4,5},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24} ,24->{22,23},25->{25},30->{32},31->{11},32->{1,6,31}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, A) (< 0,0,C>, 0) (< 0,0,D>, C) (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [0] * Step 12: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 6. transAcc(A,B,C,D) -> c2(transAcc0(C,D,A,B),transAcc1(C,D,A,B)) [B >= 1] (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{21},4->{9},5->{6},6->{4,5},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24},24->{22 ,23},25->{25},30->{32},31->{11},32->{1,6,31}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 6,0,A>, 0) (< 6,0,B>, C) (< 6,0,C>, A) (< 6,0,D>, ?) (< 6,1,A>, 0) (< 6,1,B>, C) (< 6,1,C>, A) (< 6,1,D>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) + Applied Processor: ChainProcessor False [1,4,5,6,9,11,19,20,21,22,23,24,25,30,31,32] + Details: We chained rule 6 to obtain the rules [33] . * Step 13: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 4. transAcc0(A,B,C,D) -> attach(-1 + A + D,B,C,-1 + D) True (?,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{21},4->{9},5->{33},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24},24->{22,23} ,25->{25},30->{32},31->{11},32->{1,31,33},33->{5,9}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 4,0,A>, ?) (< 4,0,B>, C) (< 4,0,C>, A) (< 4,0,D>, ?) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [4] * Step 14: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 21. matrixmultp(A,B,C,D) -> c2(matrixmultp0(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{21},5->{33},9->{9},11->{11},19->{24},20->{21},21->{19,20},22->{25},23->{24},24->{22,23},25->{25} ,30->{32},31->{11},32->{1,31,33},33->{5,9}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<21,0,A>, B + C) (<21,0,B>, D) (<21,0,C>, ?) (<21,0,D>, A) (<21,1,A>, B + C) (<21,1,B>, D) (<21,1,C>, ?) (<21,1,D>, A) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) + Applied Processor: ChainProcessor False [1,5,9,11,19,20,21,22,23,24,25,30,31,32,33] + Details: We chained rule 21 to obtain the rules [34] . * Step 15: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 19. matrixmultp0(A,B,C,D) -> linemult(A,B,C,D) True (?,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{34},5->{33},9->{9},11->{11},19->{24},20->{34},22->{25},23->{24},24->{22,23},25->{25},30->{32} ,31->{11},32->{1,31,33},33->{5,9},34->{20,24}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<19,0,A>, B + C) (<19,0,B>, D) (<19,0,C>, ?) (<19,0,D>, A) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [19] * Step 16: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 24. linemult(A,B,C,D) -> c2(linemult0(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{34},5->{33},9->{9},11->{11},20->{34},22->{25},23->{24},24->{22,23},25->{25},30->{32},31->{11},32->{1 ,31,33},33->{5,9},34->{20,24}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<24,0,A>, ?) (<24,0,B>, D) (<24,0,C>, ?) (<24,0,D>, B + C) (<24,1,A>, ?) (<24,1,B>, D) (<24,1,C>, ?) (<24,1,D>, B + C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) + Applied Processor: ChainProcessor False [1,5,9,11,20,22,23,24,25,30,31,32,33,34] + Details: We chained rule 24 to obtain the rules [35] . * Step 17: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 22. linemult0(A,B,C,D) -> mult(A,B,C,D) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{34},5->{33},9->{9},11->{11},20->{34},22->{25},23->{35},25->{25},30->{32},31->{11},32->{1,31,33} ,33->{5,9},34->{20,35},35->{23,25}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<22,0,A>, ?) (<22,0,B>, D) (<22,0,C>, ?) (<22,0,D>, B + C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [22] * Step 18: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 32. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmult1(B,A,D,C),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{34},5->{33},9->{9},11->{11},20->{34},23->{35},25->{25},30->{32},31->{11},32->{1,31,33},33->{5,9} ,34->{20,35},35->{23,25}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<32,0,A>, A) (<32,0,B>, A) (<32,0,C>, 0) (<32,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) + Applied Processor: ChainProcessor False [1,5,9,11,20,23,25,30,31,32,33,34,35] + Details: We chained rule 32 to obtain the rules [36] . * Step 19: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. matrixmult1(A,B,C,D) -> matrixmultp(B,A,A + D,C) True (1,1) 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [1->{34},5->{33},9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},33->{5,9},34->{20,35} ,35->{23,25},36->{31,33,34}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, B) (< 1,0,C>, B + C) (< 1,0,D>, D) (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [1] * Step 20: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 33. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc1(C,D,A,B)) [B >= 1] (?,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [5->{33},9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},33->{5,9},34->{20,35},35->{23,25} ,36->{31,33,34}] Sizebounds: (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<33,0,A>, ?) (<33,0,B>, C) (<33,0,C>, A) (<33,0,D>, ?) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) + Applied Processor: ChainProcessor False [5,9,11,20,23,25,30,31,33,34,35,36] + Details: We chained rule 33 to obtain the rules [37] . * Step 21: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 5. transAcc1(A,B,C,D) -> transAcc(C,-1 + D,A,B) True (?,1) 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [5->{37},9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},34->{20,35},35->{23,25},36->{31,34 ,37},37->{9,37}] Sizebounds: (< 5,0,A>, A) (< 5,0,B>, ?) (< 5,0,C>, 0) (< 5,0,D>, C) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [5] * Step 22: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 34. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp1(C,D,B,A)) [B >= 1] (?,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},20->{34},23->{35},25->{25},30->{36},31->{11},34->{20,35},35->{23,25},36->{31,34,37} ,37->{9,37}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<34,0,A>, B + C) (<34,0,B>, D) (<34,0,C>, ?) (<34,0,D>, A) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) + Applied Processor: ChainProcessor False [9,11,20,23,25,30,31,34,35,36,37] + Details: We chained rule 34 to obtain the rules [38] . * Step 23: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 20. matrixmultp1(A,B,C,D) -> matrixmultp(D,-1 + C,A,B) True (?,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},20->{38},23->{35},25->{25},30->{36},31->{11},35->{23,25},36->{31,37,38},37->{9,37} ,38->{35,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<20,0,A>, A) (<20,0,B>, ?) (<20,0,C>, B + C) (<20,0,D>, D) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) (<38,0,A>, A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [20] * Step 24: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 35. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult1(D,B,C,A)) [D >= 1] (?,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},23->{35},25->{25},30->{36},31->{11},35->{23,25},36->{31,37,38},37->{9,37},38->{35,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<35,0,A>, ?) (<35,0,B>, D) (<35,0,C>, ?) (<35,0,D>, B + C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) (<38,0,A>, A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) + Applied Processor: ChainProcessor False [9,11,23,25,30,31,35,36,37,38] + Details: We chained rule 35 to obtain the rules [39] . * Step 25: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 23. linemult1(A,B,C,D) -> linemult(D,B,C,-1 + A) True (?,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (?,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},23->{39},25->{25},30->{36},31->{11},36->{31,37,38},37->{9,37},38->{38,39},39->{25,39}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<23,0,A>, B + C) (<23,0,B>, D) (<23,0,C>, ?) (<23,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) (<38,0,A>, A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>, ?) (<39,0,D>, ?) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [23] * Step 26: ChainProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 36. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),matrixmult2(B,A,D,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0] (1,3) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (?,3) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{36},31->{11},36->{31,37,38},37->{9,37},38->{38,39},39->{25,39}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<36,0,A>, A) (<36,0,B>, B) (<36,0,C>, B + C) (<36,0,D>, D) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) (<38,0,A>, A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>, ?) (<39,0,D>, ?) + Applied Processor: ChainProcessor False [9,11,25,30,31,36,37,38,39] + Details: We chained rule 36 to obtain the rules [40] . * Step 27: UnreachableRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 31. matrixmult2(A,B,C,D) -> mkBase(A,D,C,D) [B >= 1] (1,2) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (?,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},31->{11},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<31,0,A>, B) (<31,0,B>, C) (<31,0,C>, D) (<31,0,D>, C) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) (<38,0,A>, A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>, ?) (<39,0,D>, ?) (<40,0,A>, B) (<40,0,B>, C) (<40,0,C>, D) (<40,0,D>, C) + Applied Processor: UnreachableRules + Details: The following transitions are not reachable from the starting states and are removed: [31] * Step 28: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (?,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, A) (< 9,0,D>, ?) (<11,0,A>, B) (<11,0,B>, ?) (<11,0,C>, D) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, A) (<37,0,B>, ?) (<37,0,C>, 0) (<37,0,D>, C) (<38,0,A>, A) (<38,0,B>, ?) (<38,0,C>, B + C) (<38,0,D>, D) (<39,0,A>, B + C) (<39,0,B>, D) (<39,0,C>, ?) (<39,0,D>, ?) (<40,0,A>, B) (<40,0,B>, C) (<40,0,C>, D) (<40,0,D>, C) + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 9,0,A>, A, .= 0) (< 9,0,B>, 1 + B, .+ 1) (< 9,0,C>, C, .= 0) (< 9,0,D>, 1 + D, .+ 1) (<11,0,A>, A, .= 0) (<11,0,B>, 1 + B, .+ 1) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<25,0,A>, A, .= 0) (<25,0,B>, 1 + B, .+ 1) (<25,0,C>, C, .= 0) (<25,0,D>, 1 + D, .+ 1) (<30,0,A>, A, .= 0) (<30,0,B>, B, .= 0) (<30,0,C>, C, .= 0) (<30,0,D>, D, .= 0) (<37,0,A>, 1 + B + C, .* 1) (<37,0,B>, D, .= 0) (<37,0,C>, A, .= 0) (<37,0,D>, 1 + B, .+ 1) (<37,1,A>, A, .= 0) (<37,1,B>, 2 + B, .+ 2) (<37,1,C>, 1 + B + C, .* 1) (<37,1,D>, D, .= 0) (<38,0,A>, C, .= 0) (<38,0,B>, D, .= 0) (<38,0,C>, B, .= 0) (<38,0,D>, A, .= 0) (<38,1,A>, A, .= 0) (<38,1,B>, 1 + B, .+ 1) (<38,1,C>, C, .= 0) (<38,1,D>, D, .= 0) (<39,0,A>, D, .= 0) (<39,0,B>, B, .= 0) (<39,0,C>, C, .= 0) (<39,0,D>, A, .= 0) (<39,1,A>, A, .= 0) (<39,1,B>, B, .= 0) (<39,1,C>, C, .= 0) (<39,1,D>, 1 + D, .+ 1) (<40,0,A>, A, .= 0) (<40,0,B>, A, .= 0) (<40,0,C>, 0, .= 0) (<40,0,D>, C, .= 0) (<40,1,A>, A, .= 0) (<40,1,B>, A, .= 0) (<40,1,C>, 1 + A + C, .* 1) (<40,1,D>, 0, .= 0) (<40,2,A>, A, .= 0) (<40,2,B>, C, .= 0) (<40,2,C>, 0, .= 0) (<40,2,D>, C, .= 0) * Step 29: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (?,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, ?) (<30,0,B>, ?) (<30,0,C>, ?) (<30,0,D>, ?) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, ?) (<40,0,B>, ?) (<40,0,C>, ?) (<40,0,D>, ?) (<40,1,A>, ?) (<40,1,B>, ?) (<40,1,C>, ?) (<40,1,D>, ?) (<40,2,A>, ?) (<40,2,B>, ?) (<40,2,C>, ?) (<40,2,D>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) * Step 30: LocationConstraintsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (?,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: LocationConstraintsProc + Details: We computed the location constraints 9 : True 11 : True 25 : True 30 : True 37 : True 38 : True 39 : True 40 : True . * Step 31: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (?,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (?,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (?,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: LoopRecurrenceProcessor [38] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution 2*A*B + 2*A*B*D + B . * Step 32: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (A + 2*A^2,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (A + 2*A^2,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (A + 2*A^2,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: LoopRecurrenceProcessor [39] + Details: Applying the recurrence pattern linear * f to the expression D yields the solution B*D + D . * Step 33: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (?,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (A + 2*A^2,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (?,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (A + 2*A^2,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (A + 2*A^2,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: LoopRecurrenceProcessor [37] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution B + B*D . * Step 34: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (A + A*C,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (A + 2*A^2,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (A + A*C,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (A + 2*A^2,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (A + 2*A^2,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: LoopRecurrenceProcessor [25] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution B . * Step 35: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (A + A*C,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (2*C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (A + 2*A^2,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (A + A*C,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (A + 2*A^2,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (A + 2*A^2,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: LoopRecurrenceProcessor [11] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution B . * Step 36: LoopRecurrenceProcessor WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (A + A*C,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (A + 2*A^2,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (A + A*C,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (A + 2*A^2,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (A + 2*A^2,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: LoopRecurrenceProcessor [9] + Details: Applying the recurrence pattern linear * f to the expression B yields the solution B . * Step 37: UnsatPaths WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 9. attach(A,B,C,D) -> attach(A,-1 + B,C,-1 + D) [B >= 1] (A + A*C,1) 11. mkBase(A,B,C,D) -> mkBase(A,-1 + B,C,D) [B >= 1] (C,1) 25. mult(A,B,C,D) -> mult(A,-1 + B,C,-1 + D) [B >= 1 && D >= 1] (A + 2*A^2,1) 30. start(A,B,C,D) -> matrixmult(A,B,C,D) True (1,1) 37. transAcc(A,B,C,D) -> c2(attach(-1 + B + C,D,A,-1 + B),transAcc(A,-2 + B,-1 + B + C,D)) [B >= 1] (A + A*C,3) 38. matrixmultp(A,B,C,D) -> c2(linemult(C,D,B,A),matrixmultp(A,-1 + B,C,D)) [B >= 1] (A + 2*A^2,3) 39. linemult(A,B,C,D) -> c2(mult(D,B,C,A),linemult(A,B,C,-1 + D)) [D >= 1] (A + 2*A^2,3) 40. matrixmult(A,B,C,D) -> c3(transAcc(A,A,0,C),matrixmultp(A,A,A + C,0),mkBase(A,C,0,C)) [B >= 0 && D >= 0 && A >= 0 && C >= 0 && A >= 1] (1,5) Signature: {(attach,4) ;(linemult,4) ;(linemult0,4) ;(linemult1,4) ;(makeBase,4) ;(matrixmult,4) ;(matrixmult0,4) ;(matrixmult1,4) ;(matrixmult2,4) ;(matrixmult3,4) ;(matrixmultp,4) ;(matrixmultp0,4) ;(matrixmultp1,4) ;(mkBase,4) ;(mult,4) ;(out1makeBase,4) ;(out1split,4) ;(out1transAcc,4) ;(out2split,4) ;(out2transAcc,4) ;(out3split,4) ;(outmkBase,4) ;(split,4) ;(start,4) ;(transAcc,4) ;(transAcc0,4) ;(transAcc1,4) ;(transpose,4) ;(transpose0,4) ;(transpose1,4)} Flow Graph: [9->{9},11->{11},25->{25},30->{40},37->{9,37},38->{38,39},39->{25,39},40->{11,37,38}] Sizebounds: (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (<11,0,A>, A) (<11,0,B>, A + 3*C) (<11,0,C>, 1 + A + C) (<11,0,D>, C) (<25,0,A>, ?) (<25,0,B>, ?) (<25,0,C>, ?) (<25,0,D>, ?) (<30,0,A>, A) (<30,0,B>, B) (<30,0,C>, C) (<30,0,D>, D) (<37,0,A>, ?) (<37,0,B>, ?) (<37,0,C>, ?) (<37,0,D>, ?) (<37,1,A>, ?) (<37,1,B>, ?) (<37,1,C>, ?) (<37,1,D>, ?) (<38,0,A>, ?) (<38,0,B>, ?) (<38,0,C>, ?) (<38,0,D>, ?) (<38,1,A>, ?) (<38,1,B>, ?) (<38,1,C>, ?) (<38,1,D>, ?) (<39,0,A>, ?) (<39,0,B>, ?) (<39,0,C>, ?) (<39,0,D>, ?) (<39,1,A>, ?) (<39,1,B>, ?) (<39,1,C>, ?) (<39,1,D>, ?) (<40,0,A>, A) (<40,0,B>, A) (<40,0,C>, 0) (<40,0,D>, C) (<40,1,A>, A) (<40,1,B>, A) (<40,1,C>, 1 + A + C) (<40,1,D>, 0) (<40,2,A>, A) (<40,2,B>, C) (<40,2,C>, 0) (<40,2,D>, C) + Applied Processor: UnsatPaths + Details: The problem is already solved. WORST_CASE(?,O(n^2))