YES(?, 4*a + 6)

Initial complexity problem:
1:	T:
		(1, 1)    evalndecrstart(a) -> evalndecrentryin(a)
		(?, 1)    evalndecrentryin(a) -> evalndecrbb1in(a - 1)
		(?, 1)    evalndecrbb1in(a) -> evalndecrbbin(a) [ a >= 2 ]
		(?, 1)    evalndecrbb1in(a) -> evalndecrreturnin(a) [ 1 >= a ]
		(?, 1)    evalndecrbbin(a) -> evalndecrbb1in(a - 1)
		(?, 1)    evalndecrreturnin(a) -> evalndecrstop(a)
	start location:	evalndecrstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalndecrstart(a) -> evalndecrentryin(a)
		(?, 1)    evalndecrentryin(a) -> evalndecrbb1in(a - 1)
		(?, 1)    evalndecrbb1in(a) -> evalndecrbbin(a) [ a >= 2 ]
		(?, 1)    evalndecrbbin(a) -> evalndecrbb1in(a - 1)
	start location:	evalndecrstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalndecrstart(a) -> evalndecrentryin(a)
		(1, 1)    evalndecrentryin(a) -> evalndecrbb1in(a - 1)
		(?, 1)    evalndecrbb1in(a) -> evalndecrbbin(a) [ a >= 2 ]
		(?, 1)    evalndecrbbin(a) -> evalndecrbb1in(a - 1)
	start location:	evalndecrstart
	leaf cost:	2

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

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)          evalndecrstart(a) -> evalndecrentryin(a)
		(1, 1)          evalndecrentryin(a) -> evalndecrbb1in(a - 1)
		(2*a + 1, 1)    evalndecrbb1in(a) -> evalndecrbbin(a) [ a >= 2 ]
		(2*a + 1, 1)    evalndecrbbin(a) -> evalndecrbb1in(a - 1)
	start location:	evalndecrstart
	leaf cost:	2

Complexity upper bound 4*a + 6

Time: 0.074 sec (SMT: 0.071 sec)