YES(?, pow(2, 2*a + 1) + 4*a + 4)

Initial complexity problem:
1:	T:
		(1, 1)    f(a, b, c) -> g(a, 1, 0)
		(?, 1)    g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]
		(?, 1)    g1(a, b, c) -> g(a, c + b, c)
		(?, 1)    g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(?, 1)    h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]
	start location:	f
	leaf cost:	0

A polynomial rank function with
	Pol(f) = 1
	Pol(g) = 1
	Pol(g1) = 1
	Pol(h) = -1
orients all transitions weakly and the transition
	g(a, b, c) -> h(a, b, c) [ a <= 0 ]
strictly and produces the following problem:
2:	T:
		(1, 1)    f(a, b, c) -> g(a, 1, 0)
		(?, 1)    g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]
		(?, 1)    g1(a, b, c) -> g(a, c + b, c)
		(1, 1)    g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(?, 1)    h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]
	start location:	f
	leaf cost:	0

A polynomial rank function with
	Pol(f) = 2*V_1 - 1
	Pol(g) = 2*V_1 - 1
	Pol(g1) = 2*V_1
	Pol(h) = 2*V_1 - 1
orients all transitions weakly and the transition
	g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]
strictly and produces the following problem:
3:	T:
		(1, 1)          f(a, b, c) -> g(a, 1, 0)
		(2*a + 1, 1)    g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]
		(?, 1)          g1(a, b, c) -> g(a, c + b, c)
		(1, 1)          g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(?, 1)          h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]
	start location:	f
	leaf cost:	0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(1, 1)          f(a, b, c) -> g(a, 1, 0)
		(2*a + 1, 1)    g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]
		(2*a + 1, 1)    g1(a, b, c) -> g(a, c + b, c)
		(1, 1)          g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(?, 1)          h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]
	start location:	f
	leaf cost:	0

A polynomial rank function with
	Pol(h) = V_2
and size complexities
	S("h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]", 0-0) = a
	S("h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]", 0-1) = pow(2, 2*a + 1)
	S("h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]", 0-2) = pow(2, 2*a + 1)
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-0) = a
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-1) = pow(2, 2*a + 1)
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-2) = pow(2, 2*a + 1)
	S("g1(a, b, c) -> g(a, c + b, c)", 0-0) = a
	S("g1(a, b, c) -> g(a, c + b, c)", 0-1) = pow(2, 2*a + 1)
	S("g1(a, b, c) -> g(a, c + b, c)", 0-2) = pow(2, 2*a + 1)
	S("g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]", 0-0) = a
	S("g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]", 0-1) = pow(2, 2*a + 1)
	S("g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]", 0-2) = pow(2, 2*a + 1)
	S("f(a, b, c) -> g(a, 1, 0)", 0-0) = a
	S("f(a, b, c) -> g(a, 1, 0)", 0-1) = 1
	S("f(a, b, c) -> g(a, 1, 0)", 0-2) = 0
orients the transition
	h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]
weakly and the transition
	h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]
strictly and produces the following problem:
5:	T:
		(1, 1)                  f(a, b, c) -> g(a, 1, 0)
		(2*a + 1, 1)            g(a, b, c) -> g1(a - 1, b, b) [ a > 0 ]
		(2*a + 1, 1)            g1(a, b, c) -> g(a, c + b, c)
		(1, 1)                  g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(pow(2, 2*a + 1), 1)    h(a, b, c) -> h(a, b - 1, c) [ b > 0 ]
	start location:	f
	leaf cost:	0

Complexity upper bound pow(2, 2*a + 1) + 4*a + 4

Time: 0.246 sec (SMT: 0.234 sec)