diff --git a/Complexity/Basic.lean b/Complexity/Basic.lean
index b5a64a4..6f7c333 100644
--- a/Complexity/Basic.lean
+++ b/Complexity/Basic.lean
@@ -2,6 +2,7 @@ import Complexity.Bounds
 import Complexity.Classes
 import Complexity.Dyadic
 import Complexity.MoveUntil
+import Complexity.Pop
 import Complexity.SpaceInTime
 import Complexity.Successor
 import Complexity.TapeExtension
diff --git a/Complexity/Pop.lean b/Complexity/Pop.lean
new file mode 100644
index 0000000..ffa64a9
--- /dev/null
+++ b/Complexity/Pop.lean
@@ -0,0 +1,62 @@
+import Complexity.AbstractTape
+import Complexity.TuringMachine
+import Complexity.TapeLemmas
+import Complexity.Routines
+import Complexity.MoveUntil
+import Complexity.TMComposition
+import Complexity.WithTapes
+
+import Mathlib
+
+def pop_char : TM 1 (Fin 2) SChar :=
+  let σ := fun state symbols => match state with
+    | 0 => (1, (fun _ => (.blank, .some .right)))
+    | 1 => (1, (symbols ·, .none))
+  TM.mk σ 0 1
+
+lemma pop_char.inert_after_stop :
+  pop_char.inert_after_stop := by
+  intro conf h_is_stopped
+  ext <;> simp_all [Transition.step, performTapeOps, pop_char]
+
+@[simp]
+lemma pop_char.eval (tapes : Fin 1 → Turing.Tape SChar) :
+  pop_char.eval tapes = .some (fun _ => ((tapes 0).write .blank).move .right) := by
+  apply TM.eval_of_transforms
+  exact TM.transforms_of_inert pop_char _ _ pop_char.inert_after_stop ⟨1, sorry⟩
+
+--- This is a 1-tape Turing machine that removes the left-most word
+--- from the tape.
+def pop := (Routines.while (· ≠ .sep) pop_char).seq pop_char
+
+@[simp]
+theorem pop.eval {w : List Char} {ws₁ : List (List Char)} :
+  pop.eval (list_to_tape ∘ [w :: ws₁].get) =
+    .some (list_to_tape ∘ [ws₁].get) := by
+  have h_blank : SChar.blank = default := by rfl
+  let tapes : ℕ → Fin 1 → Turing.Tape SChar :=
+    (fun i j => Turing.Tape.mk₁ ((list_to_string (w :: ws₁)).drop i))
+  have h_tapes₀ : tapes 0 = (list_to_tape ∘ [w :: ws₁].get) := by
+    funext i; simp [tapes, list_to_tape]
+  have h_inner : ∀ i, ((TM.eval pop_char (tapes i)) = Part.some (tapes i.succ)) := by
+    simp [tapes, pop_char.eval, h_blank]
+  have h_terminate : PartENat.find (fun i => (tapes i 0).head = SChar.sep) =
+      Part.some w.length := by
+    rw [Part.eq_some_iff]
+    use ⟨w.length, by simp [tapes]⟩
+    simp only [Fin.isValue, PartENat.find_get]
+    rw [Nat.find_eq_iff]
+    constructor
+    · simp [tapes]
+    · intro n h_n_lt
+      simp only [Turing.Tape.mk₁, Turing.Tape.mk₂, list_to_string_cons, Fin.isValue,
+        Turing.Tape.mk'_head, Turing.ListBlank.head_mk, tapes]
+      rw [List.drop_eq_getElem_cons (by simp; omega)]
+      simp [h_n_lt, List.coe_schar_getElem_neq_sep]
+  have h_move_blank : (fun x ↦ Turing.Tape.move .right (.write .blank (tapes w.length 0))) =
+      list_to_tape ∘ [ws₁].get := by
+    funext i; simp [h_blank, tapes, list_to_tape]
+  rw [← h_tapes₀]
+  let h_eval := Routines.while.eval' (condition := (· ≠ .sep)) (tm := pop_char) tapes h_inner
+  simp at h_eval
+  simpa [pop, h_eval, h_terminate, pop_char.eval] using h_move_blank
diff --git a/Complexity/Routines.lean b/Complexity/Routines.lean
index ac40134..b49eaeb 100644
--- a/Complexity/Routines.lean
+++ b/Complexity/Routines.lean
@@ -45,6 +45,10 @@ lemma List.coe_schar_get_neq_sep (x : List Char) (n : Fin x.coe_schar.length) :
   x.coe_schar.get n ≠ .sep := by
   simp [List.coe_schar]
 
+lemma List.coe_schar_getElem_neq_sep (x : List Char) (n : ℕ) (h_n_lt : n < x.coe_schar.length) :
+  x.coe_schar[n] ≠ .sep := by
+  simp [List.coe_schar]
+
 lemma List.coe_schar_get_neq_blank (x : List Char) (n : Fin x.coe_schar.length) :
   x.coe_schar.get n ≠ .blank := by
   simp [List.coe_schar]
diff --git a/Complexity/TapeLemmas.lean b/Complexity/TapeLemmas.lean
index 52246f6..7f12fb0 100644
--- a/Complexity/TapeLemmas.lean
+++ b/Complexity/TapeLemmas.lean
@@ -135,6 +135,11 @@ theorem Tape.left₀_nth {Γ} [Inhabited Γ] (tape : Turing.Tape Γ) (n : ℕ) :
       Turing.ListBlank.tail_cons]
     rfl
 
+@[simp]
+lemma Tape.write_eq_drop {Γ} [Inhabited Γ] (c : Γ) (l : List Γ) :
+  Turing.Tape.write c (Turing.Tape.mk₁ l) = Turing.Tape.mk₁ (c :: (l.drop 1)) := by
+  simp [Turing.Tape.mk₁, Turing.Tape.mk₂]
+
 @[simp]
 lemma Tape.move_right_blank {Γ} [Inhabited Γ] (l : List Γ) :
   Turing.Tape.move .right (Turing.Tape.mk₁ (default :: l)) = Turing.Tape.mk₁ l := by
diff --git a/Complexity/While.lean b/Complexity/While.lean
index 67dd28d..a056866 100644
--- a/Complexity/While.lean
+++ b/Complexity/While.lean
@@ -139,21 +139,48 @@ theorem Routines.while.semantics {k : ℕ} {Q Γ : Type*}
   convert congr_arg (tm_while.transition.step) ht using 1
   exact Function.iterate_succ_apply' _ _ _
 
-def TM.iterate {k : ℕ} {Q Γ}
+-- Semantics of Routines.while in terms of `eval.`.
+-- Note that this only works for Turing machines that always halt
+-- on the sequence of iterated inputs.
+@[simp]
+theorem Routines.while.eval' {k : ℕ} {Q Γ : Type*}
   [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q]
-  (tm : TM k Q Γ) (tapes : Part (Fin k → Turing.Tape Γ)) : Part (Fin k → Turing.Tape Γ) :=
-  tapes.bind tm.eval
+  {condition : Γ → Bool} {tm : TM k.succ Q Γ}
+  (tapes_seq : ℕ → (Fin k.succ → (Turing.Tape Γ)))
+  (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) :
+  (Routines.while condition tm).eval (tapes_seq 0) =
+    (PartENat.find
+      fun i => ¬condition (((tapes_seq i) 0).head)
+    ).map tapes_seq := by
+  by_cases h_halts: ∃ i, ¬condition ((tapes_seq i) 0).head
+  · convert TM.eval_of_transforms (Routines.while.semantics condition tm tapes_seq
+      (by intro i; exact TM.transforms_of_eval (h_inner i))
+      (by convert h_halts))
+    rw [Part.eq_some_iff]
+    obtain ⟨i, h_halts⟩ := h_halts
+    use ⟨i, by simp [h_halts]⟩
+    simp
+  · have h_no_halts : (PartENat.find fun i => ¬condition (tapes_seq i 0).head) = Part.none := by
+      sorry
+    sorry
+    -- rw [h_no_halts]
+    -- simp
+    -- rw [Part.eq_none_iff']
+    -- simp [TM.eval, PartENat.find]
+    -- by_contra h_does_halt
+    -- simp at h_does_halt
+    -- obtain ⟨t, h_does_halt⟩ := h_does_halt
+    -- simp at h_halts
+    -- sorry
 
--- @[simp]
--- theorem Routines.while.eval {k : ℕ} {Q Γ : Type*}
---   [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q]
---   {condition : Γ → Bool} {tm : TM k.succ Q Γ}
---   {tapes₀ : Fin k.succ → Turing.Tape Γ} :
---   (Routines.while condition tm).eval tapes₀ =
---     (PartENat.find (fun i =>
---       ((tm.iterate^[i] (.some tapes₀)).map
---         (fun tapes' : Fin k.succ → (Turing.Tape Γ) =>
---           condition (tapes' 0).head)) = Part.some true
---         )).map
---     fun i => (tm.iterate^[i] (.some tapes₀)) := by
---   sorry
+theorem Routines.while.eval {k : ℕ} {Q Γ : Type*}
+  [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q]
+  {condition : Γ → Bool} {tm : TM k.succ Q Γ}
+  (semantics : (Fin k.succ → (Turing.Tape Γ)) → (Fin k.succ → (Turing.Tape Γ)))
+  (h_inner : ∀ tapes, tm.eval tapes = .some (semantics tapes))
+  (tapes : Fin k.succ → Turing.Tape Γ) :
+  (Routines.while condition tm).eval tapes =
+    (PartENat.find
+      fun i => ¬condition (((semantics^[i] tapes) 0).head)
+    ).map (semantics^[·] tapes) := by
+  sorry