1. f
    1. 
	    1. Als $x\geq 10$ dan zien we dat $x' = x-10$ en $y'=y\cdot x'$, dus zien we dat $y\cdot (x-10)>0$. Als $x<10$ dan zien we dat $y'=-1$, dus moet $-1>0$ en dit is onmogelijk. We zien dus dat $y\cdot (x-10)>0\wedge x\geq 10=y>0 \wedge x>10$ 
	    2. We krijgen aan het einde $$\text{repby}(\text{rebpy}(a, i-1, a[0]+1), 0, 0)$$ We zien dat $\text{repby}(\text{rebpy}(a, i-1, a[0]+1), 0, 0)[0]=0$ en dat $\text{repby}(\text{rebpy}(a, i-1, a[0]+1), 0, 0)[i-1]=a[0]+1$, dus is het resultaat $a[0]+1\geq 0$, oftewel $a[0]\geq -1$.
	2. Complete tells us that the given pre-condition ensures that the program terminates.
	3. We add the pre-condition that $\text{length}(a)>e_1$.
	4. Originally what we did was the following $$\text{wlp} (a[i]:=e) Q = Q[\text{repby}(a,i,e)/a].$$Now we will have a $\text{repby}$ that takes a tuple of three indices, hence$$\text{wlp} (a[i][j][k]:=e) Q = Q[\text{repby}(a,(i,j,k),e)/a].$$
2. 
     1. 
	    1. The invariant is $x\geq 0$. 
        2. $y=10\cdot(10-x)\wedge x\geq 0$ 
        3. $(\forall i : 1\leq i <k : a[i-1]\leq a[i])$
    2. Because $I$ is an invariant we know that $I\implies I$, $\{I\wedge g\} S \{I\}$ and $I\wedge \neg g \implies Q$, hence we see that $I\implies (g\wedge I)\lor (\lnot g\wedge Q)$, We alos see that $((g\wedge I)\lor (\lnot g\wedge Q)) \land g = g\land I$, hence we get $\{((g\wedge I)\lor (\lnot g\wedge Q)) \land g\} S \{I\}$. Finally we see that $$((g\wedge I)\lor (\lnot g\wedge Q))\wedge \neg g=\neg g \wedge Q$$, hence we get $$((g\wedge I)\lor (\lnot g\wedge Q))\wedge \neg g\implies Q$$