diff --git a/content/blog/04_spa_agda_fixedpoint.md b/content/blog/04_spa_agda_fixedpoint.md
index 6c2710b..3709d03 100644
--- a/content/blog/04_spa_agda_fixedpoint.md
+++ b/content/blog/04_spa_agda_fixedpoint.md
@@ -4,12 +4,12 @@ series: "Static Program Analysis in Agda"
 description: "In this post, I give a top-level overview of my work on formally verified static analyses"
 date: 2024-08-10T17:37:42-07:00
 tags: ["Agda", "Programming Languages"]
-draft: true
 ---
 
 In the preivous post we looked at lattices of finite height, which are a crucial
 ingredient to our static analyses. In this post, I will describe the specific
-algorithm that makes use of these lattices that will be at the core of it all.
+algorithm that makes use of these lattices; this algorithm will be at the core
+of this series.
 
 Lattice-based static analyses tend to operate by iteratively combining facts
 from the program into new ones. For instance, when analyzing `y = 1 + 2`, we
@@ -79,7 +79,7 @@ arrange the ones we've seen so far into a chain:
 
 Each time we fail to find a fixed point, we add one element to our chain, growing
 it. But if our lattice \(L\) has a finite height, that means eventually this
-process will have to stop; the chain can't grow forever; eventually, we will
+process will have to stop; the chain can't grow forever. Eventually, we will
 have to find a value such that \(v = f(v)\). Thus, our algorithm is guaranteed
 to terminate, and give a fixed point.
 
@@ -119,7 +119,7 @@ it provides just a bit more gas than the maximum-length chain, which means that
 if the gas is exhausted, we've certainly arrived at a contradiction. It also
 provides an initial chain onto which `doStep` will keep tacking on new inequalities
 as it finds them. Since we haven't found any yet, this is the single-element
-chain of \(\bot\). The last thing is does is set up the reursion invariant
+chain of \(\bot\). The last thing is does is set up the recursion invariant
 (that the sum of the gas and the chain length is constant), and provides
 a proof that \(\bot \le f(\bot)\). This function always returns a fixed point.
 
@@ -147,11 +147,11 @@ the lattice, we have \(\bot \le b\).
 
 {{< latex >}}
 \begin{array}{ccccccccr}
-& & \bot    & \le &      &   & b \quad \implies & \text{(monotonicity of}\ f \text{)}\\
-& & f(\bot) & \le & f(b) & = & b \quad \implies & \text{(} b\ \text{is a fixed point, monotonicity of}\ f \text{)}\\
-& & f^2(\bot) & \le & f(b) & = & b \quad \implies & \text{(} b\ \text{is a fixed point, monotonicity of}\ f \text{)}\\
+& & \bot    & \le &      &   & b & \quad \implies & \text{(monotonicity of}\ f \text{)}\\
+& & f(\bot) & \le & f(b) & = & b & \quad \implies & \text{(} b\ \text{is a fixed point, monotonicity of}\ f \text{)}\\
+& & f^2(\bot) & \le & f(b) & = & b & \quad \implies & \text{(} b\ \text{is a fixed point, monotonicity of}\ f \text{)}\\
 \\
-& & \vdots & & \vdots & & \vdots & \\
+& & \vdots & & \vdots & & \vdots & & \\
 \\
 a & = & f^k(\bot) & \le & f(b) & = & b &
 \end{array}
@@ -159,7 +159,7 @@ a & = & f^k(\bot) & \le & f(b) & = & b &
 
 Because of the monotonicity of \(f\), each time we apply it, it preserves the
 less-than relationship that started with \(\bot \le b\). Doing that \(k\) times,
-we verify that \(a\) is our fixed point.
+we verify that \(a\) is our least fixed point.
 
 To convince Agda of this proof, we once again get in an argument with the termination
 checker, which ends the same way it did last time: with us using the notion of 'gas'