MAYBE
759.91/297.03	MAYBE
759.91/297.03	
759.91/297.03	We are left with following problem, upon which TcT provides the
759.91/297.03	certificate MAYBE.
759.91/297.03	
759.91/297.03	Strict Trs:
759.91/297.03	  { isEmpty(cons(x, xs)) -> false()
759.91/297.03	  , isEmpty(nil()) -> true()
759.91/297.03	  , isZero(0()) -> true()
759.91/297.03	  , isZero(s(x)) -> false()
759.91/297.03	  , head(cons(x, xs)) -> x
759.91/297.03	  , tail(cons(x, xs)) -> xs
759.91/297.03	  , tail(nil()) -> nil()
759.91/297.03	  , append(cons(y, ys), x) -> cons(y, append(ys, x))
759.91/297.03	  , append(nil(), x) -> cons(x, nil())
759.91/297.03	  , p(0()) -> 0()
759.91/297.03	  , p(s(0())) -> 0()
759.91/297.03	  , p(s(s(x))) -> s(p(s(x)))
759.91/297.03	  , inc(0()) -> s(0())
759.91/297.03	  , inc(s(x)) -> s(inc(x))
759.91/297.03	  , addLists(xs, ys, zs) ->
759.91/297.03	    if(isEmpty(xs),
759.91/297.03	       isEmpty(ys),
759.91/297.03	       isZero(head(xs)),
759.91/297.03	       tail(xs),
759.91/297.03	       tail(ys),
759.91/297.03	       cons(p(head(xs)), tail(xs)),
759.91/297.03	       cons(inc(head(ys)), tail(ys)),
759.91/297.03	       zs,
759.91/297.03	       append(zs, head(ys)))
759.91/297.03	  , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	    addLists(xs2, ys2, zs)
759.91/297.03	  , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	    addLists(xs, ys, zs2)
759.91/297.03	  , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	    differentLengthError()
759.91/297.03	  , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	    differentLengthError()
759.91/297.03	  , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
759.91/297.03	  , addList(xs, ys) -> addLists(xs, ys, nil()) }
759.91/297.03	Obligation:
759.91/297.03	  runtime complexity
759.91/297.03	Answer:
759.91/297.03	  MAYBE
759.91/297.03	
759.91/297.03	None of the processors succeeded.
759.91/297.03	
759.91/297.03	Details of failed attempt(s):
759.91/297.03	-----------------------------
759.91/297.03	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
759.91/297.03	   following reason:
759.91/297.03	   
759.91/297.03	   Computation stopped due to timeout after 297.0 seconds.
759.91/297.03	
759.91/297.03	2) 'Best' failed due to the following reason:
759.91/297.03	   
759.91/297.03	   None of the processors succeeded.
759.91/297.03	   
759.91/297.03	   Details of failed attempt(s):
759.91/297.03	   -----------------------------
759.91/297.03	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
759.91/297.03	      seconds)' failed due to the following reason:
759.91/297.03	      
759.91/297.03	      Computation stopped due to timeout after 148.0 seconds.
759.91/297.03	   
759.91/297.03	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
759.91/297.03	      failed due to the following reason:
759.91/297.03	      
759.91/297.03	      None of the processors succeeded.
759.91/297.03	      
759.91/297.03	      Details of failed attempt(s):
759.91/297.03	      -----------------------------
759.91/297.03	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
759.91/297.03	         failed due to the following reason:
759.91/297.03	         
759.91/297.03	         match-boundness of the problem could not be verified.
759.91/297.03	      
759.91/297.03	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
759.91/297.03	         failed due to the following reason:
759.91/297.03	         
759.91/297.03	         match-boundness of the problem could not be verified.
759.91/297.03	      
759.91/297.03	   
759.91/297.03	   3) 'Best' failed due to the following reason:
759.91/297.03	      
759.91/297.03	      None of the processors succeeded.
759.91/297.03	      
759.91/297.03	      Details of failed attempt(s):
759.91/297.03	      -----------------------------
759.91/297.03	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
759.91/297.03	         following reason:
759.91/297.03	         
759.91/297.03	         The processor is inapplicable, reason:
759.91/297.03	           Processor only applicable for innermost runtime complexity analysis
759.91/297.03	      
759.91/297.03	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
759.91/297.03	         to the following reason:
759.91/297.03	         
759.91/297.03	         The processor is inapplicable, reason:
759.91/297.03	           Processor only applicable for innermost runtime complexity analysis
759.91/297.03	      
759.91/297.03	   
759.91/297.03	
759.91/297.03	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
759.91/297.03	   the following reason:
759.91/297.03	   
759.91/297.03	   We add the following weak dependency pairs:
759.91/297.03	   
759.91/297.03	   Strict DPs:
759.91/297.03	     { isEmpty^#(cons(x, xs)) -> c_1()
759.91/297.03	     , isEmpty^#(nil()) -> c_2()
759.91/297.03	     , isZero^#(0()) -> c_3()
759.91/297.03	     , isZero^#(s(x)) -> c_4()
759.91/297.03	     , head^#(cons(x, xs)) -> c_5(x)
759.91/297.03	     , tail^#(cons(x, xs)) -> c_6(xs)
759.91/297.03	     , tail^#(nil()) -> c_7()
759.91/297.03	     , append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x))
759.91/297.03	     , append^#(nil(), x) -> c_9(x)
759.91/297.03	     , p^#(0()) -> c_10()
759.91/297.03	     , p^#(s(0())) -> c_11()
759.91/297.03	     , p^#(s(s(x))) -> c_12(p^#(s(x)))
759.91/297.03	     , inc^#(0()) -> c_13()
759.91/297.03	     , inc^#(s(x)) -> c_14(inc^#(x))
759.91/297.03	     , addLists^#(xs, ys, zs) ->
759.91/297.03	       c_15(if^#(isEmpty(xs),
759.91/297.03	                 isEmpty(ys),
759.91/297.03	                 isZero(head(xs)),
759.91/297.03	                 tail(xs),
759.91/297.03	                 tail(ys),
759.91/297.03	                 cons(p(head(xs)), tail(xs)),
759.91/297.03	                 cons(inc(head(ys)), tail(ys)),
759.91/297.03	                 zs,
759.91/297.03	                 append(zs, head(ys))))
759.91/297.03	     , if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       c_16(addLists^#(xs2, ys2, zs))
759.91/297.03	     , if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       c_17(addLists^#(xs, ys, zs2))
759.91/297.03	     , if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18()
759.91/297.03	     , if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19()
759.91/297.03	     , if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_20(zs)
759.91/297.03	     , addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) }
759.91/297.03	   
759.91/297.03	   and mark the set of starting terms.
759.91/297.03	   
759.91/297.03	   We are left with following problem, upon which TcT provides the
759.91/297.03	   certificate MAYBE.
759.91/297.03	   
759.91/297.03	   Strict DPs:
759.91/297.03	     { isEmpty^#(cons(x, xs)) -> c_1()
759.91/297.03	     , isEmpty^#(nil()) -> c_2()
759.91/297.03	     , isZero^#(0()) -> c_3()
759.91/297.03	     , isZero^#(s(x)) -> c_4()
759.91/297.03	     , head^#(cons(x, xs)) -> c_5(x)
759.91/297.03	     , tail^#(cons(x, xs)) -> c_6(xs)
759.91/297.03	     , tail^#(nil()) -> c_7()
759.91/297.03	     , append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x))
759.91/297.03	     , append^#(nil(), x) -> c_9(x)
759.91/297.03	     , p^#(0()) -> c_10()
759.91/297.03	     , p^#(s(0())) -> c_11()
759.91/297.03	     , p^#(s(s(x))) -> c_12(p^#(s(x)))
759.91/297.03	     , inc^#(0()) -> c_13()
759.91/297.03	     , inc^#(s(x)) -> c_14(inc^#(x))
759.91/297.03	     , addLists^#(xs, ys, zs) ->
759.91/297.03	       c_15(if^#(isEmpty(xs),
759.91/297.03	                 isEmpty(ys),
759.91/297.03	                 isZero(head(xs)),
759.91/297.03	                 tail(xs),
759.91/297.03	                 tail(ys),
759.91/297.03	                 cons(p(head(xs)), tail(xs)),
759.91/297.03	                 cons(inc(head(ys)), tail(ys)),
759.91/297.03	                 zs,
759.91/297.03	                 append(zs, head(ys))))
759.91/297.03	     , if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       c_16(addLists^#(xs2, ys2, zs))
759.91/297.03	     , if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       c_17(addLists^#(xs, ys, zs2))
759.91/297.03	     , if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18()
759.91/297.03	     , if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19()
759.91/297.03	     , if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_20(zs)
759.91/297.03	     , addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) }
759.91/297.03	   Strict Trs:
759.91/297.03	     { isEmpty(cons(x, xs)) -> false()
759.91/297.03	     , isEmpty(nil()) -> true()
759.91/297.03	     , isZero(0()) -> true()
759.91/297.03	     , isZero(s(x)) -> false()
759.91/297.03	     , head(cons(x, xs)) -> x
759.91/297.03	     , tail(cons(x, xs)) -> xs
759.91/297.03	     , tail(nil()) -> nil()
759.91/297.03	     , append(cons(y, ys), x) -> cons(y, append(ys, x))
759.91/297.03	     , append(nil(), x) -> cons(x, nil())
759.91/297.03	     , p(0()) -> 0()
759.91/297.03	     , p(s(0())) -> 0()
759.91/297.03	     , p(s(s(x))) -> s(p(s(x)))
759.91/297.03	     , inc(0()) -> s(0())
759.91/297.03	     , inc(s(x)) -> s(inc(x))
759.91/297.03	     , addLists(xs, ys, zs) ->
759.91/297.03	       if(isEmpty(xs),
759.91/297.03	          isEmpty(ys),
759.91/297.03	          isZero(head(xs)),
759.91/297.03	          tail(xs),
759.91/297.03	          tail(ys),
759.91/297.03	          cons(p(head(xs)), tail(xs)),
759.91/297.03	          cons(inc(head(ys)), tail(ys)),
759.91/297.03	          zs,
759.91/297.03	          append(zs, head(ys)))
759.91/297.03	     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       addLists(xs2, ys2, zs)
759.91/297.03	     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       addLists(xs, ys, zs2)
759.91/297.03	     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       differentLengthError()
759.91/297.03	     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       differentLengthError()
759.91/297.03	     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
759.91/297.03	     , addList(xs, ys) -> addLists(xs, ys, nil()) }
759.91/297.03	   Obligation:
759.91/297.03	     runtime complexity
759.91/297.03	   Answer:
759.91/297.03	     MAYBE
759.91/297.03	   
759.91/297.03	   We estimate the number of application of {1,2,3,4,7,10,11,13,18,19}
759.91/297.03	   by applications of Pre({1,2,3,4,7,10,11,13,18,19}) =
759.91/297.03	   {5,6,8,9,12,14,15,20}. Here rules are labeled as follows:
759.91/297.03	   
759.91/297.03	     DPs:
759.91/297.03	       { 1: isEmpty^#(cons(x, xs)) -> c_1()
759.91/297.03	       , 2: isEmpty^#(nil()) -> c_2()
759.91/297.03	       , 3: isZero^#(0()) -> c_3()
759.91/297.03	       , 4: isZero^#(s(x)) -> c_4()
759.91/297.03	       , 5: head^#(cons(x, xs)) -> c_5(x)
759.91/297.03	       , 6: tail^#(cons(x, xs)) -> c_6(xs)
759.91/297.03	       , 7: tail^#(nil()) -> c_7()
759.91/297.03	       , 8: append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x))
759.91/297.03	       , 9: append^#(nil(), x) -> c_9(x)
759.91/297.03	       , 10: p^#(0()) -> c_10()
759.91/297.03	       , 11: p^#(s(0())) -> c_11()
759.91/297.03	       , 12: p^#(s(s(x))) -> c_12(p^#(s(x)))
759.91/297.03	       , 13: inc^#(0()) -> c_13()
759.91/297.03	       , 14: inc^#(s(x)) -> c_14(inc^#(x))
759.91/297.03	       , 15: addLists^#(xs, ys, zs) ->
759.91/297.03	             c_15(if^#(isEmpty(xs),
759.91/297.03	                       isEmpty(ys),
759.91/297.03	                       isZero(head(xs)),
759.91/297.03	                       tail(xs),
759.91/297.03	                       tail(ys),
759.91/297.03	                       cons(p(head(xs)), tail(xs)),
759.91/297.03	                       cons(inc(head(ys)), tail(ys)),
759.91/297.03	                       zs,
759.91/297.03	                       append(zs, head(ys))))
759.91/297.03	       , 16: if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	             c_16(addLists^#(xs2, ys2, zs))
759.91/297.03	       , 17: if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	             c_17(addLists^#(xs, ys, zs2))
759.91/297.03	       , 18: if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18()
759.91/297.03	       , 19: if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19()
759.91/297.03	       , 20: if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	             c_20(zs)
759.91/297.03	       , 21: addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) }
759.91/297.03	   
759.91/297.03	   We are left with following problem, upon which TcT provides the
759.91/297.03	   certificate MAYBE.
759.91/297.03	   
759.91/297.03	   Strict DPs:
759.91/297.03	     { head^#(cons(x, xs)) -> c_5(x)
759.91/297.03	     , tail^#(cons(x, xs)) -> c_6(xs)
759.91/297.03	     , append^#(cons(y, ys), x) -> c_8(y, append^#(ys, x))
759.91/297.03	     , append^#(nil(), x) -> c_9(x)
759.91/297.03	     , p^#(s(s(x))) -> c_12(p^#(s(x)))
759.91/297.03	     , inc^#(s(x)) -> c_14(inc^#(x))
759.91/297.03	     , addLists^#(xs, ys, zs) ->
759.91/297.03	       c_15(if^#(isEmpty(xs),
759.91/297.03	                 isEmpty(ys),
759.91/297.03	                 isZero(head(xs)),
759.91/297.03	                 tail(xs),
759.91/297.03	                 tail(ys),
759.91/297.03	                 cons(p(head(xs)), tail(xs)),
759.91/297.03	                 cons(inc(head(ys)), tail(ys)),
759.91/297.03	                 zs,
759.91/297.03	                 append(zs, head(ys))))
759.91/297.03	     , if^#(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       c_16(addLists^#(xs2, ys2, zs))
759.91/297.03	     , if^#(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       c_17(addLists^#(xs, ys, zs2))
759.91/297.03	     , if^#(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_20(zs)
759.91/297.03	     , addList^#(xs, ys) -> c_21(addLists^#(xs, ys, nil())) }
759.91/297.03	   Strict Trs:
759.91/297.03	     { isEmpty(cons(x, xs)) -> false()
759.91/297.03	     , isEmpty(nil()) -> true()
759.91/297.03	     , isZero(0()) -> true()
759.91/297.03	     , isZero(s(x)) -> false()
759.91/297.03	     , head(cons(x, xs)) -> x
759.91/297.03	     , tail(cons(x, xs)) -> xs
759.91/297.03	     , tail(nil()) -> nil()
759.91/297.03	     , append(cons(y, ys), x) -> cons(y, append(ys, x))
759.91/297.03	     , append(nil(), x) -> cons(x, nil())
759.91/297.03	     , p(0()) -> 0()
759.91/297.03	     , p(s(0())) -> 0()
759.91/297.03	     , p(s(s(x))) -> s(p(s(x)))
759.91/297.03	     , inc(0()) -> s(0())
759.91/297.03	     , inc(s(x)) -> s(inc(x))
759.91/297.03	     , addLists(xs, ys, zs) ->
759.91/297.03	       if(isEmpty(xs),
759.91/297.03	          isEmpty(ys),
759.91/297.03	          isZero(head(xs)),
759.91/297.03	          tail(xs),
759.91/297.03	          tail(ys),
759.91/297.03	          cons(p(head(xs)), tail(xs)),
759.91/297.03	          cons(inc(head(ys)), tail(ys)),
759.91/297.03	          zs,
759.91/297.03	          append(zs, head(ys)))
759.91/297.03	     , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       addLists(xs2, ys2, zs)
759.91/297.03	     , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       addLists(xs, ys, zs2)
759.91/297.03	     , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       differentLengthError()
759.91/297.03	     , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
759.91/297.03	       differentLengthError()
759.91/297.03	     , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
759.91/297.03	     , addList(xs, ys) -> addLists(xs, ys, nil()) }
759.91/297.03	   Weak DPs:
759.91/297.03	     { isEmpty^#(cons(x, xs)) -> c_1()
759.91/297.03	     , isEmpty^#(nil()) -> c_2()
759.91/297.03	     , isZero^#(0()) -> c_3()
759.91/297.03	     , isZero^#(s(x)) -> c_4()
759.91/297.03	     , tail^#(nil()) -> c_7()
759.91/297.03	     , p^#(0()) -> c_10()
759.91/297.03	     , p^#(s(0())) -> c_11()
759.91/297.03	     , inc^#(0()) -> c_13()
759.91/297.03	     , if^#(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> c_18()
759.91/297.03	     , if^#(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) -> c_19() }
759.91/297.03	   Obligation:
759.91/297.03	     runtime complexity
759.91/297.03	   Answer:
759.91/297.03	     MAYBE
759.91/297.03	   
759.91/297.03	   Empty strict component of the problem is NOT empty.
759.91/297.03	
759.91/297.03	
759.91/297.03	Arrrr..
760.12/297.26	EOF