diff --git a/ahmed/day1.agda b/ahmed/day1.agda
index 4d83b7a..93e9a46 100644
--- a/ahmed/day1.agda
+++ b/ahmed/day1.agda
@@ -1,28 +1,34 @@
 module ahmed.day1 where
 
+open import Agda.Primitive
+open import Data.Nat
+open import Data.Fin
 open import Data.Product
 
 data Type : Set where
   Bool : Type
   _-→_ : Type → Type → Type
 
-data Term : Set where
-  True : Term
-  False : Term
-  If_Then_Else_ : Term → Term → Term → Term
-  λ[_::_]_ : Term → Type → Term → Term
-  _∙_ : Term → Term → Term
+data Term (n : ℕ) : Set where
+  Var : (m : Fin n) → Term n
+  True : Term n
+  False : Term n
+  If_Then_Else_ : Term n → Term n → Term n → Term n
+  λ[_::_]_ : Term n → Type → Term n → Term n
+  _∙_ : Term n → Term n → Term n
 
-data isValue : Term → Set where
-  TrueValue : isValue True
-  FalseValue : isValue False
-  LambdaValue : (x : Term) → (τ : Type) → (e : Term) → isValue (λ[ x :: τ ] e)
+data isValue (n : ℕ) : Term n → Set where
+  TrueValue : isValue n True
+  FalseValue : isValue n False
+  LambdaValue : (x : Term n) → (τ : Type) → (e : Term n) → isValue n (λ[ x :: τ ] e)
 
-Value = Σ Term isValue
+Value = (n : ℕ) → Σ (Term n) (isValue n)
 
-data evaluationContext : Set where
-  dot : evaluationContext
-  EIf_Then_Else_ : evaluationContext → Term → Term → evaluationContext
-  EAppLeft : evaluationContext → Term → evaluationContext
-  EAppRight : Value → evaluationContext → evaluationContext
+data evaluationContext : (n : ℕ) → Set where
+  dot : evaluationContext 0
+  EIf_Then_Else_ : {n : ℕ} → evaluationContext n → Term n → Term n → evaluationContext n
+  EAppLeft : {n : ℕ} → evaluationContext n → Term n → evaluationContext n
+  EAppRight : {n : ℕ} → Value → evaluationContext n → evaluationContext n
 
+data isValidValueForType (n : ℕ) (t : Type) : (e : Term n) → Set where
+  TrueV : isValidValueForType n Bool True
\ No newline at end of file
diff --git a/ahmed/notes.typ b/ahmed/notes.typ
index e66be0f..ba0d682 100644
--- a/ahmed/notes.typ
+++ b/ahmed/notes.typ
@@ -2,12 +2,11 @@
 #import "@preview/prooftrees:0.1.0": *
 #show: doc => conf("Logical Relations", doc)
 
-#let ifthenelse(e, e1, e2) = $"if" #e "then" #e1 "else" #e2$
 #let safe = $"safe"$
 
-= Lecture 1, Mon. Jun 3 \@ 14:00
+== Lecture 1
 
-== Logical relations
+=== Logical relations
 
 Logical relations are used to prove things about programs
 
@@ -31,11 +30,11 @@ Logical relations are used to prove things about programs
 You can also relate source terms to target terms in different languages.
 This can be used to prove compiler correctness.
 
-== Type safety / soundness
+=== Type safety / soundness
 
 Unary realizability relations for FFI. "all well-behaved terms from language A can be used in language B without causing problems with either language"
 
-== STLC
+=== STLC
 
 Statics
 
@@ -123,7 +122,7 @@ $forall(e' . e mapstostar e')$ either $isValue(e')$ or $exists e'' . e' mapsto e
 
 Progress and preservation are a _technique_ for proving type soundness, by just using the two functions over and over.
 
-== Logical relations
+=== Logical relations
 
 $ P_tau(e) $
 
@@ -245,7 +244,7 @@ _Proof._ Suppose $e'$ s.t. $e mapstostar e'$ .
 
 #pagebreak()
 
-= Lecture 2, Tue. Jun 4 \@ 11:00
+== Lecture 2
 
 #set enum(numbering: "A.")
 
@@ -260,7 +259,7 @@ To prove lemma A, we must prove the fundamental property: $Gamma tack.r e:tau ar
 
 $ Gamma tack.r.double e : tau :equiv forall (gamma in G db(Gamma)) . gamma(e) in Epsilon db(tau) $
 
-=== Proving A case for $lambda$
+==== Proving A case for $lambda$
 
 Case:
 
@@ -292,7 +291,7 @@ Therefore, $gamma[x mapsto v](e) in Epsilon db(tau_2)$
 
 #TODO Do the app case at home.
 
-== Adding recursive types
+=== Adding recursive types
 
 $ Omega :equiv (lambda x . x " " x) (lambda x . x " " x) $
 
@@ -319,7 +318,7 @@ $ e ::= ... | "fold"(e) | "unfold"(e) $
 
 *NOTE*: Fold usually needs to be annotated with $mu alpha . tau$ in order to guide type checking.
 
-== Type-checking $Omega$
+=== Type-checking $Omega$
 
 $ Omega :equiv (lambda (x : ?) . x " " x) (lambda (x : ?) . x " " x) $
 
@@ -333,7 +332,7 @@ Then re-define $Omega$ to be:
 
 $ Omega' :equiv "SA" ("fold" "SA") $
 
-== Proving soundness for lambda calculus with recursive types with logical relations
+=== Proving soundness for lambda calculus with recursive types with logical relations
 
 $ v ::= ... | "fold"(v) $
 
@@ -349,7 +348,7 @@ $V db(mu alpha . tau) = { "fold"(v) | forall v in V db(subst(alpha, mu alpha. ta
 
 This is *not* a well-founded relation, because $V$ would depend on itself. This was an open problem (ATTAPL exercise) for a long time.
 
-=== Step Indexing
+==== Step Indexing
 
 This shows that this is well founded.
 
@@ -370,6 +369,6 @@ $V_k db(tau_1 arrow tau_2) = {lambda (x : tau_1) . e | forall (j lt.eq k, v in V
 - Use 1 step to do the application, resulting in $j$ steps
 - Eventually reach 0 steps left.
 
-$Epsilon_k db(tau) = { e | forall (j < k, e') arrow.r.double e mapsto e' and "irreducible"(e') arrow.r.double e' in V_(k-j) db(tau)}$
+$Epsilon_k db(tau) = { e | forall (j < k, e') arrow.r.double e op(mapsto)^j e' and "irreducible"(e') arrow.r.double e' in V_(k-j) db(tau)}$
 
 What $k$ doesn't matter because the entire relations are universally quantified over all $k$s.
\ No newline at end of file
diff --git a/common.typ b/common.typ
index ae48437..11fdccb 100644
--- a/common.typ
+++ b/common.typ
@@ -6,12 +6,15 @@
 #let mapstostar = $op(arrow.r.long.bar)^*$
 #let subst(x, v, e) = $#e [#v\/#x]$
 #let TODO = text(fill: red)[*TODO*]
+#let ifthenelse(e, e1, e2) = $"if" #e "then" #e1 "else" #e2$
 
 #let conf(title, doc) = {
   show link: underline
-  set page(width: 6in, height: 9in, margin: 0.3in)
+  set page(width: 4.8in, height: 8.4in, margin: 0.3in)
 
-  text(size: 30pt)[#title]
-  doc
+  [
+    = #text(size: 24pt)[#title]
+    #doc
+  ]
 }
 
diff --git a/downen/notes.typ b/downen/notes.typ
new file mode 100644
index 0000000..0e25bd0
--- /dev/null
+++ b/downen/notes.typ
@@ -0,0 +1,25 @@
+#import "../common.typ": *
+#import "@preview/prooftrees:0.1.0": *
+#show: doc => conf("Foundations", doc)
+
+== Lecture 1
+
+Skipped.
+
+== Lecture 2
+
+Variables $in.rev x, y, z ::= "foo" | "bar" | "baz" | ...$ \
+Constant $in.rev C ::= "true" | "false"$ \
+Term $in.rev M, N ::= X | M N | lambda x . M | C | ifthenelse(M, N_1, N_2)$
+
+Eval Ctx $in.rev E ::= square | E M | ifthenelse(E, N_1, N_2)$ \
+Environment $in.rev Gamma ::= $ \
+Judgment $::= Gamma tack.r M : A$
+
+#tree(axi[], uni[$Gamma tack.r "true" : "bool"$])
+#tree(axi[], uni[$Gamma tack.r "false" : "bool"$])
+#tree(axi[$Gamma tack.r M : "bool"$], axi[$Gamma tack.r N_1 : tau$], axi[$Gamma tack.r N_2 : tau$], tri[$Gamma tack.r ifthenelse(M, N_1, N_2) : tau$])
+
+*Lemma (Progress).* If $dot tack.r M : A$ is derivable, then $M$ is a value, or $M mapsto M'$.
+
+_Proof._ Induction on derivation.
\ No newline at end of file
diff --git a/oplss.typ b/oplss.typ
index 97f237d..7c25917 100644
--- a/oplss.typ
+++ b/oplss.typ
@@ -1,4 +1,5 @@
 #include "./ahmed/notes.typ"
+#include "./downen/notes.typ"
 #include "./pfenning/notes.typ"
 #include "./silva/notes.typ"
 
diff --git a/pfenning/notes.typ b/pfenning/notes.typ
index 7c26c16..8c00986 100644
--- a/pfenning/notes.typ
+++ b/pfenning/notes.typ
@@ -1,15 +1,13 @@
 #import "../common.typ": *
 #import "@preview/prooftrees:0.1.0": *
 #import "@preview/algo:0.3.3": algo, i, d, comment, code
-#show: doc => conf(doc)
+#show: doc => conf("Adjoint Functional Programming", doc)
 
 #let n(t) = text(fill: rgb("#aa3333"))[#t]
 #let evalto = $arrow.r.hook$
 #let with = $op(\&)$
 
-= Adjoint Functional Programming
-
-== Lecture 1. Linear functional programming
+== Lecture 1
 
 - Origins of linearity is from linear logic
 - from 1987 or before
@@ -143,7 +141,7 @@ Language to be studied is called "snax"
 
 #pagebreak()
 
-== Lecture 2
+=== Lecture 2
 
 Type system
 
@@ -273,7 +271,7 @@ Example of evaluation rule that matches the typing rule:
 )
 
 
-=== Looking at typing rules as logic
+==== Looking at typing rules as logic
 
 #rect[Natural Deduction]
 
diff --git a/silva/lec1.jpg b/silva/lec1.jpg
new file mode 100644
index 0000000..ed89f15
Binary files /dev/null and b/silva/lec1.jpg differ
diff --git a/silva/notes.typ b/silva/notes.typ
index a925ff2..04a146e 100644
--- a/silva/notes.typ
+++ b/silva/notes.typ
@@ -1,13 +1,13 @@
 #import "../common.typ": *
+#import "@preview/finite:0.3.0" as finite: automaton
+#import "@preview/fletcher:0.4.5" as fletcher: diagram, node, edge
 #import "@preview/prooftrees:0.1.0": *
-#show: doc => conf(doc)
+#show: doc => conf("Program Analysis with Kleene Algebra with Tests", doc)
 
 #let tru = $"true"$
 #let fls = $"false"$
 
-= Program Analysis with Kleene Algebra with Tests
-
-== Mon Jun 3 \@ 15:40
+== Lecture 1
 
 #quote(block: true)[
   Kleene algebra with tests is an algebraic framework that can be used to reason about imperative programs. It has been applied across a wide variety of areas including program transformations, concurrency control, compiler optimizations, cache control, networking, and more. In these lectures, we will provide an overview of Kleene Algebra with Tests, including the syntax, semantics, and the coalgebraic theory underlying decision procedures for program equivalence. We will illustrate how it can be used as a core framework for program verification, including successful extensions and fundamental limitations. 
@@ -39,7 +39,7 @@
 
 Study equivalence of uninterpreted simple imperative programs.
 
-=== Regular expressions
+==== Regular expressions
 
 Basic elements
 
@@ -172,3 +172,161 @@ Merge states of a non-deterministic finite automaton, using the peanut approach.
 
 Alternative #link("https://en.wikipedia.org/wiki/Thompson%27s_construction")[*Thompson's construction*]
 
+#pagebreak()
+
+== Lecture 2
+
+Talking about the other direction from Kleene's theorem.
+
+$ A_e mapsto e $
+
+mapping an automaton $A_e$ to a regular expression $e$.
+
+Let DFA have states $S$ and transition function $S mapsto S^A$. This can be represented by a matrix.
+The matrix is indexed on rows and columns by the states. Then in the cell for each row $i$ and column $j$, put all of the letters of the alphabet that can be used to transition between the states. For example, if you can use $a$ and $b$, put $a+b$ in the matrix.
+
+This allows you to do matrix operations in order to do operations on regular expressions. This shows that the transition function actually has more structure than just an arbitrary function.
+
+Repeatedly delete states until 2 states left, replacing the transitions with regular expressions. 
+
+What does it mean to delete states?
+
+*State elimination method.* Need at least 3 states.
+
+#automaton(
+  layout: finite.layout.snake.with(columns: 2),
+  (
+    q0: (q1:("a"), q2: "b"),
+    q1: (q1: "a", q0: "b"),
+    q2: (q1: "a", q2: "b"),
+  )
+)
+
+Delete q2, by merging its transition $b b^* a$.
+
+#automaton(
+  final: "q0",
+  (
+    q0: (q1: "a + bb*a"),
+    q1: (q1: "a", q0: "b")
+  )
+)
+
+Matrix method is more robust than the state elimination method.
+
+*Question.* Is it possible to write a finite number of equations to answer the question $e_1 eq.quest e_2$
+
+$(K, 0, 1, +, op(\;), (..)*)$ satisfies the following:
+
+- K is some set
+- Semi-ring
+  - Joint semi-lattice
+    - + is idempotent ($e + e equiv e$)
+    - + is commutative ($e + f equiv f + e$)
+    - + is associative ($(e + f) + g equiv e + (f + g)$)
+    - + has a 0 element ($e + 0 equiv e$)
+  - Monoid
+    - ; is associative ($(e ; g) ; g equiv e ; (f ; g)$)
+    - ; has a 1 element ($e ; 1 equiv e equiv 1 ; e$)
+  - ; has an absorbent element ($e ; 0 equiv 0 equiv 0 ; e$)
+  - ; distributes over +, both from the right and the left
+    - $e ; (f + g) equiv e ; f + e ; g$ AND $(e + f) ; g equiv e ; g + f ; g$
+- \* is a fix point ($e^* equiv 1 + e ; e^*$)
+- \* can be unfolded on the left or the right ($e^* equiv 1 + e^* ; e$)
+
+$e^*$ is a _least_ fix point
+
+#rect[$e <= f$ iff $e + f equiv f$]
+#tree(
+  axi[$e;x+f <= x$],
+  uni[$e^*;f <= x$]
+)
+
+This forms an #link("https://en.wikipedia.org/wiki/Axiom_schema")[axiom schema].
+
+#rect[
+  Exercises:
+
+  - $x^* x^* equiv x^*$
+  - $x^* equiv (x^*)^*$
+  - $x y equiv y z arrow.r.long.double x^* y equiv y z^*$
+  - $(a + b)^* equiv (a^* b)^* a^*$
+]
+
+Need to do it in 2 steps ($<=, >=$).
+
+This structure is useful because there are many structures like this. For example ${2^(A^*), emptyset, {epsilon}, union, circle.filled, (..)^*}$ the set of all languages is a Kleene algebra.
+
+Other examples:
+
+- #[
+  Binary relations: $("BRel", emptyset, Delta, union, circle, (..)^*)$
+
+  - $Delta$ is the diagonal relation
+  - The $(..)^*$ is transitive closure
+
+  Binary relations satisfies all of the rules of a Kleene algebra.
+]
+
+- #[
+  Square matrices: $("Mat"(k), 0, I, +, times, (..)^*)$
+
+  - $times$ is the multiplcation associated with $k$
+  - #[
+    The star operation is defined:
+    $mat(a,b;c,d)^* = mat((a+b d^* c)^*, (a+b d^* c)^* b d^*;
+    (d+c a^* b)^* c a^*, (d+c a^* b)^*)$
+
+    This describes _every_ path from a state to another state, as many times:
+
+    #automaton(
+      (
+        q0: (q0: "a", q1: "b"),
+        q1: (q0: "c", q1: "d"),
+      )
+    )
+  ]
+]
+
+*Kozen '93 result.* If two expressions $e$ and $f$ have the same language, then 
+
+$ db(e) equiv db(f) arrow.long.double.l.r e equiv f$
+
+Switching between syntax and semantics.
+
+_Proof method._
+
+For every expression $e$, build an NFA $A_e$. So $e equiv f$ gets $A_e$ and $A_f$.
+(Modern proofs will directly go to the DFA).
+Determinize the NFAs to get $A'_e$ and $A'_f$.
+Then minimize the automata to get $M_e$ and $M_f$.
+
+#image("lec1.jpg")
+
+Every DFA has a _unique_ minimal automaton, modulo renaming the state names.
+If $e$ and $f$ represent the same language, then the minimal automata must be isomorphic.
+Every $A'_e$ and $M_e$ is a matrix of expressions, and can be proven sound using the axioms of Kleene algebra.
+
+=== Imperative programs
+
+What is missing from $(K, 0, 1, +, op(\;), (..)*)$ for imperative programs?
+
+- State
+- Conditionals
+
+Conditionals needs to satisfy a boolean algebra. So we need to combine a Kleene
+algebra and a Boolean algebra.
+
+Subset of $K$: $(B, 0, 1, +, ;, overline((..)))$ is a boolean algebra. _Sub-algebra_
+
+- For B, + and ; are thought of as $or$ and $and$
+- It needs to additionally satisfy demorgan laws for not
+  - $overline(a + b) equiv overline(a) ; overline(b)$
+  - $overline(a \; b) equiv overline(a) + overline(a)$
+  - $overline(0) equiv 1$
+  - $overline(overline(a)) equiv a$
+  - $a ; b equiv b ; a$ (not true normally!!)
+
+This is only true of language without effects or concurrency.
+
+- Threads can be reasoned about in a partially distributive commutative lattice
\ No newline at end of file
diff --git a/silva/test.fst b/silva/test.fst
new file mode 100644
index 0000000..9907e0c
--- /dev/null
+++ b/silva/test.fst
@@ -0,0 +1,10 @@
+module Test
+
+type re =
+  | Zero
+  | One
+  | Char of int
+  | Seq of re * re
+  | Add of re * re
+  | Star of re
+