Loop invariants in logic I am working on some questions about hoare calculus/logic. The given program $\pi$ is:  
$ x:=0; y:=1; WHILE \; \lnot x=n \; DO (y:=2y+x + 1; \; x:= x + 1) $
The hoare-logic rules that I can use are in the list below)
H1 {[$t$\x]$\varphi$} x := $t$ {$\varphi$}, provided that $t$ is free for $x$ in $\varphi$
H2 from {$\varphi$} $\pi_1$ {$\psi$} and {$\psi$} $\pi_2$ {$\chi$} follows {$\varphi$} ($\pi_1;\pi_2$) {$\chi$}
H3 from {$\varphi \wedge \epsilon$} $\pi_1$ {$\psi$} and {$\varphi \wedge \neg \epsilon$} $\pi_2$ {$\psi$} follows {$\varphi$} IF $\epsilon$ THEN $\pi_1$ ELSE $\pi_2$ {$\psi$}
H4 from {$\varphi \wedge \epsilon$} $\pi$ {$\varphi$} follows {$\varphi$} WHILE $\epsilon$ DO $\pi$ {$\neg \epsilon \wedge \varphi$}
H5 if $\varphi \rightarrow \varphi`$ and $\psi \rightarrow \psi`$ are true in M = (D, I), then: from {$\varphi`$} $\pi$ {$\psi`$} follows {$\varphi$} $\pi$ {$\psi$}
The questions are:  
1) Show that $y = 3 \cdot 2 ^x - x - 2$ is a loop variant for the while-loop from the program $\pi$.
2) Prove $\{true\} \; \pi \{y = 3 \cdot 2^n -n - 2 \} $ .
An update for my solution for the first question, so far. Made some edits.   
1) $ \{y = 3 \cdot 2 ^x - x - 2\} \; y:=2y+x + 1; \; x:= x + 1 \; \{y = 3 \cdot 2 ^x - x - 2\} $  Start   
2) $ \{y=3⋅2x^{+1}−(x+1)−2\} \; x:= x + 1 \; \{y = 3 \cdot 2 ^x - x - 2\} $ H1.  substitute $[x+1/x]$ in the precondition, starting from the right.    
3) $ \{2y +x+1 = 3 \cdot 2 ^{x+1} - x - 3\} \; y:=2y+x + 1; \; \{y = 3 \cdot 2 ^x - x - 2\}$ H1. Substitution: $[y:=2y+x + 1;/y]$ in the precondition, starting from the right.    
4) $ \{2y +x+1 = 3 \cdot 2 ^{x+1} - x - 3\} y:=2y+x + 1; \; x:= x + 1 \{y = 3 \cdot 2 ^x - x - 2\} $ H2 on 2,3  
5) $ \{y = 3 \cdot 2 ^x - x - 2 \land \lnot x = n\} y:=2y+x + 1; \; x:= x + 1 \{y = 3 \cdot 2 ^x - x - 2\} $ H5 on 4  
6)  $\{y = 3 \cdot 2 ^x - x - 2\} WHILE \lnot x = n\ DO \; y:=2y+x + 1; \; x:= x + 1 \{y = 3 \cdot 2 ^x - x - 2\} $ H4, apply the loop      
Question 2. I have continued the numbering:
7) $ \{y=1\}  y:=1 \; \{y:=1\} \; $ H1    
8) $ \{0=0\} x:=0 \{x:=0\} $ H1 
9) $ \{0=0\} x:=0; \; y:=1 \{ x:=0 \} $ H2, 7,8 
10) $ \{TRUE\} \; x:= 0 \; ;y:=1; \; \{y = 3 \cdot 2 ^x - n - 2\} \; $ H5,9   
11) $ \{TRUE\} \; x:= 0 \; ;y:=1; \; WHILE \lnot x = n\ DO \; y:=2y+x + 1; \; x:= x+1 \{y = 3 \cdot 2 ^x - x - 2\} $  H2 on 6 and 10

Here's what we want to prove:
{y = 3*2^x - x - 2}
y := 2*y + x + 1;
x := x + 1;
{y = 3*2^x - x - 2}

Indeed, this follows easily after sticking another assertion between the two assignments:
{y = 3*2^x - x - 2}
y := 2*y + x + 1;
{y = 3*2^(x + 1) - x - 3}
x := x + 1;
{y = 3*2^x - x - 2}

To see why the first 3 lines hold, observe that:
\begin{align*}
&y = 3 \cdot 2^x - x - 2 \\
&\implies 2y + x + 1 = 2(3 \cdot 2^x - x - 2) + x + 1 \\
&\implies 2y + x + 1 = (3 \cdot 2^{x + 1} - 2x - 4) + x + 1 \\
&\implies 2y + x + 1 = 3 \cdot 2^{x + 1} - x - 3
\end{align*}
Likewise, to see why the last $3$ lines hold, observe that:
\begin{align*}
&y = 3 \cdot 2^{x + 1} - x - 3 \\
&\implies y = 3 \cdot 2^{x + 1} - (x + 1) - 2
\end{align*}

For the second question, combine H4 with your loop invariant (after noting that the initial conditions satisfy the loop invariant) so that you can replace $x$ with $n$.
