MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y)) }
Obligation:
runtime complexity
Answer:
MAYBE
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
following reason:
Computation stopped due to timeout after 60.0 seconds.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
failed due to the following reason:
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(s) = {1}, Uargs(*) = {2}, Uargs(floop) = {2}, Uargs(+) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[fac](x1) = [0]
[0] = [0]
[1] = [7]
[s](x1) = [1] x1 + [0]
[*](x1, x2) = [1] x2 + [0]
[floop](x1, x2) = [1] x2 + [0]
[+](x1, x2) = [1] x1 + [0]
The following symbols are considered usable
{fac, 1, *, floop, +}
The order satisfies the following ordering constraints:
[fac(0())] = [0]
? [7]
= [1()]
[fac(0())] = [0]
>= [0]
= [s(0())]
[fac(s(x))] = [0]
>= [0]
= [*(s(x), fac(x))]
[1()] = [7]
> [0]
= [s(0())]
[*(x, 0())] = [0]
>= [0]
= [0()]
[*(x, s(y))] = [1] y + [0]
>= [1] y + [0]
= [+(*(x, y), x)]
[floop(0(), y)] = [1] y + [0]
>= [1] y + [0]
= [y]
[floop(s(x), y)] = [1] y + [0]
>= [1] y + [0]
= [floop(x, *(s(x), y))]
[+(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[+(x, s(y))] = [1] x + [0]
>= [1] x + [0]
= [s(+(x, y))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y)) }
Weak Trs: { 1() -> s(0()) }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(s) = {1}, Uargs(*) = {2}, Uargs(floop) = {2}, Uargs(+) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[fac](x1) = [0]
[0] = [1]
[1] = [7]
[s](x1) = [1] x1 + [0]
[*](x1, x2) = [1] x2 + [0]
[floop](x1, x2) = [1] x1 + [1] x2 + [0]
[+](x1, x2) = [1] x1 + [0]
The following symbols are considered usable
{fac, 1, *, floop, +}
The order satisfies the following ordering constraints:
[fac(0())] = [0]
? [7]
= [1()]
[fac(0())] = [0]
? [1]
= [s(0())]
[fac(s(x))] = [0]
>= [0]
= [*(s(x), fac(x))]
[1()] = [7]
> [1]
= [s(0())]
[*(x, 0())] = [1]
>= [1]
= [0()]
[*(x, s(y))] = [1] y + [0]
>= [1] y + [0]
= [+(*(x, y), x)]
[floop(0(), y)] = [1] y + [1]
> [1] y + [0]
= [y]
[floop(s(x), y)] = [1] x + [1] y + [0]
>= [1] x + [1] y + [0]
= [floop(x, *(s(x), y))]
[+(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[+(x, s(y))] = [1] x + [0]
>= [1] x + [0]
= [s(+(x, y))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
{ 1() -> s(0())
, floop(0(), y) -> y }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(s) = {1}, Uargs(*) = {2}, Uargs(floop) = {2}, Uargs(+) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[fac](x1) = [1] x1 + [7]
[0] = [0]
[1] = [7]
[s](x1) = [1] x1 + [7]
[*](x1, x2) = [1] x2 + [7]
[floop](x1, x2) = [1] x1 + [1] x2 + [7]
[+](x1, x2) = [1] x1 + [3]
The following symbols are considered usable
{fac, 1, *, floop, +}
The order satisfies the following ordering constraints:
[fac(0())] = [7]
>= [7]
= [1()]
[fac(0())] = [7]
>= [7]
= [s(0())]
[fac(s(x))] = [1] x + [14]
>= [1] x + [14]
= [*(s(x), fac(x))]
[1()] = [7]
>= [7]
= [s(0())]
[*(x, 0())] = [7]
> [0]
= [0()]
[*(x, s(y))] = [1] y + [14]
> [1] y + [10]
= [+(*(x, y), x)]
[floop(0(), y)] = [1] y + [7]
> [1] y + [0]
= [y]
[floop(s(x), y)] = [1] x + [1] y + [14]
>= [1] x + [1] y + [14]
= [floop(x, *(s(x), y))]
[+(x, 0())] = [1] x + [3]
> [1] x + [0]
= [x]
[+(x, s(y))] = [1] x + [3]
? [1] x + [10]
= [s(+(x, y))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
{ 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, +(x, 0()) -> x }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(s) = {1}, Uargs(*) = {2}, Uargs(floop) = {2}, Uargs(+) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[fac](x1) = [0]
[0] = [0]
[1] = [7]
[s](x1) = [1] x1 + [4]
[*](x1, x2) = [1] x2 + [0]
[floop](x1, x2) = [1] x1 + [1] x2 + [0]
[+](x1, x2) = [1] x1 + [0]
The following symbols are considered usable
{fac, 1, *, floop, +}
The order satisfies the following ordering constraints:
[fac(0())] = [0]
? [7]
= [1()]
[fac(0())] = [0]
? [4]
= [s(0())]
[fac(s(x))] = [0]
>= [0]
= [*(s(x), fac(x))]
[1()] = [7]
> [4]
= [s(0())]
[*(x, 0())] = [0]
>= [0]
= [0()]
[*(x, s(y))] = [1] y + [4]
> [1] y + [0]
= [+(*(x, y), x)]
[floop(0(), y)] = [1] y + [0]
>= [1] y + [0]
= [y]
[floop(s(x), y)] = [1] x + [1] y + [4]
> [1] x + [1] y + [0]
= [floop(x, *(s(x), y))]
[+(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[+(x, s(y))] = [1] x + [0]
? [1] x + [4]
= [s(+(x, y))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
{ 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(s) = {1}, Uargs(*) = {2}, Uargs(floop) = {2}, Uargs(+) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[fac](x1) = [1] x1 + [0]
[0] = [0]
[1] = [7]
[s](x1) = [1] x1 + [4]
[*](x1, x2) = [1] x2 + [0]
[floop](x1, x2) = [1] x1 + [1] x2 + [5]
[+](x1, x2) = [1] x1 + [0]
The following symbols are considered usable
{fac, 1, *, floop, +}
The order satisfies the following ordering constraints:
[fac(0())] = [0]
? [7]
= [1()]
[fac(0())] = [0]
? [4]
= [s(0())]
[fac(s(x))] = [1] x + [4]
> [1] x + [0]
= [*(s(x), fac(x))]
[1()] = [7]
> [4]
= [s(0())]
[*(x, 0())] = [0]
>= [0]
= [0()]
[*(x, s(y))] = [1] y + [4]
> [1] y + [0]
= [+(*(x, y), x)]
[floop(0(), y)] = [1] y + [5]
> [1] y + [0]
= [y]
[floop(s(x), y)] = [1] x + [1] y + [9]
> [1] x + [1] y + [5]
= [floop(x, *(s(x), y))]
[+(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[+(x, s(y))] = [1] x + [0]
? [1] x + [4]
= [s(+(x, y))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
{ fac(s(x)) -> *(s(x), fac(x))
, 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(s) = {1}, Uargs(*) = {2}, Uargs(floop) = {2}, Uargs(+) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[fac](x1) = [1] x1 + [6]
[0] = [0]
[1] = [7]
[s](x1) = [1] x1 + [2]
[*](x1, x2) = [1] x2 + [0]
[floop](x1, x2) = [1] x2 + [5]
[+](x1, x2) = [1] x1 + [2]
The following symbols are considered usable
{fac, 1, *, floop, +}
The order satisfies the following ordering constraints:
[fac(0())] = [6]
? [7]
= [1()]
[fac(0())] = [6]
> [2]
= [s(0())]
[fac(s(x))] = [1] x + [8]
> [1] x + [6]
= [*(s(x), fac(x))]
[1()] = [7]
> [2]
= [s(0())]
[*(x, 0())] = [0]
>= [0]
= [0()]
[*(x, s(y))] = [1] y + [2]
>= [1] y + [2]
= [+(*(x, y), x)]
[floop(0(), y)] = [1] y + [5]
> [1] y + [0]
= [y]
[floop(s(x), y)] = [1] y + [5]
>= [1] y + [5]
= [floop(x, *(s(x), y))]
[+(x, 0())] = [1] x + [2]
> [1] x + [0]
= [x]
[+(x, s(y))] = [1] x + [2]
? [1] x + [4]
= [s(+(x, y))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ fac(0()) -> 1()
, +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
{ fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x }
Obligation:
runtime complexity
Answer:
MAYBE
The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(s) = {1}, Uargs(*) = {2}, Uargs(floop) = {2}, Uargs(+) = {1}
TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).
[fac](x1) = [1] x1 + [4]
[0] = [4]
[1] = [7]
[s](x1) = [1] x1 + [0]
[*](x1, x2) = [1] x2 + [0]
[floop](x1, x2) = [1] x1 + [1] x2 + [5]
[+](x1, x2) = [1] x1 + [0]
The following symbols are considered usable
{fac, 1, *, floop, +}
The order satisfies the following ordering constraints:
[fac(0())] = [8]
> [7]
= [1()]
[fac(0())] = [8]
> [4]
= [s(0())]
[fac(s(x))] = [1] x + [4]
>= [1] x + [4]
= [*(s(x), fac(x))]
[1()] = [7]
> [4]
= [s(0())]
[*(x, 0())] = [4]
>= [4]
= [0()]
[*(x, s(y))] = [1] y + [0]
>= [1] y + [0]
= [+(*(x, y), x)]
[floop(0(), y)] = [1] y + [9]
> [1] y + [0]
= [y]
[floop(s(x), y)] = [1] x + [1] y + [5]
>= [1] x + [1] y + [5]
= [floop(x, *(s(x), y))]
[+(x, 0())] = [1] x + [0]
>= [1] x + [0]
= [x]
[+(x, s(y))] = [1] x + [0]
>= [1] x + [0]
= [s(+(x, y))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs: { +(x, s(y)) -> s(+(x, y)) }
Weak Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x }
Obligation:
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) 'WithProblem' 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) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'WithProblem' 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) 'WithProblem' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'WithProblem' 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) 'WithProblem' 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) 'WithProblem' 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) 'WithProblem' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
to the following reason:
The processor is inapplicable, reason:
Processor only applicable for innermost runtime complexity analysis
3) 'Fastest (timeout of 5 seconds) (timeout of 60 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.
3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
due to the following reason:
We add the following weak dependency pairs:
Strict DPs:
{ fac^#(0()) -> c_1(1^#())
, fac^#(0()) -> c_2()
, fac^#(s(x)) -> c_3(*^#(s(x), fac(x)))
, 1^#() -> c_4()
, *^#(x, 0()) -> c_5()
, *^#(x, s(y)) -> c_6(+^#(*(x, y), x))
, +^#(x, 0()) -> c_9(x)
, +^#(x, s(y)) -> c_10(+^#(x, y))
, floop^#(0(), y) -> c_7(y)
, floop^#(s(x), y) -> c_8(floop^#(x, *(s(x), y))) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ fac^#(0()) -> c_1(1^#())
, fac^#(0()) -> c_2()
, fac^#(s(x)) -> c_3(*^#(s(x), fac(x)))
, 1^#() -> c_4()
, *^#(x, 0()) -> c_5()
, *^#(x, s(y)) -> c_6(+^#(*(x, y), x))
, +^#(x, 0()) -> c_9(x)
, +^#(x, s(y)) -> c_10(+^#(x, y))
, floop^#(0(), y) -> c_7(y)
, floop^#(s(x), y) -> c_8(floop^#(x, *(s(x), y))) }
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y)) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {2,4,5} by applications of
Pre({2,4,5}) = {1,3,7,9}. Here rules are labeled as follows:
DPs:
{ 1: fac^#(0()) -> c_1(1^#())
, 2: fac^#(0()) -> c_2()
, 3: fac^#(s(x)) -> c_3(*^#(s(x), fac(x)))
, 4: 1^#() -> c_4()
, 5: *^#(x, 0()) -> c_5()
, 6: *^#(x, s(y)) -> c_6(+^#(*(x, y), x))
, 7: +^#(x, 0()) -> c_9(x)
, 8: +^#(x, s(y)) -> c_10(+^#(x, y))
, 9: floop^#(0(), y) -> c_7(y)
, 10: floop^#(s(x), y) -> c_8(floop^#(x, *(s(x), y))) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ fac^#(0()) -> c_1(1^#())
, fac^#(s(x)) -> c_3(*^#(s(x), fac(x)))
, *^#(x, s(y)) -> c_6(+^#(*(x, y), x))
, +^#(x, 0()) -> c_9(x)
, +^#(x, s(y)) -> c_10(+^#(x, y))
, floop^#(0(), y) -> c_7(y)
, floop^#(s(x), y) -> c_8(floop^#(x, *(s(x), y))) }
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y)) }
Weak DPs:
{ fac^#(0()) -> c_2()
, 1^#() -> c_4()
, *^#(x, 0()) -> c_5() }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {1} by applications of
Pre({1}) = {4,6}. Here rules are labeled as follows:
DPs:
{ 1: fac^#(0()) -> c_1(1^#())
, 2: fac^#(s(x)) -> c_3(*^#(s(x), fac(x)))
, 3: *^#(x, s(y)) -> c_6(+^#(*(x, y), x))
, 4: +^#(x, 0()) -> c_9(x)
, 5: +^#(x, s(y)) -> c_10(+^#(x, y))
, 6: floop^#(0(), y) -> c_7(y)
, 7: floop^#(s(x), y) -> c_8(floop^#(x, *(s(x), y)))
, 8: fac^#(0()) -> c_2()
, 9: 1^#() -> c_4()
, 10: *^#(x, 0()) -> c_5() }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ fac^#(s(x)) -> c_3(*^#(s(x), fac(x)))
, *^#(x, s(y)) -> c_6(+^#(*(x, y), x))
, +^#(x, 0()) -> c_9(x)
, +^#(x, s(y)) -> c_10(+^#(x, y))
, floop^#(0(), y) -> c_7(y)
, floop^#(s(x), y) -> c_8(floop^#(x, *(s(x), y))) }
Strict Trs:
{ fac(0()) -> 1()
, fac(0()) -> s(0())
, fac(s(x)) -> *(s(x), fac(x))
, 1() -> s(0())
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, floop(0(), y) -> y
, floop(s(x), y) -> floop(x, *(s(x), y))
, +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y)) }
Weak DPs:
{ fac^#(0()) -> c_1(1^#())
, fac^#(0()) -> c_2()
, 1^#() -> c_4()
, *^#(x, 0()) -> c_5() }
Obligation:
runtime complexity
Answer:
MAYBE
Empty strict component of the problem is NOT empty.
Arrrr..