diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 176db21b0..b76e07d0c 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -830,15 +830,15 @@ Definition prog_ok_def:
        alookup p fname = Some dec ⇒
        every (\b. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ∧
      ((* The blocks in a definition have distinct labels.*)
-      ∀fname dec.
-       alookup p fname = Some dec ⇒
-       all_distinct (map fst dec.blocks)) ∧
+      every (\(fname,dec). all_distinct (map fst dec.blocks)) p) ∧
      (* There is a main function *)
      (∃dec. alookup p (Fn "main") = Some dec) ∧
      (* No phi instruction assigns the same register twice *)
      (∀ip from_l phis.
        get_instr p ip (Inr (from_l, phis)) ⇒
-       all_distinct (map (λp. case p of Phi r _ _ => r) phis))
+       all_distinct (map (λp. case p of Phi r _ _ => r) phis)) ∧
+     (* No duplicate function names *)
+     (all_distinct (map fst p))
 End
 
 (* All call frames have a good return address, and the stack allocations of the
diff --git a/sledge/semantics/llvm_ssaScript.sml b/sledge/semantics/llvm_ssaScript.sml
index 5803018ed..c45c9b7a7 100644
--- a/sledge/semantics/llvm_ssaScript.sml
+++ b/sledge/semantics/llvm_ssaScript.sml
@@ -10,12 +10,28 @@
 
 open HolKernel boolLib bossLib Parse;
 open pred_setTheory listTheory rich_listTheory pairTheory arithmeticTheory;
+open alistTheory set_relationTheory;
 open settingsTheory miscTheory llvmTheory llvm_propTheory;
 
 new_theory "llvm_ssa";
 
 numLib.prefer_num ();
 
+(* ----- The syntactic things we need to know about a program, just for this file ---- *)
+
+Definition loc_prog_ok_def:
+  loc_prog_ok p ⇔
+    (∀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)) ∧
+    (∀fname dec.
+      alookup p fname = Some dec ⇒
+      every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ∧
+    (every (\(fname, dec). all_distinct (map fst dec.blocks)) p)
+End
+
 (* ----- Static paths through a program ----- *)
 
 Definition inc_pc_def:
@@ -250,9 +266,17 @@ Definition entry_ip_def:
   entry_ip fname = <| f := fname; b := None; i := Offset 0 |>
 End
 
+(* Equivalent instruction pointers, since we don't want to distinguish pointers
+ * to headers that have different from labels *)
+Definition ip_equiv_def:
+  ip_equiv ip1 ip2 ⇔
+    ip1.f = ip2.f ∧ ip1.b = ip2.b ∧
+    (ip1.i ≠ ip2.i ⇒ ∃l1 l2. ip1.i = Phi_ip l1 ∧ ip2.i = Phi_ip l2)
+End
+
 Definition reachable_def:
   reachable prog ip ⇔
-    ∃path. good_path prog (entry_ip ip.f :: path) ∧ last (entry_ip ip.f :: path) = ip
+    ∃path. good_path prog (entry_ip ip.f :: path) ∧ ip_equiv (last (entry_ip ip.f :: path)) ip
 End
 
 (* To get to ip2 from the entry, you must go through ip1 *)
@@ -260,8 +284,8 @@ Definition dominates_def:
   dominates prog ip1 ip2 ⇔
     ∀path.
       good_path prog (entry_ip ip2.f :: path) ∧
-      last (entry_ip ip2.f :: path) = ip2 ⇒
-      mem ip1 (front (entry_ip ip2.f :: path))
+      ip_equiv (last (entry_ip ip2.f :: path)) ip2 ⇒
+      ∃ip1'. ip_equiv ip1 ip1' ∧ mem ip1' (front (entry_ip ip2.f :: path))
 End
 
 Definition is_ssa_def:
@@ -273,12 +297,94 @@ Definition is_ssa_def:
         r ∈ image fst (assigns prog ip1) ∧ r ∈ image fst (assigns prog ip2) ∧
         ip1.f = fname ∧ ip2.f = fname
         ⇒
-        ip1 = ip2)) ∧
+        ip_equiv ip1 ip2)) ∧
     (* Each use is dominated by its assignment *)
     (∀ip1 r. r ∈ uses prog ip1 ⇒
-      ∃ip2. ip2.f = ip1.f ∧ r ∈ image fst (assigns prog ip2) ∧ dominates prog ip2 ip1)
+      ∃ip2. ip2.f = ip1.f ∧ r ∈ image fst (assigns prog ip2) ∧ dominates prog ip2 ip1) ∧
+    (* All of the blocks are reachable. Otherwise, we could have dead code that
+     * violates SSA, and this will wreck our treatment of a function body as a
+     * list of blocks in dominator tree order *)
+    (∀ip i. get_instr prog ip i ⇒ reachable prog ip)
 End
 
+Theorem ip_equiv_sym:
+  ∀ip1 ip2. ip_equiv ip1 ip2 ⇔ ip_equiv ip2 ip1
+Proof
+  rw [ip_equiv_def] >> metis_tac []
+QED
+
+Theorem ip_equiv_refl:
+  ∀ip. ip_equiv ip ip
+Proof
+  rw [ip_equiv_def]
+QED
+
+Theorem ip_equiv_trans:
+  ∀ip1 ip2 ip3. ip_equiv ip1 ip2 ∧ ip_equiv ip2 ip3 ⇒ ip_equiv ip1 ip3
+Proof
+  rw [ip_equiv_def] >> metis_tac []
+QED
+
+Theorem ip_equiv_assigns:
+  ∀prog ip1 ip2 rt.
+    ip_equiv ip1 ip2 ∧ rt ∈ assigns prog ip1 ⇒ rt ∈ assigns prog ip2
+Proof
+  rw [ip_equiv_def, assigns_cases, IN_DEF] >>
+  Cases_on `ip1 = ip2` >> rw []
+  >- metis_tac []
+  >- (fs [pc_component_equality] >> fs [get_instr_cases] >> fs [])
+  >- metis_tac []
+  >- (
+    fs [pc_component_equality] >>
+    fs [get_instr_cases, inc_pc_def, inc_bip_def, PULL_EXISTS] >>
+    rw [] >> rfs [inc_bip_def] >>
+    metis_tac [optionTheory.SOME_11])
+QED
+
+Theorem ip_equiv_next:
+  ∀prog ip1 ip2 ip3.
+    ip_equiv ip1 ip2 ∧ ip3 ∈ next_ips prog ip1 ⇒
+    ip3 ∈ next_ips prog ip2
+Proof
+  rw [ip_equiv_def, next_ips_cases, IN_DEF] >>
+  Cases_on `ip1 = ip2` >> rw []
+  >- metis_tac []
+  >- (fs [pc_component_equality] >> fs [get_instr_cases] >> fs [])
+  >- metis_tac []
+  >- (
+    fs [pc_component_equality] >>
+    fs [get_instr_cases, inc_pc_def, inc_bip_def, PULL_EXISTS] >>
+    rw [] >> rfs [inc_bip_def] >>
+    metis_tac [optionTheory.SOME_11])
+QED
+
+Theorem ip_equiv_dominates:
+  ∀prog ip1 ip2 ip3.
+   dominates prog ip1 ip2 ∧ ip_equiv ip2 ip3 ⇒ dominates prog ip1 ip3
+Proof
+  rw [dominates_def] >> metis_tac [ip_equiv_def]
+QED
+
+Theorem ip_equiv_dominates2:
+  ∀prog ip1 ip2 ip3.
+   dominates prog ip1 ip2 ∧ ip_equiv ip1 ip3 ⇒ dominates prog ip3 ip2
+Proof
+  rw [dominates_def] >> metis_tac [ip_equiv_def]
+QED
+
+Theorem ip_equiv_next_ips:
+  ∀p i ip1 ip2. ip_equiv ip1 ip2 ∧ i ∈ next_ips p ip1 ⇒ i ∈ next_ips p ip2
+Proof
+  rw [ip_equiv_def] >>
+  Cases_on `ip1.i = ip2.i`
+  >- metis_tac [pc_component_equality] >>
+  fs [] >> rw [] >> rfs [] >>
+  fs [next_ips_cases, IN_DEF, inc_pc_def, inc_bip_def] >>
+  fs [get_instr_cases] >> rw [] >> fs [] >>
+  rw [pc_component_equality, PULL_EXISTS] >>
+  rfs [] >> rw [] >> fs [inc_bip_def]
+QED
+
 Theorem dominates_trans:
   ∀prog ip1 ip2 ip3.
     dominates prog ip1 ip2 ∧ dominates prog ip2 ip3 ⇒ dominates prog ip1 ip3
@@ -289,24 +395,33 @@ Proof
   qpat_x_assum `mem _ (front _)` mp_tac >>
   simp [Once MEM_EL] >> rw [] >> fs [EL_FRONT] >>
   first_x_assum (qspec_then `take n path` mp_tac) >> simp [LAST_DEF] >>
+  simp [Once ip_equiv_sym] >>
   rw [] >> fs [entry_ip_def]
-  >- (fs [Once good_path_cases] >> rw [] >> fs [next_ips_cases, IN_DEF]) >>
+  >- (
+    fs [Once good_path_cases, ip_equiv_def] >> rw [] >>
+    fs [next_ips_cases, IN_DEF] >> metis_tac [])
+  >- (
+    fs [Once good_path_cases, ip_equiv_def] >> rw [] >>
+    fs [next_ips_cases, IN_DEF] >> metis_tac []) >>
   rfs [EL_CONS] >>
   `?m. n = Suc m` by (Cases_on `n` >> rw []) >>
   rw [] >> rfs [] >>
-  `(el m path).f = ip3.f`
+  `(el m path).f = (last (<|f := ip3.f; b := None; i := Offset 0|> ::path)).f`
   by (
     irule good_path_same_func >>
     qexists_tac `<| f:= ip3.f; b := NONE; i := Offset 0|> :: path` >>
     qexists_tac `prog` >>
     conj_tac >- rw [EL_MEM] >>
     metis_tac [MEM_LAST]) >>
+  `(el m path).f = ip3.f` by metis_tac [ip_equiv_def] >>
   fs [] >> qpat_x_assum `_ ⇒ _` mp_tac >> impl_tac
   >- (
     irule good_path_prefix >> HINT_EXISTS_TAC >> rw [] >>
-    metis_tac [take_is_prefix]) >>
-  rw [] >> drule MEM_FRONT >> rw [] >>
+    metis_tac [take_is_prefix, ip_equiv_def]) >>
+  rw [] >> drule MEM_FRONT >> rw []
+  >- (qexists_tac `<|f := ip3.f; b := None; i := Offset 0|>` >> fs [ip_equiv_def]) >>
   fs [MEM_EL, LENGTH_FRONT] >> rfs [EL_TAKE] >> rw [] >>
+  HINT_EXISTS_TAC >> rw [] >>
   disj2_tac >> qexists_tac `n'` >> rw [] >>
   irule (GSYM EL_FRONT) >>
   rw [NULL_EQ, LENGTH_FRONT]
@@ -323,59 +438,68 @@ Theorem dominates_antisym_lem:
   ∀prog ip1 ip2. dominates prog ip1 ip2 ∧ dominates prog ip2 ip1 ⇒ ¬reachable prog ip1
 Proof
   rw [dominates_def, reachable_def] >> CCONTR_TAC >> fs [] >>
-  Cases_on `ip1 = entry_ip ip1.f` >> fs []
+  Cases_on `ip_equiv ip1 (entry_ip ip1.f)` >> fs []
   >- (
     first_x_assum (qspec_then `[]` mp_tac) >> rw [] >>
     fs [Once good_path_cases, IN_DEF, next_ips_cases] >>
-    metis_tac []) >>
-  `path ≠ []` by (Cases_on `path` >> fs []) >>
-  `(OLEAST n. n < length path ∧ el n path = ip1) ≠ None`
+    metis_tac [ip_equiv_sym]) >>
+  `path ≠ []` by (Cases_on `path` >> fs [] >> metis_tac [ip_equiv_sym]) >>
+  `(OLEAST n. n < length path ∧ ip_equiv (el n path) ip1) ≠ None`
   by (
     rw [whileTheory.OLEAST_EQ_NONE] >>
     qexists_tac `PRE (length path)` >> rw [] >>
     fs [LAST_DEF, LAST_EL] >>
     Cases_on `path` >> fs []) >>
-  qabbrev_tac `path1 = splitAtPki (\n ip. ip = ip1) (\x y. x) path` >>
-  first_x_assum (qspec_then `path1 ++ [ip1]` mp_tac) >>
+  qabbrev_tac `path1 = splitAtPki (\n ip. ip_equiv ip ip1) (\x y. x++[HD y]) path` >>
+  first_x_assum (qspec_then `path1` mp_tac) >>
   simp [] >>
+  `IS_PREFIX path path1`
+  by (
+    unabbrev_all_tac >> rw [splitAtPki_EQN] >>
+    CASE_TAC >> rw [] >>
+    fs [whileTheory.OLEAST_EQ_SOME] >>
+    rw [GSYM SNOC_APPEND, SNOC_EL_TAKE, HD_DROP] >>
+    metis_tac [take_is_prefix]) >>
   conj_asm1_tac >> rw []
+  >- (irule good_path_prefix >> HINT_EXISTS_TAC >> rw [])
   >- (
-    irule good_path_prefix >>
-    HINT_EXISTS_TAC >> rw [] >>
     unabbrev_all_tac >> rw [splitAtPki_EQN] >>
     CASE_TAC >> rw [] >>
     fs [whileTheory.OLEAST_EQ_SOME] >>
-    rw [GSYM SNOC_APPEND, SNOC_EL_TAKE] >>
-    metis_tac [take_is_prefix])
-  >- rw [LAST_DEF] >>
+    rw [LAST_DEF, HD_DROP]) >>
+  `path1 ≠ []`
+  by (fs [Abbr `path1`, splitAtPki_EQN] >> CASE_TAC >> rw []) >>
   simp [GSYM SNOC_APPEND, FRONT_SNOC, FRONT_DEF] >>
   CCONTR_TAC >> fs [MEM_EL]
   >- (
     first_x_assum (qspec_then `[]` mp_tac) >>
     fs [entry_ip_def, Once good_path_cases, IN_DEF, next_ips_cases] >>
+    fs [ip_equiv_def] >>
     metis_tac []) >>
-  rw [] >>
-  rename [`n1 < length _`, `last _ = el n path`] >>
+  rw [] >> rfs [] >>
+  rename [`n1 < length (front _)`, `ip_equiv (el n _) _`,
+          `ip_equiv _ (el n1 (front _))`] >>
   first_x_assum (qspec_then `take (Suc n1) path1` mp_tac) >> rw []
   >- (
     irule good_path_prefix >> HINT_EXISTS_TAC >> rw [entry_ip_def]
     >- (
+      `(el n1 (front path1)).f = (entry_ip ip1.f).f` suffices_by fs [ip_equiv_def, entry_ip_def] >>
       irule good_path_same_func >>
-      qexists_tac `entry_ip (el n path).f::(path1 ++ [el n path])` >>
-      qexists_tac `prog` >> rw [EL_MEM]) >>
+      qexists_tac `entry_ip ip1.f::path1` >>
+      qexists_tac `prog` >> rw [EL_MEM, entry_ip_def] >>
+      rw [MEM_EL] >> disj2_tac >>
+      qexists_tac `n1` >> rw [] >> rfs [LENGTH_FRONT] >>
+      irule EL_FRONT >> rw [NULL_EQ, LENGTH_FRONT]) >>
     metis_tac [IS_PREFIX_APPEND3, take_is_prefix, IS_PREFIX_TRANS])
-  >- (rw [LAST_DEF] >> fs []) >>
+  >- (
+    rfs [LENGTH_FRONT] >> rw [LAST_DEF]  >>
+    metis_tac [EL_FRONT, NULL_EQ, ip_equiv_sym, LENGTH_FRONT]) >>
   rw [METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
   simp [EL_FRONT] >>
+  rfs [LENGTH_TAKE, LENGTH_FRONT] >>
   rename [`n2 < Suc _`] >>
   Cases_on `¬(0 < n2)` >> rw [EL_CONS]
-  >- (
-    fs [entry_ip_def] >>
-    `(el n path).f = (el n1 path1).f` suffices_by metis_tac [] >>
-    irule good_path_same_func >>
-    qexists_tac `<|f := (el n path).f; b := None; i := Offset 0|> ::(path1 ++ [el n path])` >>
-    qexists_tac `prog` >>
-    rw [EL_MEM]) >>
+  >- (fs [entry_ip_def] >> CCONTR_TAC >> fs [] >> fs [ip_equiv_def]) >>
   fs [EL_TAKE, Abbr `path1`, splitAtPki_EQN] >>
   CASE_TAC >> rw [] >> fs []
   >- metis_tac [] >>
@@ -383,7 +507,9 @@ Proof
   rfs [LENGTH_TAKE] >>
   `PRE n2 < x` by decide_tac >>
   first_x_assum drule >>
-  rw [EL_TAKE]
+  rfs [HD_DROP, LAST_DEF] >>
+  rw [EL_TAKE, EL_APPEND_EQN] >>
+  metis_tac [ip_equiv_sym]
 QED
 
 Theorem dominates_antisym:
@@ -398,6 +524,274 @@ Proof
   metis_tac [dominates_antisym]
 QED
 
+Definition bip_less_def:
+  (bip_less (Phi_ip _) (Offset _) ⇔ T) ∧
+  (bip_less (Offset m) (Offset n) ⇔ m < n) ∧
+  (bip_less _ _ ⇔ F)
+End
+
+Theorem bip_less_tri:
+  ∀ip1 ip2. ip1.f = ip2.f ∧ ip1.b = ip2.b ⇒ bip_less ip1.i ip2.i ∨ bip_less ip2.i ip1.i ∨ ip_equiv ip1 ip2
+Proof
+  rw [] >> Cases_on `ip1.i` >> Cases_on `ip2.i`>> rw [bip_less_def, ip_equiv_def]
+QED
+
+Theorem ip_equiv_less:
+  ∀ip1 ip2 ip3.
+    ip_equiv ip2 ip3 ∧
+    bip_less ip1.i ip2.i
+    ⇒
+    bip_less ip1.i ip3.i
+Proof
+  rw [ip_equiv_def] >>
+  Cases_on `ip1.i` >> Cases_on `ip2.i` >> Cases_on `ip3.i` >> fs [bip_less_def]
+QED
+
+Theorem ip_equiv_less2:
+  ∀ip1 ip2 ip3.
+    ip_equiv ip2 ip3 ∧
+    bip_less ip2.i ip1.i
+    ⇒
+    bip_less ip3.i ip1.i
+Proof
+  rw [ip_equiv_def] >>
+  Cases_on `ip1.i` >> Cases_on `ip2.i` >> Cases_on `ip3.i` >> fs [bip_less_def]
+QED
+
+
+Triviality front_cons_snoc:
+  ∀x y z. front (x::SNOC y z) = x::z
+Proof
+  Induct_on `z` >> fs [SNOC_APPEND]
+QED
+
+Triviality last_cons_snoc:
+  ∀x y z. last (x::SNOC y z) = y
+Proof
+  Induct_on `z` >> fs []
+QED
+
+Triviality prefix_snoc:
+  ∀x y. x ≼ SNOC y x
+Proof
+  Induct_on `x` >> fs []
+QED
+
+Triviality bip_lem:
+  bip_less i1 i2 ⇒ ?n. i2 = Offset n
+Proof
+  Cases_on `i1` >> Cases_on `i2` >> fs [bip_less_def]
+QED
+
+Theorem next_ips_prev_entry:
+  ∀prog ip1 ip2 ip3 f.
+  (∀fname dec.
+     alookup prog fname = Some dec ⇒
+     every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ⇒
+  ip3 ∈ next_ips prog (entry_ip f) ∧
+  (∃i. get_instr prog ip1 i) ∧
+  ip1.f = ip2.f ∧
+  ip1.b = ip2.b ∧
+  bip_less ip1.i ip2.i ∧
+  ip_equiv ip3 ip2
+  ⇒
+  ip1 = entry_ip f
+Proof
+  rw [IN_DEF, next_ips_cases, get_instr_cases, entry_ip_def, ip_equiv_def] >>
+  rw [] >>
+  Cases_on `HD b.body` >> fs [instr_next_ips_def] >>
+  rw [] >> fs [inc_pc_def, inc_bip_def] >> rw [] >>
+  fs [] >> rw [pc_component_equality] >>
+  rfs [bip_less_def] >> rw [] >>
+  res_tac >>
+  fs [EVERY_MEM] >>
+  metis_tac [blockHeader_distinct, FST, ALOOKUP_MEM, SND, EVERY_MEM, bip_lem, bip_distinct]
+QED
+
+Theorem next_ips_prev_less:
+  ip2 ∈ next_ips prog ip3 ∧
+  (∃i. get_instr prog ip1 i) ∧
+  ip1.f = ip2.f ∧
+  ip1.b = ip2.b ∧
+  ~ip_equiv ip1 ip3 ∧
+  bip_less ip1.i ip2.i
+  ⇒
+  ip3.b = ip2.b ∧ bip_less ip1.i ip3.i
+Proof
+  rw [IN_DEF, next_ips_cases, get_instr_cases, ip_equiv_def] >>
+  rw [] >>
+  Cases_on `el idx b.body` >> fs [instr_next_ips_def] >>
+  rw [] >> fs [inc_pc_def, inc_bip_def] >> rw [bip_less_def] >>
+  imp_res_tac bip_lem >>
+  fs [] >>
+  rfs [bip_less_def, inc_bip_def] >> rw [] >>
+  fs [pc_component_equality] >> rfs []
+QED
+
+Theorem good_path_end_step:
+  good_path prog (entry_ip f::SNOC ip2 (p1 ++ [ip3]))
+  ⇒
+  ip2 ∈ next_ips prog ip3
+Proof
+  rw [Once good_path_cases] >>
+  qpat_x_assum `_ = _` (mp_tac o GSYM) >>
+  rw [] >> fs [good_path_append] >>
+  Cases_on `p1` >> fs [Once good_path_cases]
+QED
+
+Theorem same_block_dominates:
+  ∀prog.
+    (∀fname dec.
+       alookup prog fname = Some dec ⇒
+       every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks) ⇒
+    ∀ip1 ip2.
+    ip1.f = ip2.f ∧ ip1.b = ip2.b ∧ (∃i. get_instr prog ip1 i) ⇒ bip_less ip1.i ip2.i ⇒ dominates prog ip1 ip2
+Proof
+  ntac 2 strip_tac >>
+  simp [dominates_def, PULL_FORALL] >>
+  ntac 3 gen_tac >>
+  Q.ID_SPEC_TAC `ip2` >>
+  Q.ID_SPEC_TAC `path` >>
+  ho_match_mp_tac SNOC_INDUCT >> rw []
+  >- (
+    simp [Once good_path_cases, ip_equiv_def] >>
+    Cases_on `ip1.i` >> Cases_on `ip2.i` >> fs [bip_less_def] >>
+    rw [entry_ip_def, pc_component_equality] >>
+    CCONTR_TAC >> fs [] >> rw [] >> fs [get_instr_cases] >> rw [] >>
+    first_x_assum drule >> simp [EXISTS_MEM] >>
+    qexists_tac `(ip1.b, b)` >> rw [] >>
+    metis_tac [optionTheory.SOME_11, ALOOKUP_MEM]) >>
+  simp [front_cons_snoc] >> fs [last_cons_snoc] >> rw [] >>
+  `good_path prog (entry_ip ip2.f::path)`
+  by (irule good_path_prefix >> HINT_EXISTS_TAC >> rw [prefix_snoc]) >>
+  Cases_on `path = []` >> rw []
+  >- (
+    fs [Once good_path_cases] >>
+    fs [Once good_path_cases] >>
+    metis_tac [next_ips_prev_entry, ip_equiv_refl]) >>
+  `?p1 ip3. path = p1 ++ [ip3]` by metis_tac [SNOC_CASES, SNOC_APPEND] >>
+  fs [] >> rw [] >>
+  rename1 `ip_equiv ip2' _` >>
+  `ip3.f = ip2'.f`
+  by (
+    irule good_path_same_func >>
+    qexists_tac `entry_ip ip2.f::SNOC ip2' (p1 ++ [ip3])` >>
+    rw [] >> metis_tac []) >>
+  Cases_on `ip_equiv ip1 ip3` >> rw []
+  >- metis_tac [] >>
+ `ip3.b = ip2'.b ∧ bip_less ip1.i ip3.i`
+  by (
+    drule good_path_end_step >> strip_tac >>
+    irule next_ips_prev_less >>
+    fs [] >> rw []
+    >- fs [ip_equiv_def]
+    >- fs [ip_equiv_def]
+    >- metis_tac []
+    >- metis_tac [ip_equiv_less, ip_equiv_sym]) >>
+  first_x_assum (qspec_then `ip3` mp_tac) >> simp [] >>
+  impl_tac
+  >- metis_tac [ip_equiv_def] >>
+  impl_tac >> rw []
+  >- fs [ip_equiv_def]
+  >- rw [LAST_DEF, ip_equiv_def] >>
+  qexists_tac `ip1'` >> rw [] >>
+  drule MEM_FRONT >> fs [ip_equiv_def]
+QED
+
+Theorem next_ips_still_leq:
+  ip2 ∈ next_ips prog ip1 ∧
+  ip2.f = ip1.f ∧
+  ip2.f = ip3.f ∧
+  ip1.b = ip3.b ∧
+  (∀inst. get_instr prog ip1 (Inl inst) ⇒ ~terminator inst) ∧
+  bip_less ip1.i ip3.i
+  ⇒
+  bip_less ip2.i ip3.i ∧ ip2.b = ip1.b ∨ ip2 = ip3
+Proof
+  rw [IN_DEF, next_ips_cases] >> rfs []
+  >- (
+    fs [get_instr_cases] >> rw [] >> rfs [] >> rw [] >> fs [] >>
+    Cases_on `el idx b.body` >> fs [instr_next_ips_def] >> rw [] >> fs [inc_pc_def] >>
+    rw [] >> rfs [inc_bip_def] >>
+    Cases_on `ip3.i` >> fs [bip_less_def, pc_component_equality] >>
+    rw [] >> fs [terminator_def])
+  >- (
+    fs [get_instr_cases, inc_pc_def] >> rw [] >> rfs [inc_bip_def] >> rw [pc_component_equality] >>
+    Cases_on `ip3.i` >> fs [bip_less_def])
+QED
+
+Theorem good_path_find_ip:
+  ∀prog path.
+    good_path prog path ⇒
+    ∀ip.
+    loc_prog_ok prog ∧
+    path ≠ [] ∧
+    (last path).b ≠ ip.b ∧
+    ip.f = (HD path).f ∧ ip.b = (HD path).b ∧ bip_less (HD path).i ip.i ∧
+    (∃inst. get_instr prog ip inst)
+    ⇒
+    mem ip (front path)
+Proof
+  ho_match_mp_tac good_path_ind >> rw []
+  >- metis_tac [] >>
+  drule next_ips_same_func >> rw [] >>
+  drule next_ips_still_leq >> simp [] >>
+  disch_then (qspec_then `ip` mp_tac) >> simp [] >>
+  impl_tac
+  >- (
+    rw [get_instr_cases] >>
+    `every (λi. ~terminator i) (front b.body) ∧ b.body ≠ []` by metis_tac [loc_prog_ok_def] >>
+    fs [EVERY_MEM, MEM_EL] >>
+    first_x_assum (qspec_then `el idx b.body` mp_tac) >>
+    impl_tac
+    >- (
+      qexists_tac `idx` >> conj_asm1_tac
+      >- (
+        Cases_on `ip.i` >> fs [bip_less_def, LENGTH_FRONT] >>
+        fs [get_instr_cases] >>
+        rw [] >> rfs [] >> rw [] >> fs []) >>
+      metis_tac [EL_FRONT, NULL_EQ]) >>
+    metis_tac []) >>
+  rw []
+  >- metis_tac [next_ips_same_func] >>
+  Cases_on `path` >> fs []
+QED
+
+Theorem dominates_same_block:
+  ∀ip1 ip2 ip3.
+    loc_prog_ok prog ∧ dominates prog ip1 ip3 ∧ ip1.f = ip2.f ∧ ip1.b = ip2.b ∧
+    ip3.b ≠ ip1.b ∧ bip_less ip1.i ip2.i ∧ (∃inst. get_instr prog ip2 instr)
+    ⇒
+    dominates prog ip2 ip3
+Proof
+  rw [dominates_def] >>
+  first_x_assum drule >> rw [] >>
+  drule MEM_FRONT >>
+  REWRITE_TAC [Once MEM_SPLIT] >> strip_tac >>
+  `good_path prog (ip1'::l2)`
+  by (
+    full_simp_tac std_ss [GSYM APPEND_ASSOC] >>
+    full_simp_tac std_ss [Once good_path_append]) >>
+  full_simp_tac std_ss [LAST_APPEND] >>
+  drule good_path_find_ip >>
+  disch_then (qspec_then `ip2` mp_tac) >>
+  impl_tac >> rw []
+  >- (fs [ip_equiv_def] >> metis_tac [])
+  >- (
+    `ip1'.f = (entry_ip ip3.f).f` suffices_by (fs [ip_equiv_def]) >>
+    irule good_path_same_func >>
+    qexists_tac `entry_ip ip3.f::path` >>
+    qexists_tac `prog` >> rw_tac std_ss []
+    >- rw []
+    >- metis_tac [MEM])
+  >- fs [ip_equiv_def]
+  >- metis_tac [ip_equiv_less2]
+  >- metis_tac []
+  >- (
+    qexists_tac `ip2` >> rw [ip_equiv_refl] >>
+    rw [FRONT_APPEND])
+QED
+
 (* ----- Liveness ----- *)
 
 Definition live_def:
@@ -476,10 +870,11 @@ Proof
         qpat_x_assum `good_path _ (_::_)` mp_tac >>
         qpat_x_assum `good_path _ (_::_)` mp_tac >>
         simp [Once good_path_cases] >>
-        rw [] >> rw []))
-    >- (Cases_on `path` >> fs [])) >>
+        rw [] >> rw [] >>
+        metis_tac [ip_equiv_next, ip_equiv_sym]))
+    >- (Cases_on `path` >> fs [] >> metis_tac [ip_equiv_refl])) >>
   rw [] >>
-  `ip2'.f = ip2.f`
+  `ip1'.f = (last (entry_ip ip2.f::path')).f`
   by (
     irule good_path_same_func >>
     qexists_tac `entry_ip ip2.f::path'` >>
@@ -489,19 +884,23 @@ Proof
       Cases_on `path` >>
       full_simp_tac std_ss [GSYM APPEND, FRONT_APPEND, APPEND_NIL, LAST_CONS]
       >- metis_tac [MEM_FRONT] >>
-      fs [] >> metis_tac [])
+      full_simp_tac std_ss [GSYM APPEND, FRONT_APPEND] >> fs [] >> rw [FRONT_DEF] >> fs [] >>
+      metis_tac [ip_equiv_assigns])
     >- metis_tac [MEM_LAST]) >>
-  `ip2' = ip1` by metis_tac [] >>
+  `ip2'.f = ip1.f` by fs [ip_equiv_def] >>
+  `ip_equiv ip2' ip1` by metis_tac [] >>
   rw [] >>
   Cases_on `path` >> fs [] >>
   full_simp_tac std_ss [GSYM APPEND, FRONT_APPEND] >> fs [] >> rw [FRONT_DEF] >> fs []
-  >- metis_tac []
+  >- (fs [FRONT_DEF] >> metis_tac [ip_equiv_sym, ip_equiv_trans])
+  >- (fs [ip_equiv_def, entry_ip_def] >> metis_tac [pc_component_equality])
+  >- (fs [FRONT_DEF] >> metis_tac [ip_equiv_sym, ip_equiv_trans])
   >- (
-    `mem ip1 path' = mem ip1 (front path' ++ [last path'])` by metis_tac [APPEND_FRONT_LAST] >>
+    `mem ip1' path' = mem ip1' (front path' ++ [last path'])` by metis_tac [APPEND_FRONT_LAST] >>
     fs [LAST_DEF] >>
-    metis_tac [])
-  >- metis_tac []
-  >- metis_tac []
+    metis_tac [ip_equiv_trans, ip_equiv_assigns])
+  >- metis_tac [ip_equiv_assigns]
+  >- metis_tac [ip_equiv_assigns]
 QED
 
 Theorem ssa_dominates_live_range:
@@ -521,6 +920,7 @@ Theorem reachable_dominates_same_func:
   ∀prog ip1 ip2. reachable prog ip2 ∧ dominates prog ip1 ip2 ⇒ ip1.f = ip2.f
 Proof
   rw [reachable_def, dominates_def] >> res_tac >>
+  `ip1'.f = (last (entry_ip ip2.f::path)).f` suffices_by fs [ip_equiv_def] >>
   irule good_path_same_func >>
   metis_tac [MEM_LAST, MEM_FRONT]
 QED
@@ -533,9 +933,10 @@ Proof
   qexists_tac `path ++ [ip2]` >>
   simp_tac std_ss [GSYM APPEND, LAST_APPEND_CONS, LAST_CONS] >>
   simp [good_path_append] >>
-  simp [Once good_path_cases] >>
-  fs [next_ips_cases, IN_DEF] >>
-  metis_tac []
+  simp [Once good_path_cases, ip_equiv_refl] >>
+  rw []
+  >- (fs [next_ips_cases, IN_DEF] >> metis_tac [])
+  >- metis_tac [ip_equiv_next, ip_equiv_sym]
 QED
 
 (* ----- A theory of *dominator ordered* programs ------ *)
@@ -570,11 +971,6 @@ Definition linear_live_def:
     let (gen,kill) = instrs_live b.body in
     header_uses b.h ∪ (gen ∪ (linear_live bs DIFF kill) DIFF header_assigns b.h))
 End
-Definition bip_less_def:
-  (bip_less (Phi_ip _) (Offset _) ⇔ T) ∧
-  (bip_less (Offset m) (Offset n) ⇔ m < n) ∧
-  (bip_less _ _ ⇔ F)
-End
 
 Definition linear_pc_less_def:
   linear_pc_less = $< LEX bip_less
@@ -834,4 +1230,648 @@ Proof
   metis_tac []
 QED
 
+Definition block_assigns_def:
+  block_assigns (l, b) =
+    header_assigns b.h ∪ image fst (bigunion (image instr_assigns (set b.body)))
+End
+
+Definition block_uses_def:
+  block_uses (l, b) =
+    header_uses b.h ∪ bigunion (image instr_uses (set b.body))
+End
+
+Definition block_order_def:
+  block_order bs =
+    tc { (b1, b2) |
+          fst b1 ≠ fst b2 ∧ mem b1 bs ∧ mem b2 bs ∧ (∃r. r ∈ block_assigns b1 ∧ r ∈ block_uses b2) }
+End
+
+Theorem prog_ok_distinct_lem:
+  loc_prog_ok p ∧ alookup p f = Some d ⇒ all_distinct (map fst d.blocks)
+Proof
+  rw [loc_prog_ok_def, EVERY_MEM] >>
+  drule ALOOKUP_MEM >> rw [] >>
+  res_tac >> fs []
+QED
+
+Theorem block_order_dominates:
+  ∀b1 b2.
+    (b1,b2) ∈ block_order d.blocks ⇒
+    loc_prog_ok prog ∧
+    is_ssa prog ∧
+    alookup prog f = Some d ⇒
+    ∃ip1 ip2.
+      dominates prog ip1 ip2 ∧
+      ip1.f = f ∧
+      ip2.f = f ∧
+      ip1.b = fst b1 ∧
+      ip2.b = fst b2 ∧
+      fst b1 ≠ fst b2 ∧
+      (∃i2. get_instr prog ip2 i2)
+Proof
+  simp [block_order_def] >>
+  ho_match_mp_tac tc_ind >> rw []
+  >- (
+    fs [is_ssa_def] >>
+    `∃ip1. r ∈ uses prog ip1 ∧ ip1.f = f ∧ ip1.b = fst b2`
+    by (
+      simp [Once IN_DEF, uses_cases] >> Cases_on `b2` >> fs [block_uses_def] >>
+      fs [get_instr_cases, PULL_EXISTS]
+      >- (
+        rename1 `_ ∈ header_uses b.h` >>
+        Cases_on `b.h` >> fs [header_uses_def] >> rw [] >>
+        rename1 `mem (l1, _) _` >>
+        qexists_tac `<| f := f; b := l1; i := Phi_ip from_l |>` >> rw [] >>
+        qexists_tac `l` >> qexists_tac `phi_uses from_l p` >> qexists_tac `b` >>
+        rw [MEM_MAP] >>
+        metis_tac [ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, prog_ok_distinct_lem])
+      >- (
+        fs [MEM_EL] >> rw [] >>
+        rename [`n1 < length b.body`, `(l1, _) = el _ _`] >>
+        qexists_tac `<| f := f; b := l1; i := Offset n1 |>` >> rw [] >>
+        metis_tac [ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, EL_MEM, prog_ok_distinct_lem])) >>
+    first_x_assum drule >> rw [] >>
+    qexists_tac `ip2` >> qexists_tac `ip1` >> rw []
+    >- (
+      rename1 `rt ∈ assigns _ _` >>
+      `∃ip3 t. (fst rt, t) ∈ assigns prog ip3 ∧ ip3.f = ip1.f ∧ ip3.b = fst b1`
+      by (
+        simp [Once IN_DEF, assigns_cases] >> Cases_on `b1` >> fs [block_assigns_def] >>
+        fs [get_instr_cases, PULL_EXISTS]
+        >- (
+          rename1 `_ ∈ header_assigns b.h` >>
+          Cases_on `b.h` >> fs [header_assigns_def] >> rw [] >>
+          rename1 `mem (l1, _) _` >>
+          fs [MEM_MAP] >>
+          qexists_tac `<| f := ip1.f; b := l1; i := Phi_ip from_l |>` >> rw [] >>
+          qexists_tac `SND (phi_assigns y)` >> qexists_tac `l` >> qexists_tac `b` >>
+          qexists_tac `o'` >> rw [] >>
+          metis_tac [FST, ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, SND, prog_ok_distinct_lem])
+        >- (
+          fs [MEM_EL] >> rw [] >>
+          rename [`n1 < length b.body`, `(l1, _) = el _ _`] >>
+          qexists_tac `<| f := ip1.f; b := l1; i := Offset n1 |>` >> rw [] >>
+          qexists_tac `snd x` >>
+          rw [] >>
+          metis_tac [ALOOKUP_ALL_DISTINCT_MEM, loc_prog_ok_def, EL_MEM, FST, SND, prog_ok_distinct_lem])) >>
+      metis_tac [ip_equiv_def, FST])
+    >- (fs [uses_cases, IN_DEF] >> metis_tac []))
+  >- (
+    first_x_assum drule >> first_x_assum drule >> rw [] >>
+    Cases_on `ip1.b = ip2.b ∨ ip1'.b = ip2'.b`
+    >- metis_tac [] >>
+    qexists_tac `ip1` >> qexists_tac `ip2'` >>
+    Cases_on `bip_less ip2.i ip1'.i`
+    >- (
+      `dominates prog ip2 ip1'` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+      rw []
+      >- metis_tac [dominates_trans]
+      >- (
+        CCONTR_TAC >> fs [] >>
+        Cases_on `bip_less ip2'.i ip1.i`
+        >- (
+          `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+          metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >>
+        Cases_on `bip_less ip1.i ip2'.i`
+        >- (
+          `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >>
+          metis_tac [dominates_antisym, dominates_trans, is_ssa_def])
+        >- (
+          `dominates prog ip1' ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >>
+          metis_tac [dominates_antisym, dominates_trans, is_ssa_def]))
+      >- metis_tac []) >>
+    Cases_on `bip_less ip1'.i ip2.i`
+    >- (
+      `dominates prog ip2 ip2'` by metis_tac [dominates_same_block] >>
+      rw []
+      >- metis_tac [dominates_trans]
+      >- (
+        CCONTR_TAC >> fs [] >>
+        Cases_on `bip_less ip2'.i ip1.i`
+        >- (
+          `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+          metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >>
+        Cases_on `bip_less ip1.i ip2'.i`
+        >- (
+          `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >>
+          metis_tac [dominates_antisym, dominates_trans, is_ssa_def])
+        >- (
+          `dominates prog ip2 ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >>
+          metis_tac [dominates_antisym, dominates_trans, is_ssa_def]))
+      >- metis_tac [])
+    >- (
+      `ip_equiv ip1' ip2` by metis_tac [bip_less_tri] >>
+      `dominates prog ip1 ip2'` by metis_tac [dominates_trans, ip_equiv_sym, ip_equiv_dominates] >>
+      rw []
+      >- (
+        CCONTR_TAC >> fs [] >>
+        Cases_on `bip_less ip2'.i ip1.i`
+        >- (
+          `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+          metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >>
+        Cases_on `bip_less ip1.i ip2'.i`
+        >- (
+          `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >>
+          `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, ip_equiv_sym] >>
+          metis_tac [dominates_antisym, is_ssa_def])
+        >- (
+          `dominates prog ip2' ip2` by metis_tac [ip_equiv_dominates2, bip_less_tri] >>
+          `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, bip_less_tri] >>
+          metis_tac [dominates_antisym, is_ssa_def]))
+      >- metis_tac []))
+QED
+
+Theorem block_order_po:
+  ∀prog f d.
+    loc_prog_ok prog ∧ is_ssa prog ∧
+    alookup prog f = Some d
+    ⇒
+    partial_order (rc (block_order d.blocks) (set d.blocks)) (set d.blocks)
+Proof
+  rw [partial_order_def]
+  >- (rw [block_order_def, domain_def, SUBSET_DEF, rc_def] >> drule tc_domain_range >> rw [domain_def])
+  >- (rw [block_order_def, range_def, SUBSET_DEF, rc_def] >> rw [] >> drule tc_domain_range >> rw [range_def])
+  >- metis_tac [block_order_def, transitive_rc, tc_transitive]
+  >- metis_tac [rc_is_reflexive]
+  >- (
+    simp [antisym_rc] >> rw [antisym_def] >>
+    pop_assum mp_tac >>
+    drule block_order_dominates >>
+    disch_then drule >> simp [] >> disch_then drule >> rw [] >>
+    drule block_order_dominates >>
+    disch_then drule >> simp [] >> disch_then drule >> rw [] >>
+    CCONTR_TAC >>
+    Cases_on `bip_less ip2.i ip1'.i`
+    >- (
+      `dominates prog ip2 ip1'` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+      Cases_on `bip_less ip2'.i ip1.i`
+      >- (
+        `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+        metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >>
+      Cases_on `bip_less ip1.i ip2'.i`
+      >- (
+        `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >>
+        metis_tac [dominates_antisym, dominates_trans, is_ssa_def])
+      >- (
+        `dominates prog ip1' ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >>
+        metis_tac [dominates_antisym, dominates_trans, is_ssa_def])) >>
+    Cases_on `bip_less ip1'.i ip2.i`
+    >- (
+      `dominates prog ip2 ip2'` by metis_tac [dominates_same_block] >>
+      Cases_on `bip_less ip2'.i ip1.i`
+      >- (
+        `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+        metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >>
+      Cases_on `bip_less ip1.i ip2'.i`
+      >- (
+        `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >>
+        metis_tac [dominates_antisym, dominates_trans, is_ssa_def])
+      >- (
+        `dominates prog ip2 ip1` by metis_tac [ip_equiv_dominates, bip_less_tri] >>
+        metis_tac [dominates_antisym, dominates_trans, is_ssa_def]))
+    >- (
+      `ip_equiv ip1' ip2` by metis_tac [bip_less_tri] >>
+      `dominates prog ip1 ip2'` by metis_tac [dominates_trans, ip_equiv_sym, ip_equiv_dominates] >>
+      Cases_on `bip_less ip2'.i ip1.i`
+      >- (
+        `dominates prog ip2' ip1` by metis_tac [same_block_dominates, loc_prog_ok_def] >>
+        metis_tac [dominates_trans, dominates_antisym, is_ssa_def]) >>
+      Cases_on `bip_less ip1.i ip2'.i`
+      >- (
+        `dominates prog ip2' ip2` by metis_tac [dominates_same_block] >>
+        `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, ip_equiv_sym] >>
+        metis_tac [dominates_antisym, is_ssa_def])
+      >- (
+        `dominates prog ip2' ip2` by metis_tac [ip_equiv_dominates2, bip_less_tri] >>
+        `dominates prog ip2 ip2'` by metis_tac [ip_equiv_dominates2, bip_less_tri] >>
+        metis_tac [dominates_antisym, is_ssa_def])))
+QED
+
+Theorem assigns_weak:
+  ∀l d p ip r. ~mem l (map fst p) ∧ r ∈ assigns p ip ⇒ r ∈ assigns ((l,d)::p) ip
+Proof
+  rw [assigns_cases, IN_DEF, get_instr_cases, PULL_EXISTS] >>
+  imp_res_tac ALOOKUP_MEM >>
+  fs [LIST_TO_SET_MAP] >> metis_tac [FST]
+QED
+
+Theorem uses_weak:
+  ∀l d p ip r. ip.f ≠ l ⇒ uses ((l,d)::p) ip = uses p ip
+Proof
+  rw [uses_cases, EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS]
+QED
+
+Theorem assigns_weak2:
+  ∀l d p ip r. ip.f ≠ l ⇒ assigns ((l,d)::p) ip = assigns p ip
+Proof
+  rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS]
+QED
+
+Theorem good_path_weak:
+  ∀l d p ip path. ip.f ≠ l ⇒ good_path ((l,d)::p) (ip::path) = good_path p (ip::path)
+Proof
+  Induct_on `path` >> rw [] >>
+  ONCE_REWRITE_TAC [good_path_cases] >> rw []
+  >- rw [EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS] >>
+  rename1 `good_path _ (p1::_)` >>
+  Cases_on `p1.f ≠ l`
+  >- (
+    first_x_assum drule >> rw [] >>
+    eq_tac >> rw [] >>
+    fs [next_ips_cases, EXTENSION, IN_DEF, get_instr_cases, PULL_EXISTS] >> rw [] >>
+    metis_tac [])
+  >- metis_tac [next_ips_same_func]
+QED
+
+Theorem dominates_weak:
+  ∀l d p ip1 ip2. ip1.f ≠ l ⇒ dominates ((l,d)::p) ip2 ip1 = dominates p ip2 ip1
+Proof
+  rw [dominates_def, EXTENSION, IN_DEF] >>
+  `(entry_ip ip1.f).f = ip1.f` by rw [entry_ip_def] >>
+  metis_tac [good_path_weak]
+QED
+
+Theorem uses_good_ip:
+  ∀r prog ip. r ∈ uses prog ip ⇒ mem ip.f (map fst prog)
+Proof
+  rw [uses_cases, IN_DEF, get_instr_cases] >>
+  imp_res_tac ALOOKUP_MEM >>
+  fs [LIST_TO_SET_MAP] >>
+  metis_tac [FST]
+QED
+
+Theorem is_ssa_weak:
+  ∀l d p. ~mem l (map fst p) ∧ is_ssa ((l,d)::p) ⇒ is_ssa p
+Proof
+  rw [is_ssa_def]
+  >- (first_x_assum irule >> rw [PULL_EXISTS] >> metis_tac [assigns_weak])
+  >- (
+    drule uses_good_ip >> rw [] >>
+    last_x_assum (qspec_then `ip1` mp_tac) >> rw [] >>
+    `ip1.f ≠ l` by metis_tac [MEM_MAP] >>
+    fs [uses_weak, assigns_weak2] >>
+    first_x_assum drule >> rw [] >>
+    qexists_tac `ip2` >> rw [] >> rfs [] >>
+    metis_tac [assigns_weak2, dominates_weak])
+  >- (
+    `get_instr ((l,d)::p) ip i`
+    by (fs [get_instr_cases, MEM_MAP] >> rw [] >> metis_tac [ALOOKUP_MEM, FST]) >>
+    first_x_assum drule >> rw [reachable_def] >>
+    qexists_tac `path` >> rw [] >>
+    `(entry_ip ip.f).f ≠ l` suffices_by metis_tac [good_path_weak] >>
+    rw [entry_ip_def] >> fs [get_instr_cases, MEM_MAP] >>
+    CCONTR_TAC >> fs [] >> rw [] >>
+    metis_tac [FST, ALOOKUP_MEM])
+QED
+
+Theorem loc_prog_ok_weak:
+  ∀l d p. ~mem l (map fst p) ∧ loc_prog_ok ((l,d)::p) ⇒ loc_prog_ok p
+Proof
+  rw [loc_prog_ok_def, MEM_MAP] >>
+  metis_tac [ALOOKUP_MEM, FST]
+QED
+
+Triviality in_uncurry:
+  (x,y) ∈ UNCURRY R ⇔ R x y
+Proof
+  rw [IN_DEF, UNCURRY_DEF]
+QED
+
+Theorem sorted_all_distinct_idx:
+  ∀R l. all_distinct l ∧ transitive R ∧ reflexive R ∧ antisym (rrestrict (UNCURRY R) (set l)) ⇒
+    (SORTED R l ⇔ (∀i j. i < length l ∧ j < length l ⇒ (R (el i l) (el j l) ⇔ i ≤ j)))
+Proof
+  Induct_on `l` >> rw [sortingTheory.SORTED_EQ] >>
+  `antisym (rrestrict (UNCURRY R) (set l))`
+  by (fs [antisym_def] >> rw [in_rrestrict]) >>
+  eq_tac >> rw []
+  >- (
+    Cases_on `i` >> Cases_on `j` >> rw [] >> fs []
+    >- fs [relationTheory.reflexive_def]
+    >- (first_x_assum irule >> rw [MEM_EL] >> metis_tac [])
+    >- (
+      fs [antisym_def] >>
+      last_x_assum (qspecl_then [`h`, `el n l`] mp_tac) >>
+      simp [in_rrestrict, in_uncurry] >> metis_tac [MEM_EL]))
+  >- (first_x_assum (qspecl_then [`Suc i`, `Suc j`] mp_tac) >> rw [])
+  >- (
+    fs [MEM_EL] >> rw [] >>
+    first_x_assum (qspecl_then [`0`, `Suc n`] mp_tac) >> rw [])
+QED
+
+Theorem lpc_uses_to_uses:
+  ∀r bs lip prog f d.
+    r ∈ lpc_uses (map snd bs) lip ∧
+    alookup prog (Fn f) = Some d ∧
+    PERM d.blocks bs ∧
+    all_distinct (map fst (d.blocks))
+    ⇒
+    r ∈ uses prog <| f := Fn f; b := fst (el (fst lip) bs); i := snd lip |> ∧
+    fst lip < length bs
+Proof
+  rw [IN_DEF, uses_cases, lpc_uses_cases, get_instr_cases, PULL_EXISTS,
+      lpc_get_instr_cases] >>
+  rw []
+  >- (
+    qexists_tac `el i' (map snd bs)` >> rw [] >>
+    irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >>
+    drule sortingTheory.MEM_PERM >> rw [MEM_EL, EL_MAP] >>
+    metis_tac [pair_CASES, FST, SND])
+  >- (
+    qexists_tac `phis` >>
+    qexists_tac `el i (map snd bs)` >> rw [] >>
+    qexists_tac `s` >> rw [] >>
+    irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >>
+    drule sortingTheory.MEM_PERM >> rw [MEM_EL, EL_MAP] >>
+    metis_tac [pair_CASES, FST, SND])
+QED
+
+Theorem assigns_to_block_assigns:
+  ∀prog ip d b r l.
+    r ∈ assigns prog ip ∧
+    alookup prog ip.f = Some d ∧
+    alookup d.blocks ip.b = Some b
+    ⇒
+    fst r ∈ block_assigns (l:label option, b)
+Proof
+  rw [] >>
+  qpat_x_assum `_ ∈ assigns _ _` mp_tac >>
+  simp [Once IN_DEF] >>
+  rw [assigns_cases, get_instr_cases, PULL_EXISTS, block_assigns_def]
+  >- (
+    disj2_tac >>
+    qexists_tac `r` >> HINT_EXISTS_TAC >>
+    metis_tac [MEM_EL])
+  >- (
+    rw [header_assigns_def, MEM_MAP] >>
+    disj1_tac >>
+    fs [MEM_MAP] >> rw [] >>
+    metis_tac [])
+QED
+
+Theorem assigns_to_lpc_assigns:
+  ∀prog ip d r idx (bs : (label option # block) list).
+    r ∈ assigns prog ip ∧
+    alookup prog ip.f = Some d ∧
+    alookup d.blocks ip.b = Some (snd (el idx bs)) ∧
+    idx < length bs
+    ⇒
+    r ∈ lpc_assigns (map snd bs) (idx, ip.i)
+Proof
+  rw [assigns_cases, get_instr_cases, PULL_EXISTS, block_assigns_def,
+      lpc_assigns_cases, IN_DEF, lpc_get_instr_cases] >>
+  fs [] >> rw [] >> fs [] >> rw [EL_MAP]
+QED
+
+Theorem uses_to_block_uses:
+  ∀prog ip d b r l.
+    r ∈ uses prog ip ∧
+    alookup prog ip.f = Some d ∧
+    alookup d.blocks ip.b = Some b
+    ⇒
+    r ∈ block_uses (l:label option, b)
+Proof
+  rw [] >>
+  qpat_x_assum `_ ∈ uses _ _` mp_tac >>
+  simp [Once IN_DEF] >>
+  rw [uses_cases, get_instr_cases, PULL_EXISTS, block_uses_def]
+  >- (
+    disj2_tac >>
+    metis_tac [MEM_EL])
+  >- (
+    rw [header_uses_def, MEM_MAP] >>
+    disj1_tac >>
+    fs [MEM_MAP] >> rw [] >>
+    metis_tac [])
+QED
+
+Theorem same_block_assigns_less_uses:
+  reachable prog ip1 ∧
+  dominates prog ip2 ip1 ∧
+  ip1.b = ip2.b ∧
+  (?i. get_instr prog ip1 i) ∧
+  (∀fname dec.
+       alookup prog fname = Some dec ⇒
+       every (λb. fst b = None ⇔ (snd b).h = Entry) dec.blocks)
+  ⇒
+  bip_less ip2.i ip1.i
+Proof
+  rw [] >> CCONTR_TAC >> fs [] >>
+  `ip1.f = ip2.f` by metis_tac [reachable_dominates_same_func] >>
+  `ip_equiv ip1 ip2 ∨ bip_less ip1.i ip2.i` by metis_tac [bip_less_tri]
+  >- metis_tac [ip_equiv_dominates2, dominates_irrefl, ip_equiv_sym] >>
+  metis_tac [dominates_antisym, same_block_dominates]
+QED
+
+Theorem ssa_to_dominator_ordered_lem:
+  ∀p1. loc_prog_ok p1 ∧ is_ssa p1 ∧ all_distinct (map fst p1) ∧ every (λ(l,d). all_distinct (map fst d.blocks)) p1 ⇒
+    ∃p2. list_rel (\(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 ∧
+         dominator_ordered p2
+Proof
+  Induct_on `p1` >> rw []
+  >- rw [dominator_ordered_def] >>
+  `is_ssa p1` by metis_tac [is_ssa_weak, pair_CASES, FST] >>
+  `loc_prog_ok p1` by metis_tac [loc_prog_ok_weak, pair_CASES, FST] >>
+  fs [PULL_EXISTS] >>
+  rename1 `is_ssa (x::_)` >>
+  `?l d. x = (l,d)` by metis_tac [pair_CASES] >>
+  `partial_order (rc (block_order d.blocks) (set d.blocks)) (set d.blocks)`
+  by metis_tac [block_order_po, ALOOKUP_def] >>
+  rw [] >>
+  `finite (set d.blocks)` by rw [] >>
+  drule finite_linear_order_of_finite_po >>
+  disch_then drule >> rw [] >>
+  drule finite_linear_order_to_list >>
+  disch_then drule >> rw [] >>
+  rename1 `set _ = set bs` >>
+  qexists_tac `(l, d with blocks := bs)` >>
+  qexists_tac `p2` >>
+  conj_asm1_tac >> rw [] >>
+  fs []
+  >- (irule sortingTheory.PERM_ALL_DISTINCT >> rw [] >> metis_tac [ALL_DISTINCT_MAP]) >>
+  qmatch_assum_abbrev_tac `SORTED R _` >>
+  `transitive R ∧ reflexive R ∧ antisym (rrestrict (UNCURRY R) (set bs))`
+  by (
+    fs [linear_order_def, transitive_def, reflexive_def, SUBSET_DEF,
+        antisym_def, domain_def, range_def, in_rrestrict] >>
+    rw [Abbr `R`, relationTheory.transitive_def, relationTheory.reflexive_def] >>
+    fs [IN_DEF] >> metis_tac []) >>
+  drule sorted_all_distinct_idx >>
+  disch_then drule >> rw [] >>
+  fs [dominator_ordered_def] >> rw [PULL_EXISTS] >> fs []
+  >- (
+    drule lpc_uses_to_uses >>
+    disch_then (qspecl_then [`(Fn f,d)::p1`, `f`, `d`] mp_tac) >>
+    rw [] >>
+    qmatch_assum_abbrev_tac `_ ∈ uses prog ip1` >>
+    `?ip2. ip2.f = Fn f ∧ r ∈ image fst (assigns prog ip2) ∧ dominates prog ip2 ip1`
+    by (fs [is_ssa_def] >> last_x_assum drule >> rw [Abbr `ip1`]) >>
+    `?idx. idx < length bs ∧ alookup d.blocks ip2.b = Some (snd (el idx bs)) ∧
+      fst (el idx bs) = ip2.b`
+    by (
+      fs [assigns_cases, IN_DEF, get_instr_cases, Abbr `prog`] >>
+      rfs [] >>
+      drule ALOOKUP_MEM >>
+      drule sortingTheory.MEM_PERM >>
+      rw [MEM_EL] >>
+      metis_tac [FST, SND]) >>
+    `?t. (r, t) ∈ assigns prog ip2` by metis_tac [IN_IMAGE, pair_CASES, FST] >>
+    drule assigns_to_block_assigns >> rw [Abbr `prog`] >>
+    qexists_tac `(idx, ip2.i)` >>
+    qexists_tac `(r, t)` >>
+    rw []
+    >- (
+      `(el idx bs, el (fst lip1) bs) ∈ rc (block_order d.blocks) (set d.blocks)`
+      by (
+        simp [rc_def, block_order_def, EL_MEM] >>
+        drule uses_to_block_uses >> simp [Abbr `ip1`] >>
+        `alookup d.blocks (fst (el (fst lip1) bs)) = Some (snd (el (fst lip1) bs))`
+        by (
+          qmatch_goalsub_abbrev_tac `(fst b)` >>
+          `mem b bs` by (rw [Abbr `b`, MEM_EL] >> metis_tac []) >>
+          metis_tac [ALOOKUP_ALL_DISTINCT_MEM, PAIR]) >>
+        rw [METIS_PROVE [] ``a ∨ b ⇔ ~b ⇒ a``] >>
+        simp [Once tc_cases] >>
+        disj1_tac >> rw [MEM_EL]
+        >- (
+          `all_distinct (map fst bs)`
+          by (
+            irule ALL_DISTINCT_MAP_INJ >> rw [] >>
+            `mem x d.blocks ∧ mem y d.blocks` by metis_tac [sortingTheory.MEM_PERM] >>
+            metis_tac [PAIR, ALOOKUP_ALL_DISTINCT_MEM, optionTheory.SOME_11]) >>
+          metis_tac [PAIR, optionTheory.SOME_11]) >>
+        metis_tac [PAIR, FST]) >>
+      rw [] >>
+      `idx ≤ fst lip1`
+      by (
+        `R (el idx bs) (el (fst lip1) bs)` suffices_by metis_tac [] >>
+        fs [Abbr `R`, SUBSET_DEF, rc_def] >> metis_tac []) >>
+      PairCases_on `lip1` >>
+      rw [linear_pc_less_def, LEX_DEF_THM] >> fs [LESS_OR_EQ] >>
+      rw [] >>
+      `reachable ((Fn f,d)::p1) ip1`
+      by (
+        fs [is_ssa_def] >> first_x_assum irule >>
+        fs [uses_cases, IN_DEF] >> metis_tac []) >>
+      drule same_block_assigns_less_uses >>
+      disch_then drule >> simp [Abbr `ip1`] >>
+      disch_then irule >> rw [] >>
+      fs [uses_cases, IN_DEF, loc_prog_ok_def] >>
+      metis_tac [])
+    >- (drule assigns_to_lpc_assigns >> simp []))
+  >- metis_tac []
+QED
+
+Theorem prog_ok_to_loc_prog_ok:
+  ∀p. prog_ok p ⇒ loc_prog_ok p
+Proof
+  rw [prog_ok_def, loc_prog_ok_def] >> metis_tac []
+QED
+
+Theorem alookup_perm_blocks:
+  ∀p1 p2.
+    list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2
+    ⇒
+    (∀l d. alookup p2 l = Some d ⇒ ?d'. alookup p1 l = Some d' ∧ PERM d'.blocks d.blocks) ∧
+    (∀l d. alookup p1 l = Some d ⇒ ?d'. alookup p2 l = Some d' ∧ PERM d.blocks d'.blocks) ∧
+    (map fst p1 = map fst p2)
+Proof
+  Induct_on `p1` >> rw [] >>
+  pairarg_tac >> fs [] >> pairarg_tac >> fs [] >> rw [] >> rw [] >> fs [] >>
+  metis_tac []
+QED
+
+Theorem alookup_perm:
+  ∀b1 b2. PERM b1 b2 ∧ all_distinct (map fst b1) ⇒ alookup b1 = alookup b2
+Proof
+  rw [] >>
+  irule ALOOKUP_ALL_DISTINCT_PERM_same >>
+  rw [sortingTheory.PERM_MAP, sortingTheory.PERM_LIST_TO_SET]
+QED
+
+Theorem get_instr_perm_blocks:
+  every (\(l,d). all_distinct (map fst d.blocks)) p1 ∧
+  list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2
+  ⇒
+  get_instr p1 = get_instr p2
+Proof
+  rw [get_instr_cases, FUN_EQ_THM] >>
+  eq_tac >> rw [] >>
+  drule alookup_perm_blocks >> rw [] >>
+  first_x_assum drule >> rw [] >> rw [] >>
+  `all_distinct (map fst d.blocks)`
+  by (
+    fs [EVERY_MEM] >>
+    imp_res_tac ALOOKUP_MEM >>
+    res_tac >> fs [] >>
+    metis_tac [sortingTheory.ALL_DISTINCT_PERM, sortingTheory.PERM_MAP]) >>
+  metis_tac [alookup_perm, sortingTheory.PERM_SYM]
+QED
+
+Theorem next_ips_perm_blocks:
+  every (\(l,d). all_distinct (map fst d.blocks)) p1 ∧
+  list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2
+  ⇒
+  next_ips p1 = next_ips p2
+Proof
+  rw [FUN_EQ_THM, next_ips_cases] >> metis_tac [get_instr_perm_blocks]
+QED
+
+Theorem good_path_perm_blocks:
+  ∀p1 p2.
+    every (\(l,d). all_distinct (map fst d.blocks)) p1 ∧
+    list_rel (λ(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2
+    ⇒
+    good_path p1 = good_path p2
+Proof
+  rw [] >> simp [FUN_EQ_THM] >>
+  Induct >> rw [] >>
+  ONCE_REWRITE_TAC [good_path_cases] >> rw [] >>
+  metis_tac [next_ips_perm_blocks, get_instr_perm_blocks]
+QED
+
+Theorem ssa_to_dominator_ordered:
+  ∀p1.
+    prog_ok p1 ∧ is_ssa p1
+    ⇒
+    ∃p2. list_rel (\(l1,d1) (l2,d2). l1 = l2 ∧ PERM d1.blocks d2.blocks) p1 p2 ∧
+         dominator_ordered p2 ∧ prog_ok p2 ∧ is_ssa p2
+Proof
+  rw [] >>
+  drule prog_ok_to_loc_prog_ok >> rw [] >>
+  drule ssa_to_dominator_ordered_lem >> simp [] >>
+  impl_tac
+  >- (
+    fs [prog_ok_def] >> rw [EVERY_MEM] >>
+    pairarg_tac >> fs [] >> rw [] >> metis_tac [ALOOKUP_ALL_DISTINCT_MEM]) >>
+  rw [] >>
+  qexists_tac `p2` >> rw [] >>
+  `every (λ(l,d). all_distinct (map fst d.blocks)) p1`
+  by fs [prog_ok_def] >>
+  drule get_instr_perm_blocks >> disch_then drule >> rw [] >>
+  drule good_path_perm_blocks >> disch_then drule >> rw []
+  >- (
+    drule alookup_perm_blocks >> rw [] >>
+    fs [prog_ok_def] >>
+    conj_tac
+    >- (
+      rw [] >> rpt (last_x_assum (qspec_then `fname` mp_tac)) >> rw [] >>
+      metis_tac [alookup_perm, sortingTheory.MEM_PERM, prog_ok_distinct_lem]) >>
+    conj_tac >- metis_tac [alookup_perm, sortingTheory.MEM_PERM, prog_ok_distinct_lem] >>
+    conj_tac >- (fs [EVERY_MEM] >> metis_tac [alookup_perm, sortingTheory.MEM_PERM]) >>
+    conj_tac
+    >- (
+      rfs [LIST_REL_EL_EQN, EVERY_EL] >> rw [] >>
+      pairarg_tac >> fs [] >>
+      rpt (first_x_assum (qspec_then `n` mp_tac)) >> rw [] >>
+      pairarg_tac >> fs [] >>
+      metis_tac [sortingTheory.ALL_DISTINCT_PERM, sortingTheory.PERM_MAP]) >>
+    conj_tac >- metis_tac [alookup_perm, sortingTheory.MEM_PERM]
+    >- metis_tac [alookup_perm, sortingTheory.MEM_PERM])
+  >- (
+    fs [is_ssa_def, IN_DEF, uses_cases, assigns_cases, reachable_def, dominates_def] >>
+    rw [] >>
+    first_x_assum irule >> metis_tac [])
+QED
+
 export_theory ();
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
index 65cc82f9e..9c5f36932 100644
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -31,6 +31,8 @@ Proof
   rw [prog_ok_def] >> rpt (first_x_assum drule) >>
   rw [] >> fs [EVERY_MEM] >> rw [] >>
   pairarg_tac >> rw [] >>
+  `mem (Fn f,d) prog` by metis_tac [ALOOKUP_MEM] >>
+  last_x_assum drule >> rw [] >> fs [] >>
   `alookup d.blocks l = Some b` by metis_tac [ALOOKUP_ALL_DISTINCT_MEM] >>
   last_x_assum drule >> rw [] >>
   CCONTR_TAC >> fs [] >>
@@ -42,6 +44,7 @@ Proof
   `~mem (el i b.body) (front b.body)` by metis_tac [] >>
   metis_tac [mem_el_front]
 QED
+
 Theorem prog_ok_nonterm:
   ∀prog i ip.
     prog_ok prog ∧ get_instr prog ip (Inl i) ∧ ¬terminator i ⇒ inc_pc ip ∈ next_ips prog ip
@@ -935,7 +938,14 @@ Proof
     imp_res_tac ALOOKUP_MEM >>
     fs [MEM_MAP] >>
     metis_tac [FST])
-  >- metis_tac [ALOOKUP_ALL_DISTINCT_MEM, prog_ok_def]
+  >- (
+    fs [prog_ok_def] >>
+    qexists_tac `prog` >> rw [] >>
+    irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >>
+    fs [EVERY_MEM] >>
+    `(λ(fname,dec). all_distinct (map fst dec.blocks)) (Fn f, d)`
+    by metis_tac [ALOOKUP_MEM] >>
+    fs [])
 QED
 
 Theorem alookup_translate_header_lab:
diff --git a/sledge/semantics/llvm_to_llair_sem_propScript.sml b/sledge/semantics/llvm_to_llair_sem_propScript.sml
index 30396d0be..c1ed339b7 100644
--- a/sledge/semantics/llvm_to_llair_sem_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_sem_propScript.sml
@@ -328,7 +328,7 @@ Proof
     first_x_assum drule >> simp [] >>
     disch_then (qspec_then `translate_reg r1 ty1` mp_tac) >> rw [] >>
     CCONTR_TAC >> fs [] >>
-    `ip2 = s.ip`
+    `ip_equiv ip2 s.ip`
     by (
       fs [is_ssa_def, EXTENSION, IN_DEF] >>
       Cases_on `r1` >> fs [translate_reg_def, untranslate_reg_def] >>
@@ -337,7 +337,7 @@ Proof
       `assigns prog s.ip (Reg reg, ty1)`
       suffices_by metis_tac [reachable_dominates_same_func, FST] >>
       metis_tac [EL_MEM, IN_DEF]) >>
-    metis_tac [dominates_irrefl]) >>
+    metis_tac [dominates_irrefl, ip_equiv_dominates2]) >>
   drule ALOOKUP_MEM >> rw [MEM_MAP, MEM_ZIP] >>
   metis_tac [EL_MEM, LIST_REL_LENGTH, LENGTH_MAP]
 QED
@@ -1493,9 +1493,10 @@ Proof
           >- (
             fs [reachable_def] >>
             qexists_tac `path ++ [<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>]` >>
-            rw_tac std_ss [good_path_append, GSYM APPEND] >> rw [] >>
-            rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >>
-            metis_tac [])))
+            rw_tac std_ss [good_path_append, GSYM APPEND] >> rw []
+            >- (rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >> metis_tac [])
+            >- metis_tac [ip_equiv_next_ips, ip_equiv_sym]
+            >- metis_tac [ip_equiv_refl])))
       >- fs [is_implemented_def]
       >- fs [is_implemented_def]
       >- ( (* Exit *)
@@ -1923,7 +1924,11 @@ Proof
     rw [] >>
     drule alookup_translate_blocks >> rpt (disch_then drule) >>
     impl_tac
-    >- metis_tac [ALOOKUP_ALL_DISTINCT_MEM, prog_ok_def] >>
+    >- (
+      fs [prog_ok_def, EVERY_MEM] >> rw [] >>
+      irule ALOOKUP_ALL_DISTINCT_MEM >> rw [] >>
+      imp_res_tac ALOOKUP_MEM >>
+      res_tac >> fs []) >>
     simp [translate_label_def] >>
     rw [] >> rw [dest_label_def, num_calls_def] >>
     rw [translate_instrs_take_to_call] >>
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index b890398e0..1dcb0efca 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -11,7 +11,8 @@
 open HolKernel boolLib bossLib Parse;
 open listTheory rich_listTheory arithmeticTheory integerTheory llistTheory pathTheory;
 open integer_wordTheory wordsTheory pred_setTheory alistTheory;
-open finite_mapTheory open logrootTheory numposrepTheory;
+open finite_mapTheory open logrootTheory numposrepTheory set_relationTheory;
+open sortingTheory;
 open settingsTheory;
 
 new_theory "misc";
@@ -965,4 +966,62 @@ Proof
   rw []
 QED
 
+(* ---- set_relation theorems ---- *)
+
+Theorem finite_imp_finite_prefixes:
+  ∀r s. finite s ∧ domain r ⊆ s ⇒ finite_prefixes r s
+Proof
+  rw [finite_prefixes_def] >>
+  irule SUBSET_FINITE_I >> fs [SUBSET_DEF, domain_def] >> metis_tac []
+QED
+
+Theorem finite_linear_order_of_finite_po:
+  ∀r s. finite s ∧ partial_order r s ⇒ ∃r'. linear_order r' s ∧ r ⊆ r'
+Proof
+  rw [] >>
+  `countable s` by metis_tac [finite_countable] >>
+  `finite_prefixes r s` by metis_tac [finite_imp_finite_prefixes, partial_order_def] >>
+  metis_tac [linear_order_of_countable_po]
+QED
+
+Theorem finite_linear_order_to_list:
+  ∀lo X. finite X ∧ linear_order lo X ⇒
+    ∃l. X = set l ∧ SORTED (λx y. (x, y) ∈ lo ∨ y ∉ X) l ∧ all_distinct l
+Proof
+  rw [] >>
+  qmatch_goalsub_abbrev_tac `SORTED R _` >>
+  qexists_tac `QSORT R (SET_TO_LIST X)` >> rw [SET_TO_LIST_INV]
+  >- rw [EXTENSION, QSORT_MEM]
+  >- (
+    irule QSORT_SORTED >>
+    rw [Abbr `R`, relationTheory.total_def]
+    >- (fs [linear_order_def] >> metis_tac []) >>
+    fs [linear_order_def, transitive_def, relationTheory.transitive_def,
+        domain_def, range_def, SUBSET_DEF] >>
+    rw [] >> metis_tac [])
+  >- metis_tac [ALL_DISTINCT_SET_TO_LIST, ALL_DISTINCT_PERM, QSORT_PERM]
+QED
+
+Definition rc_def:
+  rc R s = R ∪ {(x,x) | x ∈ s}
+End
+
+Theorem rc_is_reflexive:
+  ∀R s. reflexive (rc R s) s
+Proof
+  rw [rc_def, reflexive_def]
+QED
+
+Theorem transitive_rc:
+  ∀R s. transitive R ⇒ transitive (rc R s)
+Proof
+  rw [rc_def, transitive_def] >> metis_tac []
+QED
+
+Theorem antisym_rc:
+  ∀R s. antisym (rc R s) ⇔ antisym R
+Proof
+  rw [rc_def, antisym_def] >> metis_tac []
+QED
+
 export_theory ();