YES(?, pow(2, a) + a + 2)

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

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

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

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

Complexity upper bound pow(2, a) + a + 2

Time: 0.239 sec (SMT: 0.229 sec)