WORST_CASE(?, O(n^1))

Initial complexity problem:
1:	T:
		(Comp: ?, Cost: 1)    evalndecrstart(Ar_0) -> Com_1(evalndecrentryin(Ar_0))
		(Comp: ?, Cost: 1)    evalndecrentryin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: ?, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrbbin(Ar_0)) [ Ar_0 >= 2 ]
		(Comp: ?, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrreturnin(Ar_0)) [ 1 >= Ar_0 ]
		(Comp: ?, Cost: 1)    evalndecrbbin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: ?, Cost: 1)    evalndecrreturnin(Ar_0) -> Com_1(evalndecrstop(Ar_0))
		(Comp: 1, Cost: 0)    koat_start(Ar_0) -> Com_1(evalndecrstart(Ar_0)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2:	T:
		(Comp: 1, Cost: 1)    evalndecrstart(Ar_0) -> Com_1(evalndecrentryin(Ar_0))
		(Comp: 1, Cost: 1)    evalndecrentryin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: ?, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrbbin(Ar_0)) [ Ar_0 >= 2 ]
		(Comp: ?, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrreturnin(Ar_0)) [ 1 >= Ar_0 ]
		(Comp: ?, Cost: 1)    evalndecrbbin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: ?, Cost: 1)    evalndecrreturnin(Ar_0) -> Com_1(evalndecrstop(Ar_0))
		(Comp: 1, Cost: 0)    koat_start(Ar_0) -> Com_1(evalndecrstart(Ar_0)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(evalndecrstart) = 2
	Pol(evalndecrentryin) = 2
	Pol(evalndecrbb1in) = 2
	Pol(evalndecrbbin) = 2
	Pol(evalndecrreturnin) = 1
	Pol(evalndecrstop) = 0
	Pol(koat_start) = 2
orients all transitions weakly and the transitions
	evalndecrreturnin(Ar_0) -> Com_1(evalndecrstop(Ar_0))
	evalndecrbb1in(Ar_0) -> Com_1(evalndecrreturnin(Ar_0)) [ 1 >= Ar_0 ]
strictly and produces the following problem:
3:	T:
		(Comp: 1, Cost: 1)    evalndecrstart(Ar_0) -> Com_1(evalndecrentryin(Ar_0))
		(Comp: 1, Cost: 1)    evalndecrentryin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: ?, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrbbin(Ar_0)) [ Ar_0 >= 2 ]
		(Comp: 2, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrreturnin(Ar_0)) [ 1 >= Ar_0 ]
		(Comp: ?, Cost: 1)    evalndecrbbin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: 2, Cost: 1)    evalndecrreturnin(Ar_0) -> Com_1(evalndecrstop(Ar_0))
		(Comp: 1, Cost: 0)    koat_start(Ar_0) -> Com_1(evalndecrstart(Ar_0)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

A polynomial rank function with
	Pol(evalndecrstart) = 2*V_1
	Pol(evalndecrentryin) = 2*V_1
	Pol(evalndecrbb1in) = 2*V_1 + 2
	Pol(evalndecrbbin) = 2*V_1 + 1
	Pol(evalndecrreturnin) = 2*V_1 + 2
	Pol(evalndecrstop) = 2*V_1 + 2
	Pol(koat_start) = 2*V_1
orients all transitions weakly and the transition
	evalndecrbb1in(Ar_0) -> Com_1(evalndecrbbin(Ar_0)) [ Ar_0 >= 2 ]
strictly and produces the following problem:
4:	T:
		(Comp: 1, Cost: 1)         evalndecrstart(Ar_0) -> Com_1(evalndecrentryin(Ar_0))
		(Comp: 1, Cost: 1)         evalndecrentryin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: 2*Ar_0, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrbbin(Ar_0)) [ Ar_0 >= 2 ]
		(Comp: 2, Cost: 1)         evalndecrbb1in(Ar_0) -> Com_1(evalndecrreturnin(Ar_0)) [ 1 >= Ar_0 ]
		(Comp: ?, Cost: 1)         evalndecrbbin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: 2, Cost: 1)         evalndecrreturnin(Ar_0) -> Com_1(evalndecrstop(Ar_0))
		(Comp: 1, Cost: 0)         koat_start(Ar_0) -> Com_1(evalndecrstart(Ar_0)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(Comp: 1, Cost: 1)         evalndecrstart(Ar_0) -> Com_1(evalndecrentryin(Ar_0))
		(Comp: 1, Cost: 1)         evalndecrentryin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: 2*Ar_0, Cost: 1)    evalndecrbb1in(Ar_0) -> Com_1(evalndecrbbin(Ar_0)) [ Ar_0 >= 2 ]
		(Comp: 2, Cost: 1)         evalndecrbb1in(Ar_0) -> Com_1(evalndecrreturnin(Ar_0)) [ 1 >= Ar_0 ]
		(Comp: 2*Ar_0, Cost: 1)    evalndecrbbin(Ar_0) -> Com_1(evalndecrbb1in(Ar_0 - 1))
		(Comp: 2, Cost: 1)         evalndecrreturnin(Ar_0) -> Com_1(evalndecrstop(Ar_0))
		(Comp: 1, Cost: 0)         koat_start(Ar_0) -> Com_1(evalndecrstart(Ar_0)) [ 0 <= 0 ]
	start location:	koat_start
	leaf cost:	0

Complexity upper bound 4*Ar_0 + 6

Time: 0.306 sec (SMT: 0.296 sec)