+\end{equation}
+}
+
+\paragraph{Postcondition}
+Finally the post condition can be described as $a_i>50$ and some other
+$a_i= a_j\wedge i\neq j$ for all $i$. This is expressed in
+Equation~\ref{eq:4pst}
+
+\begin{equation}\label{eq:4pst}
+ \bigvee_{k=2}^{I-1}\left(
+ (i_Na_k >= 50)\wedge
+ \left(\bigvee_{j=2}^{I-1}(i_Na_k=i_Na_j)\wedge(k\neq j)\right)
+ \right)
+\end{equation}
+
+\paragraph{Total}
+To tie this all together we just put $\wedge$ in between and that results in:
+$$\text{precondition }\wedge\text{ program }\wedge\text{ postcondition}$$
+
+\subsection{SMT format solution}
+Naming the precondition, program and postcondition respectively $p_1, p_2, p_3$
+we can easily convert it to a SMT format. The converting is tedious and takes a
+lot of time and therefore an automatization script has been created that is
+visible in the appendices in Listing~\ref{listing:4.py}. The script
+automatically assumes $11$ iterations and $7$ $a_i$ variables but via command
+line arguments this is easily extendable. To determine the minimal number of
+iterations a simple bash script can be made that iteratively increases the
+iterations as shown in Listing~\ref{listing:4bash}. The shortest solution with
+length $11$ is found in around $30$ seconds. Finding the smallest solution
+length incrementally takes around $75$ seconds.
+
+\begin{lstlisting}[language=bash,
+ caption={Iteratively find the shortest solution},label={listing:4bash}]
+i=1
+while [ "$(python a4.py $i | yices-smt)" = "unsat" ]
+do
+ i=$((i+1))
+ echo $i;
+done
+\end{lstlisting}