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

Initial complexity problem:
1:	T:
		(1, 1)    f(a, b) -> g(a, b)
		(?, 1)    g(a, b) -> g(2*a, b - 1) [ b > 0 ]
		(?, 1)    g(a, b) -> h(a, b) [ 0 >= b ]
		(?, 1)    h(a, b) -> h(a - 1, b) [ a > 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) [ 0 >= b ]
strictly and produces the following problem:
2:	T:
		(1, 1)    f(a, b) -> g(a, b)
		(?, 1)    g(a, b) -> g(2*a, b - 1) [ b > 0 ]
		(1, 1)    g(a, b) -> h(a, b) [ 0 >= b ]
		(?, 1)    h(a, b) -> h(a - 1, b) [ a > 0 ]
	start location:	f
	leaf cost:	0

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

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

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

Time: 0.236 sec (SMT: 0.225 sec)