MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) , matrixMult#1(nil(), @m2) -> nil() } 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: { bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , matrixMult#1(nil(), @m2) -> nil() } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [2] x1 + [2] x2 + [1] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [2] x1 + [2] x2 + [0] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [2] x1 + [2] x2 + [0] [bftMult'#3](x1, x2, x3) = [2] x1 + [2] x2 + [2] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [2] x1 + [2] x2 + [2] x3 + [0] [leaf] = [0] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [2] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [1] [computeLine](x1, x2, x3) = [1] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [1] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [2] @t + [1] > [2] @acc + [2] @t + [0] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [2] @acc + [2] @queue + [0] >= [2] @acc + [2] @queue + [0] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [2] @acc + [2] @elem + [2] @queue + [0] >= [2] @acc + [2] @elem + [2] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [2] @_@3 + [2] @acc + [2] @queue + [2] @t + [0] >= [2] @acc + [2] @queue + [2] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [2] @acc + [2] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [2] @acc + [2] @queue + [0] >= [2] @acc + [2] @queue + [0] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [2] @acc + [2] @queue + [2] @t1 + [2] @t2 + [2] @y + [4] > [1] @acc + [2] @queue + [2] @t1 + [2] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [2] @queue' + [2] >= [2] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] >= [1] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [1] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] >= [1] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [1] > [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , matrixMult#1(nil(), @m2) -> nil() , #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: { bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [2] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [2] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [0] [computeLine](x1, x2, x3) = [1] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [1] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [0] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [2] >= [1] @acc + [1] @t + [2] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [2] > [1] @acc + [1] @queue + [0] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [0] >= [1] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [0] >= [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [2] >= [1] @acc + [1] @queue + [2] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [2] >= [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [0] >= [0] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [1] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [0] >= [0] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [0] >= [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , matrixMult#1(nil(), @m2) -> nil() , #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: { bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [1] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [0] [matrixMult](x1, x2) = [0] [computeLine](x1, x2, x3) = [2] x3 + [0] [computeLine#1](x1, x2, x3) = [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [0] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [2] > [1] @acc + [1] @t + [0] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [1] @queue + [0] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [0] >= [1] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [0] >= [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [1] > [1] @acc + [1] @queue + [0] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [0] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [0] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [0] >= [1] @queue' + [0] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [0] >= [0] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [0] >= [0] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [0] >= [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , matrixMult#1(nil(), @m2) -> nil() , #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: { enqueue(@t, @queue) -> enqueue#1(@queue, @t) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [2] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [2] x1 + [1] x2 + [0] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [2] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [2] x1 + [1] x2 + [2] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [2] x1 + [1] x2 + [2] x3 + [0] [leaf] = [0] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#5](x1, x2, x3) = [2] x1 + [1] x2 + [0] [matrixMult](x1, x2) = [0] [computeLine](x1, x2, x3) = [2] x3 + [0] [computeLine#1](x1, x2, x3) = [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [0] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [2] @t + [2] > [1] @acc + [2] @t + [0] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [2] @queue + [0] >= [1] @acc + [2] @queue + [0] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [2] @elem + [2] @queue + [0] >= [1] @acc + [2] @elem + [2] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [2] @_@3 + [1] @acc + [2] @queue + [2] @t + [0] >= [1] @acc + [2] @queue + [2] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [2] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [2] @queue + [0] >= [1] @acc + [2] @queue + [0] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [2] @queue + [2] @t1 + [2] @t2 + [2] @y + [4] >= [1] @acc + [2] @queue + [2] @t1 + [2] @t2 + [4] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [1] > [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [2] @queue' + [0] >= [2] @queue' + [0] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [0] >= [0] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [0] >= [0] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [0] >= [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , matrixMult#1(nil(), @m2) -> nil() , #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: { bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [2] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [0] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [1] [matrixMult](x1, x2) = [0] [computeLine](x1, x2, x3) = [2] x3 + [0] [computeLine#1](x1, x2, x3) = [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [0] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [2] @t + [2] > [1] @acc + [1] @t + [0] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [1] @queue + [0] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [0] >= [1] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [0] >= [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [1] @queue + [0] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [1] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [1] > [1] @queue' + [0] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [0] >= [0] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [0] >= [0] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [0] >= [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , matrixMult#1(nil(), @m2) -> nil() , #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: { dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [1] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [2] x2 + [2] [bftMult'#2](x1) = [1] x1 + [1] [bftMult'#1](x1, x2) = [1] x1 + [2] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#4](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [0] [leaf] = [2] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [0] [computeLine](x1, x2, x3) = [2] x3 + [0] [computeLine#1](x1, x2, x3) = [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [1] [reverse](x1) = [1] x1 + [1] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [0] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#succ](x1) = [1] x1 + [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [1] x2 + [0] This order satisfies following ordering constraints [*(@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)] = [1] @x + [1] @y + [0] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [2] >= [2] @acc + [1] @t + [2] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [2] @acc + [1] @queue + [2] > [2] @acc + [1] @queue + [1] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [1] >= [1] @dequeue@1 + [1] @dequeue@2 + [1] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [2] @acc + [1] @elem + [1] @queue + [0] >= [2] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [2] @acc + [1] @queue + [1] @t + [0] >= [2] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [2] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [1] >= [1] @inq + [1] @outq + [1] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [2] @acc + [1] @queue + [2] >= [2] @acc + [1] @queue + [2] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [2] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [2] >= [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [0] >= [0] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [1] > [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [1] >= [1] @inq + [1] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [1] > [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [0] >= [0] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [0] >= [0] = [nil()] [#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)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#natadd(#s(@x), @y)] = [1] @y + [0] >= [1] @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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , matrixMult#1(nil(), @m2) -> nil() , #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: { enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [2] x2 + [0] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [1] x1 + [2] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [0] [leaf] = [0] [node](x1, x2, x3) = [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [0] [matrixMult](x1, x2) = [0] [computeLine](x1, x2, x3) = [2] x3 + [0] [computeLine#1](x1, x2, x3) = [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [1] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [0] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [2] > [2] @acc + [1] @t + [0] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [2] @acc + [1] @queue + [0] >= [2] @acc + [1] @queue + [0] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [2] @acc + [1] @elem + [1] @queue + [0] >= [2] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [2] @acc + [1] @queue + [1] @t + [0] >= [2] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [2] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [2] @acc + [1] @queue + [0] >= [2] @acc + [1] @queue + [0] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [2] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [1] >= [1] @queue + [1] @t + [1] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [0] >= [1] @queue' + [0] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [0] >= [0] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [0] >= [2] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [1] > [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [0] >= [0] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [0] >= [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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: { dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [2] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [2] x2 + [2] [bftMult'#2](x1) = [1] x1 + [2] [bftMult'#1](x1, x2) = [1] x1 + [2] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [2] [bftMult'#4](x1, x2, x3) = [1] x1 + [2] x2 + [1] x3 + [0] [leaf] = [2] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [2] x2 + [2] [matrixMult](x1, x2) = [1] x1 + [0] [computeLine](x1, x2, x3) = [1] x1 + [2] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x1 + [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [1] x4 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [2] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [2] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] x1 + [0] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [2] @t + [2] >= [2] @acc + [1] @t + [2] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [2] @acc + [1] @queue + [2] >= [2] @acc + [1] @queue + [2] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [2] >= [1] @dequeue@1 + [1] @dequeue@2 + [2] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [2] @acc + [1] @elem + [1] @queue + [0] >= [2] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [2] @acc + [1] @queue + [1] @t + [0] >= [2] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [2] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [2] >= [1] @inq + [1] @outq + [2] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [2] @acc + [1] @queue + [2] >= [2] @acc + [1] @queue + [2] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [2] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [2] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [2] @acc + [1] @queue' + [2] >= [2] @acc + [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] @m1 + [0] >= [1] @m1 + [0] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [1] @line + [0] >= [2] @acc + [1] @line + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [1] @x + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [2] > [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [2] >= [1] @inq + [2] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [2] > [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [2] > [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [0] >= [1] @l + [1] @ls + [0] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [0] >= [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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: { bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [2] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [2] x1 + [1] x2 + [1] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [2] x1 + [1] x2 + [1] [bftMult'#3](x1, x2, x3) = [2] x1 + [1] x2 + [2] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [2] x1 + [1] x2 + [2] x3 + [0] [leaf] = [2] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [2] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [1] [computeLine](x1, x2, x3) = [1] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [1] x2 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [2] @t + [2] > [1] @acc + [2] @t + [1] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [2] @queue + [1] >= [1] @acc + [2] @queue + [1] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [2] @elem + [2] @queue + [1] > [1] @acc + [2] @elem + [2] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [2] @_@3 + [1] @acc + [2] @queue + [2] @t + [0] >= [1] @acc + [2] @queue + [2] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [2] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [2] @queue + [4] > [1] @acc + [2] @queue + [1] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [2] @queue + [2] @t1 + [2] @t2 + [2] @y + [2] >= [1] @acc + [2] @queue + [2] @t1 + [2] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [2] @queue' + [2] >= [2] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] >= [1] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [1] @acc + [0] >= [1] @acc + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [1] @acc + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] >= [1] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [1] > [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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: { bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [1] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [1] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#2](x1) = [1] x1 + [1] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [1] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [1] x1 + [1] [computeLine](x1, x2, x3) = [1] x1 + [2] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x1 + [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [1] x4 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] x1 + [1] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#succ](x1) = [1] x1 + [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [1] x2 + [0] This order satisfies following ordering constraints [*(@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)] = [1] @x + [1] @y + [0] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [1] >= [1] @acc + [1] @t + [1] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [1] > [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [0] >= [1] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [0] >= [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [2] >= [1] @acc + [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] @m1 + [1] >= [1] @m1 + [1] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [1] @line + [0] >= [2] @acc + [1] @line + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [1] @x + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [1] >= [1] @l + [1] @ls + [1] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [1] > [0] = [nil()] [#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)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#natadd(#s(@x), @y)] = [1] @y + [0] >= [1] @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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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: { bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [1] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [2] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#2](x1) = [1] x1 + [0] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] [dequeue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [1] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [1] x1 + [1] [computeLine](x1, x2, x3) = [1] x1 + [1] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x1 + [1] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [1] x2 + [1] x4 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] x1 + [1] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#succ](x1) = [1] x1 + [0] [#natmult](x1, x2) = [0] [#natadd](x1, x2) = [1] x2 + [0] This order satisfies following ordering constraints [*(@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)] = [1] @x + [1] @y + [0] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [2] @t + [2] > [1] @acc + [1] @t + [1] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [0] >= [1] @dequeue@1 + [1] @dequeue@2 + [0] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [1] >= [1] @acc + [1] @elem + [1] @queue + [1] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [1] > [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [1] > [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [0] >= [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [2] >= [1] @acc + [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] @m1 + [1] >= [1] @m1 + [1] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [1] @acc + [1] @line + [0] >= [1] @acc + [1] @line + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [1] @acc + [1] @x + [1] @xs + [0] >= [1] @acc + [1] @xs + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [1] @acc + [1] @xs + [0] >= [1] @acc + [1] @xs + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [1] @acc + [1] @xs + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [1] >= [1] @l + [1] @ls + [1] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [1] > [0] = [nil()] [#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)] = [1] @y + [0] >= [1] @y + [0] = [@y] [#natadd(#s(@x), @y)] = [1] @y + [0] >= [1] @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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , appendreverse#1(nil(), @sofar) -> @sofar , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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: { appendreverse#1(nil(), @sofar) -> @sofar } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [1] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [1] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#2](x1) = [1] x1 + [1] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [1] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [1] x1 + [1] [computeLine](x1, x2, x3) = [1] x1 + [1] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x1 + [1] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [1] x2 + [1] x4 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [1] [reverse](x1) = [1] x1 + [1] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] x1 + [1] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [1] >= [1] @sofar + [1] @toreverse + [1] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [1] >= [1] @a + [1] @as + [1] @sofar + [1] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [1] > [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [2] > [1] @acc + [1] @t + [1] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [1] >= [1] @dequeue@1 + [1] @dequeue@2 + [1] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [0] >= [1] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [0] >= [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [1] >= [1] @inq + [1] @outq + [1] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [2] >= [1] @acc + [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] @m1 + [1] >= [1] @m1 + [1] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [1] @acc + [1] @line + [0] >= [1] @acc + [1] @line + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [1] @acc + [1] @x + [1] @xs + [0] >= [1] @acc + [1] @xs + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [1] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [1] @acc + [1] @xs + [0] >= [1] @acc + [1] @xs + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [1] @acc + [1] @xs + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [1] > [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [1] >= [1] @inq + [1] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [1] >= [1] @xs + [1] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [1] >= [1] @l + [1] @ls + [1] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [1] > [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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: { dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#2](x1) = [1] x1 + [1] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [1] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [1] x1 + [1] [computeLine](x1, x2, x3) = [1] x1 + [2] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x1 + [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [1] x4 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [1] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] x1 + [1] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [2] > [1] @acc + [1] @t + [1] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [1] >= [1] @dequeue@1 + [1] @dequeue@2 + [1] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [0] >= [1] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [0] >= [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [1] >= [1] @inq + [1] @outq + [1] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [2] >= [1] @acc + [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] @m1 + [1] >= [1] @m1 + [1] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [1] @line + [0] >= [2] @acc + [1] @line + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [1] @x + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [1] > [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [1] > [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [1] >= [1] @l + [1] @ls + [1] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [1] > [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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: { dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) } 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(+) = {1}, Uargs(::) = {1, 2}, Uargs(bftMult') = {2}, Uargs(bftMult'#1) = {1}, Uargs(enqueue) = {2}, Uargs(bftMult'#5) = {1}, Uargs(computeLine) = {3}, Uargs(dequeue#2) = {1}, Uargs(#s) = {1}, Uargs(#neg) = {1}, Uargs(#pred) = {1}, Uargs(#pos) = {1}, Uargs(#succ) = {1}, Uargs(#natadd) = {2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [*](x1, x2) = [0] [#mult](x1, x2) = [0] [+](x1, x2) = [2] x1 + [1] x2 + [0] [#add](x1, x2) = [1] x2 + [0] [appendreverse](x1, x2) = [1] x1 + [1] x2 + [0] [appendreverse#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [0] [bftMult](x1, x2) = [1] x1 + [2] x2 + [2] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#2](x1) = [1] x1 + [1] [bftMult'#1](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [dequeue](x1, x2) = [1] x1 + [1] x2 + [1] [bftMult'#4](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0] [leaf] = [1] [node](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2] [enqueue](x1, x2) = [1] x1 + [1] x2 + [0] [bftMult'#5](x1, x2, x3) = [1] x1 + [1] x2 + [2] [matrixMult](x1, x2) = [1] x1 + [1] [computeLine](x1, x2, x3) = [1] x1 + [2] x3 + [0] [computeLine#1](x1, x2, x3) = [1] x1 + [2] x2 + [0] [computeLine#2](x1, x2, x3, x4) = [2] x2 + [1] x4 + [0] [lineMult](x1, x2, x3) = [1] x3 + [0] [dequeue#1](x1, x2) = [1] x1 + [1] x2 + [0] [reverse](x1) = [1] x1 + [0] [dequeue#2](x1) = [1] x1 + [0] [enqueue#1](x1, x2) = [1] x1 + [1] x2 + [0] [lineMult#1](x1, x2, x3) = [1] x2 + [0] [lineMult#2](x1, x2, x3, x4) = [1] x1 + [0] [matrixMult#1](x1, x2) = [1] x1 + [1] [#0] = [0] [#s](x1) = [1] x1 + [0] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] x1 + [0] [#pos](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 [*(@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] >= [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)] = [1] @y + [0] >= [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)] = [1] @y + [0] >= [1] @y + [0] = [#succ(#add(#pos(#s(@x)), @y))] [appendreverse(@toreverse, @sofar)] = [1] @sofar + [1] @toreverse + [0] >= [1] @sofar + [1] @toreverse + [0] = [appendreverse#1(@toreverse, @sofar)] [appendreverse#1(::(@a, @as), @sofar)] = [1] @a + [1] @as + [1] @sofar + [0] >= [1] @a + [1] @as + [1] @sofar + [0] = [appendreverse(@as, ::(@a, @sofar))] [appendreverse#1(nil(), @sofar)] = [1] @sofar + [0] >= [1] @sofar + [0] = [@sofar] [bftMult(@t, @acc)] = [2] @acc + [1] @t + [2] > [1] @acc + [1] @t + [1] = [bftMult'(tuple#2(::(@t, nil()), nil()), @acc)] [bftMult'(@queue, @acc)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'#1(bftMult'#2(@queue), @acc)] [bftMult'#2(tuple#2(@dequeue@1, @dequeue@2))] = [1] @dequeue@1 + [1] @dequeue@2 + [1] >= [1] @dequeue@1 + [1] @dequeue@2 + [1] = [dequeue(@dequeue@1, @dequeue@2)] [bftMult'#1(tuple#2(@elem, @queue), @acc)] = [1] @acc + [1] @elem + [1] @queue + [0] >= [1] @acc + [1] @elem + [1] @queue + [0] = [bftMult'#3(@elem, @acc, @queue)] [bftMult'#3(::(@t, @_@3), @acc, @queue)] = [1] @_@3 + [1] @acc + [1] @queue + [1] @t + [0] >= [1] @acc + [1] @queue + [1] @t + [0] = [bftMult'#4(@t, @acc, @queue)] [bftMult'#3(nil(), @acc, @queue)] = [1] @acc + [1] @queue + [0] >= [1] @acc + [0] = [@acc] [dequeue(@outq, @inq)] = [1] @inq + [1] @outq + [1] > [1] @inq + [1] @outq + [0] = [dequeue#1(@outq, @inq)] [bftMult'#4(leaf(), @acc, @queue)] = [1] @acc + [1] @queue + [1] >= [1] @acc + [1] @queue + [1] = [bftMult'(@queue, @acc)] [bftMult'#4(node(@y, @t1, @t2), @acc, @queue)] = [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [1] @y + [2] >= [1] @acc + [1] @queue + [1] @t1 + [1] @t2 + [2] = [bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)] [enqueue(@t, @queue)] = [1] @queue + [1] @t + [0] >= [1] @queue + [1] @t + [0] = [enqueue#1(@queue, @t)] [bftMult'#5(@queue', @acc, @y)] = [1] @acc + [1] @queue' + [2] >= [1] @acc + [1] @queue' + [2] = [bftMult'(@queue', matrixMult(@acc, @y))] [matrixMult(@m1, @m2)] = [1] @m1 + [1] >= [1] @m1 + [1] = [matrixMult#1(@m1, @m2)] [computeLine(@line, @m, @acc)] = [2] @acc + [1] @line + [0] >= [2] @acc + [1] @line + [0] = [computeLine#1(@line, @acc, @m)] [computeLine#1(::(@x, @xs), @acc, @m)] = [2] @acc + [1] @x + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine#2(@m, @acc, @x, @xs)] [computeLine#1(nil(), @acc, @m)] = [2] @acc + [0] >= [1] @acc + [0] = [@acc] [computeLine#2(::(@l, @ls), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [2] @acc + [1] @xs + [0] = [computeLine(@xs, @ls, lineMult(@x, @l, @acc))] [computeLine#2(nil(), @acc, @x, @xs)] = [2] @acc + [1] @xs + [0] >= [0] = [nil()] [lineMult(@n, @l1, @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#1(@l1, @l2, @n)] [dequeue#1(::(@t, @ts), @inq)] = [1] @inq + [1] @t + [1] @ts + [0] >= [1] @inq + [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, @inq))] [dequeue#1(nil(), @inq)] = [1] @inq + [0] >= [1] @inq + [0] = [dequeue#2(reverse(@inq))] [reverse(@xs)] = [1] @xs + [0] >= [1] @xs + [0] = [appendreverse(@xs, nil())] [dequeue#2(::(@t, @ts))] = [1] @t + [1] @ts + [0] >= [1] @t + [1] @ts + [0] = [tuple#2(::(@t, nil()), tuple#2(@ts, nil()))] [dequeue#2(nil())] = [0] >= [0] = [tuple#2(nil(), tuple#2(nil(), nil()))] [enqueue#1(tuple#2(@outq, @inq), @t)] = [1] @inq + [1] @outq + [1] @t + [0] >= [1] @inq + [1] @outq + [1] @t + [0] = [tuple#2(@outq, ::(@t, @inq))] [lineMult#1(::(@x, @xs), @l2, @n)] = [1] @l2 + [0] >= [1] @l2 + [0] = [lineMult#2(@l2, @n, @x, @xs)] [lineMult#1(nil(), @l2, @n)] = [1] @l2 + [0] >= [0] = [nil()] [lineMult#2(::(@y, @ys), @n, @x, @xs)] = [1] @y + [1] @ys + [0] >= [1] @y + [1] @ys + [0] = [::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))] [lineMult#2(nil(), @n, @x, @xs)] = [0] >= [0] = [::(*(@x, @n), lineMult(@n, @xs, nil()))] [matrixMult#1(::(@l, @ls), @m2)] = [1] @l + [1] @ls + [1] >= [1] @l + [1] @ls + [1] = [::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))] [matrixMult#1(nil(), @m2)] = [1] > [0] = [nil()] [#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: { *(@x, @y) -> #mult(@x, @y) , +(@x, @y) -> #add(@x, @y) , appendreverse(@toreverse, @sofar) -> appendreverse#1(@toreverse, @sofar) , appendreverse#1(::(@a, @as), @sofar) -> appendreverse(@as, ::(@a, @sofar)) , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2) , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m) , computeLine#1(::(@x, @xs), @acc, @m) -> computeLine#2(@m, @acc, @x, @xs) , computeLine#1(nil(), @acc, @m) -> @acc , computeLine#2(::(@l, @ls), @acc, @x, @xs) -> computeLine(@xs, @ls, lineMult(@x, @l, @acc)) , computeLine#2(nil(), @acc, @x, @xs) -> nil() , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n) , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs) , lineMult#1(nil(), @l2, @n) -> nil() , lineMult#2(::(@y, @ys), @n, @x, @xs) -> ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys)) , lineMult#2(nil(), @n, @x, @xs) -> ::(*(@x, @n), lineMult(@n, @xs, nil())) , matrixMult#1(::(@l, @ls), @m2) -> ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2)) } 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)) , appendreverse#1(nil(), @sofar) -> @sofar , bftMult(@t, @acc) -> bftMult'(tuple#2(::(@t, nil()), nil()), @acc) , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc) , bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) -> dequeue(@dequeue@1, @dequeue@2) , bftMult'#1(tuple#2(@elem, @queue), @acc) -> bftMult'#3(@elem, @acc, @queue) , bftMult'#3(::(@t, @_@3), @acc, @queue) -> bftMult'#4(@t, @acc, @queue) , bftMult'#3(nil(), @acc, @queue) -> @acc , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq) , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc) , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) -> bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y) , enqueue(@t, @queue) -> enqueue#1(@queue, @t) , bftMult'#5(@queue', @acc, @y) -> bftMult'(@queue', matrixMult(@acc, @y)) , dequeue#1(::(@t, @ts), @inq) -> tuple#2(::(@t, nil()), tuple#2(@ts, @inq)) , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq)) , reverse(@xs) -> appendreverse(@xs, nil()) , dequeue#2(::(@t, @ts)) -> tuple#2(::(@t, nil()), tuple#2(@ts, nil())) , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil())) , enqueue#1(tuple#2(@outq, @inq), @t) -> tuple#2(@outq, ::(@t, @inq)) , matrixMult#1(nil(), @m2) -> nil() , #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..