[Ctx C: a, b: nat & b>=0
	{Q: T}

	x, y, z := a, b, 1;
	
	{Inv P: y>=0 & z*x^y = a^b}
	
	{cota t: y}
	
	do y > 1 ->
		if y mod 2 = 0 -> 
			x, y := x * x, y / 2;
		[] y mod 2 != 0 -> 
			z, x, y := z * x, x * x, (y - 1) / 2;
		fi
	od
	
	z = x * y;
	
	{R: z = a^b}
]