diff --git a/SoftwareFoundations2/StackMachine/Compile.lean b/SoftwareFoundations2/StackMachine/Compile.lean
index 7ad1d7f..b57e86c 100644
--- a/SoftwareFoundations2/StackMachine/Compile.lean
+++ b/SoftwareFoundations2/StackMachine/Compile.lean
@@ -6,23 +6,26 @@ def AExp.compile : AExp → List Instruction
   | ANum n       => [ PUSH n ]
   | AId x        => [ LOAD x ]
   | AMult a1 a2  => a1.compile ++ a2.compile ++ [ MUL ]
-  | AMinus a1 a2 => sorry
-  | APlus a1 a2  => sorry
+  | AMinus a1 a2 => a1.compile ++ a2.compile ++ [ SUB ]
+  | APlus a1 a2  => a1.compile ++ a2.compile ++ [ ADD ]
 
 def BExp.compile : BExp → List Instruction
   | BTrue        => [ PUSH 1 ]
   | BFalse       => [ PUSH 0 ]
   | BEq a1 a2    => a1.compile ++ a2.compile ++ [ EQ ]
-  | BNeq a1 a2   => sorry
+  | BNeq a1 a2   => a1.compile ++ a2.compile ++ [ EQ, ISZERO ]
   | BLe a1 a2    => a1.compile ++ a2.compile ++ [ .LE ]
-  | BGt a1 a2    => sorry
-  | BNot b       => sorry
-  | BAnd b1 b2   => sorry
+  | BGt a1 a2    => a1.compile ++ a2.compile ++ [ .LE, ISZERO ]
+  | BNot b       => b.compile ++ [ISZERO]
+  | BAnd b1 b2   => b1.compile ++ b2.compile ++ [ MUL ]
 
 def Com.compileOffset (pcOffset : ℕ) : Com → List Instruction
-  | CSkip       => sorry
-  | CAsgn x a   => sorry
-  | CSeq c1 c2  => sorry
+  | CSkip       => [ NOP ]
+  | CAsgn x a   => a.compile ++ [ STORE x ]
+  | CSeq c1 c2  =>
+      let c1c := c1.compileOffset pcOffset
+      let c2c := c2.compileOffset (pcOffset + c1c.length)
+      c1c ++ c2c
   | CIf b c1 c2 =>
       -- See comment below for stack layout
       let bCode := b.compile
@@ -47,7 +50,7 @@ def Com.compileOffset (pcOffset : ℕ) : Com → List Instruction
 def Com.compile (com : Com) := com.compileOffset 0 ++ [.STOP]
 
 /-
-  Stack layout for a compiled `if b then l1 else l2`.
+  Code layout for a compiled `if b then l1 else l2`.
   First column: code section;
   Second column: offset within the code.
 
@@ -64,12 +67,12 @@ def Com.compile (com : Com) := com.compileOffset 0 ++ [.STOP]
       JUMP             pcOffset + bCode.length + l1.length + l2.length + 7
                        pcOffset + bCode.length + l1.length + l2.length + 8   { == pcJumpPost }
 
-  Stack layout for a compiled `while b do l od`:
+  Code layout for a compiled `while b do l od`:
 
       bCode            pcOffset                                              { == pcCheck }
       pcJumpTrue       pcOffset + bCode.length
       JUMPI            pcOffset + bCode.length + 1
-      pcJumpPost       pcOffset + bCode.length + 2      
+      pcJumpPost       pcOffset + bCode.length + 2
       JUMP             pcOffset + bCode.length + 3
       l                pcOffset + bCode.length + 4                           { == pcJumpTrue }
       pcCheck          pcOffset + bCode.length + l.length + 4
@@ -77,9 +80,6 @@ def Com.compile (com : Com) := com.compileOffset 0 ++ [.STOP]
                        pcOffset + bCode.length + l.length + 6                { == pcJumpPost }
 -/
 
-/-
-  Uncomment after filling all sorries:
-
 #eval aexp⟨{ (x * 2) - 1 + 30 }⟩.compile
 #eval aexp⟨{ x - (2 * y) }⟩.compile
 #eval ⟨{
@@ -136,4 +136,3 @@ def Com.compile (com : Com) := com.compileOffset 0 ++ [.STOP]
   pc    := 0,
   mem   := [ "x" ↦ 161 ],
 })
--/
diff --git a/SoftwareFoundations2/StackMachine/Lemmas.lean b/SoftwareFoundations2/StackMachine/Lemmas.lean
index 48415a0..56c2d1c 100644
--- a/SoftwareFoundations2/StackMachine/Lemmas.lean
+++ b/SoftwareFoundations2/StackMachine/Lemmas.lean
@@ -15,42 +15,122 @@ attribute [local simp] fetchInstr
 attribute [local simp] stackPeek2
 attribute [local simp] stackPeek1
 
-set_option warn.sorry false in
 lemma isErrorLemma {err st'} : ¬ Reachable (.error err) st' := by
-  sorry
+  intros h
+  generalize eq : (Except.error err) = st at h
+  induction h with
+  | step h => cases eq
+  | trans s1 s2 ih1 ih2 =>
+    cases eq
+    simp only [imp_false, not_true_eq_false] at ih1
 
-set_option warn.sorry false in
 lemma isOOFLemma {st} : ¬ Reachable st (.error .OutOfFuel) := by
-  sorry
+  intros h
+  generalize eq : (Except.error ExecutionException.OutOfFuel) = st' at h
+  induction h with
+  | @step μ _ h =>
+    cases eq
+    simp [step, Bind.bind, Except.bind] at h
+    aesop
+  | trans s1 s2 ih1 ih2 =>
+    cases eq
+    simp only [imp_false, not_true_eq_false] at ih2
 
-set_option warn.sorry false in
 lemma isFinalStepLemma {μ st} (h : isFinal (.ok μ)) :
     step μ = st → isError st := by
-  sorry
+  rw [isFinal] at h
+  simp only [step, bind, Except.bind, fetchInstr, h, Nat.lt_irrefl, ↓reduceDIte]
+  intro h1
+  rw [←h1, isError]
+  trivial
 
-set_option warn.sorry false in
 lemma isFinalLemma {st st'} (h : isFinal st) :
     Reachable st st' → isError st' := by
-  sorry
+  intro h
+  induction h with
+  | @step μ st'' hx =>
+    exact isFinalStepLemma h hx
+  | @trans _ stx st'' s1 s2 ih1 ih2 =>
+    apply ih1 at h
+    cases st'' with
+    | ok => contradiction
+    | error e =>
+      have := @isErrorLemma e stx
+      contradiction
 
-set_option warn.sorry false in
 lemma executeFinal {μ st fuel} (h : isFinal (.ok μ)) :
     execute fuel μ = st → st = .ok μ := by
-  sorry
+  intro h1
+  rw [execute.eq_def] at h1
+  simp [h] at h1
+  symm
+  assumption
 
-set_option warn.sorry false in
 lemma executeExtend {μ μ' fuel} (h : step μ = .ok μ') :
     execute (fuel + 1) μ = execute fuel μ' := by
-  sorry
+  rw [execute]
+  by_cases hx : μ.pc < μ.code.length
+  · rw [h]
+    by_cases hf : isFinal (Except.ok μ)
+    · rw [isFinal] at hf
+      aesop
+    · simp [hf]
+  · simp [step, hx, Bind.bind, Except.bind] at h
 
-set_option warn.sorry false in
 lemma executeStepFinal {μ st} (h1 : isFinal st) (h2 : step μ = st) :
     execute 1 μ = st := by
-  sorry
+    rw [execute]
+    by_cases hx : μ.pc < μ.code.length
+    · have hf : ¬ isFinal (Except.ok μ) := by
+        rw [isFinal]
+        intro habs
+        rw [habs] at hx
+        exact Nat.lt_irrefl μ.code.length hx
+      rw [h2]
+      simp only [hf, ↓reduceIte]
+      cases st with
+      | ok μ' =>
+        simp only [execute, ite_eq_left_iff, reduceCtorEq, imp_false, Decidable.not_not]
+        exact h1
+      | error => contradiction
+    · simp only [step, bind, Except.bind, fetchInstr, hx, ↓reduceDIte] at h2
+      rw [←h2] at h1
+      contradiction
+
+lemma executeLemmaAux {n : Nat} {μ μ' : MachineState} (h : Reachable (.ok μ) (.ok μ'))
+  : ∃m, execute m μ = execute n μ' := by
+  generalize eq1 : Except.ok μ = st at h
+  generalize eq2 : Except.ok μ' = st' at h
+  induction h generalizing n μ μ' with
+  | step hs =>
+    cases eq1
+    cases eq2
+    use n + 1
+    exact executeExtend hs
+  | @trans _ _ sti _ _ ih1 ih2 =>
+    cases eq1
+    cases eq2
+    simp only [Except.ok.injEq, forall_eq_apply_imp_iff] at *
+    cases sti with
+    | error x =>
+      have := @isErrorLemma x (Except.ok μ')
+      contradiction
+    | ok μi =>
+      specialize @ih2 n μi rfl
+      obtain ⟨m2, hm2⟩ := ih2
+      specialize @ih1 m2 μ μi rfl rfl
+      obtain ⟨m1, hm1⟩ := ih1
+      rw [hm2] at hm1
+      use m1
 
-set_option warn.sorry false in
 /-- Hard exercise, you will likely need the lemmas above,
     and possibly additional intermediary results. -/
 lemma executeLemma {μ st} (h1 : Reachable (.ok μ) st) (h2 : isFinal st) :
     ∃ fuel : ℕ, execute fuel μ = st := by
-  sorry
+  cases st with
+  | error => contradiction
+  | ok μx =>
+    obtain ⟨m, hm⟩ := @executeLemmaAux 0 _ _ h1
+    use m
+    rw [hm, execute]
+    simp [h2]
diff --git a/SoftwareFoundations2/StackMachine/Semantics.lean b/SoftwareFoundations2/StackMachine/Semantics.lean
index 36c41fa..245a41a 100644
--- a/SoftwareFoundations2/StackMachine/Semantics.lean
+++ b/SoftwareFoundations2/StackMachine/Semantics.lean
@@ -44,9 +44,11 @@ def step (μ : MachineState) : ExecutionState := do
       let ⟨n1, n2, s⟩ ← stackPeek2 μ
       .ok <| replaceStackAndIncrPC μ ((n2 + n1) :: s)
   | SUB      =>
-      sorry
+      let ⟨n1, n2, s⟩ ← stackPeek2 μ
+      .ok <| replaceStackAndIncrPC μ ((n2 - n1) :: s)
   | MUL      =>
-      sorry
+      let ⟨n1, n2, s⟩ ← stackPeek2 μ
+      .ok <| replaceStackAndIncrPC μ ((n2 * n1) :: s)
   | EQ       =>
       let ⟨n1, n2, s⟩ ← stackPeek2 μ
       if n2 == n1 then
@@ -54,9 +56,17 @@ def step (μ : MachineState) : ExecutionState := do
       else
         .ok <| replaceStackAndIncrPC μ (0 :: s)
   | .LE       =>
-      sorry
+      let ⟨n1, n2, s⟩ ← stackPeek2 μ
+      if n2 ≤ n1 then
+        .ok <| replaceStackAndIncrPC μ (1 :: s)
+      else
+        .ok <| replaceStackAndIncrPC μ (0 :: s)
   | .ISZERO     =>
-      sorry
+      let ⟨n1, s⟩ ← stackPeek1 μ
+      if n1 == 0 then
+        .ok <| replaceStackAndIncrPC μ (1 :: s)
+      else
+        .ok <| replaceStackAndIncrPC μ (0 :: s)
   | JUMP =>
       let ⟨pc, s⟩ ← stackPeek1 μ
       .ok <| { μ with pc := pc, stack := s }
diff --git a/SoftwareFoundations2/StackMachine/SemanticsPreservation.lean b/SoftwareFoundations2/StackMachine/SemanticsPreservation.lean
index 94697ff..7a6c9cc 100644
--- a/SoftwareFoundations2/StackMachine/SemanticsPreservation.lean
+++ b/SoftwareFoundations2/StackMachine/SemanticsPreservation.lean
@@ -20,13 +20,179 @@ lemma AExp.compileCorrectAux {pre suf stack mem} (a : AExp) :
   Reachable
     (.ok ⟨pre ++ (a.compile ++ suf), stack, mem, pre.length⟩)
     (.ok ⟨pre ++ (a.compile ++ suf), a.eval mem :: stack, mem, (pre ++ a.compile).length⟩) := by
-    sorry
+  induction a generalizing pre suf stack with
+  | ANum n =>
+      simp only [compile]
+      apply Reachable.step
+      simp [step, fetchInstr, replaceStackAndIncrPC, incrPC]
+  | AId x =>
+      simp only [compile]
+      apply Reachable.step
+      simp [step, fetchInstr, replaceStackAndIncrPC, incrPC]
+  | APlus a1 a2 ih1 ih2 =>
+      simp only [List.length_append] at ih2
+      simp only [compile, List.append_assoc, eval, List.length_append]
+      apply Reachable.trans ih1
+      rw [List.length_append, ←List.append_assoc]
+      apply @Reachable.trans _ _ (.ok {
+          code := pre ++ a1.compile ++ (a2.compile ++ ADD :: suf),
+          stack := eval mem a2 :: eval mem a1 :: stack,
+          mem := mem,
+          pc := pre.length + a1.compile.length + a2.compile.length
+        })
+      · rw [←List.length_append]
+        apply ih2
+      · apply Reachable.step
+        rw [step, fetchInstr]
+        simp [←Nat.add_assoc]
+        have : pre.length + a1.compile.length + a2.compile.length <
+          pre.length + a1.compile.length + a2.compile.length + suf.length + 1 := by omega
+        simp [this, ←List.append_assoc, stackPeek2, replaceStackAndIncrPC, incrPC]
+  | AMinus a1 a2 ih1 ih2 =>
+      simp only [List.length_append] at ih2
+      simp only [compile, List.append_assoc, eval, List.length_append]
+      apply Reachable.trans ih1
+      rw [List.length_append, ←List.append_assoc]
+      apply @Reachable.trans _ _ (.ok {
+          code := pre ++ a1.compile ++ (a2.compile ++ SUB :: suf),
+          stack := eval mem a2 :: eval mem a1 :: stack,
+          mem := mem,
+          pc := pre.length + a1.compile.length + a2.compile.length
+        })
+      · rw [←List.length_append]
+        apply ih2
+      · apply Reachable.step
+        rw [step, fetchInstr]
+        simp [←Nat.add_assoc]
+        have : pre.length + a1.compile.length + a2.compile.length <
+          pre.length + a1.compile.length + a2.compile.length + suf.length + 1 := by omega
+        simp [this, ←List.append_assoc, stackPeek2, replaceStackAndIncrPC, incrPC]
+  | AMult a1 a2 ih1 ih2 =>
+      simp only [List.length_append] at ih2
+      simp only [compile, List.append_assoc, eval, List.length_append]
+      apply Reachable.trans ih1
+      rw [List.length_append, ←List.append_assoc]
+      apply @Reachable.trans _ _ (.ok {
+          code := pre ++ a1.compile ++ (a2.compile ++ MUL :: suf),
+          stack := eval mem a2 :: eval mem a1 :: stack,
+          mem := mem,
+          pc := pre.length + a1.compile.length + a2.compile.length
+        })
+      · rw [←List.length_append]
+        apply ih2
+      · apply Reachable.step
+        rw [step, fetchInstr]
+        simp [←Nat.add_assoc]
+        have : pre.length + a1.compile.length + a2.compile.length <
+          pre.length + a1.compile.length + a2.compile.length + suf.length + 1 := by omega
+        simp [this, ←List.append_assoc, stackPeek2, replaceStackAndIncrPC, incrPC]
 
 lemma BExp.compileCorrectAux {pre suf stack mem} (b : BExp) :
   Reachable
     (.ok ⟨pre ++ (b.compile ++ suf), stack, mem, pre.length⟩)
     (.ok ⟨pre ++ (b.compile ++ suf), (b.eval mem).toValue :: stack, mem, (pre ++ b.compile).length⟩) := by
-    sorry
+    induction b generalizing pre suf stack with
+    | BTrue =>
+      apply Reachable.step
+      simp only [compile]
+      simp [step, fetchInstr, replaceStackAndIncrPC, incrPC]
+    | BFalse =>
+      apply Reachable.step
+      simp only [compile]
+      simp [step, fetchInstr, replaceStackAndIncrPC, incrPC]
+    | BEq a1 a2 =>
+      simp only [compile, List.append_assoc, eval, List.length_append]
+      apply Reachable.trans
+      · apply AExp.compileCorrectAux
+      · apply Reachable.trans
+        · rw [←List.append_assoc]
+          apply AExp.compileCorrectAux a2
+        · apply Reachable.step
+          simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek2]
+          by_cases h : AExp.eval mem a1 = AExp.eval mem a2
+          · simp +arith [h]
+          · simp +arith [h]
+            have : (AExp.eval mem a1 == AExp.eval mem a2) = false := by
+              simp only [beq_eq_false_iff_ne]
+              assumption
+            simp only [this]
+    | BNeq a1 a2 =>
+      simp only [compile, List.append_assoc, eval, List.length_append]
+      apply Reachable.trans
+      · apply AExp.compileCorrectAux
+      · apply Reachable.trans
+        · rw [←List.append_assoc]
+          apply AExp.compileCorrectAux a2
+        · apply Reachable.trans (Reachable.step rfl)
+          simp only [step, Except.instMonad, Except.bind, fetchInstr, List.append_assoc, List.length_append,
+            Nat.le_add_right, List.getElem_append_right, Nat.add_sub_cancel_left, Nat.le_refl,
+            Nat.sub_self, replaceStackAndIncrPC, incrPC, stackPeek2, beq_iff_eq]
+          by_cases h : AExp.eval mem a1 = AExp.eval mem a2
+          · simp +arith only [h, bne_self_eq_false]
+            apply Reachable.step
+            simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek1, ←List.append_assoc]
+          · simp +arith only [h]
+            have : (AExp.eval mem a1 != AExp.eval mem a2) = true := by
+              simp only [bne_iff_ne, ne_eq]
+              assumption
+            simp only [this]
+            apply Reachable.step
+            simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek1, ←List.append_assoc]
+    | BLe a1 a2 =>
+      simp only [compile, List.append_assoc, eval, List.length_append]
+      apply Reachable.trans
+      · apply AExp.compileCorrectAux
+      · apply Reachable.trans
+        · rw [←List.append_assoc]
+          apply AExp.compileCorrectAux a2
+        · apply Reachable.step
+          simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek2]
+          by_cases h : AExp.eval mem a1 ≤ AExp.eval mem a2 <;> simp +arith [h]
+    | BGt a1 a2 =>
+      simp only [compile, List.append_assoc, eval, List.length_append]
+      apply Reachable.trans
+      · apply AExp.compileCorrectAux
+      · apply Reachable.trans
+        · rw [←List.append_assoc]
+          apply AExp.compileCorrectAux a2
+        · apply Reachable.trans
+          · apply Reachable.step
+            rfl
+          · simp only [step, Except.instMonad, Except.bind, fetchInstr, List.append_assoc, List.length_append,
+              Nat.le_add_right, List.getElem_append_right, Nat.add_sub_cancel_left, Nat.le_refl,
+              Nat.sub_self, replaceStackAndIncrPC, incrPC, stackPeek2, beq_iff_eq]
+            by_cases h : AExp.eval mem a1 ≤ AExp.eval mem a2
+            · simp +arith only [h]
+              apply Reachable.step
+              simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek1, ←List.append_assoc]
+              have h : (AExp.eval mem a2 < AExp.eval mem a1) = false := by
+                simp only [Bool.false_eq_true, eq_iff_iff, iff_false, Nat.not_lt, h]
+              simp only [h, Bool.false_eq_true, decide_false]
+            · simp +arith only [h]
+              apply Reachable.step
+              simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek1, ←List.append_assoc]
+              have : (AExp.eval mem a2 < AExp.eval mem a1) = true := by
+                simp only [Nat.not_le] at h
+                simp only [h]
+              simp only [this, decide_true]
+    | BNot b1 ih =>
+        simp only [compile, List.append_assoc, eval, List.length_append]
+        apply Reachable.trans
+        · apply ih
+        · apply Reachable.step
+          simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek2, stackPeek1]
+          by_cases h : eval mem b1 = true <;> simp [h] <;> omega
+    | BAnd b1 b2 ih1 ih2 =>
+        simp only [compile, List.append_assoc, eval, List.length_append]
+        apply Reachable.trans ih1
+        rw [←List.append_assoc]
+        apply Reachable.trans ih2
+        apply Reachable.step
+        simp [step, fetchInstr, replaceStackAndIncrPC, incrPC, stackPeek2]
+        by_cases h1 : eval mem b1 = true <;> by_cases h2 : eval mem b2 = true
+        all_goals
+        simp only [h1, h2, Nat.mul_one, Bool.and_true, true_and, Bool.and_false]
+        omega
 
 /- For this proof, don't be set off if it becomes super technical and long.
    You can likely split the definition of Com.compileOffset into multiple sub-operations,
@@ -37,18 +203,199 @@ lemma Com.compileCorrectAux (pgm σ σ' stack pre suf) (h : σ =[pgm]=> σ') :
   Reachable
     (.ok ⟨pre ++ pgm.compileOffset pre.length ++ suf, stack, σ, pre.length⟩)
     (.ok ⟨pre ++ pgm.compileOffset pre.length ++ suf, stack, σ', (pre ++ pgm.compileOffset pre.length).length⟩) := by
-    sorry
+  induction h generalizing pre suf with
+  | ESkip =>
+      simp only [Com.compileOffset, List.append_assoc, List.cons_append, List.nil_append,
+        List.length_append, List.length_cons, List.length_nil, Nat.zero_add]
+      apply Reachable.step
+      simp [step, fetchInstr, Except.instMonad, Except.bind, incrPC]
+  | EAsgn h1 h2 =>
+      subst h1
+      subst h2
+      simp only [Com.compileOffset, List.append_assoc, List.cons_append, List.nil_append,
+        List.length_append, List.length_cons, List.length_nil, Nat.zero_add]
+      apply Reachable.trans
+      · apply AExp.compileCorrectAux
+      · apply Reachable.step
+        simp [step, fetchInstr, Except.instMonad, Except.bind, stackPeek1, replaceMemStackAndIncrPC, replaceStackAndIncrPC, incrPC]
+        rfl
+  | ESeq c1 c2 ih1 ih2 =>
+      simp only [Com.compileOffset, List.append_assoc, List.length_append]
+      apply Reachable.trans
+      · rw [←List.append_assoc]
+        apply ih1
+      · rename_i c₁ _ c₂ _
+        specialize ih2 (pre ++ c₁.compileOffset pre.length) suf
+        simp_all only [List.append_assoc, List.length_append]
+  | EWhileTrue htrue h1 h2 ih1 ih2 =>
+      rename_i c _ b _
+      simp only [Com.compileOffset, List.append_assoc, List.cons_append, List.nil_append,
+        List.length_append, List.length_cons, List.length_nil, Nat.zero_add, Nat.reduceAdd]
+      apply Reachable.trans
+      · apply BExp.compileCorrectAux
+      · apply Reachable.trans
+        · apply Reachable.step
+          simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC]
+          rfl
+        · apply Reachable.trans
+          · apply Reachable.step
+            simp only [step, Except.instMonad, Except.bind, fetchInstr, Nat.add_assoc,
+              List.length_append, List.length_cons, Nat.reduceAdd, Nat.add_lt_add_iff_left,
+              Nat.le_add_right, List.getElem_append_right, Nat.add_sub_cancel_left,
+              List.getElem_cons_succ, List.getElem_cons_zero, dite_eq_ite, replaceStackAndIncrPC,
+              incrPC, beq_iff_eq, gt_iff_lt]
+            simp only [← Nat.add_assoc, Nat.lt_add_left_iff_pos, Nat.zero_lt_succ, ↓reduceIte,
+              stackPeek2, htrue, Nat.lt_add_one]
+            rfl
+          · apply Reachable.trans
+            · specialize ih1 (pre ++ b.compile ++ [PUSH (pre.length + b.compile.length + 4),
+              JUMPI, PUSH (pre.length + b.compile.length + (Com.compileOffset (pre.length + b.compile.length + 4) c).length + 6), JUMP]) (PUSH pre.length :: JUMP :: suf)
+              simp_all only [List.append_assoc, List.length_append, List.length_cons, List.length_nil, Nat.zero_add,
+                Nat.reduceAdd, List.cons_append, List.nil_append]
+              exact ih1
+            · clear ih1
+              simp only [Nat.add_assoc, Nat.reduceAdd]
+              apply Reachable.trans
+              · apply Reachable.step
+                simp only [step, Except.instMonad, Except.bind, fetchInstr, List.length_append,
+                  List.length_cons, Nat.add_assoc, Nat.reduceAdd, Nat.add_lt_add_iff_left,
+                  Nat.lt_add_left_iff_pos, Nat.zero_lt_succ, ↓reduceDIte, Nat.le_add_right,
+                  List.getElem_append_right, Nat.add_sub_cancel_left, List.getElem_cons_succ,
+                  Nat.le_refl, Nat.sub_self, List.getElem_cons_zero, replaceStackAndIncrPC, incrPC,
+                  beq_iff_eq, gt_iff_lt]
+                rfl
+              · apply Reachable.trans
+                · apply Reachable.step
+                  simp [step, fetchInstr, Except.instMonad, Except.bind, Nat.add_assoc, stackPeek1]
+                  rfl
+                · simp only [Com.compileOffset, Nat.add_assoc, List.append_assoc, List.cons_append,
+                  List.nil_append, List.length_append, List.length_cons, List.length_nil,
+                  Nat.zero_add, Nat.reduceAdd] at ih2
+                  apply ih2
+  | EWhileFalse hfalse =>
+      rename_i c b σ
+      apply Reachable.trans
+      · simp only [Com.compileOffset, List.append_assoc, List.cons_append, List.nil_append]
+        apply BExp.compileCorrectAux
+      · apply Reachable.trans
+        · apply Reachable.step
+          simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC]
+          rfl
+        · apply Reachable.trans
+          · apply Reachable.step
+            simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC, Nat.add_assoc]
+            simp [←Nat.add_assoc, hfalse]
+            rfl
+          · apply Reachable.trans
+            · apply Reachable.step
+              simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC, Nat.add_assoc]
+              simp [←Nat.add_assoc]
+              rfl
+            · apply Reachable.step
+              simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC, Nat.add_assoc]
+              simp [←Nat.add_assoc, Com.compileOffset, stackPeek1]
+  | EIfTrue htrue h ih =>
+      rename_i σ c₁ σ' b c₂
+      simp only [Com.compileOffset, Nat.add_assoc, List.append_assoc, List.cons_append,
+        List.nil_append, List.length_append, List.length_cons, List.length_nil, Nat.zero_add,
+        Nat.reduceAdd]
+      apply Reachable.trans
+      · apply BExp.compileCorrectAux
+      · apply Reachable.trans
+        · apply Reachable.step
+          simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC]
+          rfl
+        · apply Reachable.trans
+          · apply Reachable.step
+            simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC, Nat.add_assoc]
+            simp [←Nat.add_assoc, htrue]
+            rfl
+          · simp only [Nat.add_assoc, stackPeek2]
+            apply Reachable.trans
+            · specialize ih (pre ++ b.compile ++ [PUSH (pre.length + (b.compile.length + 4)),
+              JUMPI, PUSH (pre.length + (b.compile.length + ((Com.compileOffset (pre.length + (b.compile.length + 4)) c₁).length + 6))), JUMP])
+              aesop
+            · clear ih
+              apply Reachable.trans
+              · apply Reachable.step
+                simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC]
+                rfl
+              · apply Reachable.step
+                simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC, Nat.add_assoc]
+                simp [←Nat.add_assoc, stackPeek1]
+  | EIfFalse hfalse h ih =>
+      rename_i σ c₂ σ' b c₁
+      simp only [Com.compileOffset, Nat.add_assoc, List.append_assoc, List.cons_append,
+        List.nil_append, List.length_append, List.length_cons, List.length_nil, Nat.zero_add,
+        Nat.reduceAdd]
+      apply Reachable.trans
+      · apply BExp.compileCorrectAux
+      · apply Reachable.trans
+        · apply Reachable.step
+          simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC]
+          rfl
+        · apply Reachable.trans
+          · apply Reachable.step
+            simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC, Nat.add_assoc]
+            simp [←Nat.add_assoc, hfalse]
+            rfl
+          · simp only [Nat.add_assoc]
+            apply Reachable.trans
+            · apply Reachable.step
+              simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC]
+              rfl
+            · apply Reachable.trans
+              · apply Reachable.step
+                simp [step, fetchInstr, Except.instMonad, Except.bind, Nat.add_assoc]
+                simp [←Nat.add_assoc]
+                rfl
+              · apply Reachable.trans
+                · simp [Nat.add_assoc, stackPeek1]
+                  specialize ih <|
+                    pre ++ b.compile ++
+                      [PUSH (pre.length + (b.compile.length + 4)), JUMPI, PUSH (pre.length +
+              (b.compile.length + ((Com.compileOffset (pre.length + (b.compile.length + 4)) c₁).length + 6))), JUMP] ++
+                    (Com.compileOffset (pre.length + (b.compile.length + 4)) c₁) ++
+                    [PUSH (pre.length +
+                    (b.compile.length +
+                      ((Com.compileOffset (pre.length + (b.compile.length + 4)) c₁).length +
+                        ((Com.compileOffset
+                              (pre.length +
+                                (b.compile.length +
+                                  ((Com.compileOffset (pre.length + (b.compile.length + 4)) c₁).length + 6)))
+                              c₂).length +
+                          8)))), JUMP]
+                  aesop
+                · clear ih
+                  apply Reachable.trans
+                  · apply Reachable.step
+                    simp [step, fetchInstr, Except.instMonad, Except.bind, replaceStackAndIncrPC, incrPC]
+                    rfl
+                  · apply Reachable.step
+                    simp only [step, Except.instMonad, Except.bind, fetchInstr, Nat.add_assoc,
+                      Nat.reduceAdd, List.length_append, List.length_cons, Nat.add_lt_add_iff_left,
+                      Nat.lt_add_left_iff_pos, Nat.zero_lt_succ, ↓reduceDIte, Nat.le_add_right,
+                      List.getElem_append_right, Nat.add_sub_cancel_left, beq_iff_eq, gt_iff_lt]
+                    simp only [← Nat.add_assoc, List.getElem_cons_succ]
+                    simp [Nat.add_assoc, stackPeek1]
 
 lemma Com.compileCorrectAux2 (pgm σ σ' stack) (h : σ =[pgm]=> σ') :
   Reachable
     (.ok ⟨pgm.compile, stack, σ, 0⟩)
     (.ok ⟨pgm.compile, stack, σ', pgm.compile.length⟩) := by
-    sorry
+    rw [Com.compile]
+    have hx := Com.compileCorrectAux _ σ σ' stack [] [STOP] h
+    simp only [List.length_nil, List.nil_append] at hx
+    apply Reachable.trans hx
+    apply Reachable.step
+    simp only [step, Except.instMonad, Except.bind, fetchInstr, List.length_append, List.length_cons, List.length_nil,
+    Nat.zero_add, Nat.lt_add_one, ↓reduceDIte, Nat.le_refl, List.getElem_append_right, Nat.sub_self,
+    List.getElem_cons_zero, replaceStackAndIncrPC, incrPC, stackPeek1, stackPeek2, beq_iff_eq, gt_iff_lt]
 
 /- With these lemmas on hand, proving correctness of compilation for {`AExp`, `BExp`, whole programs} is an easy consequence.
   I kept the proofs in full, they do not need to be filled out.
   Try to work out their reasoning and understand how the lemmas come into play!
-  
+
   Important: `executeLemma` plays a crucial role here, which is marked as a
   hard optional exercise in `Lemmas.lean`. Why is it so important?
 -/