MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, app(nil(), y) -> y
, app(add(n, x), y) -> add(n, app(x, y))
, min(add(n, nil())) -> n
, min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x)))
, if_min(true(), add(n, add(m, x))) -> min(add(n, x))
, if_min(false(), add(n, add(m, x))) -> min(add(m, x))
, head(add(n, x)) -> n
, tail(nil()) -> nil()
, tail(add(n, x)) -> x
, null(nil()) -> true()
, null(add(n, x)) -> false()
, rm(n, nil()) -> nil()
, rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
, if_rm(true(), n, add(m, x)) -> rm(n, x)
, if_rm(false(), n, add(m, x)) -> add(m, rm(n, x))
, minsort(x) -> mins(x, nil(), nil())
, mins(x, y, z) -> if(null(x), x, y, z)
, if(true(), x, y, z) -> z
, if(false(), x, y, z) -> if2(eq(head(x), min(x)), x, y, z)
, if2(true(), x, y, z) ->
mins(app(rm(head(x), tail(x)), y),
nil(),
app(z, add(head(x), nil())))
, if2(false(), x, y, z) -> mins(tail(x), add(head(x), y), z) }
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:
Computation stopped due to timeout after 30.0 seconds.
2) '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 minimal-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
failed due to the following reason:
match-boundness of the problem could not be verified.
3) 'Best' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) '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
2) '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
3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
due to the following reason:
We add the following weak dependency pairs:
Strict DPs:
{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(x)) -> c_2()
, eq^#(s(x), 0()) -> c_3()
, eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
, le^#(0(), y) -> c_5()
, le^#(s(x), 0()) -> c_6()
, le^#(s(x), s(y)) -> c_7(le^#(x, y))
, app^#(nil(), y) -> c_8(y)
, app^#(add(n, x), y) -> c_9(n, app^#(x, y))
, min^#(add(n, nil())) -> c_10(n)
, min^#(add(n, add(m, x))) ->
c_11(if_min^#(le(n, m), add(n, add(m, x))))
, if_min^#(true(), add(n, add(m, x))) -> c_12(min^#(add(n, x)))
, if_min^#(false(), add(n, add(m, x))) -> c_13(min^#(add(m, x)))
, head^#(add(n, x)) -> c_14(n)
, tail^#(nil()) -> c_15()
, tail^#(add(n, x)) -> c_16(x)
, null^#(nil()) -> c_17()
, null^#(add(n, x)) -> c_18()
, rm^#(n, nil()) -> c_19()
, rm^#(n, add(m, x)) -> c_20(if_rm^#(eq(n, m), n, add(m, x)))
, if_rm^#(true(), n, add(m, x)) -> c_21(rm^#(n, x))
, if_rm^#(false(), n, add(m, x)) -> c_22(m, rm^#(n, x))
, minsort^#(x) -> c_23(mins^#(x, nil(), nil()))
, mins^#(x, y, z) -> c_24(if^#(null(x), x, y, z))
, if^#(true(), x, y, z) -> c_25(z)
, if^#(false(), x, y, z) ->
c_26(if2^#(eq(head(x), min(x)), x, y, z))
, if2^#(true(), x, y, z) ->
c_27(mins^#(app(rm(head(x), tail(x)), y),
nil(),
app(z, add(head(x), nil()))))
, if2^#(false(), x, y, z) ->
c_28(mins^#(tail(x), add(head(x), y), z)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(x)) -> c_2()
, eq^#(s(x), 0()) -> c_3()
, eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
, le^#(0(), y) -> c_5()
, le^#(s(x), 0()) -> c_6()
, le^#(s(x), s(y)) -> c_7(le^#(x, y))
, app^#(nil(), y) -> c_8(y)
, app^#(add(n, x), y) -> c_9(n, app^#(x, y))
, min^#(add(n, nil())) -> c_10(n)
, min^#(add(n, add(m, x))) ->
c_11(if_min^#(le(n, m), add(n, add(m, x))))
, if_min^#(true(), add(n, add(m, x))) -> c_12(min^#(add(n, x)))
, if_min^#(false(), add(n, add(m, x))) -> c_13(min^#(add(m, x)))
, head^#(add(n, x)) -> c_14(n)
, tail^#(nil()) -> c_15()
, tail^#(add(n, x)) -> c_16(x)
, null^#(nil()) -> c_17()
, null^#(add(n, x)) -> c_18()
, rm^#(n, nil()) -> c_19()
, rm^#(n, add(m, x)) -> c_20(if_rm^#(eq(n, m), n, add(m, x)))
, if_rm^#(true(), n, add(m, x)) -> c_21(rm^#(n, x))
, if_rm^#(false(), n, add(m, x)) -> c_22(m, rm^#(n, x))
, minsort^#(x) -> c_23(mins^#(x, nil(), nil()))
, mins^#(x, y, z) -> c_24(if^#(null(x), x, y, z))
, if^#(true(), x, y, z) -> c_25(z)
, if^#(false(), x, y, z) ->
c_26(if2^#(eq(head(x), min(x)), x, y, z))
, if2^#(true(), x, y, z) ->
c_27(mins^#(app(rm(head(x), tail(x)), y),
nil(),
app(z, add(head(x), nil()))))
, if2^#(false(), x, y, z) ->
c_28(mins^#(tail(x), add(head(x), y), z)) }
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, app(nil(), y) -> y
, app(add(n, x), y) -> add(n, app(x, y))
, min(add(n, nil())) -> n
, min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x)))
, if_min(true(), add(n, add(m, x))) -> min(add(n, x))
, if_min(false(), add(n, add(m, x))) -> min(add(m, x))
, head(add(n, x)) -> n
, tail(nil()) -> nil()
, tail(add(n, x)) -> x
, null(nil()) -> true()
, null(add(n, x)) -> false()
, rm(n, nil()) -> nil()
, rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
, if_rm(true(), n, add(m, x)) -> rm(n, x)
, if_rm(false(), n, add(m, x)) -> add(m, rm(n, x))
, minsort(x) -> mins(x, nil(), nil())
, mins(x, y, z) -> if(null(x), x, y, z)
, if(true(), x, y, z) -> z
, if(false(), x, y, z) -> if2(eq(head(x), min(x)), x, y, z)
, if2(true(), x, y, z) ->
mins(app(rm(head(x), tail(x)), y),
nil(),
app(z, add(head(x), nil())))
, if2(false(), x, y, z) -> mins(tail(x), add(head(x), y), z) }
Obligation:
runtime complexity
Answer:
MAYBE
We estimate the number of application of {1,2,3,5,6,15,17,18,19} by
applications of Pre({1,2,3,5,6,15,17,18,19}) =
{4,7,8,9,10,14,16,21,22,25}. Here rules are labeled as follows:
DPs:
{ 1: eq^#(0(), 0()) -> c_1()
, 2: eq^#(0(), s(x)) -> c_2()
, 3: eq^#(s(x), 0()) -> c_3()
, 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
, 5: le^#(0(), y) -> c_5()
, 6: le^#(s(x), 0()) -> c_6()
, 7: le^#(s(x), s(y)) -> c_7(le^#(x, y))
, 8: app^#(nil(), y) -> c_8(y)
, 9: app^#(add(n, x), y) -> c_9(n, app^#(x, y))
, 10: min^#(add(n, nil())) -> c_10(n)
, 11: min^#(add(n, add(m, x))) ->
c_11(if_min^#(le(n, m), add(n, add(m, x))))
, 12: if_min^#(true(), add(n, add(m, x))) -> c_12(min^#(add(n, x)))
, 13: if_min^#(false(), add(n, add(m, x))) ->
c_13(min^#(add(m, x)))
, 14: head^#(add(n, x)) -> c_14(n)
, 15: tail^#(nil()) -> c_15()
, 16: tail^#(add(n, x)) -> c_16(x)
, 17: null^#(nil()) -> c_17()
, 18: null^#(add(n, x)) -> c_18()
, 19: rm^#(n, nil()) -> c_19()
, 20: rm^#(n, add(m, x)) -> c_20(if_rm^#(eq(n, m), n, add(m, x)))
, 21: if_rm^#(true(), n, add(m, x)) -> c_21(rm^#(n, x))
, 22: if_rm^#(false(), n, add(m, x)) -> c_22(m, rm^#(n, x))
, 23: minsort^#(x) -> c_23(mins^#(x, nil(), nil()))
, 24: mins^#(x, y, z) -> c_24(if^#(null(x), x, y, z))
, 25: if^#(true(), x, y, z) -> c_25(z)
, 26: if^#(false(), x, y, z) ->
c_26(if2^#(eq(head(x), min(x)), x, y, z))
, 27: if2^#(true(), x, y, z) ->
c_27(mins^#(app(rm(head(x), tail(x)), y),
nil(),
app(z, add(head(x), nil()))))
, 28: if2^#(false(), x, y, z) ->
c_28(mins^#(tail(x), add(head(x), y), z)) }
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict DPs:
{ eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
, le^#(s(x), s(y)) -> c_7(le^#(x, y))
, app^#(nil(), y) -> c_8(y)
, app^#(add(n, x), y) -> c_9(n, app^#(x, y))
, min^#(add(n, nil())) -> c_10(n)
, min^#(add(n, add(m, x))) ->
c_11(if_min^#(le(n, m), add(n, add(m, x))))
, if_min^#(true(), add(n, add(m, x))) -> c_12(min^#(add(n, x)))
, if_min^#(false(), add(n, add(m, x))) -> c_13(min^#(add(m, x)))
, head^#(add(n, x)) -> c_14(n)
, tail^#(add(n, x)) -> c_16(x)
, rm^#(n, add(m, x)) -> c_20(if_rm^#(eq(n, m), n, add(m, x)))
, if_rm^#(true(), n, add(m, x)) -> c_21(rm^#(n, x))
, if_rm^#(false(), n, add(m, x)) -> c_22(m, rm^#(n, x))
, minsort^#(x) -> c_23(mins^#(x, nil(), nil()))
, mins^#(x, y, z) -> c_24(if^#(null(x), x, y, z))
, if^#(true(), x, y, z) -> c_25(z)
, if^#(false(), x, y, z) ->
c_26(if2^#(eq(head(x), min(x)), x, y, z))
, if2^#(true(), x, y, z) ->
c_27(mins^#(app(rm(head(x), tail(x)), y),
nil(),
app(z, add(head(x), nil()))))
, if2^#(false(), x, y, z) ->
c_28(mins^#(tail(x), add(head(x), y), z)) }
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(x)) -> false()
, eq(s(x), 0()) -> false()
, eq(s(x), s(y)) -> eq(x, y)
, le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, app(nil(), y) -> y
, app(add(n, x), y) -> add(n, app(x, y))
, min(add(n, nil())) -> n
, min(add(n, add(m, x))) -> if_min(le(n, m), add(n, add(m, x)))
, if_min(true(), add(n, add(m, x))) -> min(add(n, x))
, if_min(false(), add(n, add(m, x))) -> min(add(m, x))
, head(add(n, x)) -> n
, tail(nil()) -> nil()
, tail(add(n, x)) -> x
, null(nil()) -> true()
, null(add(n, x)) -> false()
, rm(n, nil()) -> nil()
, rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x))
, if_rm(true(), n, add(m, x)) -> rm(n, x)
, if_rm(false(), n, add(m, x)) -> add(m, rm(n, x))
, minsort(x) -> mins(x, nil(), nil())
, mins(x, y, z) -> if(null(x), x, y, z)
, if(true(), x, y, z) -> z
, if(false(), x, y, z) -> if2(eq(head(x), min(x)), x, y, z)
, if2(true(), x, y, z) ->
mins(app(rm(head(x), tail(x)), y),
nil(),
app(z, add(head(x), nil())))
, if2(false(), x, y, z) -> mins(tail(x), add(head(x), y), z) }
Weak DPs:
{ eq^#(0(), 0()) -> c_1()
, eq^#(0(), s(x)) -> c_2()
, eq^#(s(x), 0()) -> c_3()
, le^#(0(), y) -> c_5()
, le^#(s(x), 0()) -> c_6()
, tail^#(nil()) -> c_15()
, null^#(nil()) -> c_17()
, null^#(add(n, x)) -> c_18()
, rm^#(n, nil()) -> c_19() }
Obligation:
runtime complexity
Answer:
MAYBE
Empty strict component of the problem is NOT empty.
Arrrr..