-After processing each $\pc$ we will have created:
-
-\begin{itemize}
-
-\item $\tipcn$ and $\tipcy$ such that $\baseof{\tipcy} = \tipcn$.
-
-\end{itemize}
+After processing each $\pc$ we will have created $\tipcn$ and $\tipcy$
+such that:
+
+\statement{Correct Base}{
+ \baseof{\tipcy} = \tipcn
+}
+\statement{Tip Exceeds Inputs}{
+ \tipcy \ge \pendsof{\allsrcs}{\pcy}
+}
+\statement{Base Exceeds Inputs' Bases}{
+ \bigforall_{E \in \pendsof{\allsrcs}{\pcy}} \tipcn \ge \baseof{E}
+}
+\statement{Base Exceeds Base Inputs}{
+ \bigforall_{H \in \set H^{\pn}} \tipcn \ge H
+}