MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , attach(@line, @m) -> attach#1(@line, @m) , attach#1(::(@x, @xs), @m) -> attach#2(@m, @x, @xs) , attach#1(nil(), @m) -> nil() , attach#2(::(@l, @ls), @x, @xs) -> ::(::(@x, @l), attach(@xs, @ls)) , attach#2(nil(), @x, @xs) -> nil() , lineMult(@l, @m2) -> lineMult#1(@m2, @l) , lineMult#1(::(@x, @xs), @l) -> ::(mult(@l, @x), lineMult(@l, @xs)) , lineMult#1(nil(), @l) -> nil() , mult(@l1, @l2) -> mult#1(@l1, @l2) , makeBase(@m) -> makeBase#1(@m) , makeBase#1(::(@l, @m')) -> mkBase(@l) , makeBase#1(nil()) -> nil() , mkBase(@m) -> mkBase#1(@m) , matrixMult(@m1, @m2) -> matrixMult'(@m1, transAcc(@m2, makeBase(@m2))) , transAcc(@m, @base) -> transAcc#1(@m, @base) , matrixMult'(@m1, @m2) -> matrixMult'#1(@m1, @m2) , matrixMult'#1(::(@l, @ls), @m2) -> ::(lineMult(@l, @m2), matrixMult'(@ls, @m2)) , matrixMult'#1(nil(), @m2) -> nil() , matrixMult3(@m1, @m2, @m3) -> matrixMult(matrixMult(@m1, @m2), @m3) , matrixMultList(@acc, @mm) -> matrixMultList#1(@mm, @acc) , matrixMultList#1(::(@m, @ms), @acc) -> matrixMultList(matrixMult(@acc, @m), @ms) , matrixMultList#1(nil(), @acc) -> @acc , matrixMultOld(@m1, @m2) -> matrixMult'(@m1, transpose(@m2)) , transpose(@m) -> transpose#1(@m, @m) , mkBase#1(::(@l, @m')) -> ::(nil(), mkBase(@m')) , mkBase#1(nil()) -> nil() , mult#1(::(@x, @xs), @l2) -> mult#2(@l2, @x, @xs) , mult#1(nil(), @l2) -> #abs(#0()) , mult#2(::(@y, @ys), @x, @xs) -> +(*(@x, @y), mult(@xs, @ys)) , mult#2(nil(), @x, @xs) -> #abs(#0()) , split(@m) -> split#1(@m) , split#1(::(@l, @ls)) -> split#2(@l, @ls) , split#1(nil()) -> tuple#2(nil(), nil()) , split#2(::(@x, @xs), @ls) -> split#3(split(@ls), @x, @xs) , split#2(nil(), @ls) -> tuple#2(nil(), nil()) , split#3(tuple#2(@ys, @m'), @x, @xs) -> tuple#2(::(@x, @ys), ::(@xs, @m')) , transAcc#1(::(@l, @m'), @base) -> attach(@l, transAcc(@m', @base)) , transAcc#1(nil(), @base) -> @base , transpose#1(::(@xs, @xss), @m) -> transpose#2(split(@m)) , transpose#1(nil(), @m) -> nil() , transpose#2(tuple#2(@l, @m')) -> transpose#3(@m', @l) , transpose#3(::(@y, @ys), @l) -> ::(@l, transpose(::(@y, @ys))) , transpose#3(nil(), @l) -> nil() , transpose'(@m) -> transAcc(@m, makeBase(@m)) } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { matrixMult3(@m1, @m2, @m3) -> matrixMult(matrixMult(@m1, @m2), @m3) , matrixMultList#1(nil(), @acc) -> @acc , transpose#1(nil(), @m) -> nil() , transpose#3(nil(), @l) -> nil() , transpose'(@m) -> transAcc(@m, makeBase(@m)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(#neg) = {1}, Uargs(#pos) = {1}, Uargs(#s) = {1}, Uargs(+) = {1, 2}, Uargs(attach) = {2}, Uargs(::) = {1, 2}, Uargs(matrixMult) = {1}, Uargs(transAcc) = {2}, Uargs(matrixMult') = {2}, Uargs(matrixMultList) = {1}, Uargs(split#3) = {1}, Uargs(transpose#2) = {1}, Uargs(#pred) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#abs](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#s](x1) = [1] x1 + [0] [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [2] x1 + [1] x2 + [0] [attach](x1, x2) = [1] x1 + [1] x2 + [0] [attach#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [attach#2](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [nil] = [0] [lineMult](x1, x2) = [0] [lineMult#1](x1, x2) = [0] [mult](x1, x2) = [0] [makeBase](x1) = [0] [makeBase#1](x1) = [0] [mkBase](x1) = [0] [matrixMult](x1, x2) = [1] x1 + [1] x2 + [0] [transAcc](x1, x2) = [1] x1 + [1] x2 + [0] [matrixMult'](x1, x2) = [1] x1 + [1] x2 + [0] [matrixMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [matrixMult3](x1, x2, x3) = [1] x1 + [2] x2 + [2] x3 + [1] [matrixMultList](x1, x2) = [1] x1 + [2] x2 + [2] [matrixMultList#1](x1, x2) = [2] x1 + [1] x2 + [2] [matrixMultOld](x1, x2) = [1] x1 + [2] x2 + [2] [transpose](x1) = [2] x1 + [2] [mkBase#1](x1) = [0] [mult#1](x1, x2) = [0] [mult#2](x1, x2, x3) = [0] [split](x1) = [1] x1 + [1] [split#1](x1) = [1] x1 + [1] [split#2](x1, x2) = [1] x1 + [1] x2 + [1] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [1] [split#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [transAcc#1](x1, x2) = [1] x1 + [1] x2 + [0] [transpose#1](x1, x2) = [2] x2 + [2] [transpose#2](x1) = [2] x1 + [0] [transpose#3](x1, x2) = [2] x1 + [1] x2 + [2] [transpose'](x1) = [2] x1 + [1] [#pred](x1) = [1] x1 + [0] [#succ](x1) = [1] x1 + [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [2] x2 + [0] This order satisfies following ordering constraints [#abs(#0())] = [0] >= [0] = [#0()] [#abs(#neg(@x))] = [1] @x + [0] >= [1] @x + [0] = [#pos(@x)] [#abs(#pos(@x))] = [1] @x + [0] >= [1] @x + [0] = [#pos(@x)] [#abs(#s(@x))] = [1] @x + [0] >= [1] @x + [0] = [#pos(#s(@x))] [*(@x, @y)] = [0] >= [0] = [#mult(@x, @y)] [#mult(#0(), #0())] = [0] >= [0] = [#0()] [#mult(#0(), #neg(@y))] = [0] >= [0] = [#0()] [#mult(#0(), #pos(@y))] = [0] >= [0] = [#0()] [#mult(#neg(@x), #0())] = [0] >= [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [0] >= [0] = [#pos(#natmult(@x, @y))] [#mult(#neg(@x), #pos(@y))] = [0] >= [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [0] >= [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [0] >= [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #pos(@y))] = [0] >= [0] = [#pos(#natmult(@x, @y))] [+(@x, @y)] = [2] @x + [1] @y + [0] >= [2] @x + [1] @y + [0] = [#add(@x, @y)] [#add(#0(), @y)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [2] @x + [1] @y + [0] >= [2] @x + [1] @y + [0] = [#pred(#add(#pos(#s(@x)), @y))] [#add(#pos(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [2] @x + [1] @y + [0] >= [2] @x + [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [attach(@line, @m)] = [1] @line + [1] @m + [0] >= [1] @line + [1] @m + [0] = [attach#1(@line, @m)] [attach#1(::(@x, @xs), @m)] = [1] @m + [1] @x + [1] @xs + [0] >= [1] @m + [1] @x + [1] @xs + [0] = [attach#2(@m, @x, @xs)] [attach#1(nil(), @m)] = [1] @m + [0] >= [0] = [nil()] [attach#2(::(@l, @ls), @x, @xs)] = [1] @l + [1] @ls + [1] @x + [1] @xs + [0] >= [1] @l + [1] @ls + [1] @x + [1] @xs + [0] = [::(::(@x, @l), attach(@xs, @ls))] [attach#2(nil(), @x, @xs)] = [1] @x + [1] @xs + [0] >= [0] = [nil()] [lineMult(@l, @m2)] = [0] >= [0] = [lineMult#1(@m2, @l)] [lineMult#1(::(@x, @xs), @l)] = [0] >= [0] = [::(mult(@l, @x), lineMult(@l, @xs))] [lineMult#1(nil(), @l)] = [0] >= [0] = [nil()] [mult(@l1, @l2)] = [0] >= [0] = [mult#1(@l1, @l2)] [makeBase(@m)] = [0] >= [0] = [makeBase#1(@m)] [makeBase#1(::(@l, @m'))] = [0] >= [0] = [mkBase(@l)] [makeBase#1(nil())] = [0] >= [0] = [nil()] [mkBase(@m)] = [0] >= [0] = [mkBase#1(@m)] [matrixMult(@m1, @m2)] = [1] @m1 + [1] @m2 + [0] >= [1] @m1 + [1] @m2 + [0] = [matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))] [transAcc(@m, @base)] = [1] @base + [1] @m + [0] >= [1] @base + [1] @m + [0] = [transAcc#1(@m, @base)] [matrixMult'(@m1, @m2)] = [1] @m1 + [1] @m2 + [0] >= [1] @m1 + [1] @m2 + [0] = [matrixMult'#1(@m1, @m2)] [matrixMult'#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [1] @m2 + [0] >= [1] @ls + [1] @m2 + [0] = [::(lineMult(@l, @m2), matrixMult'(@ls, @m2))] [matrixMult'#1(nil(), @m2)] = [1] @m2 + [0] >= [0] = [nil()] [matrixMult3(@m1, @m2, @m3)] = [1] @m1 + [2] @m2 + [2] @m3 + [1] > [1] @m1 + [1] @m2 + [1] @m3 + [0] = [matrixMult(matrixMult(@m1, @m2), @m3)] [matrixMultList(@acc, @mm)] = [1] @acc + [2] @mm + [2] >= [1] @acc + [2] @mm + [2] = [matrixMultList#1(@mm, @acc)] [matrixMultList#1(::(@m, @ms), @acc)] = [1] @acc + [2] @m + [2] @ms + [2] >= [1] @acc + [1] @m + [2] @ms + [2] = [matrixMultList(matrixMult(@acc, @m), @ms)] [matrixMultList#1(nil(), @acc)] = [1] @acc + [2] > [1] @acc + [0] = [@acc] [matrixMultOld(@m1, @m2)] = [1] @m1 + [2] @m2 + [2] >= [1] @m1 + [2] @m2 + [2] = [matrixMult'(@m1, transpose(@m2))] [transpose(@m)] = [2] @m + [2] >= [2] @m + [2] = [transpose#1(@m, @m)] [mkBase#1(::(@l, @m'))] = [0] >= [0] = [::(nil(), mkBase(@m'))] [mkBase#1(nil())] = [0] >= [0] = [nil()] [mult#1(::(@x, @xs), @l2)] = [0] >= [0] = [mult#2(@l2, @x, @xs)] [mult#1(nil(), @l2)] = [0] >= [0] = [#abs(#0())] [mult#2(::(@y, @ys), @x, @xs)] = [0] >= [0] = [+(*(@x, @y), mult(@xs, @ys))] [mult#2(nil(), @x, @xs)] = [0] >= [0] = [#abs(#0())] [split(@m)] = [1] @m + [1] >= [1] @m + [1] = [split#1(@m)] [split#1(::(@l, @ls))] = [1] @l + [1] @ls + [1] >= [1] @l + [1] @ls + [1] = [split#2(@l, @ls)] [split#1(nil())] = [1] >= [1] = [tuple#2(nil(), nil())] [split#2(::(@x, @xs), @ls)] = [1] @ls + [1] @x + [1] @xs + [1] >= [1] @ls + [1] @x + [1] @xs + [1] = [split#3(split(@ls), @x, @xs)] [split#2(nil(), @ls)] = [1] @ls + [1] >= [1] = [tuple#2(nil(), nil())] [split#3(tuple#2(@ys, @m'), @x, @xs)] = [1] @m' + [1] @x + [1] @xs + [1] @ys + [1] >= [1] @m' + [1] @x + [1] @xs + [1] @ys + [1] = [tuple#2(::(@x, @ys), ::(@xs, @m'))] [transAcc#1(::(@l, @m'), @base)] = [1] @base + [1] @l + [1] @m' + [0] >= [1] @base + [1] @l + [1] @m' + [0] = [attach(@l, transAcc(@m', @base))] [transAcc#1(nil(), @base)] = [1] @base + [0] >= [1] @base + [0] = [@base] [transpose#1(::(@xs, @xss), @m)] = [2] @m + [2] >= [2] @m + [2] = [transpose#2(split(@m))] [transpose#1(nil(), @m)] = [2] @m + [2] > [0] = [nil()] [transpose#2(tuple#2(@l, @m'))] = [2] @l + [2] @m' + [2] >= [1] @l + [2] @m' + [2] = [transpose#3(@m', @l)] [transpose#3(::(@y, @ys), @l)] = [1] @l + [2] @y + [2] @ys + [2] >= [1] @l + [2] @y + [2] @ys + [2] = [::(@l, transpose(::(@y, @ys)))] [transpose#3(nil(), @l)] = [1] @l + [2] > [0] = [nil()] [transpose'(@m)] = [2] @m + [1] > [1] @m + [0] = [transAcc(@m, makeBase(@m))] [#pred(#0())] = [0] >= [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [1] @x + [0] >= [1] @x + [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [0] >= [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [1] @x + [0] >= [1] @x + [0] = [#pos(#s(@x))] [#succ(#0())] = [0] >= [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] >= [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [1] @x + [0] >= [1] @x + [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [1] @x + [0] >= [1] @x + [0] = [#pos(#s(#s(@x)))] [#natmult(#0(), @y)] = [0] >= [0] = [#0()] [#natmult(#s(@x), @y)] = [0] >= [0] = [#natadd(@y, #natmult(@x, @y))] [#natadd(#0(), @y)] = [2] @y + [0] >= [1] @y + [0] = [@y] [#natadd(#s(@x), @y)] = [2] @y + [0] >= [2] @y + [0] = [#s(#natadd(@x, @y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , attach(@line, @m) -> attach#1(@line, @m) , attach#1(::(@x, @xs), @m) -> attach#2(@m, @x, @xs) , attach#1(nil(), @m) -> nil() , attach#2(::(@l, @ls), @x, @xs) -> ::(::(@x, @l), attach(@xs, @ls)) , attach#2(nil(), @x, @xs) -> nil() , lineMult(@l, @m2) -> lineMult#1(@m2, @l) , lineMult#1(::(@x, @xs), @l) -> ::(mult(@l, @x), lineMult(@l, @xs)) , lineMult#1(nil(), @l) -> nil() , mult(@l1, @l2) -> mult#1(@l1, @l2) , makeBase(@m) -> makeBase#1(@m) , makeBase#1(::(@l, @m')) -> mkBase(@l) , makeBase#1(nil()) -> nil() , mkBase(@m) -> mkBase#1(@m) , matrixMult(@m1, @m2) -> matrixMult'(@m1, transAcc(@m2, makeBase(@m2))) , transAcc(@m, @base) -> transAcc#1(@m, @base) , matrixMult'(@m1, @m2) -> matrixMult'#1(@m1, @m2) , matrixMult'#1(::(@l, @ls), @m2) -> ::(lineMult(@l, @m2), matrixMult'(@ls, @m2)) , matrixMult'#1(nil(), @m2) -> nil() , matrixMultList(@acc, @mm) -> matrixMultList#1(@mm, @acc) , matrixMultList#1(::(@m, @ms), @acc) -> matrixMultList(matrixMult(@acc, @m), @ms) , matrixMultOld(@m1, @m2) -> matrixMult'(@m1, transpose(@m2)) , transpose(@m) -> transpose#1(@m, @m) , mkBase#1(::(@l, @m')) -> ::(nil(), mkBase(@m')) , mkBase#1(nil()) -> nil() , mult#1(::(@x, @xs), @l2) -> mult#2(@l2, @x, @xs) , mult#1(nil(), @l2) -> #abs(#0()) , mult#2(::(@y, @ys), @x, @xs) -> +(*(@x, @y), mult(@xs, @ys)) , mult#2(nil(), @x, @xs) -> #abs(#0()) , split(@m) -> split#1(@m) , split#1(::(@l, @ls)) -> split#2(@l, @ls) , split#1(nil()) -> tuple#2(nil(), nil()) , split#2(::(@x, @xs), @ls) -> split#3(split(@ls), @x, @xs) , split#2(nil(), @ls) -> tuple#2(nil(), nil()) , split#3(tuple#2(@ys, @m'), @x, @xs) -> tuple#2(::(@x, @ys), ::(@xs, @m')) , transAcc#1(::(@l, @m'), @base) -> attach(@l, transAcc(@m', @base)) , transAcc#1(nil(), @base) -> @base , transpose#1(::(@xs, @xss), @m) -> transpose#2(split(@m)) , transpose#2(tuple#2(@l, @m')) -> transpose#3(@m', @l) , transpose#3(::(@y, @ys), @l) -> ::(@l, transpose(::(@y, @ys))) } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , matrixMult3(@m1, @m2, @m3) -> matrixMult(matrixMult(@m1, @m2), @m3) , matrixMultList#1(nil(), @acc) -> @acc , transpose#1(nil(), @m) -> nil() , transpose#3(nil(), @l) -> nil() , transpose'(@m) -> transAcc(@m, makeBase(@m)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { matrixMultOld(@m1, @m2) -> matrixMult'(@m1, transpose(@m2)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(#neg) = {1}, Uargs(#pos) = {1}, Uargs(#s) = {1}, Uargs(+) = {1, 2}, Uargs(attach) = {2}, Uargs(::) = {1, 2}, Uargs(matrixMult) = {1}, Uargs(transAcc) = {2}, Uargs(matrixMult') = {2}, Uargs(matrixMultList) = {1}, Uargs(split#3) = {1}, Uargs(transpose#2) = {1}, Uargs(#pred) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#abs](x1) = [2] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#s](x1) = [1] x1 + [0] [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [2] x1 + [1] x2 + [0] [attach](x1, x2) = [1] x1 + [1] x2 + [0] [attach#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [attach#2](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [nil] = [0] [lineMult](x1, x2) = [0] [lineMult#1](x1, x2) = [0] [mult](x1, x2) = [0] [makeBase](x1) = [0] [makeBase#1](x1) = [0] [mkBase](x1) = [0] [matrixMult](x1, x2) = [1] x1 + [2] x2 + [0] [transAcc](x1, x2) = [1] x1 + [2] x2 + [0] [matrixMult'](x1, x2) = [1] x1 + [2] x2 + [0] [matrixMult'#1](x1, x2) = [1] x1 + [2] x2 + [0] [matrixMult3](x1, x2, x3) = [1] x1 + [2] x2 + [2] x3 + [1] [matrixMultList](x1, x2) = [1] x1 + [2] x2 + [2] [matrixMultList#1](x1, x2) = [2] x1 + [1] x2 + [2] [matrixMultOld](x1, x2) = [1] x1 + [2] x2 + [2] [transpose](x1) = [1] x1 + [0] [mkBase#1](x1) = [0] [mult#1](x1, x2) = [0] [mult#2](x1, x2, x3) = [0] [split](x1) = [1] x1 + [0] [split#1](x1) = [1] x1 + [0] [split#2](x1, x2) = [1] x1 + [1] x2 + [0] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [split#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [transAcc#1](x1, x2) = [1] x1 + [2] x2 + [0] [transpose#1](x1, x2) = [1] x2 + [0] [transpose#2](x1) = [1] x1 + [0] [transpose#3](x1, x2) = [1] x1 + [1] x2 + [0] [transpose'](x1) = [1] x1 + [2] [#pred](x1) = [1] x1 + [0] [#succ](x1) = [1] x1 + [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [2] x2 + [0] This order satisfies following ordering constraints [#abs(#0())] = [0] >= [0] = [#0()] [#abs(#neg(@x))] = [2] @x + [0] >= [1] @x + [0] = [#pos(@x)] [#abs(#pos(@x))] = [2] @x + [0] >= [1] @x + [0] = [#pos(@x)] [#abs(#s(@x))] = [2] @x + [0] >= [1] @x + [0] = [#pos(#s(@x))] [*(@x, @y)] = [0] >= [0] = [#mult(@x, @y)] [#mult(#0(), #0())] = [0] >= [0] = [#0()] [#mult(#0(), #neg(@y))] = [0] >= [0] = [#0()] [#mult(#0(), #pos(@y))] = [0] >= [0] = [#0()] [#mult(#neg(@x), #0())] = [0] >= [0] = [#0()] [#mult(#neg(@x), #neg(@y))] = [0] >= [0] = [#pos(#natmult(@x, @y))] [#mult(#neg(@x), #pos(@y))] = [0] >= [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #0())] = [0] >= [0] = [#0()] [#mult(#pos(@x), #neg(@y))] = [0] >= [0] = [#neg(#natmult(@x, @y))] [#mult(#pos(@x), #pos(@y))] = [0] >= [0] = [#pos(#natmult(@x, @y))] [+(@x, @y)] = [2] @x + [1] @y + [0] >= [2] @x + [1] @y + [0] = [#add(@x, @y)] [#add(#0(), @y)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [2] @x + [1] @y + [0] >= [2] @x + [1] @y + [0] = [#pred(#add(#pos(#s(@x)), @y))] [#add(#pos(#s(#0())), @y)] = [1] @y + [0] >= [1] @y + [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [2] @x + [1] @y + [0] >= [2] @x + [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [attach(@line, @m)] = [1] @line + [1] @m + [0] >= [1] @line + [1] @m + [0] = [attach#1(@line, @m)] [attach#1(::(@x, @xs), @m)] = [1] @m + [1] @x + [1] @xs + [0] >= [1] @m + [1] @x + [1] @xs + [0] = [attach#2(@m, @x, @xs)] [attach#1(nil(), @m)] = [1] @m + [0] >= [0] = [nil()] [attach#2(::(@l, @ls), @x, @xs)] = [1] @l + [1] @ls + [1] @x + [1] @xs + [0] >= [1] @l + [1] @ls + [1] @x + [1] @xs + [0] = [::(::(@x, @l), attach(@xs, @ls))] [attach#2(nil(), @x, @xs)] = [1] @x + [1] @xs + [0] >= [0] = [nil()] [lineMult(@l, @m2)] = [0] >= [0] = [lineMult#1(@m2, @l)] [lineMult#1(::(@x, @xs), @l)] = [0] >= [0] = [::(mult(@l, @x), lineMult(@l, @xs))] [lineMult#1(nil(), @l)] = [0] >= [0] = [nil()] [mult(@l1, @l2)] = [0] >= [0] = [mult#1(@l1, @l2)] [makeBase(@m)] = [0] >= [0] = [makeBase#1(@m)] [makeBase#1(::(@l, @m'))] = [0] >= [0] = [mkBase(@l)] [makeBase#1(nil())] = [0] >= [0] = [nil()] [mkBase(@m)] = [0] >= [0] = [mkBase#1(@m)] [matrixMult(@m1, @m2)] = [1] @m1 + [2] @m2 + [0] >= [1] @m1 + [2] @m2 + [0] = [matrixMult'(@m1, transAcc(@m2, makeBase(@m2)))] [transAcc(@m, @base)] = [2] @base + [1] @m + [0] >= [2] @base + [1] @m + [0] = [transAcc#1(@m, @base)] [matrixMult'(@m1, @m2)] = [1] @m1 + [2] @m2 + [0] >= [1] @m1 + [2] @m2 + [0] = [matrixMult'#1(@m1, @m2)] [matrixMult'#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [2] @m2 + [0] >= [1] @ls + [2] @m2 + [0] = [::(lineMult(@l, @m2), matrixMult'(@ls, @m2))] [matrixMult'#1(nil(), @m2)] = [2] @m2 + [0] >= [0] = [nil()] [matrixMult3(@m1, @m2, @m3)] = [1] @m1 + [2] @m2 + [2] @m3 + [1] > [1] @m1 + [2] @m2 + [2] @m3 + [0] = [matrixMult(matrixMult(@m1, @m2), @m3)] [matrixMultList(@acc, @mm)] = [1] @acc + [2] @mm + [2] >= [1] @acc + [2] @mm + [2] = [matrixMultList#1(@mm, @acc)] [matrixMultList#1(::(@m, @ms), @acc)] = [1] @acc + [2] @m + [2] @ms + [2] >= [1] @acc + [2] @m + [2] @ms + [2] = [matrixMultList(matrixMult(@acc, @m), @ms)] [matrixMultList#1(nil(), @acc)] = [1] @acc + [2] > [1] @acc + [0] = [@acc] [matrixMultOld(@m1, @m2)] = [1] @m1 + [2] @m2 + [2] > [1] @m1 + [2] @m2 + [0] = [matrixMult'(@m1, transpose(@m2))] [transpose(@m)] = [1] @m + [0] >= [1] @m + [0] = [transpose#1(@m, @m)] [mkBase#1(::(@l, @m'))] = [0] >= [0] = [::(nil(), mkBase(@m'))] [mkBase#1(nil())] = [0] >= [0] = [nil()] [mult#1(::(@x, @xs), @l2)] = [0] >= [0] = [mult#2(@l2, @x, @xs)] [mult#1(nil(), @l2)] = [0] >= [0] = [#abs(#0())] [mult#2(::(@y, @ys), @x, @xs)] = [0] >= [0] = [+(*(@x, @y), mult(@xs, @ys))] [mult#2(nil(), @x, @xs)] = [0] >= [0] = [#abs(#0())] [split(@m)] = [1] @m + [0] >= [1] @m + [0] = [split#1(@m)] [split#1(::(@l, @ls))] = [1] @l + [1] @ls + [0] >= [1] @l + [1] @ls + [0] = [split#2(@l, @ls)] [split#1(nil())] = [0] >= [0] = [tuple#2(nil(), nil())] [split#2(::(@x, @xs), @ls)] = [1] @ls + [1] @x + [1] @xs + [0] >= [1] @ls + [1] @x + [1] @xs + [0] = [split#3(split(@ls), @x, @xs)] [split#2(nil(), @ls)] = [1] @ls + [0] >= [0] = [tuple#2(nil(), nil())] [split#3(tuple#2(@ys, @m'), @x, @xs)] = [1] @m' + [1] @x + [1] @xs + [1] @ys + [0] >= [1] @m' + [1] @x + [1] @xs + [1] @ys + [0] = [tuple#2(::(@x, @ys), ::(@xs, @m'))] [transAcc#1(::(@l, @m'), @base)] = [2] @base + [1] @l + [1] @m' + [0] >= [2] @base + [1] @l + [1] @m' + [0] = [attach(@l, transAcc(@m', @base))] [transAcc#1(nil(), @base)] = [2] @base + [0] >= [1] @base + [0] = [@base] [transpose#1(::(@xs, @xss), @m)] = [1] @m + [0] >= [1] @m + [0] = [transpose#2(split(@m))] [transpose#1(nil(), @m)] = [1] @m + [0] >= [0] = [nil()] [transpose#2(tuple#2(@l, @m'))] = [1] @l + [1] @m' + [0] >= [1] @l + [1] @m' + [0] = [transpose#3(@m', @l)] [transpose#3(::(@y, @ys), @l)] = [1] @l + [1] @y + [1] @ys + [0] >= [1] @l + [1] @y + [1] @ys + [0] = [::(@l, transpose(::(@y, @ys)))] [transpose#3(nil(), @l)] = [1] @l + [0] >= [0] = [nil()] [transpose'(@m)] = [1] @m + [2] > [1] @m + [0] = [transAcc(@m, makeBase(@m))] [#pred(#0())] = [0] >= [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [1] @x + [0] >= [1] @x + [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [0] >= [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [1] @x + [0] >= [1] @x + [0] = [#pos(#s(@x))] [#succ(#0())] = [0] >= [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [0] >= [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [1] @x + [0] >= [1] @x + [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [1] @x + [0] >= [1] @x + [0] = [#pos(#s(#s(@x)))] [#natmult(#0(), @y)] = [0] >= [0] = [#0()] [#natmult(#s(@x), @y)] = [0] >= [0] = [#natadd(@y, #natmult(@x, @y))] [#natadd(#0(), @y)] = [2] @y + [0] >= [1] @y + [0] = [@y] [#natadd(#s(@x), @y)] = [2] @y + [0] >= [2] @y + [0] = [#s(#natadd(@x, @y))] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , attach(@line, @m) -> attach#1(@line, @m) , attach#1(::(@x, @xs), @m) -> attach#2(@m, @x, @xs) , attach#1(nil(), @m) -> nil() , attach#2(::(@l, @ls), @x, @xs) -> ::(::(@x, @l), attach(@xs, @ls)) , attach#2(nil(), @x, @xs) -> nil() , lineMult(@l, @m2) -> lineMult#1(@m2, @l) , lineMult#1(::(@x, @xs), @l) -> ::(mult(@l, @x), lineMult(@l, @xs)) , lineMult#1(nil(), @l) -> nil() , mult(@l1, @l2) -> mult#1(@l1, @l2) , makeBase(@m) -> makeBase#1(@m) , makeBase#1(::(@l, @m')) -> mkBase(@l) , makeBase#1(nil()) -> nil() , mkBase(@m) -> mkBase#1(@m) , matrixMult(@m1, @m2) -> matrixMult'(@m1, transAcc(@m2, makeBase(@m2))) , transAcc(@m, @base) -> transAcc#1(@m, @base) , matrixMult'(@m1, @m2) -> matrixMult'#1(@m1, @m2) , matrixMult'#1(::(@l, @ls), @m2) -> ::(lineMult(@l, @m2), matrixMult'(@ls, @m2)) , matrixMult'#1(nil(), @m2) -> nil() , matrixMultList(@acc, @mm) -> matrixMultList#1(@mm, @acc) , matrixMultList#1(::(@m, @ms), @acc) -> matrixMultList(matrixMult(@acc, @m), @ms) , transpose(@m) -> transpose#1(@m, @m) , mkBase#1(::(@l, @m')) -> ::(nil(), mkBase(@m')) , mkBase#1(nil()) -> nil() , mult#1(::(@x, @xs), @l2) -> mult#2(@l2, @x, @xs) , mult#1(nil(), @l2) -> #abs(#0()) , mult#2(::(@y, @ys), @x, @xs) -> +(*(@x, @y), mult(@xs, @ys)) , mult#2(nil(), @x, @xs) -> #abs(#0()) , split(@m) -> split#1(@m) , split#1(::(@l, @ls)) -> split#2(@l, @ls) , split#1(nil()) -> tuple#2(nil(), nil()) , split#2(::(@x, @xs), @ls) -> split#3(split(@ls), @x, @xs) , split#2(nil(), @ls) -> tuple#2(nil(), nil()) , split#3(tuple#2(@ys, @m'), @x, @xs) -> tuple#2(::(@x, @ys), ::(@xs, @m')) , transAcc#1(::(@l, @m'), @base) -> attach(@l, transAcc(@m', @base)) , transAcc#1(nil(), @base) -> @base , transpose#1(::(@xs, @xss), @m) -> transpose#2(split(@m)) , transpose#2(tuple#2(@l, @m')) -> transpose#3(@m', @l) , transpose#3(::(@y, @ys), @l) -> ::(@l, transpose(::(@y, @ys))) } Weak Trs: { #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , matrixMult3(@m1, @m2, @m3) -> matrixMult(matrixMult(@m1, @m2), @m3) , matrixMultList#1(nil(), @acc) -> @acc , matrixMultOld(@m1, @m2) -> matrixMult'(@m1, transpose(@m2)) , transpose#1(nil(), @m) -> nil() , transpose#3(nil(), @l) -> nil() , transpose'(@m) -> transAcc(@m, makeBase(@m)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..