diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index 72daf7d43..f10cb4330 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -433,7 +433,7 @@ Inductive step_term:
    Lab_name fname bname = (case alookup table idx of Some lab => lab | None => default)
    ⇒
    step_term prog s
-     (Switch e table default)
+     (Switch e table default) Tau
      (s with bp := Lab_name fname bname)) ∧
 
   (∀prog s e labs i idx idx_size.
@@ -441,7 +441,7 @@ Inductive step_term:
    idx < length labs
    ⇒
    step_term prog s
-     (Iswitch e labs)
+     (Iswitch e labs) Tau
      (s with bp := el i labs)) ∧
 
   (∀prog s v fname bname es t ret1 ret2 vals f.
@@ -450,7 +450,7 @@ Inductive step_term:
    list_rel (eval_exp s) es vals
    ⇒
    step_term prog s
-     (Call v (Lab_name fname bname) es t ret1 ret2)
+     (Call v (Lab_name fname bname) es t ret1 ret2) Tau
      <| bp := Lab_name fname bname;
         glob_addrs := s.glob_addrs;
         locals := alist_to_fmap (zip (f.params, vals));
@@ -466,7 +466,7 @@ Inductive step_term:
    s.stack = top::rest
    ⇒
    step_term prog s
-     (Return e)
+     (Return e) Tau
      <| bp := top.ret;
         glob_addrs := s.glob_addrs;
         locals := top.saved_locals |+ (top.ret_var, r);
@@ -476,7 +476,7 @@ Inductive step_term:
   (∀prog s e i size.
    eval_exp s e (FlatV (IntV i size))
    ⇒
-   step_term prog s (Exit e) (s with status := Complete i))
+   step_term prog s (Exit e) (Exit i) (s with status := Complete i))
   (* TODO Throw *)
 
 End
@@ -485,22 +485,26 @@ End
  * instruction pointer and do a big-step evaluation for each block *)
 Inductive step_block:
 
-  (∀prog s1 t s2.
-   step_term prog s1 t s2
+  (∀prog s1 t l s2.
+   step_term prog s1 t l s2
    ⇒
-   step_block prog s1 [] [] t s2) ∧
+   step_block prog s1 [] t [l] s2) ∧
 
-  (∀prog s1 i1 i2 l1 is t s2.
-   step_inst s1 i1 l1 s2 ∧
-   (¬?l2 s3. step_inst s2 i2 l2 s3)
+  (∀prog s1 t.
+   ¬(∃s2 (l:var obs). step_term prog s1 t l s2)
    ⇒
-   step_block prog s1 (i1::i2::is) [l1] t (s2 with status := Stuck)) ∧
+   step_block prog s1 [] t [Error] (s1 with status := Stuck)) ∧
+
+  (∀prog s1 i1 is t.
+   (¬∃l s2. step_inst s1 i1 l s2)
+   ⇒
+   step_block prog s1 (i1::is) t [Error] (s1 with status := Stuck)) ∧
 
   (∀prog s1 i l is ls t s2 s3.
    step_inst s1 i l s2 ∧
-   step_block prog s2 is ls t s3
+   step_block prog s2 is t ls s3
    ⇒
-   step_block prog s1 (i::is) (l::ls) t s3)
+   step_block prog s1 (i::is) t (l::ls) s3)
 
 End
 
@@ -516,7 +520,7 @@ End
 Inductive step:
   ∀prog s b ls s'.
     get_block prog s.bp b ∧
-    step_block prog s b.cmnd ls b.term s' ∧
+    step_block prog s b.cmnd b.term ls s' ∧
     s.status = Partial
     ⇒
     step prog s ls s'
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index ffe8ac3e0..9d5624da4 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -197,7 +197,7 @@ Datatype:
        locals : reg |-> pv;
        stack : frame list;
        heap : bool heap;
-       exited : int option |>
+       status : trace_type |>
 End
 
 (* ----- Things about types ----- *)
@@ -513,7 +513,8 @@ Inductive step_instr:
           globals := s.globals;
           locals := fr.saved_locals;
           stack := st;
-          heap := new_h |>)) ∧
+          heap := new_h;
+          status := s.status |>)) ∧
 
   (eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
    l = Some (if tf = 0w then l2 else l1)
@@ -529,8 +530,8 @@ Inductive step_instr:
   signed_v_to_int v1.value = Some exit_code
    ⇒
    step_instr prog s
-     (Exit a) Tau
-     (s with exited := Some (exit_code))) ∧
+     (Exit a) (Exit exit_code)
+     (s with status := Complete exit_code)) ∧
 
   (eval s a1 = Some v1 ∧
    eval s a2 = Some v2 ∧
@@ -651,7 +652,8 @@ Inductive step_instr:
              saved_locals := s.locals;
              result_var := r;
              stack_allocs := [] |> :: s.stack;
-        heap := s.heap |>)(* ∧
+        heap := s.heap;
+        status := s.status |>)(* ∧
 
   (* TODO *)
   (step_instr prog s (Cxa_allocate_exn r a) Tau s) ∧
@@ -685,7 +687,6 @@ End
 
 Inductive step:
  (get_instr p s.ip (Inl i) ∧
-  s.exited = None ∧
   step_instr p s i l s'
   ⇒
   step p s l s') ∧
@@ -702,21 +703,20 @@ Inductive step:
  * %r1 = phi [0, %l]
  *)
  (get_instr p s.ip (Inr (from_l, phis)) ∧
-  s.exited = None ∧
   map (do_phi from_l s) phis = map Some updates
   ⇒
   step p s Tau (inc_pc (s with locals := locals |++ updates)))
-
 End
 
-Definition get_observation_def:
-  get_observation prog last_s =
-    if last_s.exited ≠ None then
-      Complete (THE last_s.exited)
-    else if ∃s l. step prog last_s l s then
-      Partial
-    else
-      Stuck
+Inductive sem_step:
+  (step p s1 l s2 ∧
+   s1.status = Partial
+   ⇒
+   sem_step p s1 l s2) ∧
+  ((¬∃l s2. step p s1 l s2) ∧
+   s1.status = Partial
+   ⇒
+   sem_step p s1 Error (s1 with status := Stuck))
 End
 
 (* The semantics of a program will be the finite traces of stores to global
@@ -724,8 +724,8 @@ End
  * *)
 Definition sem_def:
   sem p s1 =
-    { (get_observation p (last path), filter ($≠ Tau) l)  | (path, l) |
-      toList (labels path) = Some l ∧ finite path ∧ okpath (step p) path ∧ first path = s1 }
+    { ((last path).status, filter ($≠ Tau) l)  | (path, l) |
+      toList (labels path) = Some l ∧ finite path ∧ okpath (sem_step p) path ∧ first path = s1 }
 End
 
 (* ----- Invariants on state ----- *)
@@ -756,14 +756,15 @@ End
 Definition prog_ok_def:
   prog_ok p ⇔
     ((* All blocks end with terminators and terminators only appear at the end.
-      * All labels mentioned in instructions actually exist *)
+      * All labels mentioned in branches actually exist, and target non-entry
+      * blocks *)
      ∀fname dec bname block.
        alookup p fname = Some dec ∧
        alookup dec.blocks bname = Some block
        ⇒
        block.body ≠ [] ∧ terminator (last block.body) ∧
        every (λi. ¬terminator i) (front block.body) ∧
-       every (λlab. alookup dec.blocks (Some lab) ≠ None)
+       every (λlab. ∃b. alookup dec.blocks (Some lab) = Some b ∧ b.h ≠ Entry)
              (instr_to_labs (last block.body)) ∧
        (∀phis lands. block.h = Head phis lands ⇒
          every (λx. case x of Phi _ _ l => every (λ(lab, _). alookup dec.blocks lab ≠ None) l) phis)) ∧
@@ -809,7 +810,7 @@ Definition is_init_state_def:
     s.ip.i = Offset 0 ∧
     s.locals = fempty ∧
     s.stack = [] ∧
-    s.exited = None ∧
+    s.status = Partial ∧
     globals_ok s ∧
     heap_ok s.heap ∧
     fdom s.globals = fdom global_init ∧
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 6ba346fb1..14950149c 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -498,11 +498,13 @@ Proof
   >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac [])
 QED
 
+(* TODO: remove
 Theorem exit_no_step:
   !p s1. s1.exited ≠ None ⇒ ¬?l s2. step p s1 l s2
 Proof
   rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``]
 QED
+*)
 
 Definition is_call_def:
   (is_call (Call _ _ _ _) ⇔ T) ∧
@@ -534,30 +536,33 @@ Proof
   >- rw [stack_ok_def]
 QED
 
-
 (* ----- A bigger-step semantics ----- *)
 
-Definition last_step_def:
-  last_step p s1 l s2 ⇔
-   ∃i.
-     step p s1 l s2 ∧ get_instr p s1.ip i ∧
-     ((∃x. i = Inr x) ∨
-      (∃i'. i = Inl i' ∧ (terminator i' ∨ is_call i')) ∨
-      ¬∃l s3. step p s2 l s3)
+Inductive last_step:
+  (∀p s1 l s2 i.
+    step p s1 l s2 ∧ get_instr p s1.ip i ∧
+    ((∃x. i = Inr x) ∨ (∃i'. i = Inl i' ∧ (terminator i' ∨ is_call i')))
+    ⇒
+    last_step p s1 l s2) ∧
+  (∀p s1.
+   (¬∃l s2. step p s1 l s2)
+   ⇒
+   last_step p s1 Error (s1 with status := Stuck))
 End
 
 (* Run all of the instructions up-to-and-including the next Call or terminator.
  * Stop after the phis too.
  * *)
 Inductive multi_step:
-
   (∀p s1 s2 l.
-   last_step p s1 l s2
+   last_step p s1 l s2 ∧
+   s1.status = Partial
    ⇒
    multi_step p s1 [l] s2) ∧
 
   (∀p s1 s2 s3 i l ls.
    step p s1 l s2 ∧
+   s1.status = Partial ∧
    get_instr p s1.ip (Inl i) ∧
    ¬(terminator i ∨ is_call i) ∧
    multi_step p s2 ls s3
@@ -567,7 +572,7 @@ End
 
 Definition multi_step_sem_def:
   multi_step_sem p s1 =
-    { l1 | ∃path l2. l1 ∈ observation_prefixes (get_observation p (last path), flat l2) ∧
+    { l1 | ∃path l2. l1 ∈ observation_prefixes ((last path).status, flat l2) ∧
            toList (labels path) = Some l2 ∧
            finite path ∧ okpath (multi_step p) path ∧ first path = s1 }
 End
@@ -576,15 +581,15 @@ Theorem multi_step_to_step_path:
   ∀p s1 l s2.
     multi_step p s1 l s2 ⇒
       ∃path.
-        finite path ∧ okpath (step p) path ∧ first path = s1 ∧ last path = s2 ∧
+        finite path ∧ okpath (sem_step p) path ∧ first path = s1 ∧ last path = s2 ∧
         toList (labels path) = Some l
 Proof
   ho_match_mp_tac multi_step_ind >> conj_tac
-  >- (rw [] >> qexists_tac `pcons s1 l (stopped_at s2)` >> fs [toList_THM, last_step_def]) >>
+  >- (rw [] >> qexists_tac `pcons s1 l (stopped_at s2)` >> fs [sem_step_cases, toList_THM, last_step_cases]) >>
   rw [] >>
   qexists_tac `pcons s1 l path` >> rw [toList_THM] >>
   `LFINITE (labels path)` by metis_tac [finite_labels] >>
-  drule LFINITE_toList >> rw [] >> rw []
+  simp [sem_step_cases]
 QED
 
 Theorem expand_multi_step_path:
@@ -592,7 +597,7 @@ Theorem expand_multi_step_path:
     !l. toList (labels path) = Some l ⇒
     ∃path'.
       toList (labels path') = Some (flat l) ∧ finite path' ∧
-      okpath (step prog) path' ∧ first path' = first path ∧ last path' = last path
+      okpath (sem_step prog) path' ∧ first path' = first path ∧ last path' = last path
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw []
   >- (qexists_tac `stopped_at x` >> fs [toList_THM] >> rw []) >>
@@ -606,8 +611,10 @@ Proof
 QED
 
 Theorem contract_step_path:
-  ∀path. okpath (step prog) path ∧ finite path ⇒
-    ∀l1 l s. last_step prog (last path) l s ∧
+  ∀path. okpath (sem_step prog) path ∧ finite path ⇒
+    ∀l1 l s.
+      last_step prog (last path) l s ∧
+      (last path).status = Partial ∧
       toList (labels path) = Some l1
     ⇒
     ∃path' l2.
@@ -626,19 +633,23 @@ Proof
   Cases_on `last_step prog x r (first path)`
   >- (
     qexists_tac `pcons x [r] path'` >> simp [] >>
-    simp [Once multi_step_cases, toList_THM])
+    fs [sem_step_cases] >>
+    simp [Once multi_step_cases, toList_THM] >>
+    simp [last_step_cases])
   >- (
     qpat_x_assum `okpath (multi_step _) _` mp_tac >>
     simp [Once okpath_cases] >> rw [] >> fs [toList_THM] >> rw [] >> fs [] >>
     qexists_tac `pcons x (r::r') p` >> fs [toList_THM] >> rw [Once multi_step_cases] >>
-    disj2_tac >> qexists_tac `first path` >> rw [] >> fs [last_step_def] >> rfs [] >>
-    fs [step_cases, get_instr_cases] >>
-    metis_tac [])
+    disj2_tac >> qexists_tac `first path` >> rw [] >> fs [sem_step_cases]
+    >- (fs [last_step_cases, step_cases, get_instr_cases] >> metis_tac []) >>
+    qpat_x_assum `okpath (sem_step _) _` mp_tac >>
+    simp [Once okpath_cases, sem_step_cases] >> CCONTR_TAC >> fs [] >> rw [] >>
+    fs [first_def, last_thm] >> rw [] >> fs [])
 QED
 
 Definition get_next_step_def:
   get_next_step p s1 =
-    some (s2, l). step p s1 l s2 ∧ ¬last_step p s1 l s2
+    some (s2, l). sem_step p s1 l s2 ∧ ¬last_step p s1 l s2
 End
 
 Triviality finite_plink_trivial:
@@ -660,12 +671,61 @@ Definition instrs_left_def:
         | Offset idx => length b.body - idx
 End
 
+Theorem sem_step_stuck:
+  ∀p s1. (∀l s2. ¬sem_step p s1 l s2) ⇔ s1.status ≠ Partial
+Proof
+  rw [sem_step_cases] >> metis_tac []
+QED
+
+Theorem sem_step_then_stuck:
+  ∀p s1 l1 s2.
+    sem_step p s1 l1 s2 ∧ (∀l2 s3. ¬sem_step p s2 l2 s3)
+    ⇒
+    (l1 = Error ∧ s2 = s1 with status := Stuck ∧ ∀l2 s3. ¬step p s1 l2 s3) ∨
+    (∃i e. l1 = Exit i ∧ s2 = s1 with status := Complete i ∧
+      get_instr p s1.ip (Inl (Exit e)))
+Proof
+  rw [sem_step_stuck] >>
+  fs [sem_step_cases] >>
+  disj2_tac >> fs [step_cases] >> rfs [inc_pc_def] >>
+  fs [step_instr_cases] >> rfs [update_result_def, inc_pc_def] >>
+  metis_tac []
+QED
+
+Theorem sem_step_not_last:
+  ∀p s1 l1 s2.
+    sem_step p s1 l1 s2 ∧ ¬last_step p s1 l1 s2 ⇒
+    ∃l2 s3. sem_step p s2 l2 s3
+Proof
+  rw [] >> CCONTR_TAC >> fs [] >> drule sem_step_then_stuck >>
+  simp [] >>
+  CCONTR_TAC >> fs [] >> rw []
+  >- fs [last_step_cases] >>
+  fs [last_step_cases, sem_step_cases] >> rw [] >>
+  first_x_assum (qspec_then `Inl (Exit e)` mp_tac) >>
+  rw [terminator_def]
+QED
+
+Triviality some_lemma:
+  ∀P a b. (some (x, y). P x y) = Some (a, b) ⇒ P a b
+Proof
+  rw [optionTheory.some_def] >>
+  qmatch_assum_abbrev_tac `(@x. Q x) = _` >>
+  `Q (@x. Q x)` suffices_by (rw [Abbr `Q`]) >>
+  `?x. Q x` suffices_by rw [SELECT_THM] >>
+  unabbrev_all_tac >> rw [] >>
+  pairarg_tac >> fs [] >> rw [EXISTS_PROD] >>
+  metis_tac []
+QED
+
 Theorem extend_step_path:
   ∀path.
-    okpath (step p) path ∧ finite path
+    okpath (sem_step p) path ∧ finite path
     ⇒
-    (∀s. path = stopped_at s ⇒ ∃s' l. step p s l s') ⇒
-    ?path' l s n. finite path' ∧ okpath (step p) path' ∧ last_step p (last path') l s ∧
+    (∀s. path = stopped_at s ⇒ ∃s' l. sem_step p s l s') ⇒
+    ∃path' l s n.
+      finite path' ∧ okpath (sem_step p) path' ∧ (last path').status = Partial ∧
+      last_step p (last path') l s ∧
       length path = Some (Suc n) ∧ n ∈ PL (pconcat path' l (stopped_at s)) ∧
       path = take n (pconcat path' l (stopped_at s))
 Proof
@@ -673,8 +733,8 @@ Proof
   Cases_on `get_next_step p (last path) = None ∧ ∀s. path ≠ stopped_at s`
   >- (
     fs [get_next_step_def, optionTheory.some_def, FORALL_PROD, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
-    Cases_on `?l2 s2. step p (last path) l2 s2` >> fs []
-    >- (
+    Cases_on `∃l2 s2. sem_step p (last path) l2 s2` >> fs []
+    >- ( (* Can take a last step from the end of the path *)
       first_x_assum drule >> rw [] >>
       qexists_tac `path` >> qexists_tac `l2` >> qexists_tac `s2` >> rw [] >>
       fs [finite_length] >>
@@ -684,21 +744,21 @@ Proof
       `length (pconcat path l2 (stopped_at s2)) = Some (n + 1)`
       by metis_tac [length_pconcat, alt_length_thm] >>
       rw [take_pconcat]
+      >- fs [sem_step_cases]
       >- metis_tac [take_all] >>
       fs [PL_def] >> rfs [])
-    >- (
+    >- ( (* The path is stuck, so we need to extract the last step from it *)
       drule finite_path_end_cases >>
       rw [] >> fs [] >> rfs [] >>
       qexists_tac `p'` >> rw [] >>
       qexists_tac `l` >> qexists_tac `s` >> rw [] >>
       fs [finite_length] >>
-      qexists_tac `n` >> rw []
-      >- (
-        qpat_x_assum `step _ _ _ _` mp_tac >>
-        rw [last_step_def, step_cases] >> metis_tac []) >>
+      qexists_tac `n` >> rw [] >>
       `length (plink p' (pcons (last p') l (stopped_at s))) = Some (n + Suc 1 - 1)`
       by metis_tac [length_plink, alt_length_thm, optionTheory.OPTION_MAP_DEF] >>
       rw []
+      >- fs [sem_step_cases]
+      >- metis_tac [sem_step_not_last]
       >- (
         rw [PL_def] >> fs [finite_length] >>
         `length (pconcat p' l (stopped_at s)) = Some (n + 1)`
@@ -718,19 +778,21 @@ Proof
     simp [Abbr `path1`] >> irule unfold_finite >>
     WF_REL_TAC `measure (instrs_left p)` >>
     rpt gen_tac >>
-    simp [instrs_left_def, get_next_step_def, optionTheory.some_def, EXISTS_PROD] >>
-    qmatch_goalsub_abbrev_tac `@x. P x` >> rw [] >>
-    `?x. P x` by (fs [Abbr `P`, EXISTS_PROD] >> metis_tac []) >>
-    `P (@x. P x)` by metis_tac [SELECT_THM] >>
-    qunabbrev_tac `P` >> pop_assum mp_tac >> simp [] >>
-    simp [last_step_def] >> rw [] >>
-    pop_assum mp_tac >> simp [] >>
-    `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
-    disch_then (qspec_then `i` mp_tac) >> simp [] >>
-    drule step_same_block >> disch_then drule >> simp [] >>
-    pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
-    rw [] >> fs [get_instr_cases, inc_bip_def] >> rw [] >> fs [] >>
-    rw [inc_bip_def] >> fs []) >>
+    rw [instrs_left_def, get_next_step_def] >>
+    qabbrev_tac `P = (\s3 l. sem_step p s2 l s3 ∧ ¬last_step p s2 l s3)` >>
+    `P s3 l` by (irule some_lemma >> simp [Abbr `P`]) >>
+    pop_assum mp_tac >> simp [Abbr `P`] >> strip_tac >>
+    drule sem_step_not_last >> simp [] >> strip_tac >>
+    qpat_x_assum `sem_step p s2 l s3` mp_tac >> rw [Once sem_step_cases]
+    >- (
+      `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
+      `?x. i = Inl x` by (fs [last_step_cases] >> metis_tac [sumTheory.sum_CASES]) >>
+      drule step_same_block >> disch_then drule >> simp [] >>
+      impl_tac
+      >- (fs [last_step_cases] >> metis_tac []) >>
+      fs [step_cases, get_instr_cases, inc_bip_def] >> rw [] >> fs [] >>
+      rw [inc_bip_def] >> fs [])
+    >- fs [last_step_cases]) >>
  `last path = first path1`
   by (
     unabbrev_all_tac >> simp [Once unfold_thm] >>
@@ -741,68 +803,63 @@ Proof
     unabbrev_all_tac >>
     irule okpath_unfold >> rw [] >>
     qexists_tac `\x.T` >> rw [get_next_step_def] >>
-    fs [optionTheory.some_def] >>
-    pairarg_tac >> fs [] >>
-    qmatch_assum_abbrev_tac `(@x. P x) = _` >>
-    `P (@x. P x)`
-    by (
-      simp [SELECT_THM] >>
-      unabbrev_all_tac >> fs [EXISTS_PROD] >>
-      metis_tac []) >>
-    rfs [] >>
-    unabbrev_all_tac >> fs []) >>
+    qabbrev_tac `P = (\s2 l. sem_step p s l s2 ∧ ¬last_step p s l s2)` >>
+    `P s' l` by (irule some_lemma >> simp [Abbr `P`]) >>
+    pop_assum mp_tac >> simp [Abbr `P`]) >>
   `?n. length path1 = Some n` by fs [finite_length] >>
   `n ≠ 0` by metis_tac [length_never_zero] >>
   `length (plink path path1) = Some (Suc m + n - 1)` by metis_tac [length_plink] >>
   simp [take_pconcat, PL_def, finite_pconcat, length_plink] >>
   `!l s. length (pconcat (plink path path1) l (stopped_at s)) = Some ((Suc m + n − 1) + 1)`
   by metis_tac [length_pconcat, alt_length_thm] >>
-  rw [GSYM PULL_EXISTS]
+  simp [GSYM PULL_EXISTS] >>
+  unabbrev_all_tac >> drule unfold_last >>
+  qmatch_goalsub_abbrev_tac `last_step _ (last path1) _ _` >>
+  simp [Once get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
+  strip_tac >>
+  simp [CONJ_ASSOC, Once CONJ_SYM] >>
+  simp [GSYM CONJ_ASSOC] >>
+  conj_tac
   >- (
-    unabbrev_all_tac >> drule unfold_last >>
-    qmatch_goalsub_abbrev_tac `last_step _ (last path1) _ _` >>
-    simp [get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
-    rw [METIS_PROVE [] ``~x ∨ y ⇔ (~y ⇒ ~x)``] >> CCONTR_TAC >>
-    Cases_on `1 ∈ PL path1`
-    >- (
-      fs [] >> pairarg_tac >> fs [] >> rw [] >>
-      qmatch_assum_abbrev_tac `(@x. P x) = _` >>
-      `P (@x. P x)`
-      by (
-        simp [SELECT_THM] >>
-        unabbrev_all_tac >> fs [EXISTS_PROD] >>
-        metis_tac []) >>
-      fs [Abbr `P`] >> pairarg_tac >> fs [] >> rw [] >>
-      fs [last_step_def] >> rfs  [] >>
-      `?i. get_instr p x.ip i` by (fs [step_cases] >> metis_tac []) >>
-      metis_tac []) >>
-    `n = 1` by (rfs [PL_def, finite_length] >> decide_tac) >> rw [] >>
+    rw [take_plink]
+    >- (imp_res_tac take_all >> fs []) >>
+    metis_tac [finite_plink_trivial]) >>
+  pop_assum mp_tac >>
+  Cases_on `1 ∈ PL path1` >> simp []
+  >- (
+    simp [get_next_step_def] >> strip_tac >>
+    qabbrev_tac `P = (\s2 l. sem_step p x l s2 ∧ ¬last_step p x l s2)` >>
+    `P (last path1) l` by (irule some_lemma >> simp [Abbr `P`]) >>
+    pop_assum mp_tac >> simp [Abbr `P`] >>
+    strip_tac >>
+    drule sem_step_not_last >> rw []
+    >- fs [sem_step_cases] >>
+    metis_tac [])
+  >- (
+    `n = 1` by (rfs [PL_def, finite_length] >> decide_tac) >>
     qspec_then `path1` strip_assume_tac path_cases
     >- (
-      unabbrev_all_tac >> fs [] >> rw [] >>
-      fs [Once unfold_thm] >>
+      unabbrev_all_tac >> simp [] >>
+      fs [] >> fs [Once unfold_thm] >>
       Cases_on `get_next_step p (last path)` >> simp [] >> fs [] >> rw [] >>
       fs [get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
-      split_pair_case_tac >> fs []) >>
-    fs [alt_length_thm, length_never_zero])
-  >- (
-    rw [take_plink]
-    >-  (imp_res_tac take_all >> fs []) >>
-    metis_tac [finite_plink_trivial])
+      TRY split_pair_case_tac >> fs [sem_step_cases] >>
+      metis_tac [])
+    >- fs [alt_length_thm, length_never_zero])
 QED
 
 Theorem find_path_prefix:
   ∀path.
-     okpath (step p) path ∧ finite path
+     okpath (sem_step p) path ∧ finite path
     ⇒
     !obs l1. toList (labels path) = Some l1 ∧
-    obs ∈ observation_prefixes (get_observation p (last path), l1)
+    obs ∈ observation_prefixes ((last path).status, l1)
     ⇒
     ∃n l2. n ∈ PL path ∧ toList (labels (take n path)) = Some l2 ∧
-      obs = (get_observation p (last (take n path)), filter ($≠ Tau) l2)
+      obs = ((last (take n path)).status, filter ($≠ Tau) l2)
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw [toList_THM]
-  >- fs [observation_prefixes_cases, get_observation_def, IN_DEF] >>
+  >- fs [observation_prefixes_cases, IN_DEF] >>
   `?s ls. obs = (s, ls)` by metis_tac [pairTheory.pair_CASES] >>
   fs [] >>
   `∃l. length path = Some l ∧ l ≠ 0` by metis_tac [finite_length, length_never_zero] >>
@@ -821,11 +878,11 @@ Proof
   rename1 `short_l ≼ first_l::long_l` >>
   Cases_on `short_l` >> fs []
   >- (
-    qexists_tac `0` >> rw [toList_THM, get_observation_def] >>
-    metis_tac [exit_no_step]) >>
+    qexists_tac `0` >> rw [toList_THM] >>
+    fs [sem_step_cases]) >>
   rename1 `short_l ≼ long_l` >>
   rfs [] >>
-  `(Partial, filter ($≠ Tau) short_l) ∈ observation_prefixes (get_observation p (last path),long_l)`
+  `(Partial, filter ($≠ Tau) short_l) ∈ observation_prefixes ((last path).status,long_l)`
   by (simp [observation_prefixes_cases, IN_DEF] >> metis_tac []) >>
   first_x_assum drule >> strip_tac >>
   qexists_tac `Suc n` >> simp [toList_THM] >> rw [] >> rfs [last_take]
@@ -839,7 +896,7 @@ Proof
 QED
 
 Theorem big_sem_equiv:
-  !p s1. multi_step_sem p s1 = sem p s1
+  ∀p s1. multi_step_sem p s1 = sem p s1
 Proof
   rw [multi_step_sem_def, sem_def, EXTENSION] >> eq_tac >> rw []
   >- (
@@ -848,15 +905,16 @@ Proof
     `?n short_l.
       n ∈ PL s_path ∧
       toList (labels (take n s_path)) = Some short_l ∧
-      x = (get_observation p (last (take n s_path)), filter ($≠ Tau) short_l)`
+      x = ((last (take n s_path)).status, filter ($≠ Tau) short_l)`
     by metis_tac [find_path_prefix] >>
     qexists_tac `take n s_path` >> rw [])
   >- (
-    Cases_on `¬∀s. path = stopped_at s ⇒ ∃s' l. step p s l s'`
+    Cases_on `¬∀s. path = stopped_at s ⇒ ∃s' l. sem_step p s l s'`
     >- (
       fs [] >> rw [] >> fs [toList_THM] >> rw [] >>
       qexists_tac `stopped_at s` >> rw [toList_THM] >>
-      rw [observation_prefixes_cases, IN_DEF, get_observation_def]) >>
+      rw [observation_prefixes_cases, IN_DEF] >>
+      metis_tac [trace_type_nchotomy]) >>
     drule extend_step_path >> disch_then drule >>
     impl_tac >> rw []
     >- metis_tac [] >>
@@ -877,7 +935,7 @@ Proof
       rw [observation_prefixes_cases, IN_DEF] >> rw [] >>
       unabbrev_all_tac >> rw [last_pconcat] >> fs [] >>
       drule toList_LAPPEND_APPEND >> rw [toList_THM] >>
-      Cases_on `get_observation p (last m_path)` >> simp [] >>
+      Cases_on `(last m_path).status` >> simp [] >>
       qexists_tac `s_ext_l ++ [last_l]` >> rw []) >>
     fs [PL_def, finite_pconcat] >> rfs [] >>
     `?m. length s_ext_path = Some m` by metis_tac [finite_length] >>
@@ -887,7 +945,7 @@ Proof
     fs [] >>
     `n < m` by decide_tac >> fs [] >> rw [] >>
     `n ∈ PL s_ext_path` by rw [PL_def] >>
-    Cases_on `get_observation p (last orig_path) = Partial`
+    Cases_on `(last orig_path).status = Partial`
     >- (
       rw [observation_prefixes_cases, IN_DEF] >> rw [] >>
       unabbrev_all_tac >> fs [] >>
@@ -901,16 +959,14 @@ Proof
         fs [ltake_fromList2] >>
         rw [take_is_prefix])
       >- (drule LTAKE_LENGTH >> rw [])) >>
-    `¬∃l s. step p (last orig_path) l s`
-    by (fs [get_observation_def] >> BasicProvers.EVERY_CASE_TAC >> fs [] >> metis_tac [exit_no_step]) >>
     unabbrev_all_tac >> rfs [last_take] >>
     fs [okpath_pointwise] >>
     Cases_on `Suc n ∈ PL s_ext_path` >> rw []
-    >- (last_x_assum (qspec_then `n` mp_tac) >> rw []) >>
+    >- (last_x_assum (qspec_then `n` mp_tac) >> rw [sem_step_cases]) >>
     `n = m - 1` by (fs [PL_def] >> rfs []) >>
     rw [] >>
     `el (m - 1) s_ext_path = last s_ext_path` by metis_tac [take_all, pathTheory.last_take] >>
-    fs [last_step_def])
+    fs [last_step_cases])
 QED
 
 export_theory ();
diff --git a/sledge/semantics/llvm_ssaScript.sml b/sledge/semantics/llvm_ssaScript.sml
index 55c735939..414e5646f 100644
--- a/sledge/semantics/llvm_ssaScript.sml
+++ b/sledge/semantics/llvm_ssaScript.sml
@@ -151,6 +151,7 @@ Definition instr_uses_def:
   (instr_uses (Invoke _ _ a targs _ _) =
     arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
   (instr_uses Unreachable = {}) ∧
+  (instr_uses (Exit a) = arg_to_regs a) ∧
   (instr_uses (Sub _ _ _ _ a1 a2) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
   (instr_uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index d37975f88..fb6e335ae 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -187,8 +187,10 @@ End
 
 (* TODO *)
 Definition translate_instr_to_term_def:
-  translate_instr_to_term f emap (Br a l1 l2) =
-    Switch (translate_arg emap a) [(0, translate_label f l2)] (translate_label f l1)
+  (translate_instr_to_term f emap (Br a l1 l2) =
+    Switch (translate_arg emap a) [(0, translate_label f l2)] (translate_label f l1)) ∧
+  (translate_instr_to_term f emap (Exit a) =
+    Exit (translate_arg emap a))
 End
 
 Datatype:
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
index a8759aab7..5f4f69ca5 100644
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -44,7 +44,7 @@ End
 Inductive pc_rel:
  (* LLVM side points to a normal instruction *)
  (∀prog emap ip bp d b idx b' prev_i fname.
-    (* Both are valid pointers to blocks n the same function *)
+    (* Both are valid pointers to blocks in the same function *)
     dest_fn ip.f = fst (dest_llair_lab bp) ∧
     alookup prog ip.f = Some d ∧
     alookup d.blocks ip.b = Some b ∧
@@ -74,12 +74,6 @@ Definition untranslate_reg_def:
   untranslate_reg (Var_name x t) = Reg x
 End
 
-Inductive complete_trace_rel:
-  (∀i. complete_trace_rel (Some i) (Complete i)) ∧
-  (complete_trace_rel None Partial) ∧
-  (complete_trace_rel None Stuck)
-End
-
 (* Define when an LLVM state is related to a llair one.
  * Parameterised on a map for locals relating LLVM registers to llair
  * expressions that compute the value in that register. This corresponds to part
@@ -100,7 +94,7 @@ Definition mem_state_rel_def:
           ∃ip2. untranslate_reg r' ∈ assigns prog ip2 ∧ dominates prog ip2 ip1))) ∧
     reachable prog s.ip ∧
     erase_tags s.heap = s'.heap ∧
-    complete_trace_rel s.exited s'.status
+    s.status = s'.status
 End
 
 (* Define when an LLVM state is related to a llair one
@@ -110,12 +104,11 @@ End
  *)
 Definition state_rel_def:
   state_rel prog emap (s:llvm$state) (s':llair$state) ⇔
-    pc_rel prog emap s.ip s'.bp ∧
-    mem_state_rel prog emap s s' ∧
-    s'.status = get_observation prog s
+    (s.status = Partial ⇒ pc_rel prog emap s.ip s'.bp) ∧
+    mem_state_rel prog emap s s'
 End
 
-Theorem mem_state_ignore_bp:
+Theorem mem_state_ignore_bp[simp]:
   ∀prog emap s s' b. mem_state_rel prog emap s (s' with bp := b) ⇔ mem_state_rel prog emap s s'
 Proof
   rw [mem_state_rel_def] >> eq_tac >> rw [] >>
@@ -125,6 +118,22 @@ Proof
   metis_tac []
 QED
 
+Triviality lemma:
+  ((s:llair$state) with status := Complete code).locals = s.locals
+Proof
+  rw []
+QED
+
+Theorem mem_state_rel_exited:
+  ∀prog emap s s' code.
+    mem_state_rel prog emap s s'
+    ⇒
+    mem_state_rel prog emap (s with status := Complete code) (s' with status := Complete code)
+Proof
+  rw [mem_state_rel_def] >>
+  metis_tac [eval_exp_ignores, lemma]
+QED
+
 Theorem mem_state_rel_no_update:
   ∀prog emap s1 s1' v res_v r i i'.
   assigns prog s1.ip = {} ∧
@@ -723,7 +732,9 @@ QED
 *)
 
 Definition translate_trace_def:
-  (translate_trace types Tau = Tau ) ∧
+  (translate_trace types Tau = Tau) ∧
+  (translate_trace types Error = Error) ∧
+  (translate_trace types (Exit i) = (Exit i)) ∧
   (translate_trace types (W gv bytes) = W (translate_glob_var gv (types gv)) bytes)
 End
 
@@ -732,7 +743,9 @@ Definition untranslate_glob_var_def:
 End
 
 Definition untranslate_trace_def:
-  (untranslate_trace Tau = Tau ) ∧
+  (untranslate_trace Tau = Tau) ∧
+  (untranslate_trace Error = Error) ∧
+  (untranslate_trace (Exit i) = (Exit i)) ∧
   (untranslate_trace (W gv bytes) = W (untranslate_glob_var gv) bytes)
 End
 
@@ -763,9 +776,8 @@ QED
 Theorem translate_instrs_correct1:
   ∀prog s1 tr s2.
     multi_step prog s1 tr s2 ⇒
-    !s1' b' emap regs_to_keep d b types idx.
-      prog_ok prog ∧
-      is_ssa prog ∧
+    ∀s1' b' emap regs_to_keep d b types idx.
+      prog_ok prog ∧ is_ssa prog ∧
       mem_state_rel prog emap s1 s1' ∧
       alookup prog s1.ip.f = Some d ∧
       alookup d.blocks s1.ip.b = Some b ∧
@@ -773,32 +785,55 @@ Theorem translate_instrs_correct1:
       b' = fst (translate_instrs (dest_fn s1.ip.f) emap regs_to_keep (take_to_call (drop idx b.body)))
       ⇒
       ∃emap s2' tr'.
-        step_block (translate_prog prog) s1' b'.cmnd tr' b'.term s2' ∧
+        step_block (translate_prog prog) s1' b'.cmnd b'.term tr' s2' ∧
         filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace types) tr)  ∧
         state_rel prog emap s2 s2'
 Proof
   ho_match_mp_tac multi_step_ind >> rw_tac std_ss []
   >- (
-    fs [last_step_def]
+    fs [last_step_cases]
     >- ( (* Phi (not handled here) *)
       fs [get_instr_cases])
     >- ( (* Terminator *)
-      `l = Tau`
+      `(∃code. l = Exit code) ∨ l = Tau `
       by (
         fs [llvmTheory.step_cases] >>
         `i' = i''` by metis_tac [get_instr_func, sumTheory.INL_11] >>
         fs [step_instr_cases] >> rfs [terminator_def]) >>
-      fs [get_instr_cases] >> rw [] >>
+      fs [get_instr_cases, translate_trace_def] >> rw [] >>
       `el idx b.body = el 0 (drop idx b.body)` by rw [EL_DROP] >>
       fs [] >>
-      Cases_on `drop idx b.body` >> fs [DROP_NIL] >> rw [] >>
+      Cases_on `drop idx b.body` >> fs [DROP_NIL] >> rw []
+      >- ( (* Exit *)
+        fs [llvmTheory.step_cases, get_instr_cases, step_instr_cases,
+            translate_instrs_def, take_to_call_def, classify_instr_def,
+            translate_instr_to_term_def, translate_instr_to_inst_def,
+            llvmTheory.get_obs_cases] >>
+        simp [Once step_block_cases, step_term_cases, PULL_EXISTS, step_inst_cases] >>
+        drule translate_arg_correct >>
+        disch_then drule >> impl_tac
+        >- (
+          `get_instr prog s1.ip (Inl (Exit a))` by rw [get_instr_cases] >>
+          drule get_instr_live >>
+          simp [uses_cases, SUBSET_DEF, IN_DEF, PULL_EXISTS] >>
+          rw [] >> first_x_assum irule >>
+          disj1_tac >>
+          metis_tac [instr_uses_def]) >>
+        rw [] >>
+        qexists_tac `emap` >>
+        qexists_tac `s1' with status := Complete code` >>
+        qexists_tac `[Exit code]` >>
+        rw []
+        >- (fs [v_rel_cases] >> fs [signed_v_to_int_def] >> metis_tac []) >>
+        rw [state_rel_def] >>
+        metis_tac [mem_state_rel_exited]) >>
       simp [take_to_call_def, translate_instrs_def] >>
       Cases_on `el idx b.body` >> fs [terminator_def, classify_instr_def, translate_trace_def] >> rw []
       >- ( (* Ret *)
         cheat)
       >- ( (* Br *)
         simp [translate_instr_to_term_def, Once step_block_cases] >>
-        simp [step_term_cases, PULL_EXISTS] >>
+        simp [step_term_cases, PULL_EXISTS, RIGHT_AND_OVER_OR, EXISTS_OR_THM] >>
         fs [llvmTheory.step_cases] >>
         drule get_instr_live >> disch_tac >>
         drule translate_arg_correct >>
@@ -838,40 +873,40 @@ Proof
           >- (
             qpat_x_assum `!r. r ∈ live _ _ ⇒ P r` mp_tac >>
             simp [Once live_gen_kill] >> disch_then (qspec_then `r` mp_tac) >>
-            impl_tac >> rw []
+            impl_tac >> rw [] >>
+            rw [PULL_EXISTS] >>
+            disj1_tac >>
+            qexists_tac `<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>` >>
+            rw [next_ips_cases, IN_DEF, assigns_cases]
             >- (
-              rw [PULL_EXISTS] >>
               disj1_tac >>
-              qexists_tac `<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>` >>
-              rw [next_ips_cases, IN_DEF, assigns_cases]
-              >- (
-                disj1_tac >>
-                qexists_tac `Br a l1 l2` >>
-                rw [instr_next_ips_def, Abbr `target`] >>
-                cheat) >>
-              CCONTR_TAC >> fs [] >>
-              imp_res_tac get_instr_func >> fs [] >> rw [] >>
-              fs [instr_assigns_def])
-            >- (
-              rpt HINT_EXISTS_TAC >> rw [] >>
-              qmatch_goalsub_abbrev_tac `eval_exp s3 _` >>
-              `s1'.locals = s3.locals` by fs [Abbr `s3`] >>
-              metis_tac [eval_exp_ignores]))
-          >- cheat
-          >- cheat)
-        >- (
-          cheat))
+              qexists_tac `Br a l1 l2` >>
+              rw [instr_next_ips_def, Abbr `target`] >>
+              fs [prog_ok_def, get_instr_cases] >>
+              last_x_assum drule >> disch_then drule >> rw [] >>
+              `last b.body = Br a l1 l2` by cheat >>
+              fs [instr_to_labs_def] >>
+              metis_tac [blockHeader_nchotomy]) >>
+            CCONTR_TAC >> fs [] >>
+            imp_res_tac get_instr_func >> fs [] >> rw [] >>
+            fs [instr_assigns_def])
+          >- cheat))
       >- ( (* Invoke *)
         cheat)
       >- ( (* Unreachable *)
         cheat)
       >- ( (* Exit *)
-        cheat)
+        fs [llvmTheory.step_cases, get_instr_cases, step_instr_cases])
       >- ( (* Throw *)
         cheat))
     >- ( (* Call *)
       cheat)
     >- ( (* Stuck *)
+      rw [translate_trace_def] >>
+      (* TODO: need to know that stuck LLVM instructions translate to stuck
+       * llair instructions. This will follow from knowing that when a llair
+       * instruction takes a step, the LLVM source can take the same step, ie,
+       * the backward direction of the proof. *)
       cheat))
   >- ( (* Middle of the block *)
     fs [llvmTheory.step_cases] >> TRY (fs [get_instr_cases] >> NO_TAC) >>
@@ -910,11 +945,12 @@ Theorem multi_step_to_step_block:
   ∀prog s1 tr s2 s1'.
     prog_ok prog ∧ is_ssa prog ∧
     multi_step prog s1 tr s2 ∧
+    s1.status = Partial ∧
     state_rel prog emap s1 s1'
     ⇒
     ∃s2' emap2 b tr'.
       get_block (translate_prog prog) s1'.bp b ∧
-      step_block (translate_prog prog) s1' b.cmnd tr' b.term s2' ∧
+      step_block (translate_prog prog) s1' b.cmnd b.term tr' s2' ∧
       filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace types) tr) ∧
       state_rel prog emap2 s2 s2'
 Proof
@@ -932,9 +968,11 @@ Proof
   reverse (fs [Once multi_step_cases])
   >- metis_tac [get_instr_func, sumTheory.sum_distinct] >>
   qpat_x_assum `last_step _ _ _ _` mp_tac >>
+  (*
   simp [last_step_def] >> simp [Once llvmTheory.step_cases] >>
   rw [] >> imp_res_tac get_instr_func >> fs [] >> rw [] >>
   fs [translate_trace_def] >>
+  *)
   (* TODO: unfinished *)
   cheat
 QED
@@ -943,7 +981,7 @@ Theorem step_block_to_multi_step:
   ∀prog s1 s1' tr s2' b.
     state_rel prog emap s1 s1' ∧
     get_block (translate_prog prog) s1'.bp b ∧
-    step_block (translate_prog prog) s1' b.cmnd tr b.term s2'
+    step_block (translate_prog prog) s1' b.cmnd b.term tr s2'
     ⇒
     ∃s2.
       multi_step prog s1 (map untranslate_trace tr) s2 ∧
@@ -986,16 +1024,19 @@ Proof
   ho_match_mp_tac finite_okpath_ind >> rw []
   >- (qexists_tac `stopped_at s1'` >> rw [] >> metis_tac []) >>
   fs [] >>
-  drule multi_step_to_step_block >> ntac 3 (disch_then drule) >>
+  rename1 `state_rel _ _ s1 s1'` >>
+  Cases_on `s1.status ≠ Partial`
+  >- fs [Once multi_step_cases, llvmTheory.step_cases, last_step_cases] >>
+  fs [] >>
+  drule multi_step_to_step_block >> ntac 4 (disch_then drule) >>
   disch_then (qspec_then `types` mp_tac) >> rw [] >>
   first_x_assum drule >> rw [] >>
   qexists_tac `pcons s1' tr' path'` >> rw [] >>
   rw [FILTER_MAP, combinTheory.o_DEF, trans_trace_not_tau] >>
   HINT_EXISTS_TAC >> simp [] >>
   simp [step_cases] >> qexists_tac `b` >> simp [] >>
-  fs [state_rel_def, mem_state_rel_def] >> simp [get_observation_def] >>
-  fs [Once multi_step_cases, last_step_def] >> rw [] >>
-  metis_tac [get_instr_func, exit_no_step]
+  qpat_x_assum `state_rel _ _ _ s1'` mp_tac >>
+  rw [state_rel_def, mem_state_rel_def]
 QED
 
 Theorem translate_prog_correct_lem2:
@@ -1035,6 +1076,42 @@ Proof
   cheat
 QED
 
+Theorem prefix_take_filter_lemma:
+  ∀l lsub.
+    lsub ≼ l
+    ⇒
+    filter (λy. Tau ≠ y) lsub =
+    take (length (filter (λy. Tau ≠ y) lsub)) (filter (λy. Tau ≠ y) l)
+Proof
+  Induct_on `lsub` >> rw [] >>
+  Cases_on `l` >> fs [] >> rw []
+QED
+
+Theorem multi_step_lab_label:
+  ∀prog s1 ls s2.
+    multi_step prog s1 ls s2 ⇒ s2.status ≠ Partial
+    ⇒
+    ∃ls'. (∃i. ls = ls' ++ [Exit i]) ∨ ls = ls' ++ [Error]
+Proof
+  ho_match_mp_tac multi_step_ind >> rw [] >> fs [] >>
+  fs [last_step_cases, llvmTheory.step_cases, step_instr_cases,
+      update_result_def, llvmTheory.inc_pc_def] >>
+  rw [] >> fs []
+QED
+
+Theorem prefix_filter_len_eq:
+  ∀l1 l2 x.
+    l1 ≼ l2 ++ [x] ∧
+    length (filter P l1) = length (filter P (l2 ++ [x])) ∧
+    P x
+    ⇒
+    l1 = l2 ++ [x]
+Proof
+  Induct_on `l1` >> rw [FILTER_APPEND] >>
+  Cases_on `l2` >> fs [] >> rw [] >> rfs [ADD1] >>
+  first_x_assum irule >> rw [FILTER_APPEND]
+QED
+
 Theorem translate_prog_correct:
   ∀prog s1 s1'.
     prog_ok prog ∧ is_ssa prog ∧
@@ -1063,16 +1140,36 @@ Proof
     >- fs [state_rel_def, mem_state_rel_def] >>
     rename [`labels path' = fromList l'`, `labels path = fromList l`,
             `state_rel _ _ (last path) (last path')`, `lsub ≼ flat l`] >>
-    cheat)
-(*
-    `INJ (translate_trace types) (set l2' ∪ set (flat l2)) UNIV`
-    by (
-      simp [INJ_DEF] >> rpt gen_tac >>
-      Cases_on `x` >> Cases_on `y` >> simp [translate_trace_def] >>
-      Cases_on `a` >> Cases_on `a'` >> simp [translate_glob_var_def]) >>
-    fs [INJ_MAP_EQ_IFF, inj_map_prefix_iff] >> rw [] >>
-    fs [state_rel_def, mem_state_rel_def])
-    *)
+    Cases_on `lsub = flat l` >> fs []
+    >- (
+      qexists_tac `flat l'` >>
+      rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF] >>
+      fs [state_rel_def, mem_state_rel_def]) >>
+    `filter (λy. Tau ≠ y) (flat l') = map (translate_trace types) (filter (λy. Tau ≠ y) (flat l))`
+    by rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF, FILTER_MAP] >>
+    qexists_tac `take_prop ($≠ Tau) (length (filter ($≠ Tau) lsub)) (flat l')` >>
+    rw [] >> rw [GSYM MAP_TAKE]
+    >- metis_tac [prefix_take_filter_lemma] >>
+    CCONTR_TAC >> fs [] >>
+    `(last path).status = (last path').status` by fs [state_rel_def, mem_state_rel_def] >>
+    drule take_prop_eq >> strip_tac >>
+    `length (filter (λy. Tau ≠ y) (flat l')) = length (filter (λy. Tau ≠ y) (flat l))`
+    by rw [] >>
+    fs [] >> drule filter_is_prefix >>
+    disch_then (qspec_then `$≠ Tau` assume_tac) >>
+    drule IS_PREFIX_LENGTH >> strip_tac >> fs [] >>
+    `length (filter (λy. Tau ≠ y) lsub) = length (filter (λy. Tau ≠ y) (flat l))` by rw [] >>
+    fs [] >> rw [] >>
+    qspec_then `path` assume_tac finite_path_end_cases >> rfs [] >> fs [] >> rw []
+    >- (`l = []` by metis_tac [llistTheory.fromList_EQ_LNIL] >> fs [] >> rfs []) >>
+    rfs [labels_plink] >>
+    rename1 `LAPPEND (labels path) [|last_l'|] = _` >>
+    `toList (LAPPEND (labels path) [|last_l'|]) = Some l` by metis_tac [llistTheory.from_toList] >>
+    drule llistTheory.toList_LAPPEND_APPEND >> strip_tac >>
+    fs [llistTheory.toList_THM] >> rw [] >>
+    drule multi_step_lab_label >> strip_tac >> rfs [] >> fs [] >>
+    drule prefix_filter_len_eq >> rw [] >>
+    qexists_tac `$≠ Tau` >> rw [])
   >- (
     fs [toList_some] >>
     drule translate_prog_correct_lem2 >> simp [] >>
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index df57ee0bc..93679f2c5 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -25,6 +25,8 @@ Datatype:
   obs =
   | Tau
   | W 'a (word8 list)
+  | Exit int
+  | Error
 End
 
 Datatype:
@@ -43,6 +45,55 @@ Inductive observation_prefixes:
     observation_prefixes (x, l1) (Partial, filter ($≠ Tau) l2))
 End
 
+Definition take_prop_def:
+  (take_prop P n [] = []) ∧
+  (take_prop P n (x::xs) =
+    if n = 0 then
+      []
+    else if P x then
+      x :: take_prop P (n - 1) xs
+    else
+      x :: take_prop P n xs)
+End
+
+Theorem filter_take_prop[simp]:
+  ∀P n l. filter P (take_prop P n l) = take n (filter P l)
+Proof
+  Induct_on `l` >> rw [take_prop_def]
+QED
+
+Theorem take_prop_prefix[simp]:
+  ∀P n l. take_prop P n l ≼ l
+Proof
+  Induct_on `l` >> rw [take_prop_def]
+QED
+
+(*
+Theorem take_prop_eq:
+  ∀P n l. take_prop P n l = l ∧ l ≠ [] ∧ n ≤ length (filter P l) ⇒ P (last l)
+Proof
+  Induct_on `l` >> simp_tac (srw_ss()) [take_prop_def] >> rpt gen_tac >>
+  Cases_on `n = 0` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  Cases_on `P h` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  strip_tac >> strip_tac >>
+  Cases_on `l` >> pop_assum mp_tac >> simp_tac (srw_ss()) []
+  >- metis_tac [take_prop_def] >>
+  ntac 2 strip_tac >> first_x_assum drule >>
+  simp []
+QED
+*)
+
+Theorem take_prop_eq:
+  ∀P n l. take_prop P n l = l ⇒ length (filter P l) ≤ n
+Proof
+  Induct_on `l` >> simp_tac (srw_ss()) [take_prop_def] >> rpt gen_tac >>
+  Cases_on `n = 0` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  Cases_on `P h` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  strip_tac >> strip_tac >>
+  Cases_on `l` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  ntac 2 strip_tac >> first_x_assum drule >> simp []
+QED
+
 (* ----- Theorems about list library functions ----- *)
 
 Theorem dropWhile_map:
@@ -143,6 +194,12 @@ Proof
   rw [] >> fs []
 QED
 
+Theorem filter_is_prefix:
+  ∀l1 l2 P. l1 ≼ l2 ⇒ filter P l1 ≼ filter P l2
+Proof
+  Induct >> rw [] >> Cases_on `l2` >> fs []
+QED
+
 (* ----- Theorems about log ----- *)
 
 Theorem mul_div_bound: