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