Find the loop invariant and prove the termination for the following pseudocode algorithm:

Mystery(x):

y=0

c=0

while c <= x:

y = y+2^c

c = c+1

return y