diff --git a/.gitignore b/.gitignore
index 834c601..c2ba089 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,15 @@
+# LaTeX
+*.synctex.gz
+*.cls
+*.aux
+*.fdb_latexmk
+*.fls
+*.log
+*.out
+*.bbl
+*.blg
+
+# OCaml
 *.annot
 *.cmo
 *.cma
@@ -25,6 +37,9 @@ setup.log
 # Dune generated files
 *.install
 
-# Local OPAM switch
+# local OPAM switch
 _opam/
 .DS_Store
+
+# VS code
+.vscode/
diff --git a/.vscode/settings.json b/.vscode/settings.json
deleted file mode 100644
index f440e5a..0000000
--- a/.vscode/settings.json
+++ /dev/null
@@ -1,6 +0,0 @@
-{
-    "ocaml.sandbox": {
-        "kind": "opam",
-        "switch": "cs3110-2023fa"
-    }
-}
\ No newline at end of file
diff --git a/pieo-trees/notes.pdf b/pieo-trees/notes.pdf
new file mode 100644
index 0000000..5d9b33a
Binary files /dev/null and b/pieo-trees/notes.pdf differ
diff --git a/pieo-trees/notes.tex b/pieo-trees/notes.tex
new file mode 100644
index 0000000..2370fca
--- /dev/null
+++ b/pieo-trees/notes.tex
@@ -0,0 +1,750 @@
+\documentclass{amsart}
+
+% font
+\usepackage{cmbright}
+
+% margin 
+\usepackage[margin=1in]{geometry}
+
+% references
+\usepackage[colorlinks]{hyperref} 
+\PassOptionsToPackage{colorlinks}{hyperref}
+\hypersetup{urlcolor = RedViolet, linkcolor = RoyalBlue, citecolor = NavyBlue}
+
+% basics
+\usepackage[leqno]{amsmath}
+\usepackage{amssymb, amsthm} 
+\usepackage[svgnames, dvipsnames]{xcolor}
+\usepackage{mhsetup, mathtools}
+\usepackage[capitalise]{cleveref}
+
+% commutative diagram
+\usepackage{tikz-cd}
+
+% hats
+\usepackage{yhmath}
+
+% PL macros
+\usepackage{mathpartir}
+\usepackage{stmaryrd}
+\newcommand{\inference}[3]{\inferrule*[Right=#1]{#2}{#3}}
+\newcommand{\axiom}[2]{\inferrule*[Right=#1]{\;}{#2}}
+
+% (Formal Abstractions macros)++
+\DeclareMathOperator{\halfto}{\rightharpoonup}
+\DeclareMathOperator{\pkt}{\mathrm{pkt}}
+\DeclareMathOperator{\push}{\mathrm{push}}
+\DeclareMathOperator{\pop}{\mathrm{pop}}
+\DeclareMathOperator{\proj}{\mathrm{proj}}
+\DeclareMathOperator{\Pkt}{\mathbf{Pkt}}
+\DeclareMathOperator{\Rk}{\mathbf{Rk}}
+\DeclareMathOperator{\Data}{\mathbf{Data}}
+\DeclareMathOperator{\Topo}{\mathbf{Topo}}
+\DeclareMathOperator{\Path}{\mathbf{Path}}
+\DeclareMathOperator{\PIEO}{\mathbf{PIEO}}
+\DeclareMathOperator{\PIFO}{\mathbf{PIFO}}
+\DeclareMathOperator{\PIEOTree}{\mathbf{PIEOTree}}
+\DeclareMathOperator{\PIFOTree}{\mathbf{PIFOTree}}
+\DeclareMathOperator{\Leaf}{\mathrm{Leaf}}
+\DeclareMathOperator{\Internal}{\mathrm{Internal}}
+\DeclareMathOperator{\Node}{\mathrm{Node}}
+
+% theorems
+\newtheorem{thm}{Theorem}[section]
+\newtheorem{lem}[thm]{Lemma}
+\theoremstyle{definition}
+\newtheorem{dfn}[thm]{Definition}
+\newtheorem{abuse}[thm]{Abuse of Notation}
+\newtheorem{ex}[thm]{Example}
+\newtheorem{rem}[thm]{Remark}
+
+% no more indent
+\setlength{\parindent}{0pt}
+
+% right-justified sections hack
+\usepackage{titlesec}
+\newcommand{\marginsecnumber}[1]{%
+  \makebox[0pt][r]{#1\hspace{6pt}}%
+}
+\titleformat{\section}
+  {\normalfont\Large\bfseries}
+  {\marginsecnumber\thesection}
+  {0pt}
+  {}
+\titleformat{\subsection}
+  {\normalfont\large\bfseries}
+  {\marginsecnumber\thesubsection}
+  {0pt}
+  {}
+\titleformat{\subsubsection}
+  {\normalfont\normalsize\bfseries}
+  {\marginsecnumber\thesubsubsection}
+  {0pt}
+  {}
+
+% tag on the right hack
+\makeatletter
+\newcommand{\leqnomode}{\tagsleft@true\let\veqno\@@leqno}
+\newcommand{\reqnomode}{\tagsleft@false\let\veqno\@@eqno}
+\makeatother
+
+\begin{document}
+
+\pagestyle{empty}
+
+{\LARGE \textbf{PIEO Trees for Fun and Profit}}
+
+\hrulefill\\
+
+\reqnomode
+
+We assume familiarity with \cite{OG}, adopt its notational conventions, and borrow many of its definitions!
+
+\section{Structure \& Semantics}
+
+\begin{dfn}
+    \label{dfn:pieo}
+    For sets $S$, $D$, and predicates $F$ over $D$,
+    let $\PIEO(S, D, F)$ denote the set of \emph{PIEO}s that
+    \begin{enumerate}
+        \item hold entries in $S$, decorated with meta-data in $D$
+        \item are ordered by $\Rk$
+        \item support predicates in $F$
+        \item admit partial functions 
+        \begin{align*}
+            \pop &: \PIEO(S, D, F) \times F \halfto S \times \PIEO(S, D, F) \\
+            \push &: \PIEO(S, D, F) \times S \times D \times \Rk \to \PIEO(S, D, F) \\
+            \proj &: \PIEO(S, D, F) \times F \to \PIFO(S)
+        \end{align*}
+    \end{enumerate}
+    Maps $\push$ and $\pop$ are as usual.
+    The \emph{projection} $\proj(p, f)$ is the PIFO of entries in $p$ with data satisfying $f$.
+    These three maps play nicely together: 
+    \begin{align}
+        \pop(p, f) \text{ is undefined} &\iff \pop(\proj(p, f)) \text{ is undefined} \label{eq:pieo1}\\
+        \pop(p, f) = (\pkt, p^\prime) &\implies \pop(\proj(p, f)) = (\pkt, \proj(p^\prime, f)) \label{eq:pieo2}\\
+        \proj(\push(p, s, d, r), f) &= 
+        \begin{cases}
+            \push(\proj(p, f), s, r) & f(d) \text{ holds true}\\
+            \proj(p, f) & \text{otherwise}
+        \end{cases}
+        \label{eq:pieo3}
+    \end{align}
+    We consider PIEOs $p, p^\prime$ equal if, for all $f \in F$, $\proj(p,f) = \proj(p^\prime, f)$, i.e. their projections are always equal.
+
+    For PIEO $p$, entry $s \in S$, and predicate $f \in F$, we write 
+    \begin{enumerate}
+        \item $|p|$ for the number of entries in $p$
+        \item $|p|_{f}$ for the number of entries in $p$ satisfying $f$
+        \item $|p|_{s,f}$ for the number of times $s$ occurs in $p$ with associated $d \in D$ such that $f(d)$ holds
+    \end{enumerate}
+\end{dfn}
+
+We fix an opaque set $\Data$ and a collection $\mathcal F$ of predicates defined on it.
+These predicates come with a total order $\leq$ and the property that, $\forall d \in \Data$ and $f,f^\prime \in \mathcal F$,
+$f \leq f^\prime \land f(d) \implies f^\prime(d)$.
+
+\begin{dfn}
+    The set of \emph{PIEO trees} over $t \in \Topo$, denoted $\mathbf{PIEOTree}(t)$, is defined inductively by
+    \begin{align*}
+        \inference{}
+        {
+            p \in \mathbf{PIEO}(\Pkt, \Data, \mathcal F)
+        }
+        {
+            \Leaf(p) \in \mathbf{PIEOTree}(\ast)
+        }
+        &&
+        \inference{}
+        {
+            n \in \mathbb N\\
+            ts \in \mathbf{Topo}^n\\
+            p \in \mathbf{PIEO}(\{1,\ldots, n\}, \mathbf{Data}, \mathcal F)\\\\
+            \forall i \in [1, n]. \; qs[i] \in \mathbf{PIEOTree}(ts[i])
+        }
+        {
+            \Internal(qs, p) \in \PIEOTree(\Node(ts))
+        }
+    \end{align*}
+\end{dfn}
+
+\begin{dfn}
+    \label{dfn:pop}
+    Define $\pop : \PIEOTree(t) \times \mathcal F \halfto \Pkt \times \PIEOTree(t)$ by
+    \begin{align*}
+        \inference{}
+        {
+            \pop(p, f) = (\pkt, p^\prime)
+        }
+        {
+            \pop(\Leaf(p), f) = (\pkt, \Leaf(p^\prime))
+        }
+        &&
+        \inference{}
+        {
+            \pop(p, f) = (i, p^\prime)\\
+            \pop(qs[i], f) = (\pkt, q^\prime)
+        }
+        {
+            \pop(\Internal(qs, p), f) = (\pkt, \Internal(qs[q^\prime/i], p^\prime))
+        }
+    \end{align*}
+\end{dfn}
+
+\begin{dfn}
+    \label{dfn:push}
+    Define $\push : \PIEOTree(t) \times \Pkt \times \Data \times \Path(t) \to \PIEOTree(t)$ by
+    \begin{align*}
+        \inference{}
+        {
+            \push(p, \pkt, d, r) = p^\prime
+        }
+        {
+            \push(\Leaf(p), \pkt, d, r) = \Leaf(p^\prime)
+        }
+        &&
+        \inference{}
+        {
+            \push(p, i, d, r) = p^\prime\\ 
+            \push(qs[i],  \pkt, d, pt) = q^\prime
+        }
+        {
+            \push(\Internal(qs, p), \pkt, d, (i, r) :: pt) = \Internal(qs[q^\prime/i], p^\prime)
+        }
+    \end{align*}
+\end{dfn}
+
+\begin{dfn}
+    Let $t \in \Topo$. 
+    A \emph{control} over $t$ is a triple $(s, q, z)$, where $s \in \mathrm{St}$ is the \emph{current state},
+    $q$ is a PIEO tree of topology $t$, and 
+    $$z : \mathrm{St} \times \Pkt \to \Data \times \Path(t) \times \mathrm{St}$$
+    is a function called the \emph{scheduling transaction}.
+\end{dfn}
+
+\section{Well-Formedness}
+
+\begin{dfn}
+    Fix $f \in \mathcal F$.
+    Define $|\cdot|_f : \PIEOTree(t) \to \mathbb N$ by
+    \begin{align*}
+        |\Leaf(p)|_f = |p|_f && |\Internal(qs, p)|_f = \sum_{i=1}^{|qs|} |qs[i]|_f
+    \end{align*}
+
+    We say $q \in \PIEOTree(t)$ is \emph{well-formed} w.r.t. $f$, denoted $\models_f q$, if it adheres to the following rules.
+    \begin{align*}
+        \axiom{}
+        {\vdash_f \Leaf(p)}
+        &&
+        \inference{}
+        {
+            \forall i \in [1, |qs|], \; \vdash_f qs[i] \land |p|_{i, f} = |qs[i]|_f
+        }
+        {
+            \vdash_f \Internal(qs, p)
+        }
+    \end{align*}
+
+    We say $q$ is $f$-well-formed, denoted $\vdash_f q$, if for all $f^\prime \geq f$, $\models_{f^\prime} q$.
+\end{dfn}
+
+\begin{thm}
+    Let $t \in \Topo$, $\pkt \in \Pkt$, $d \in \Data$, $f,f^\prime \in \mathcal F$, and $q \in \PIEOTree(t)$ such that $\vdash_f q$.
+    \begin{enumerate}
+        \item If $pt \in \Path(t)$, then $\push(q, \pkt, d, pt)$ is well-defined and $\vdash_f \push(q, \pkt, d, pt)$.
+        \item If $|q|_{f^\prime} > 0$ and $f^\prime \geq f$, then $\pop(q, f^{\prime})$ is well-defined and $\vdash_{f^\prime} q^\prime$, where $\pop(q, f^{\prime}) = (\pkt, q^\prime)$.
+    \end{enumerate}
+\end{thm}
+
+\begin{proof}
+    \textcolor{red}{TBD}
+\end{proof}
+
+\section{Projection}
+
+\begin{dfn}
+    \label{dfn:proj}
+    For $f \in \mathcal F$, define $\proj_f: \PIEOTree(t) \to \PIFOTree(t)$ by
+    \begin{align*}
+        \inference{}  
+        {
+            p^\prime = \proj(p, f)
+        }
+        {
+            \proj_f(\Leaf(p)) = \Leaf(p^\prime)
+        }
+        &&
+        \inference{}
+        {
+            p^\prime = \proj(p, f)\\
+            \forall i \in [1, |qs|], \; qs^\prime[i] = \proj_f(qs[i])
+        }
+        {
+            \proj_f(\Internal(qs, p)) = \Internal(qs^\prime, p^\prime)
+        }
+    \end{align*}
+\end{dfn}
+
+\begin{lem}
+    \label{lem:pieotree_eq}
+    For $q, q^\prime \in \PIEOTree(t)$,
+    $$\forall f \in \mathcal F, \; \proj_f(q) = \proj_f(q^\prime) \implies q = q^\prime$$
+\end{lem}
+
+\begin{proof}
+    Suppose $\proj_f(q) = \proj_f(q^\prime)$ for all $f \in \mathcal F$.
+    We'll proceed by induction on $t$ to show $q = q^\prime$.
+    \begin{itemize}
+        \item[(Leaf)] For $t = \ast$, let $q = \Leaf(p)$ and $q^\prime = \Leaf(p^\prime)$.
+            Since $$\proj_f(q) = \Leaf(\proj(p, f)) = \Leaf(\proj(p^\prime, f)) = \proj_f(q^\prime)$$
+            we know $\proj(p, f) = \proj(p^\prime, f)$ for all $f \in \mathcal F$.
+            By \Cref{dfn:pieo}, $p = p^\prime$ and hence $q = q^\prime$.
+
+        \item[(Node)] For $t = \Node(ts)$ and $n = |ts|$, let $q = \Internal(qs, p)$ and $q^\prime = \Internal(qs^\prime, p^{\prime})$.
+            Notice
+            \begin{align*}
+                \proj(p, f) &= \proj(p^\prime, f)\\
+                \proj_f(qs[i]) &= \proj_f(qs^\prime[i]) \tag{$i = 1,\ldots, n$}
+            \end{align*}
+            for all $f \in \mathcal F$. 
+            Hence, $p = p^\prime$ via \Cref{dfn:pieo} and $qs = qs^\prime$ by the inductive hypothesis, i.e. $q = q^\prime$.
+    \end{itemize}
+\end{proof}
+
+\begin{lem}
+    \label{lem:pop_undef}
+    For $q \in \PIEOTree(t)$ and $f \in \mathcal F$, $\pop(q, f)$ is undefined if and only if $\pop(\proj_f(q))$ is undefined.
+\end{lem}
+
+\begin{proof}
+    We'll do induction on $t$.
+    \begin{itemize}
+        \item[(Leaf)] For $t = \ast$, let $q = \Leaf(p)$ and $\proj_f(q) = \Leaf(p^\prime)$.
+            By \Cref{eq:pieo1} in \Cref{dfn:pieo},
+            \begin{align*}
+                \pop(q, f) \text{ is undefined} &\iff \pop(p, f) \text{ is undefined} \\
+                                                &\iff \pop(p^\prime) \text{ is undefined} \\
+                                                &\iff \pop(\proj_f(q)) \text{ is undefined}
+            \end{align*}
+
+        \item[(Node)] For $t = \Node(ts)$, let $q = \Internal(qs, p)$ and $\proj_f(q) = \Internal(qs^\prime, p^\prime)$.
+            As before, 
+            $$\pop(p, f) \text{ is undefined} \iff \pop(p^\prime) \text{ is undefined}$$
+            by \Cref{eq:pieo1} in \Cref{dfn:pieo} and 
+            $$\pop(qs[i], f) \text{ is undefined} \iff \pop(qs^\prime[i]) \text{ is undefined $\forall i \in [1, |ts|]$}$$
+            by the inductive hypothesis.
+            Hence, using \Cref{eq:pieo2} in \Cref{dfn:pieo}, 
+            \begin{align*}
+                \pop(q, f) \text{ is undefined} &\iff \pop(p, f) \text{ is undefined} \lor (\pop(p, f) = (i, \_) \land \pop(qs[i], f) \text{ is undefined})\\
+                                                &\iff \pop(p^\prime) \text{ is undefined} \lor (\pop(p^{\prime}) = (i, \_) \land \pop(qs^{\prime}[i]) \text{ is undefined})\\
+                                                &\iff \pop(\proj_f(q)) \text{ is undefined}
+            \end{align*}
+    \end{itemize}
+\end{proof}
+
+\begin{lem}
+    \label{lem:pop}
+    For $q \in \PIEOTree(t)$ and $f \in \mathcal F$, 
+    $$
+        \pop(q, f) = (\pkt, q^\prime) \implies \pop(\proj_f(q)) = (\pkt, \proj_f(q^\prime))
+    $$
+\end{lem}
+
+\begin{proof}
+    More induction on $t$!
+    \begin{itemize}
+        \item[(Leaf)] For $t = \ast$, let
+            \begin{align*}
+                q = \Leaf(p_1) && \proj_f(q) = \Leaf(p_2)\\
+                q^{\prime} = \Leaf(p_1^\prime) && \proj_f(q^\prime) = \Leaf(p_2^\prime)
+            \end{align*}
+            By \Cref{eq:pieo2} in \Cref{dfn:pieo},
+            \begin{align*}
+                \pop(q, f) = (\pkt, q^\prime) &\implies \pop(p_1, f) = (\pkt, p_1^\prime)\\
+                                              &\implies \pop(p_2) = \pop(\proj(p_1, f)) = (\pkt, \proj(p_1^\prime, f)) = (\pkt, p_2^\prime)\\
+                                              &\implies \pop(\proj_f(q)) = (\pkt, \proj_f(q^\prime))
+            \end{align*}
+
+        \item[(Node)] For $t = \Node(ts)$, Let
+            \begin{align*}
+                q = \Internal(qs_1, p_1) && \proj_f(q) = \Internal(qs_2, p_2)\\
+                q^{\prime} = \Internal(qs_1^\prime, p_1^\prime) && \proj_f(q^\prime) = \Internal(qs_2^\prime, p_2^\prime)
+            \end{align*}
+            Using \Cref{eq:pieo2} in \Cref{dfn:pieo} again and the inductive hypothesis,
+            \begin{align*}
+                \pop(q, f) = (\pkt, q^\prime) &\implies \pop(p_1, f) = (i, p_1^\prime) \land \pop(qs_1[i], f) = (\pkt, qs_1^\prime[i])\\
+                                              &\implies \pop(\proj(p_1, f)) = (i, \proj(p_1^\prime, f)) \land \pop(\proj_f(qs_1[i])) = (\pkt, \proj_f(qs_1^\prime[i]))\\
+                                              &\implies \pop(p_2) = (i, p_2^\prime) \land \pop(qs_2[i]) = (\pkt, qs_2^\prime[i])\\
+                                              &\implies \pop(\proj_f(q)) = (\pkt, \proj_f(q^\prime))
+            \end{align*}
+    \end{itemize}
+\end{proof}
+
+\begin{lem}
+    \label{lem:push}
+    For $q \in \PIEOTree(t)$, $\pkt \in \Pkt$, $d \in \Data$, $pt \in \Path(t)$, and $f \in \mathcal F$,
+    $$
+        \proj_f(\push(q, \pkt, d, pt)) = 
+        \begin{cases}
+            \push(\proj_f(q), \pkt, pt) & f(d) \text{ holds true}\\
+            \proj_f(q) & \text{otherwise}
+        \end{cases}
+    $$
+\end{lem}
+
+\begin{proof}
+    Even more induction on $t$!
+    \begin{itemize}
+        \item[(Leaf)] For $t = \ast$, let $q = \Leaf(p)$ and $pt = r$.
+            By \Cref{eq:pieo3} in \Cref{dfn:pieo}.
+            \begin{align*}
+                \proj_f(\push(q, \pkt, d, pt)) &= \Leaf(\proj(\push(p, \pkt, d, r), f)) \\
+                                              &=
+                \begin{cases}
+                    \Leaf(\push(\proj(p, f), \pkt, r)) & f(d) \text{ holds true}\\
+                    \Leaf(\proj(p, f)) & \text{otherwise}
+                \end{cases}\\
+                                              &= 
+                \begin{cases}
+                    \push(\proj_f(q), \pkt, pt) & f(d) \text{ holds true}\\
+                    \proj_f(q) & \text{otherwise}
+                \end{cases}
+            \end{align*}
+
+        \item[(Node)] For $t = \Node(ts)$, let $pt = (i, r) :: pt^\prime$ and
+            \begin{align*}
+                q &= \Internal(qs, p)\\
+                \proj_f(q) &= \Internal(qs^\prime, p^\prime)\\
+                \push(\proj_f(q), \pkt, pt) &= \Internal(qs^{\prime\prime}, p^{\prime\prime})\\
+                \proj_f(\push(q, \pkt, d, pt)) &= \Internal(qs^{\prime\prime\prime}, p^{\prime\prime\prime})\\
+            \end{align*}
+            By \Cref{eq:pieo3} in \Cref{dfn:pieo} and the inductive hypothesis,
+            \begin{align*}
+                p^{\prime\prime\prime} &= 
+                \begin{cases}
+                    \push(\proj(p, f), i, r) & f(d) \text{ holds true}\\
+                    \proj(p, f) & \text{otherwise}
+                \end{cases}\\
+                                                 &=
+                \begin{cases}
+                    \push(p^\prime, i, r) & f(d) \text{ holds true}\\
+                    p^\prime & \text{otherwise}
+                \end{cases}
+                                                 =
+                \begin{cases}
+                    p^{\prime\prime} & f(d) \text{ holds true}\\
+                    p^\prime & \text{otherwise}
+                \end{cases}\\
+                qs^{\prime\prime\prime}[i] &= 
+                \begin{cases}
+                    \push(\proj_f(qs[i]), \pkt, pt^\prime) & f(d) \text{ holds true}\\
+                    \proj_f(qs[i]) & \text{otherwise}
+                \end{cases}\\
+                                                            &=
+                \begin{cases}
+                    \push(qs^\prime[i], \pkt, pt^\prime) & f(d) \text{ holds true}\\
+                    qs^\prime[i] & \text{otherwise}
+                \end{cases}
+                                                            =
+                \begin{cases}
+                    qs^{\prime\prime}[i] & f(d) \text{ holds true}\\
+                    qs^\prime[i] & \text{otherwise}
+                \end{cases}
+            \end{align*}
+            By inspection of \Cref{dfn:push} and \Cref{dfn:proj},
+            $$qs^\prime[j] = qs^{\prime\prime}[j] = qs^{\prime\prime\prime}[j] = \proj_f(qs[j])$$
+            for all $j \in [1, |ts|]$ such that $j \neq i$.
+            Hence,
+            $$
+            qs^{\prime\prime\prime}
+            =
+            \begin{cases}
+                qs^{\prime\prime} & f(d) \text{ holds true}\\
+                qs^{\prime} & \text{otherwise}
+            \end{cases}
+            $$
+            Putting everything together, 
+            \begin{align*}
+                \proj_f(\push(q, \pkt, d, pt)) &= \Internal(qs^{\prime\prime\prime}, p^{\prime\prime\prime})\\
+                                               &=
+                \begin{cases}
+                    \Internal(qs^{\prime\prime}, p^{\prime\prime}) & f(d) \text{ holds true}\\
+                    \Internal(qs^{\prime}, p^{\prime}) & \text{otherwise}
+                \end{cases}\\
+                                               &=
+                \begin{cases}
+                    \push(\proj_f(q), \pkt, pt) & f(d) \text{ holds true}\\
+                    \proj_f(q) & \text{otherwise}
+                \end{cases}
+            \end{align*}
+    \end{itemize}
+\end{proof}
+
+\section{Embedding \& Simulation}
+
+\begin{dfn}
+    \label{dfn:sim}
+    Let $t_1, t_2 \in \Topo$. 
+    We call a relation $R \subseteq \PIEOTree(t_1) \times \PIEOTree(t_2)$ a \emph{simulation} if, 
+    for all $\pkt \in \Pkt$, $f \in \mathcal F$, and $q_1 \; R \; q_2$,
+    \begin{enumerate}
+        \item If $\pop(q_1, f)$ is undefined, then so is $\pop(q_2, f)$
+        \item If $\pop(q_1, f) = (\pkt, q_1^\prime)$, then $\pop(q_2, f) = (\pkt, q_2^\prime)$ such that $q_1^\prime \; R \; q_2^\prime$.
+        \item For all $pt_1 \in \Path(t_1)$ and $d \in \Data$, there exists $pt_2 \in \Path(t_2)$ such that
+            $$\push(q_1, \pkt, d, pt_1) \; R \; \push(q_2, \pkt, d, pt_2)$$
+    \end{enumerate}
+    If such a simulation exists, we say that $q_1$ is \emph{simulated} by $q_2$, and we write $q_1 \preccurlyeq q_2$.
+\end{dfn}
+
+\begin{rem}
+    For all further discussion, we assume our embeddings are injective.
+\end{rem}
+
+\begin{dfn}
+    \label{dfn:f_bar}
+    For $t_1, t_2 \in \Topo$, let $f$ be an embedding from $t_1$ to $t_2$.
+    We lift $f$ to a map $\overline{f}$ from $\PIEOTree(t_1)$ to $\PIEOTree(t_2)$ inductively.
+    \begin{itemize}
+        \item For $t_1 = \ast$, define $\overline{f}(q) = q$. This is well-defined by \cite[Lemma ~5.2]{OG}.
+        \item For $t_1 = \Node(ts_1)$, $n = |ts_1|$, $q = \Internal(qs, p)$, 
+            construct $\overline{f}_{\alpha}(q) \in \PIEOTree(t_2/\alpha)$ for each prefix $\alpha$ of $f(i)$ for some $i \in [1,n]$.
+            Inductively, we'll build up from $f(i)$'s to $\epsilon$ and set $\overline{f}(q) = \overline{f}_\epsilon(q)$.
+            \begin{itemize}
+                \item Let $\alpha = f(i)$ for some $i \in [1,n]$. We'll set $\overline{f}_\alpha(q) = \overline{f_i}(qs[i])$, 
+                    where $f_i$ embeds $t_1/i$ into $t_2/f(i)$ as per \cite[Lemma 5.2]{OG}.
+                    This well-defined by the injectivity of $f$.
+                \item Let $\alpha$ point to a transient node, say with $m$ children.
+                    For $1 \leq j \leq m$ such that $\alpha \cdot j$ is not a prefix of some $f(i)$, 
+                    define $\overline{f}(q)_{\alpha \cdot j}$ to be the PIEO tree with empty PIEOs on all leaves and internal nodes. 
+                    With this and recursion, we know $\overline{f}(q)_{\alpha \cdot j} \in \PIEOTree(t_2/(\alpha \cdot j))$ for all $j \in [1, m]$.
+
+                    We create a new PIEO $p_\alpha$ as follows:
+                    \begin{enumerate} 
+                        \item Start with $p_\alpha$ empty
+                        \item For each $i$ in $p$ such that $\alpha \cdot j$ is a prefix of $f(i)$, push $j$ into $p_\alpha$ with $i$'s data and rank
+                    \end{enumerate}
+
+                    Finally, for all $j \in [1,m]$, set $qs_\alpha[j] = \overline{f}(q)_{\alpha \cdot j}$ and $\overline{f}(q)_\alpha = \Internal(qs_\alpha, p_\alpha)$.
+            \end{itemize}
+    \end{itemize}
+\end{dfn}
+
+\reqnomode
+
+\begin{thm}
+    \label{thm:cd}
+    The following diagram commutes
+    $$
+    \begin{tikzcd}
+    	{\PIEOTree(t_1)} &&& {\PIEOTree(t_2)} \\
+    	\\
+    	{\PIFOTree(t_1)} &&& {\PIFOTree(t_2)}
+    	\arrow["{\overline{f}}", from=1-1, to=1-4]
+    	\arrow["{\proj_g}"{description}, from=1-1, to=3-1]
+    	\arrow["{\proj_g}"{description}, from=1-4, to=3-4]
+    	\arrow["{\widehat{f}}", from=3-1, to=3-4]
+    \end{tikzcd}
+    $$
+    In other words, for $q \in \PIEOTree(t_1)$ and $g \in \mathcal F$, $\proj_g(\overline{f}(q)) = \widehat{f}(\proj_g(q))$.
+\end{thm}
+
+\begin{proof}
+    We'll proceed by induction on $t_1$.
+    Suppose $t_1 = \ast$ and $q = \Leaf(p)$. 
+    By \cite[Lemma ~5.3]{OG}, $t_2 = \ast$ as well.
+    By \Cref{dfn:f_bar} and \cite[Definition ~5.4]{OG}, both $\overline{f}$ and $\widehat{f}$ are the identity.
+    Hence,
+    $$\proj_g(\overline{f}(q)) = \proj_g(q) = \widehat{f}(\proj_g(q))$$
+
+    Suppose $t_1 = \Node(ts)$ and $q = \Internal(qs, p)$.
+    For any prefix $\alpha$ of $f(i)$ for $i \in [1, |ts|]$, we'll show
+    \begin{equation}
+        \label{eq:cd1}
+        \proj_g(\overline{f}(q)_{\alpha}) = \widehat{f}(\proj_g(q))_{\alpha}
+        \tag{$\ast$}
+    \end{equation}
+    by inverse induction on $\alpha$. 
+    Instantiating \Cref{eq:cd1} with $\alpha = \epsilon$ yields the desired result. 
+    \begin{itemize}
+        \item For $\alpha = f(i)$, \Cref{eq:cd1} holds by the outer inductive hypothesis because
+            $$\proj_g(\overline{f}(q)_{\alpha}) = \proj_g(\overline{f_i}(q)) = \widehat{f_i}(\proj_g(q)) = \widehat{f}(\proj_g(q))_{\alpha}$$
+
+        \item Suppose $\alpha$ is some strict prefix of $f(i)$, pointing to a node with $m$ children. Let
+            \begin{align*}
+                \proj_g(\overline{f}(q)) = \Internal(qs^\prime, p^\prime) 
+                &&\text{and}&&
+                \widehat{f}(\proj_g(q)) = \Internal(qs^{\prime\prime}, p^{\prime\prime})
+            \end{align*}
+
+            There's two parts to showing \Cref{eq:cd1}, namely $qs^{\prime} = qs^{\prime\prime}$ and $p^\prime = p^{\prime\prime}$.
+
+            \begin{itemize}
+                \item For all $j \in [1,m]$,
+                    $$\proj_g(\overline{f}(q)_{\alpha \cdot j}) = \widehat{f}(\proj_g(q))_{\alpha \cdot j}$$
+                    For $j$ such that $\alpha \cdot j$ is a prefix of some $f(i)$, this follows from the inner inductive hypothesis.
+                    For all other $j$, notice the LHS and RHS are both PIFO trees of topology $t_2$, with empty PIFOs on all leaves and internal nodes.
+                    Hence, $qs^{\prime}[j] = qs^{\prime\prime}[j]$ for all $j \in [1,m]$, i.e. $qs^{\prime} = qs^{\prime\prime}$.
+                \item By inspection, it's clear following the construction for $p_\alpha$ from \Cref{dfn:f_bar} and then computing the projection $\proj(p_\alpha, g)$ 
+                    yields the same result as following the recipe for $p_\alpha$ from \cite[Definition ~5.4]{OG} on the projection $\proj_g(q)$: 
+                    that is, exactly when we filter out elements not satisfying $g$ does not matter.
+                    Hence, $p^{\prime} = p^{\prime\prime}$.
+            \end{itemize}
+    \end{itemize}
+\end{proof}
+
+\begin{lem}
+    \label{lem:sim1}
+    Let $t_1, t_2 \in \Topo$ and $f$ be an embedding of $t_1$ inside $t_2$. For $g \in \mathcal F$,
+    $$\pop(q, g) \text{ is undefined} \implies \pop(\overline{f}(q), g) \text{ is undefined}$$
+\end{lem}
+
+\begin{proof}
+    Suppose $\pop(q, g)$ is undefined. 
+    Applying both \Cref{lem:pop_undef} and \cite[Lemma ~5.6]{OG}, notice $\pop(\widehat{f}(\proj_g(q)))$ is undefined.
+    By \Cref{thm:cd}, $\widehat{f}(\proj_g(q)) = \proj_g(\overline{f}(q))$.
+    Hence, $\pop(\proj_g(\overline{f}(q)))$ is undefined.
+    Applying \Cref{lem:pop_undef} once more, $\pop(\overline{f}(q), g)$ is undefined.
+\end{proof}
+
+\begin{lem}
+    \label{lem:sim2}
+    Let $t_1, t_2 \in \Topo$ and $f$ be an embedding of $t_1$ inside $t_2$. For $g \in \mathcal F$,
+    $$\pop(q, g) = (\pkt, q^\prime) \implies \pop(\overline{f}(q), g) = (\pkt, \overline{f}(q^\prime))$$
+\end{lem}
+
+\textcolor{red}{Almost a clone of the proof \cite[Lemma ~5.7]{OG}.}
+
+\begin{proof}
+    We'll proceed by induction on $t_1$.
+    Suppose $t_1 = \ast$.
+    By \cite[Lemma ~5.3]{OG}, $t_2 = \ast$ as well.
+    By \Cref{dfn:f_bar}, $\overline{f}$ is the identity.
+    Hence, 
+    $$\pop(q, g) = (\pkt, q^\prime) \implies \pop(\overline{f}(q), g) = \pop(q, g) = (\pkt, q^\prime) = (\pkt, \overline{f}(q^\prime))$$
+    Suppose $t_1 = \Node(ts)$. 
+    Let 
+    \begin{align*}
+        q = \Internal(qs, p) &&
+        q^\prime = \Internal(qs^\prime, p^\prime) &&
+        \pop(p, g) = (j, p^\prime)
+    \end{align*}
+    For any prefix $\alpha$ of some $f(i)$ (where $i \in [1, |ts|]$), we'll show
+    \begin{align*}
+        \pop(\overline{f}(q)_\alpha, g) &= (\pkt, \overline{f}(q^\prime)_\alpha) &\text{ if $\alpha$ is a prefix of $f(j)$} \tag{$\dagger$} \label{eq:popinduc}\\
+        \overline{f}(q)_\alpha &= \overline{f}(q^\prime)_\alpha &\text{ otherwise}
+    \end{align*}
+    by inverse induction on $\alpha$. Instantiating \Cref{eq:popinduc} with $\alpha = \epsilon$ yields the desired result.
+    \begin{itemize}
+        \item Suppose $\alpha = f(i)$. 
+            If $\alpha$ is a prefix of $f(j)$, $i = j$ by injectivity and \cite[Definition ~5.2, Equation (3)]{OG}.
+            Recall $\pop(qs[j], g) = (\pkt, qs^\prime[j])$.
+            Hence, by the outer inductive hypothesis,
+            $$
+                \pop(\overline{f}(q)_\alpha, g) = 
+                \pop(\overline{f_j}(qs[j]), g) = 
+                (\pkt, \overline{f_j}(qs^\prime[j])) = 
+                (\pkt, \overline{f}(q^\prime)_\alpha)
+            $$
+        \item Once more, suppose $\alpha = f(i)$.
+            If $\alpha$ is not a prefix of $f(j)$, then $i \neq j$.
+            Since $qs[i] = qs^\prime[i]$,
+            $$
+                \overline{f}(q)_\alpha =
+                \overline{f_i}(qs[i]) =
+                \overline{f_i}(qs^\prime[i]) = 
+                \overline{f}(q^\prime)_\alpha
+            $$
+        \item Suppose $\alpha$ is some strict prefix of $f(j)$, pointing to a node with $m$ children.
+            Let 
+            \begin{align*}
+                \overline{f}(q)_\alpha = \Internal(qs_\alpha, p_\alpha) &&
+                \overline{f}(q^\prime)_\alpha = \Internal(qs^{\prime}_\alpha, p^{\prime}_\alpha)
+            \end{align*}
+            There exists $k \in [1, m]$ such that $\alpha \cdot k$ is a prefix of $f(j)$.
+            By the inner inductive hypothesis,
+            \begin{align*}
+                qs_\alpha[i] &= \overline{f}(q)_{\alpha \cdot i} = \overline{f}(q^\prime)_{\alpha \cdot i} = qs_\alpha[i] \text{ for $i \in [1,m]$ with $i \neq k$} \label{eq:empty1} \tag{!}\\
+                \pop(qs_\alpha[k], g) &=  \pop(\overline{f}(q)_{\alpha \cdot k}, g) = (\pkt, \overline{f}(q^\prime)_{\alpha \cdot k}) = (\pkt, qs^\prime[k])
+            \end{align*}
+            Via the construction in \Cref{dfn:f_bar} and since $\pop(p, g) = p^\prime$, $\pop(p_\alpha, g) = (k, p_\alpha^\prime)$.
+            Putting everything together, $\pop(\overline{f}(q)_\alpha, g) = (\pkt, \overline{f}(q^\prime)_\alpha)$, as desired.
+
+        \item Suppose $\alpha$ is some strict prefix of some $f(i)$ but not $f(j)$, pointing to a node with $m$ children.
+            Let 
+            \begin{align*}
+                \overline{f}(q)_\alpha = \Internal(qs_\alpha, p_\alpha) &&
+                \overline{f}(q^\prime)_\alpha = \Internal(qs^{\prime}_\alpha, p^{\prime}_\alpha)
+            \end{align*}
+            Since $p$ and $p^\prime$ agree on all indices $i$ such that $f(i)$ is a child of $\alpha$, $p_\alpha = p^\prime_\alpha$.
+            For $i \in [1,m]$, since $\alpha \cdot i$ is not a prefix of $f(j)$, the inner inductive hypothesis yields
+            \begin{align*}
+                qs_\alpha[i] = \overline{f}(q)_{\alpha\cdot i} = \overline{f}(q^\prime)_{\alpha\cdot i} = qs^\prime_\alpha[i] \label{eq:empty2} \tag{!!}
+            \end{align*}
+            Putting everything together, $\overline{f}(q)_\alpha = \overline{f}(q^\prime)_\alpha$, as desired.
+    \end{itemize}
+    \textbf{NOTE:}
+    even when $\alpha \cdot i$ is not a prefix of any $f(i)$, \Cref{eq:empty1} and \Cref{eq:empty2} hold!
+    Both $\overline{f}(q)_{\alpha \cdot i}$ and $\overline{f}(q^\prime)_{\alpha \cdot i}$ would be PIEO trees with empty PIEOs on all leaf and internal nodes.
+\end{proof}
+
+\leqnomode
+
+\begin{lem}
+    \label{lem:sim3}
+    Let $t_1, t_2 \in \Topo$ and $f$ be an embedding of $t_1$ inside $t_2$. 
+    For $\pkt \in \Pkt$, $d \in \Data$, and $pt \in \Path(t_1)$,
+    $$\overline{f}(\push(q, \pkt, d, pt)) = \push(\overline{f}(q), \pkt, d, \widetilde{f}(pt))$$
+\end{lem}
+
+\begin{proof}
+    Let $q_2 = \overline{f}(q_1)$.
+    For $g \in \mathcal F$ such that $g(d)$ holds true,
+    \begin{align*}
+        \proj_g(\overline{f}(\push(q_1, \pkt, d, pt)))
+        &= \widehat{f}(\proj_g(\push(q_1, \pkt, d, pt))) \tag{by \Cref{thm:cd}}\\
+        &= \widehat{f}(\push(\proj_g(q_1), \pkt, pt)) \tag{by \Cref{lem:push}}\\
+        &= \push(\widehat{f}(\proj_g(q_1)), \pkt, \widetilde{f}(pt)) \tag{by \cite[Lemma ~5.9]{OG}}\\
+        &= \push(\proj_g(q_2), \pkt, \widetilde{f}(pt)) \tag{by \Cref{thm:cd}}\\
+        &= \proj_g(\push(q_2, \pkt, d, \widetilde{f}(pt))) \tag{by \Cref{lem:push}}
+    \end{align*}
+    For $g \in \mathcal F$ such that $g(d)$ does not hold true,
+    \begin{align*}
+        \proj_g(\overline{f}(\push(q_1, \pkt, d, pt)))
+        &= \widehat{f}(\proj_g(\push(q_1, \pkt, d, pt))) \tag{by \Cref{thm:cd}}\\
+        &= \widehat{f}(\proj_g(q_1)) \tag{by \Cref{lem:push}}\\
+        &= \proj_g(q_2) \tag{by \Cref{thm:cd}}\\
+        &= \proj_g(\push(q_2, \pkt, d, \widetilde{f}(pt))) \tag{by \Cref{lem:push}}
+    \end{align*}
+    Overall,
+    $
+        \proj_g(\overline{f}(\push(q_1, \pkt, d, pt)))
+        = 
+        \proj_g(\push(q_2, \pkt, d, \widetilde{f}(pt)))
+    $
+    for all $g \in \mathcal F$. 
+    Hence,
+    $$
+        \overline{f}(\push(q_1, \pkt, d, pt))
+        = 
+        \push(q_2, \pkt, d, \widetilde{f}(pt))
+    $$
+    by \Cref{lem:pieotree_eq}, as desired.
+\end{proof}
+
+\begin{thm}
+    Let $t_1, t_2 \in \Topo$. If $f$ embeds $t_1$ into $t_2$, then 
+    $$R = \{(q, \overline{f}(q)) \mid q \in \PIEOTree(t_1)\}$$ 
+    is a simulation.
+\end{thm}
+
+\begin{proof}
+    By \Cref{lem:sim1}, \Cref{lem:sim2}, and \Cref{lem:sim3}, the conditions from \Cref{dfn:sim} hold.
+\end{proof}
+
+\newpage 
+
+\renewcommand\refname{\LARGE References}
+\bibliographystyle{alpha}
+\bibliography{refs}
+
+\end{document}
diff --git a/pieo-trees/refs.bib b/pieo-trees/refs.bib
new file mode 100644
index 0000000..a6edd07
--- /dev/null
+++ b/pieo-trees/refs.bib
@@ -0,0 +1,9 @@
+@misc{OG,
+      title={Formal Abstractions for Packet Scheduling}, 
+      author={Anshuman Mohan and Yunhe Liu and Nate Foster and Tobias Kappé and Dexter Kozen},
+      year={2023},
+      eprint={2211.11659},
+      archivePrefix={arXiv},
+      primaryClass={cs.NI},
+      url={https://arxiv.org/abs/2211.11659}, 
+}
diff --git a/pieo-trees/well-formedness/pieo_tree_wellformed.pdf b/pieo-trees/well-formedness/pieo_tree_wellformed.pdf
new file mode 100644
index 0000000..e81d1c8
Binary files /dev/null and b/pieo-trees/well-formedness/pieo_tree_wellformed.pdf differ
diff --git a/pieo-trees/well-formedness/pieo_tree_wellformed.tex b/pieo-trees/well-formedness/pieo_tree_wellformed.tex
new file mode 100644
index 0000000..0eb39c4
--- /dev/null
+++ b/pieo-trees/well-formedness/pieo_tree_wellformed.tex
@@ -0,0 +1,262 @@
+\documentclass{amsart}
+
+% font
+\usepackage{cmbright}
+
+% margin 
+\usepackage[margin=1in]{geometry}
+
+% references
+\usepackage[colorlinks]{hyperref} 
+\PassOptionsToPackage{colorlinks}{hyperref}
+\hypersetup{urlcolor = RedViolet, linkcolor = RoyalBlue, citecolor = NavyBlue}
+
+% basics
+\usepackage[leqno]{amsmath}
+\usepackage{amssymb, amsthm} 
+\usepackage[svgnames, dvipsnames]{xcolor}
+\usepackage{mhsetup, mathtools}
+\usepackage[capitalise]{cleveref}
+
+% commutative diagram
+\usepackage{tikz-cd}
+
+% hats
+\usepackage{yhmath}
+
+% PL macros
+\usepackage{mathpartir}
+\usepackage{stmaryrd}
+
+\usepackage{geometry}
+ \geometry{
+ a4paper,
+ top=25mm,
+ bottom=25mm,
+ }
+
+ % no more indent
+\setlength{\parindent}{0pt}
+
+% right-justified sections hack
+\usepackage{titlesec}
+\newcommand{\marginsecnumber}[1]{%
+  \makebox[0pt][r]{#1\hspace{6pt}}%
+}
+\titleformat{\section}
+  {\normalfont\Large\bfseries}
+  {\marginsecnumber\thesection}
+  {0pt}
+  {}
+\titleformat{\subsection}
+  {\normalfont\large\bfseries}
+  {\marginsecnumber\thesubsection}
+  {0pt}
+  {}
+\titleformat{\subsubsection}
+  {\normalfont\normalsize\bfseries}
+  {\marginsecnumber\thesubsubsection}
+  {0pt}
+  {}
+
+\begin{document}
+
+\pagestyle{empty}
+
+{\LARGE \textbf{Preservation of Well-Formedness in PIEO Trees}}
+
+\hrulefill\\
+
+\section{Relevant Definitions}
+
+\textbf{\textit{Defining $| \cdot |$ on PIEOs With Regards to Pushes}}\newline
+
+
+\textbf{Definition 1A}: \textit{Given a predicate $f \in \mathcal{F}$, element $i$ and data $d$, if $d$ satisfies $f$, then pushing $i$ to $p$ with data $d$ increments the number of instances of $i$ that satisfy $f$.}
+
+$$\frac{p \in \text{PIEO}  \hspace{0.7cm} f \in \mathcal{F} \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} r \in \text{Rank} \hspace{0.7cm} |p|_{i, f} = n \hspace{0.7cm} \text{PUSH}(p, i, d, r) = p' \hspace{0.7cm} f(d)}{|p'|_{i, f} = n+1}$$
+
+\textbf{Definition 1B}: \textit{Given a predicate $f \in \mathcal{F}$, element $i$ and data $d$, if $d$ does not satisfy $f$, then pushing $i$ to $p$ with data $d$ preserves the number of instances of $i$ that satisfy $f$.}
+
+$$\frac{p \in \text{PIEO}  \hspace{0.7cm} f \in \mathcal{F} \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} r \in \text{Rank} \hspace{0.7cm} |p|_{i, f} = n \hspace{0.7cm} \text{PUSH}(p, i, d, r) = p' \hspace{0.7cm} \neg f(d)}{|p'|_{i, f} = n}$$
+
+\textbf{Definition 1C}: \textit{Given elements $i, j$ and data $d \in \mathcal{D}$, pushing $i$ to $p$ with data $d$ does not modify how many times $j$ appears in $p$.}
+
+$$\frac{p \in \text{PIEO}  \hspace{0.7cm} f \in \mathcal{F} \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} r \in \text{Rank} \hspace{0.7cm} |p|_{j, f} = n \hspace{0.7cm} \text{PUSH}(p, i, d, r) = p' \hspace{0.7cm} i \neq j}{|p'|_{j, f} = n}$$
+
+\section{Relevant Lemmas}
+
+\subsection{Lemma 1}
+
+\text{Given $f \in \mathcal{F}, pkt \in \text{Pkt}, d \in \mathcal{D}, pt \in \text{Path}, t \in \text{Topo}$ and $q \in \text{PIEOTree}(t)$:}
+
+$$\begin{cases}
+    \hspace{0.25cm} \text{$f(d) \implies |push(q, pkt, d, pt)|_f = |q|_f + 1$}\\
+    \text{$\neg f(d) \implies |push(q, pkt, d, pt)|_f = |q|_f$}
+\end{cases}$$
+
+\textbf{Proof}: We proceed about this proof by Structural Induction over the derivation of $| \cdot |$ as follows:\newline
+
+\textbf{Base Case}: $q = \text{Leaf}(p)$ for some PIEO $p$.\newline
+
+By definition 2.1, we have that $|\text{Leaf}(p)|_{i, f} = |p|_{i, f}$, where $|p|_{i, f}$ is the number of occurrences of $i$ in PIEO $p$ that satisfy predicate $f$. The definition of $\text{push}$ in 1.4 gives the following:\newline
+
+$$\frac{\text{PUSH}(p, i, d, r) = p'}{\text{push}(\text{Leaf}(p), pkt, d, r) = \text{Leaf}(p')}$$\\[-10pt]
+
+Where $\text{Leaf}(p')$ is the result of $\text{push}$ing into $\text{Leaf}(p)$.\newline
+
+By definition 1A, we now know that $f(d) \implies |p'|_f = |p|_f + 1$.\newline
+
+By definition 1B, we now know that $\neg f(d) \implies |p'|_f = |p|_f$.\newline
+
+By definition 2.1, we know that $|\text{Leaf}(p')|_f = |p'|_f$ and $|\text{Leaf}(p)|_f = |p|_f$.\newline
+
+Combining these together, we obtain the following:
+
+$$\begin{cases}
+    \hspace{0.25cm} \text{$f(d) \implies |\text{Leaf}(p')|_f = |\text{Leaf}(p)|_f + 1$}\\
+    \text{$\neg f(d) \implies |\text{Leaf}(p')|_f = |\text{Leaf}(p)|_f$}
+\end{cases}$$
+
+Thus, we have proven our base case.\\[10pt]
+
+\textbf{Inductive Case}: Assume an arbitrary PIEO $p$, set of subtrees $qs$, node $q = \text{Internal}(qs, p)$, index $i$, data $d$ and packet $pkt$.
+Also assume a set of paths $pts : |pts| = |qs|$.\newline
+
+\textbf{Inductive Hypothesis}:
+$\forall 1 \leq j \leq |qs|:$
+
+$$\begin{cases}
+    \hspace{0.25cm} \text{$f(d) \implies |push(qs[j], pkt, d, pts[j])|_f = |qs[j]|_f + 1$}\\
+    \text{$\neg f(d) \implies |push(qs[j], pkt, d, pts[j])|_f = |qs[j]|_f$}
+\end{cases}$$\\[-5pt]
+
+We now push a packet $pkt$ with an arbitrary index $i$ and rank $r$.\newline
+
+Let $q' = push(q, pkt, d, (i, r) :: pts[i])$.\newline
+
+\textbf{Show}: 
+
+$$\begin{cases}
+    \hspace{0.25cm} \text{$f(d) \implies |q'|_f = |q|_f + 1$}\\
+    \text{$\neg f(d) \implies |q'|_f = |q|_f$}
+\end{cases}$$
+
+Recall Definition 1.4 for push on Internal Nodes:
+
+$$\frac{\text{push}(qs[i], pkt, d, pt) = q' \hspace{0.5cm} \text{PUSH}(p, i, d, r) = p' }{\text{push}(\text{Internal}(qs, p), pkt, d, (i, r) :: pt) = \text{Internal}(qs[q'/i], p')}$$
+
+Recall Definition 2.1 for $|\cdot|_f$ on Internal Nodes:
+
+$$m = |\text{Internal}(qs, p)|_f = \sum_{j=1}^{|qs|} |qs[j]|_f$$
+
+Thus, we can further conclude the following:
+
+$$|\text{push}(\text{Internal}(qs, p), pkt, d, (i, r) :: pt)|_f = \sum_{j=1}^{|qs|} |qs[q'/i][j]|_f$$
+
+From our Inductive Hypothesis, we know the following:
+
+$$\begin{cases}
+    \hspace{0.25cm} \text{$f(d) \implies |push(qs[i], pkt, d, pts[i])|_f = |qs[i]|_f + 1$}\\
+    \text{$\neg f(d) \implies |push(qs[i], pkt, d, pts[i])|_f = |qs[i]|_f$}
+\end{cases}$$\\[-5pt]
+
+From the definition of $\text{push}$, pushing changes only $qs[i]$, while the remaining subtrees remain the same. Subsequently, we can assert that $\forall 
+1 \leq j \leq |qs|, i \neq j \implies |qs[j]|_f = |qs[q'/i][j]|_f$. With this in mind, we make the following claim:\\[-15pt]
+
+$$|\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)|_f = \sum_{j=1}^{|qs|} |qs[j]|_f - |qs[i]|_f + |qs[q'/i][i]|_f$$
+
+Substituting what we know gives the following:
+
+$$\begin{cases}
+    \hspace{0.25cm} f(d) \implies |\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)|_f = |\text{Internal}(qs, p)|_f - |qs[i]|_f + |qs[i]|_f + 1\\
+    \hspace{0.25cm} \neg f(d) \implies |\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)|_f = |\text{Internal}(qs, p)|_f - |qs[i]|_f + |qs[i]|_f\\
+\end{cases}$$
+
+$$\implies \begin{cases}
+    \hspace{0.25cm} f(d) \implies |\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)|_f = |q|_f + 1\\
+    \hspace{0.25cm} \neg f(d) \implies |\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)|_f = |q|_f \\
+\end{cases}$$
+
+$$\implies \begin{cases}
+    \hspace{0.25cm} f(d) \implies |q'|_f = |q|_f + 1\\
+    \hspace{0.25cm} \neg f(d) \implies|q'|_f = |q|_f \\
+\end{cases}$$
+
+With this, we have shown the desired equality, and proven our Inductive case.\newline
+
+Thus, it follows that Lemma 1 holds.\newline
+
+\newpage
+
+\section{Proof Of Theorem 2.2}
+
+Let $t \in \text{Topo}$, $\text{pkt} \in \text{Pkt}$, $d \in \mathcal{D}$, $f,f' \in \mathcal{F}$, and $q \in \text{PIEOTree}(t)$ such that $\vdash_f q$.\newline
+
+1. If $pt \in \text{Path}(t)$, then $\text{push}(q, pkt, d, pt)$ is well-defined and $\vdash_f \text{push}(q, pkt, d, pt)$.\newline
+
+2. If $|q|_{f'} > 0$ and $f' \geq f$, then $\text{pop}(q, f')$ is well-defined and $\vdash_{f'} q'$, where $\text{pop}(q, f') = (pkt, q')$.
+
+\subsection{Proof of Theorem 2.2.1}
+\textit{\textbf{Well-Formedness Is Preserved in PIEO Trees Upon Pushes}}\\[10pt]
+
+We proceed with this proof by inducting upon the definition of $\text{push}$ for PIEO Trees.\newline
+
+\textbf{Base Case : $\text{Leaf}(p)$}\newline
+
+By definition 1.4 of $\text{push}$ for PIEOs, we have the following for Leaf nodes:
+
+$$\frac{\text{PUSH}(p, pkt, d, r) = p'}{\text{push}(\text{Leaf}(p), pkt, d, r) = \text{Leaf}(p')}$$\\[-10pt]
+
+It follows that after pushing, the resultant tree is expressed as $\text{Leaf}(p')$ for some packet $p'$. By definition 2.1, we know the following holds for any arbitrary PIEO $p$, under any predicate $f \in \mathcal{F}$:\\[-10pt]
+
+$$\frac{}{\vdash_f \text{Leaf}(p)}$$
+
+We now have: $\forall (p, pkt, d, f, r), \vdash_f \text{push}(\text{Leaf}(p), pkt, d, r)$\newline
+
+With this, our Base Case is proven.\\[10pt]
+
+\textbf{Inductive Case:} $q = \text{Internal}(qs, p), f \in \mathcal{F}, \vdash_f q$\newline
+
+\textbf{Inductive Hypothesis}: $\forall 1 \leq i \leq |qs|. \vdash_f \text{push}(qs[i], pkt, d, pt)$\newline
+
+Recall Definition 2.1 for $\vdash_f$ on Internal Nodes, given a predicate $f$:
+
+$$\frac{\forall 1 \leq i \leq |qs|. \vdash_f qs[i] \land |p|_{i, f} = |qs[i]|_f}{\vdash_f \text{Internal}(\text{qs, p})}$$\newline
+
+Recall Definition 1.4 for $\text{push}$ on Internal Nodes:
+
+$$\frac{\text{push}(qs[i], pkt, d, pt) = q' \hspace{1cm} \text{PUSH}(p, i, d, r) = p'}{\text{push}(\text{Internal}(qs, p), pkt, d, (i, r) :: pt) = \text{Internal}(qs[q'/i], p')}$$\newline
+
+Now, let $q' = \text{push}(qs[i], pkt, d, pt)$, and let $p' = \text{PUSH}(p, i, d, r)$.\newline
+
+\noindent Let $f$ be any totally-ordered predicate.\newline
+
+\textbf{Show}: $\vdash_f q \implies \vdash_f \text{Internal}(qs[q'/i], p')$.\newline
+
+Using definition 2.1 and our Inductive Hypothesis, we can conclude that $\vdash_f q'$. Furthermore, note that the only subtree to be modified in $qs$ is in $qs[i]$, per the definition of $\text{push}$.\newline
+
+\textbf{Now we make the following claim:}\\[-20pt]
+
+\begin{alignat*}{5}
+&(1) \vdash_f \text{Internal}(qs, p) && \hspace{0.3cm} \textit{By definition}\\[10pt]
+&(2) \implies \forall 1 \leq j \leq |qs|. \hspace{0.2cm} \vdash_f qs[j] \land |p|_{j, f} = |qs[j]|_f&& \hspace{0.3cm} \textit{Inversion Lemma (Definition 2.1)}\\[5pt]
+&(3) \implies |p|_{i, f} = |qs[i]|_f&& \hspace{0.3cm} \textit{Instance of universal quantifier (2)}\\[5pt]
+&(4.1)  \hspace{0.2cm} f(d) \implies \indent |p'|_{i, f} = |p|_{i, f} + 1&& \hspace{0.3cm} \textit{Definition 1A}\\[5pt]
+&(4.2)  \hspace{0.2cm} \neg f(d) \implies \indent |p'|_{i, f} = |p|_{i, f} && \hspace{0.3cm} \textit{Definition 1B}\\[5pt]
+&(5.1) \hspace{0.2cm} f(d) \implies \indent |q'|_f = |qs[i]|_f + 1&& \hspace{0.3cm} \textit{Lemma 1}\\[5pt]
+&(5.2) \hspace{0.2cm}  \neg f(d) \implies \indent |q'|_f = |qs[i]|_f && \hspace{0.3cm} \textit{Lemma 1}\\[5pt]
+&(6) \hspace{0.2cm} |p|_{i, f} + 1 = |qs[i]|_f + 1&& \hspace{0.3cm} \textit{Addition Property of Equality (3)}\\[5pt]
+&(7) \implies |p'|_{i, f} = |q'|_f && \hspace{0.3cm} \textit{Substitution (3 - 6)}\\[5pt]
+&(8) \indent \forall 1 \leq j \leq |p'|, i \neq j \implies |p'|_{j, f} = |p|_{j, f}&& \hspace{0.3cm} \textit{Definition 1C}\\[5pt]
+&(9) \implies \forall 1 \leq j \leq |p'|, i \neq j \implies |p'|_{j, f} = |qs[j]|_f&& \hspace{0.3cm} \textit{By (2) and (8)}\\[5pt]
+&(10) \implies \forall 1 \leq j \leq |p'|, |p'|_{j, f} = |qs[q' / i][j]|_f&& \hspace{0.3cm} \textit{By (7) and (9)}\\[5pt]
+&(11)  \indent \forall 1 \leq j \leq |qs|. \vdash_f qs[q'/i][j] && \hspace{0.3cm} \textit{Inductive Hypothesis}\\[5pt]
+&(12) \implies \forall 1 \leq j \leq |qs|. \vdash_f qs[q'/i][j] \land |p'|_{j, f} = |qs[q'/i][j]|_f&&\hspace{0.3cm} \textit{By (10) and (11)}\\[5pt]
+&(13) \implies \vdash_f \text{Internal}(qs[q'/i], p') && \hspace{0.3cm} \textit{Definition of } \vdash_f\\[-10pt]
+\end{alignat*}
+
+With this, we have proven our Inductive Statement and completed the proof. We have shown that pushing to an arbitrary PIEO Tree preserves its well-formedness.\\[-10pt]
+
+\end{document}
+
diff --git a/pieo-trees/well-formedness/pifo_tree_wellformed.pdf b/pieo-trees/well-formedness/pifo_tree_wellformed.pdf
new file mode 100644
index 0000000..a961bee
Binary files /dev/null and b/pieo-trees/well-formedness/pifo_tree_wellformed.pdf differ
diff --git a/pieo-trees/well-formedness/pifo_tree_wellformed.tex b/pieo-trees/well-formedness/pifo_tree_wellformed.tex
new file mode 100644
index 0000000..b92f601
--- /dev/null
+++ b/pieo-trees/well-formedness/pifo_tree_wellformed.tex
@@ -0,0 +1,304 @@
+\documentclass{article}
+\usepackage{graphicx} % Required for inserting images
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{geometry}
+ \geometry{
+ a4paper,
+ top=25mm,
+ bottom=25mm,
+ }
+
+ % no more indent
+\setlength{\parindent}{0pt}
+
+\begin{document}
+
+\section{Preservation of Well-Formedness In PIFO Trees}
+
+This set of definitions and proofs completes the proof sketch outlined in Section 3.3, Definition 3.8 of Formal Abstractions In Packet Scheduling. In particular, it fleshes out the relationships between the functions push, pop and $|\cdot|$, in order to formally define (and by extension, prove) the preservation of well-formedness in PIFO Trees.\newline
+
+This defines how pushing and popping modifies length in PIFOs, and supplies lemmas (with proof) clarifying how length changes with regards to pushing and popping in PIFO Trees. This then proves preservation of well-formedness in PIFO Trees following push and pop operations.\newline
+
+This also lays some of the foundation for proving for well-formedness in PIEO Trees. Proofs of pushing translate almost one-to-one for PIEO Trees, while popping follows as an extension of this system, but with an inculsion of a totally ordered predicate.
+
+\section{Relevant Definitions and Lemmas}
+
+\subsection{Definition 1}
+
+\textbf{\textit{Defining $|\cdot|$ on PIFOs With Regards to Pushes}}
+
+\hfill \break 
+
+\textbf{Definition 1A}: \textit{Pushing an element to a PIFO increments how many times it appears}
+ $$\frac{p \in \text{PIFO}  \hspace{0.7cm} |p|_i = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} \text{PUSH}(p, i, r) = p' \hspace{0.7cm} n' = n+1}{|p'|_i = n'}$$
+
+\textbf{Definition 1B:} \textit{Pushing an element to a PIFO does not change how much others appear}
+$$\frac{p \in \text{PIFO}  \hspace{0.7cm} |p|_i = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} \text{PUSH}(p, j, r) = p' \hspace{0.7cm} i \neq j}{|p'|_i = n}$$
+
+\textbf{Definition 1C:} \textit{Pushing an element to a PIFO increments its size}
+$$\frac{p \in \text{PIFO}  \hspace{0.7cm} |p| = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} \text{PUSH}(p, i, r) = p' \hspace{0.7cm} n' = n+1}{|p'| = n'}$$\newline
+
+\subsection{Definition 2}
+\textbf{\textit{Defining $|\cdot|$ on PIFOs With Regards to Pops}}
+
+\hfill\break
+
+\textbf{Definition 2A}: \textit{Popping an element from a PIFO decrements how many times it appears}
+ $$\frac{p \in \text{PIFO}  \hspace{0.7cm} |p|_i = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} \text{POP}(p) = (i, p') \hspace{0.7cm} n' = n-1}{|p'|_i = n'}$$
+
+\textbf{Definition 2B:} \textit{Popping an element from a PIFO does not change how much others appear}
+$$\frac{p \in \text{PIFO}  \hspace{0.7cm} |p|_i = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} \text{POP}(p) = (j, p') \hspace{0.7cm} i \neq j}{|p'|_i = n}$$
+
+\textbf{Definition 2C:} \textit{Popping an element from a PIFO decrements its size}
+$$\frac{p \in \text{PIFO}  \hspace{0.7cm} |p| = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} \text{POP}(p) = (i, p') \hspace{0.7cm} n' = n-1}{|p'| = n'}$$\newpage
+
+\section{Lemmas 1 and 2}
+\textbf{\textit{Defining $|\cdot|$ on PIFO Trees With Regards to Pushes and Pops}}\newline
+
+\subsection{Lemma 1: Pushing to a PIFO Tree increments its size}
+
+\par\
+
+$$\frac{q \in \text{PIFOTree} \hspace{0.7cm} |q| = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} \text{push}(q, pkt, p) = q' \hspace{0.7cm} n' = n+1}{|q'| = n'}$$
+
+\textbf{Proof}. We proceed upon this proof by structural induction over the definition of $|\cdot|$ as follows.\newline
+
+\textbf{Base Case}: $q = \text{Leaf}(p)$ for some PIFO $p$.\newline
+
+By definition 3.8, we have that $|\text{Leaf}(p)|_i = |p|_i$, where $|p|_i$ is the number of occurrences of $i$ in PIFO $p$. The definition of $\text{push}$ in 3.6 gives the following:
+
+$$\frac{\text{PUSH}(p, pkt, r) = p'}{\text{push}(\text{Leaf}(p), pkt, r) = \text{Leaf}(p')}$$\\[-10pt]
+
+Where $\text{Leaf}(p')$ is the result of $\text{push}$ing into $\text{Leaf}(p)$.\newline
+
+By definition 1A, we now know that $|p'|_i = |p|_i + 1$.\newline
+
+By definition 3.8, we know that $|\text{Leaf}(p')|_i = |p'|_i$ and $|\text{Leaf}(p)|_i = |p|_i$.\newline
+
+Combining these together, we obtain the following:
+
+$$|\text{Leaf}(p')| = |\text{Leaf}(p)| + 1$$
+
+Thus, we have proven our base case.\\[10pt]
+
+\textbf{Inductive Case}:\newline
+
+Assume an arbitrary PIFO $p$, Node $q = \text{Internal}(qs, p)$, packet $pkt$, path $pt$, index $i$ and rank $r$.\newline
+
+\textbf{Inductive Hypothesis}: $|qs[i]| = n \implies |\text{push}(qs[i], pkt, pt)| = n+1$\newline
+
+\textbf{Show}: $|\text{Internal}(qs, p)| = m \implies |\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)| = m+1$\newline
+
+Note that $\text{push}$ is defined for internal nodes as follows:
+
+$$\frac{\text{push}(qs[i], pkt, pt) = q' \hspace{1cm} \text{PUSH}(p, i, r) = p'}{\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt) = \text{Internal}(qs[q'/i], p')}$$\\[-10pt]
+
+Since $q$ is a PIFO Tree, we know from Definition 3.8 the following:
+
+$$m = |q| = \sum_{j=1}^{|qs|} |qs[j]|$$
+
+Thus, we can further conclude the following:
+
+$$|\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)| = \sum_{j=1}^{|qs|} |qs[q'/i][j]|$$
+
+From our Inductive Hypothesis, we know that $|q'| = |\text{push}(qs[i], pkt, pt| = n+1$.\newline
+
+From the definition of $\text{push}$, pushing changes only $qs[i]$, while the remaining subtrees remain the same. Subsequently, we can assert that $\forall 
+1 \leq j \leq |qs|, i \neq j \implies |qs[j]| = |qs[q'/i][j]$. With this in mind, we make the following claim:\\[-15pt]
+
+$$|\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)| = \sum_{j=1}^{|qs|} |qs[j]| - |qs[i]| + |qs[q'/i][i]|$$
+
+Substituting what we know, this gives us the following:
+
+$$|\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)| = m - n + n + 1$$
+
+$$\implies |\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt)| = m + 1$$\\[-15pt]
+
+With this, we have shown the desired equality, and proven our Inductive case.\newline
+
+Thus, it follows that Lemma 1 holds.\newline
+
+\subsection{Lemma 2: Popping from a PIFO Tree decrements its size}
+
+\par\
+
+$$\frac{q \in \text{PIFOTree} \hspace{0.7cm} |q| = n \hspace{0.7cm} n \in \mathbb{N} \hspace{0.7cm} (pkt, q') = \text{pop}(q) \hspace{0.7cm} n' = n-1}{|q'| = n'}$$
+
+\textbf{Proof}. We proceed upon this proof by structural induction over the definition of $|\cdot|$ as follows.\newline
+
+\textbf{Base Case}: $q = \text{Leaf}(p)$ for some PIFO $p$.\newline
+
+By definition 3.8, we have that $|\text{Leaf}(p)|_i = |p|_i$, where $|p|_i$ is the number of occurrences of $i$ in PIFO $p$. The definition of $\text{pop}$ in 3.6 gives the following:
+
+$$\frac{\text{POP}(p) = p'}{\text{pop}(\text{Leaf}(p)) = \text{Leaf}(pkt, p')}$$\\[-10pt]
+
+Where $\text{Leaf}(p')$ is the result of $\text{pop}$ping from $\text{Leaf}(p)$.\newline
+
+By definition 2A, we now know that $|p'|_i = |p|_i - 1$.\newline
+
+By definition 3.8, we know that $|\text{Leaf}(p')|_i = |p'|_i$ and $|\text{Leaf}(p)|_i = |p|_i$.\newline
+
+Combining these together, we obtain the following:
+
+$$|\text{Leaf}(p')| = |\text{Leaf}(p)| - 1$$
+
+Thus, we have proven our base case.\\[10pt]
+
+\textbf{Inductive Case}:\newline
+
+Assume an arbitrary PIFO $p$, Node $q = \text{Internal}(qs, p)$ and index $i$.\newline
+
+\textbf{Inductive Hypothesis}: $|qs[i]| = n \implies |q'| = n-1$ where $(pkt, q') = \text{pop}(qs[i])$.\newline
+
+\textbf{Show}: $|\text{Internal}(qs, p)| = m \implies |q''| = m-1$ where $(pkt, q'') =\text{pop}(\text{Internal}(qs, p)$.\newline
+
+Note that $\text{pop}$ is defined for internal nodes as follows:
+
+$$\frac{\text{POP(p) = (i, p') \hspace{1cm} \text{pop}(qs[i]) = (pkt, q')}}{{\text{pop}(\text{Internal}(qs, p)) = (pkt, \text{Internal}(qs[q'/i], p'))}}$$\\[-10pt]
+
+Since $q$ is a PIFO Tree, we know from Definition 3.8 the following:
+
+$$m = |q| = \sum_{j=1}^{|qs|} |qs[j]|$$
+
+Thus, we can further conclude the following:
+
+$$(pkt, q'') = \text{pop}(\text{Internal}(qs, p) \implies |q''| = \sum_{j=1}^{|qs|} |qs[q'/i][j]|$$
+
+From our Inductive Hypothesis, we know that $|q'| = n-1$ where $pkt, q' = \text{pop}(qs[i])$.\newline
+
+From the definition of $\text{pop}$, popping changes only $qs[i]$, while the remaining subtrees remain the same. Subsequently, we can assert that $\forall 
+1 \leq j \leq |qs|, i \neq j \implies |qs[j]| = |qs[q'/i][j]$. With this in mind, we make the following claim:\\[-15pt]
+
+$$(pkt, q'') = \text{pop}(\text{Internal}(qs, p)) \implies |q''| = \sum_{j=1}^{|qs|} |qs[j]| - |qs[i]| + |qs[q'/i][i]|$$
+
+Substituting what we know, this gives us the following:
+
+$$(pkt, qs'') = \text{pop}(\text{Internal}(qs, p)) \implies |q''| = m - n + n - 1$$
+
+$$\implies (pkt, qs'') = \text{pop}(\text{Internal}(qs, p)) \implies |qs''| = m - 1$$\\[-15pt]
+
+With this, we have shown the desired equality, and proven our Inductive case.\newline
+
+Thus, it follows that Lemma 2 holds.\newline
+
+
+\section{Proofs For Lemma 3.9 (Well-Formedness)}
+
+\subsection{Proof of Lemma 3.9.1}
+\textit{\textbf{Well-Formedness Is Preserved in PIFO Trees Upon Pushes}}\\[10pt]
+
+We proceed with this proof by inducting upon the definition of $\text{push}$ for PIFO Trees.\newline
+
+\textbf{Base Case : $Leaf(p)$}\newline
+
+By definition 3.6 of $\text{push}$, we have the following for Leaf nodes:
+
+$$\frac{\text{PUSH}(p, pkt, r) = p'}{\text{push}(\text{Leaf}(p), pkt, r) = \text{Leaf}(p')}$$\\[-10pt]
+
+It follows that after pushing, the resultant tree is expressed as $\text{Leaf}(p')$ for some PIFO $p'$ By definition 3.8 (cited above), we know the following holds for any arbitrary PIFO $p$:\\[-10pt]
+
+$$\frac{}{\vdash \text{Leaf}(p)}$$
+
+We now have: $\forall p, pkt, r, \vdash \text{push}(\text{Leaf}(p), pkt, r)$\newline
+
+With this, our Base Case is proven.\\[10pt]
+
+\textbf{Inductive Case:} $q = \text{Internal}(qs, p), \vdash q$\newline
+
+\textbf{Inductive Hypothesis}: $\forall 1 \leq i \leq |qs|. \vdash \text{push}(qs[i], pkt, pt)$\newline
+
+Recall Definition 3.8 for $\vdash$ on Internal Nodes:
+
+$$\frac{\forall 1 \leq i \leq |qs|. \vdash qs[i] \land |p|_i = |qs[i]|}{\vdash \text{Internal}(\text{qs, p})}$$\newline
+
+Recall Definition 3.6 for $\text{push}$ on Internal Nodes:
+
+$$\frac{\text{push}(qs[i], pkt, pt) = q' \hspace{1cm} \text{PUSH}(p, i, r) = p'}{\text{push}(\text{Internal}(qs, p), pkt, (i, r) :: pt) = \text{Internal}(qs[q'/i], p')}$$\newline
+
+Now, let $q' = \text{push}(qs[i], pkt, pt)$, and let $p' = \text{PUSH}(p, i, r)$.\newline
+
+\textbf{Show}: $\vdash q \implies \vdash \text{Internal}(qs[q'/i], p')$.\newline
+
+Using definition 3.6 and our Inductive Hypothesis, we can conclude that $\vdash q'$. Furthermore, note that the only subtree to be modified in $qs$ is in $qs[i]$, per the definition of $\text{push}$.\newline
+
+\textbf{Now we make the following claim:}\\[-20pt]
+
+\begin{alignat*}{5}
+&(1) \vdash \text{Internal}(qs, p) && \hspace{0.3cm} \textit{By definition}\\[10pt]
+&(2) \implies \forall 1 \leq j \leq |qs|. \hspace{0.2cm} \vdash qs[j] \land |p|_j = |qs[j]|&& \hspace{0.3cm} \textit{Inversion Lemma (Definition 3.8)}\\[5pt]
+&(3) \implies |p|_i = |qs[i]|&& \hspace{0.3cm} \textit{Instance of universal quantifier (2)}\\[5pt]
+&(4) \indent |p'|_i = |p|_i + 1&& \hspace{0.3cm} \textit{Definition 1A}\\[5pt]
+&(5) \indent |q'| = |qs[i]| + 1&& \hspace{0.3cm} \textit{Lemma 1}\\[5pt]
+&(6) \implies |p|_i + 1 = |qs[i]| + 1&& \hspace{0.3cm} \textit{Addition Property of Equality}\\[5pt]
+&(7) \implies |p'|_i = |q'|&& \hspace{0.3cm} \textit{Substitution (4, 5, 6)}\\[5pt]
+&(8) \indent \forall 1 \leq j \leq |p'|, i \neq j \implies |p'|_j = |p|_j&& \hspace{0.3cm} \textit{Definition 1B}\\[5pt]
+&(9) \implies \forall 1 \leq j \leq |p'|, i \neq j \implies |p'|_j = |qs[j]|&& \hspace{0.3cm} \textit{By (2) and (8)}\\[5pt]
+&(10) \implies \forall 1 \leq j \leq |p'|, |p'|_j = |qs[q' / i][j]|&& \hspace{0.3cm} \textit{By (7) and (9)}\\[5pt]
+&(11)  \indent \forall 1 \leq j \leq |qs|. \vdash qs[q'/i][j]&& \hspace{0.3cm} \textit{Inductive Hypothesis}\\[5pt]
+&(12) \implies \forall 1 \leq j \leq |qs|. \vdash qs[q'/i][j] \land |p'|_j = |qs[q'/i][j]|&&\hspace{0.3cm} \textit{By (10) and (11)}\\[5pt]
+&(13) \implies \vdash \text{Internal}(qs[q'/i], p') && \hspace{0.3cm} \textit{Definition of } \vdash\\[-10pt]
+\end{alignat*}
+
+With this, we have proven our Inductive Statement and completed the proof. We have shown that pushing to an arbitrary PIFO Tree preserves its well-formedness.\\[-10pt]
+
+\subsection{Proof of Lemma 3.9.2}
+\textit{\textbf{Well-Formedness Is Preserved in PIFO Trees Upon Pops}}\\[5pt]
+
+We proceed with this proof by inducting upon the definition of $\text{pop}$ for PIFO Trees.\newline
+
+\textbf{Base Case : $Leaf(p)$}\newline
+
+By definition 3.4 of $\text{pop}$, the following holds for Leaf nodes:
+
+$$\frac{\text{POP}(p) = (pkt, p')}{\text{pop}(\text{Leaf}(p)) = (pkt, \text{Leaf}(p'))}$$\\[-15pt]
+
+It follows that after popping, the resultant tree is of form $\text{Leaf}(p')$ for some PIFO $p'$. By definition 3.8 (cited above), we know the following holds for any arbitrary PIFO $p$:\\[-20pt]
+
+$$\frac{}{\vdash \text{Leaf}(p)}$$\\[-10pt]
+
+We now have: $\forall p, \vdash p'$ where $(pkt, p') = \text{pop}(\text{Leaf}(p))$.\newline
+
+With this, our Base Case is proven.\newline
+
+
+\textbf{Inductive Case:} $q = \text{Internal}(qs, p), \vdash q$\newline
+
+\textbf{Inductive Hypothesis}: $\forall 1 \leq j \leq |qs|. \vdash qs[j]',$ where $(pkt[j], qs[j]') = \text{pop}(qs[j])$\newline
+
+Recall Definition 3.8 for $\vdash$ on Internal Nodes:
+
+$$\frac{\forall 1 \leq i \leq |qs|. \vdash qs[i] \land |p|_i = |qs[i]|}{\vdash \text{Internal}(\text{qs, p})}$$\\[-10pt]
+
+Recall Definition 3.6 for $\text{pop}$ on Internal Nodes:
+
+$$\frac{\text{POP(p) = (i, p') \hspace{1cm} \text{pop}(qs[i]) = (pkt, q')}}{{\text{pop}(\text{Internal}(qs, p)) = (pkt, \text{Internal}(qs[q'/i], p'))}}$$\\[-10pt]
+
+Now, let $(pkt, q') = \text{pop}(qs[i])$, and let $(i, p') = \text{POP}(p)$.\newline
+
+\textbf{Show}: $\vdash q \implies \vdash \text{Internal}(qs[q'/i], p')$.\newline
+
+Using definition 3.6 and our Inductive Hypothesis, we can conclude that $\vdash q'$. Furthermore, note that the only subtree to be modified in $qs$ is in $qs[i]$, per the definition of $\text{pop}$.\newline
+
+\textbf{Now we make the following claim:}\\[-20pt]
+
+\begin{alignat*}{5}
+&(1) \vdash \text{Internal}(qs, p) && \hspace{0.3cm} \textit{By definition}\\[10pt]
+&(2) \implies \forall 1 \leq j \leq |qs|. \hspace{0.2cm} \vdash qs[j] \land |p|_j = |qs[j]|&& \hspace{0.3cm} \textit{Inversion Lemma (Definition 3.8)}\\[5pt]
+&(3) \implies |p|_i = |qs[i]|&& \hspace{0.3cm} \textit{Instance of universal quantifier (2)}\\[5pt]
+&(4) \indent |p'|_i = |p|_i - 1&& \hspace{0.3cm} \textit{Definition 1A}\\[5pt]
+&(5) \indent |q'| = |qs[i]| - 1&& \hspace{0.3cm} \textit{Lemma 1}\\[5pt]
+&(6) \implies |p|_i - 1 = |qs[i]| - 1&& \hspace{0.3cm} \textit{Subtraction Property of Equality}\\[5pt]
+&(7) \implies |p'|_i = |q'|&& \hspace{0.3cm} \textit{Substitution (4, 5, 6)}\\[5pt]
+&(8) \indent \forall 1 \leq j \leq |p'|, i \neq j \implies |p'|_j = |p|_j&& \hspace{0.3cm} \textit{Definition 1B}\\[5pt]
+&(9) \implies \forall 1 \leq j \leq |p'|, i \neq j \implies |p'|_j = |qs[j]|&& \hspace{0.3cm} \textit{By (2) and (8)}\\[5pt]
+&(10) \implies \forall 1 \leq j \leq |p'|, |p'|_j = |qs[q' / i][j]|&& \hspace{0.3cm} \textit{By (7) and (9)}\\[5pt]
+&(11)  \indent \forall 1 \leq j \leq |qs|. \vdash qs[q'/i][j]&& \hspace{0.3cm} \textit{Inductive Hypothesis}\\[5pt]
+&(12) \implies \forall 1 \leq j \leq |qs|. \vdash qs[q'/i][j] \land |p'|_j = |qs[q'/i][j]|&&\hspace{0.3cm} \textit{By (10) and (11)}\\[5pt]
+&(13) \implies \vdash \text{Internal}(qs[q'/i], p') && \hspace{0.3cm} \textit{Definition of } \vdash\\[-10pt]
+\end{alignat*}
+
+With this, we have proven our Inductive Statement and completed the proof. We have shown that popping from an arbitrary PIFO Tree preserves its well-formedness.\\[-10pt]
+
+\end{document}
+
diff --git a/pieo-trees/well-formedness/refs.bib b/pieo-trees/well-formedness/refs.bib
new file mode 100644
index 0000000..e69de29