diff --git a/pancake/proofs/crep_to_loopProofScript.sml b/pancake/proofs/crep_to_loopProofScript.sml
index 0da3316552..9f783a7519 100644
--- a/pancake/proofs/crep_to_loopProofScript.sml
+++ b/pancake/proofs/crep_to_loopProofScript.sml
@@ -5444,5 +5444,16 @@ Proof
   gs [loop_liveTheory.mark_all_def]
 QED
 
+(* first_name offset *)
+
+Theorem crep_to_loop_compile_prog_lab_min:
+  crep_to_loop$compile_prog cprog = lprog ⇒
+  EVERY (λprog. 60 ≤ FST prog) lprog
+Proof
+  gs[crep_to_loopTheory.compile_prog_def]>>
+  gs[MAP2_MAP, EVERY_MEM]>>
+  rpt strip_tac>>gvs[MEM_MAP,MEM_ZIP]>>
+  pairarg_tac>>gs[crep_to_loopTheory.first_name_def]
+QED
 
 val _ = export_theory();
diff --git a/pancake/proofs/loop_removeProofScript.sml b/pancake/proofs/loop_removeProofScript.sml
index 708ea3cd07..31ed86cc00 100644
--- a/pancake/proofs/loop_removeProofScript.sml
+++ b/pancake/proofs/loop_removeProofScript.sml
@@ -1863,4 +1863,85 @@ Proof
   fs []
 QED
 
+(* first_name offset *)
+
+Theorem store_const_lab_min:
+  x ≤ FST prog ∧
+  EVERY (λp. x ≤ FST p) (SND prog) ∧
+  store_cont s cont prog = (cont',prog') ⇒
+  x ≤ FST prog' ∧ EVERY (λp. x ≤ FST p) (SND prog')
+Proof
+  strip_tac>>
+  PairCases_on ‘prog’>>
+  gs[loop_removeTheory.store_cont_def]>>
+  rveq>>
+  gs[EVERY_MEM]>>strip_tac>>strip_tac>>rveq>>gs[]
+QED
+
+Theorem comp_with_loop_lab_min:
+  comp_with_loop p p' cont prog = (q2, s')∧
+  x ≤ FST prog ∧
+  EVERY (λp. x ≤ FST p) (SND prog) ⇒
+  (x ≤ FST s' ∧ EVERY (λp. x ≤ FST p) (SND s'))
+Proof
+  MAP_EVERY qid_spec_tac [‘s'’, ‘q2’, ‘prog’, ‘cont’, ‘p'’, ‘p’]>>
+  recInduct loop_removeTheory.comp_with_loop_ind>>rw[]>>
+  qpat_x_assum ‘comp_with_loop _ _ _ _ = _’ mp_tac>>
+  rewrite_tac[loop_removeTheory.comp_with_loop_def]>>
+  strip_tac>>fs[]>>
+  rpt (pairarg_tac>>fs[])
+  >- metis_tac[store_const_lab_min]
+  >- metis_tac[store_const_lab_min]
+  >- (Cases_on ‘handler’>>fs[]>>
+      PairCases_on ‘x'’>>fs[]>>
+      rpt (pairarg_tac>>fs[])>>
+      metis_tac[store_const_lab_min])
+  >- (Cases_on ‘handler’>>fs[]>>
+      PairCases_on ‘x'’>>fs[]>>
+      rpt (pairarg_tac>>fs[])>>
+      metis_tac[store_const_lab_min])>>
+  rveq>>gs[]>>
+  drule_all store_const_lab_min>>
+  strip_tac>>gs[]
+QED
+
+Theorem FOLDR_min:
+  EVERY (λp. x ≤ FST p) prog ∧ prog ≠ [] ⇒
+  x ≤ FOLDR MAX 0 (MAP FST prog)
+Proof
+  Induct_on ‘prog’>>gs[]
+QED
+
+Theorem loop_remove_comp_lab_min:
+  FOLDR comp (m + 1,[]) prog = (n, prog') ∧
+  (prog ≠ [] ⇒ x ≤ m) ∧
+  EVERY (λp. x ≤ FST p) prog ⇒
+  (prog ≠[] ⇒ x ≤ n) ∧ EVERY (λp. x ≤ FST p) prog'
+Proof
+  MAP_EVERY qid_spec_tac [‘n’, ‘m’, ‘prog'’, ‘prog’]>>
+  Induct>>gs[]>>ntac 5 strip_tac>>
+  PairCases_on ‘h’>>gs[loop_removeTheory.comp_def]>>
+  pairarg_tac>>gs[]>>rveq>>gs[]>>
+  drule comp_with_loop_lab_min>>
+  disch_then $ qspec_then ‘x’ mp_tac>>
+  qmatch_goalsub_abbrev_tac ‘FST xxx’>>
+  Cases_on ‘xxx’>>gs[]>>
+  first_x_assum $ qspecl_then [‘r’, ‘m’, ‘q’] assume_tac>>
+  gs[]>>
+  Cases_on ‘prog’>>gs[]
+QED
+
+Theorem loop_remove_comp_prog_lab_min:
+  comp_prog prog = prog' ∧
+  EVERY (λp. x ≤ FST p) prog ⇒
+  EVERY (λp. x ≤ FST p) prog'
+Proof
+  gs[loop_removeTheory.comp_prog_def]>>strip_tac>>
+  qmatch_asmsub_abbrev_tac ‘SND xxx’>>
+  Cases_on ‘xxx’>>gs[]>>
+  drule loop_remove_comp_lab_min>>
+  disch_then $ qspec_then ‘x’ mp_tac>>gs[]>>
+  impl_tac >-metis_tac[FOLDR_min]>>rw[]
+QED
+
 val _ = export_theory();
diff --git a/pancake/proofs/loop_to_wordProofScript.sml b/pancake/proofs/loop_to_wordProofScript.sml
index 372c9ea21f..531e7e26d2 100644
--- a/pancake/proofs/loop_to_wordProofScript.sml
+++ b/pancake/proofs/loop_to_wordProofScript.sml
@@ -1485,4 +1485,511 @@ Proof
   rveq >> fs [EVERY_DEF]
 QED
 
+(*** no_install/no_alloc/no_mt lemmas ***)
+
+Theorem loop_to_word_comp_no_install:
+  wprog = comp ctxt prog l ⇒
+  no_install (FST wprog)
+Proof
+  MAP_EVERY qid_spec_tac [‘wprog’, ‘l’, ‘prog’, ‘ctxt’]>>
+  recInduct comp_ind>>
+  gs[comp_def, wordPropsTheory.no_install_def]>>
+  rw[]>>
+  TRY (pairarg_tac>>gs[]>>
+       pairarg_tac>>gs[]>>
+       gs[wordPropsTheory.no_install_def])>>
+  rpt (CASE_TAC>>gs[wordPropsTheory.no_install_def])>>
+  rpt (pairarg_tac>>gs[wordPropsTheory.no_install_def])
+QED
+
+Theorem loop_to_word_comp_func_no_install:
+  no_install (comp_func name params body)
+Proof
+  MAP_EVERY qid_spec_tac [‘wprog’, ‘name’, ‘params’, ‘body’]>>Induct>>
+  gs[comp_func_def]>>
+  gs[comp_def, wordPropsTheory.no_install_def]>>
+  rw[loop_to_word_comp_no_install]>>
+  rpt (last_x_assum (qspecl_then [‘params’, ‘name’] assume_tac)>>
+       gs[loopLangTheory.acc_vars_def])>>
+  rpt (CASE_TAC>>gs[wordPropsTheory.no_install_def])>>
+  pairarg_tac>>gs[]>>
+  pairarg_tac>>
+  gs[wordPropsTheory.no_install_def]>>
+  rpt (qpat_x_assum ‘comp _ _ _ = _’ (assume_tac o GSYM))>>
+  drule loop_to_word_comp_no_install>>gs[]>>
+  qpat_x_assum ‘(p1, _) = _’ kall_tac>>
+  drule loop_to_word_comp_no_install>>gs[]
+QED
+
+Theorem loop_to_word_compile_no_install:
+  wprog = compile_prog pan_prog ⇒
+  EVERY no_install (MAP (SND o SND) wprog)
+Proof
+  qid_spec_tac ‘wprog’>>
+  Induct_on ‘pan_prog’>>
+  gs[compile_def, compile_prog_def]>>
+  strip_tac>>pairarg_tac>>gs[loop_to_word_comp_func_no_install]
+QED
+
+Theorem loop_compile_no_install_code:
+  compile prog = prog' ⇒
+  no_install_code (fromAList prog')
+Proof
+  disch_then (assume_tac o GSYM)>>
+  gs[compile_def]>>
+  drule loop_to_word_compile_no_install>>
+  rw[wordPropsTheory.no_install_code_def]>>
+  gs[lookup_fromAList, EVERY_MEM, MEM_MAP]>>
+  drule ALOOKUP_MEM>>strip_tac>>
+  first_x_assum (qspec_then ‘p’ assume_tac)>>
+  res_tac>>gs[]
+QED
+
+Theorem loop_to_word_comp_no_alloc:
+  wprog = comp ctxt prog l ⇒
+  no_alloc (FST wprog)
+Proof
+  MAP_EVERY qid_spec_tac [‘wprog’, ‘l’, ‘prog’, ‘ctxt’]>>
+  recInduct comp_ind>>
+  gs[comp_def, wordPropsTheory.no_alloc_def]>>
+  rw[]>>
+  TRY (pairarg_tac>>gs[]>>
+       pairarg_tac>>gs[]>>
+       gs[wordPropsTheory.no_alloc_def])>>
+  rpt (CASE_TAC>>gs[wordPropsTheory.no_alloc_def])>>
+  rpt (pairarg_tac>>gs[wordPropsTheory.no_alloc_def])
+QED
+
+Theorem loop_to_word_comp_func_no_alloc:
+  no_alloc (comp_func name params body)
+Proof
+  MAP_EVERY qid_spec_tac [‘wprog’, ‘name’, ‘params’, ‘body’]>>Induct>>
+  gs[comp_func_def]>>
+  gs[comp_def, wordPropsTheory.no_alloc_def]>>
+  rw[loop_to_word_comp_no_alloc]>>
+  rpt (last_x_assum (qspecl_then [‘params’, ‘name’] assume_tac)>>
+       gs[loopLangTheory.acc_vars_def])>>
+  rpt (CASE_TAC>>gs[wordPropsTheory.no_alloc_def])>>
+  pairarg_tac>>gs[]>>
+  pairarg_tac>>
+  gs[wordPropsTheory.no_alloc_def]>>
+  rpt (qpat_x_assum ‘comp _ _ _ = _’ (assume_tac o GSYM))>>
+  drule loop_to_word_comp_no_alloc>>gs[]>>
+  qpat_x_assum ‘(p1, _) = _’ kall_tac>>
+  drule loop_to_word_comp_no_alloc>>gs[]
+QED
+
+Theorem loop_to_word_compile_no_alloc:
+  wprog = compile_prog pan_prog ⇒
+  EVERY no_alloc (MAP (SND o SND) wprog)
+Proof
+  qid_spec_tac ‘wprog’>>
+  Induct_on ‘pan_prog’>>
+  gs[compile_def, compile_prog_def]>>
+  strip_tac>>pairarg_tac>>gs[loop_to_word_comp_func_no_alloc]
+QED
+
+Theorem loop_compile_no_alloc_code:
+  compile prog = prog' ⇒
+  no_alloc_code (fromAList prog')
+Proof
+  disch_then (assume_tac o GSYM)>>
+  gs[compile_def]>>
+  drule loop_to_word_compile_no_alloc>>
+  rw[wordPropsTheory.no_alloc_code_def]>>
+  gs[lookup_fromAList, EVERY_MEM, MEM_MAP]>>
+  drule ALOOKUP_MEM>>strip_tac>>
+  first_x_assum (qspec_then ‘p’ assume_tac)>>
+  res_tac>>gs[]
+QED
+
+Theorem loop_to_word_comp_no_mt:
+  wprog = comp ctxt prog l ⇒
+  no_mt (FST wprog)
+Proof
+  MAP_EVERY qid_spec_tac [‘wprog’, ‘l’, ‘prog’, ‘ctxt’]>>
+  recInduct comp_ind>>
+  gs[comp_def, wordPropsTheory.no_mt_def]>>
+  rw[]>>
+  TRY (pairarg_tac>>gs[]>>
+       pairarg_tac>>gs[]>>
+       gs[wordPropsTheory.no_mt_def])>>
+  rpt (CASE_TAC>>gs[wordPropsTheory.no_mt_def])>>
+  rpt (pairarg_tac>>gs[wordPropsTheory.no_mt_def])
+QED
+
+Theorem loop_to_word_comp_func_no_mt:
+  no_mt (comp_func name params body)
+Proof
+  MAP_EVERY qid_spec_tac [‘wprog’, ‘name’, ‘params’, ‘body’]>>Induct>>
+  gs[comp_func_def]>>
+  gs[comp_def, wordPropsTheory.no_mt_def]>>
+  rw[loop_to_word_comp_no_mt]>>
+  rpt (last_x_assum (qspecl_then [‘params’, ‘name’] assume_tac)>>
+       gs[loopLangTheory.acc_vars_def])>>
+  rpt (CASE_TAC>>gs[wordPropsTheory.no_mt_def])>>
+  pairarg_tac>>gs[]>>
+  pairarg_tac>>
+  gs[wordPropsTheory.no_mt_def]>>
+  rpt (qpat_x_assum ‘comp _ _ _ = _’ (assume_tac o GSYM))>>
+  drule loop_to_word_comp_no_mt>>gs[]>>
+  qpat_x_assum ‘(p1, _) = _’ kall_tac>>
+  drule loop_to_word_comp_no_mt>>gs[]
+QED
+
+Theorem loop_to_word_compile_no_mt:
+  wprog = compile_prog pan_prog ⇒
+  EVERY no_mt (MAP (SND o SND) wprog)
+Proof
+  qid_spec_tac ‘wprog’>>
+  Induct_on ‘pan_prog’>>
+  gs[compile_def, compile_prog_def]>>
+  strip_tac>>pairarg_tac>>gs[loop_to_word_comp_func_no_mt]
+QED
+
+Theorem loop_compile_no_mt_code:
+  compile prog = prog' ⇒
+  no_mt_code (fromAList prog')
+Proof
+  disch_then (assume_tac o GSYM)>>
+  gs[compile_def]>>
+  drule loop_to_word_compile_no_mt>>
+  rw[wordPropsTheory.no_mt_code_def]>>
+  gs[lookup_fromAList, EVERY_MEM, MEM_MAP]>>
+  drule ALOOKUP_MEM>>strip_tac>>
+  first_x_assum (qspec_then ‘p’ assume_tac)>>
+  res_tac>>gs[]
+QED
+
+(*** loop_to_word good_handlers ***)
+
+Theorem comp_l_invariant:
+  ∀ctxt prog l prog' l'. comp ctxt prog l = (prog',l') ⇒ FST l' = FST l
+Proof
+  ho_match_mp_tac comp_ind >>
+  rw[comp_def] >>
+  gvs[ELIM_UNCURRY,PULL_FORALL,AllCaseEqs()] >> metis_tac[PAIR]
+QED
+
+Theorem good_handlers_comp:
+  ∀ctxt prog l. good_handlers (FST l) (FST (comp ctxt prog l))
+Proof
+  ho_match_mp_tac comp_ind >>
+  rw[wordPropsTheory.good_handlers_def,
+     comp_def] >>
+  gvs[ELIM_UNCURRY] >>
+  rpt(PURE_TOP_CASE_TAC >> gvs[]) >>
+  metis_tac[PAIR,FST,SND,comp_l_invariant]
+QED
+
+Theorem loop_to_word_good_handlers:
+  (compile_prog prog) = prog' ⇒
+  EVERY (λ(n,m,pp). good_handlers n pp) prog'
+Proof
+  fs[compile_def,
+     compile_prog_def,
+     comp_func_def]>>
+  rw[]>>
+  fs[EVERY_MEM,MEM_MAP,PULL_EXISTS]>>
+  PairCases >>
+  rw[] >>
+  pop_assum kall_tac >>
+  rename1 ‘comp ctxt prog’ >>
+  rename1 ‘(n,m)’ >>
+  metis_tac[PAIR,FST,SND,good_handlers_comp]
+QED
+
+(**** lab_pres for loop_to_word ****)
+
+Theorem loop_to_word_comp_SND_LE:
+  ∀ctxt prog l p r.
+    comp ctxt prog l = (p,r) ⇒
+    SND l ≤ SND r
+Proof
+  ho_match_mp_tac loop_to_wordTheory.comp_ind>>
+  rw[loop_to_wordTheory.comp_def]>>
+  rpt (FULL_CASE_TAC>>gs[])>>gvs[]>>
+  pairarg_tac>>gs[]>>pairarg_tac>>gs[]>>
+  rveq>>gs[]
+QED
+
+Theorem loop_to_word_comp_extract_labels_len:
+  ∀ctxt prog l p r.
+    comp ctxt prog l = (p,r) ⇒
+    LENGTH (extract_labels p) = SND r - SND l
+Proof
+  ho_match_mp_tac loop_to_wordTheory.comp_ind>>
+  rw[loop_to_wordTheory.comp_def]>>
+  gs[wordPropsTheory.extract_labels_def]
+  >- (pairarg_tac>>gs[]>>
+      pairarg_tac>>gs[]>>
+      rveq>>gs[wordPropsTheory.extract_labels_def]>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      qpat_x_assum ‘_= (_, l')’ assume_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      gs[])
+  >- (pairarg_tac>>gs[]>>
+      pairarg_tac>>gs[]>>
+      rveq>>gs[wordPropsTheory.extract_labels_def]>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      qpat_x_assum ‘_= (_, l')’ assume_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      gs[])>>
+  rpt (FULL_CASE_TAC>>gs[])>>
+  rveq>>gs[wordPropsTheory.extract_labels_def]
+  >~[‘LENGTH _ = 1’]>- (Cases_on ‘l’>>gs[])>>
+  pairarg_tac>>gs[]>>pairarg_tac>>gs[]>>
+  rveq>>gs[wordPropsTheory.extract_labels_def]>>
+  Cases_on ‘l’>>gs[]>>
+  rename1 ‘comp _ _ l1 = (_, l1')’>>
+  Cases_on ‘l1'’>>gs[]>>
+  drule loop_to_word_comp_SND_LE>>strip_tac>>gs[]>>
+  qpat_x_assum ‘_= (_, l1)’ assume_tac>>
+  drule loop_to_word_comp_SND_LE>>strip_tac>>gs[]
+QED
+
+Theorem loop_to_word_comp_extract_labels:
+  ∀ctxt prog l p l'.
+    loop_to_word$comp ctxt prog l = (p,l') ⇒
+    EVERY (λ(q, r). q = FST l ∧ SND l ≤ r ∧ r < SND l') (extract_labels p)
+Proof
+  ho_match_mp_tac loop_to_wordTheory.comp_ind>>
+  rw[loop_to_wordTheory.comp_def]>>
+  gs[wordPropsTheory.extract_labels_def]
+  >- (pairarg_tac>>gs[]>>
+      pairarg_tac>>gs[]>>
+      rveq>>gs[wordPropsTheory.extract_labels_def]>>
+      ‘FST l'' = FST l’ by metis_tac[comp_l_invariant]>>gs[]>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      qpat_x_assum ‘_= (_, l'')’ assume_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      conj_tac>>gs[EVERY_EL]>>strip_tac>>strip_tac>>pairarg_tac>>gs[]
+      >- (first_x_assum $ qspec_then ‘n’ assume_tac>>gs[])>>
+      last_x_assum $ qspec_then ‘n’ assume_tac>>gs[])
+  >- (pairarg_tac>>gs[]>>
+      pairarg_tac>>gs[]>>
+      rveq>>gs[wordPropsTheory.extract_labels_def]>>
+      ‘FST l'' = FST l’ by metis_tac[comp_l_invariant]>>gs[]>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      qpat_x_assum ‘_= (_, l'')’ assume_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      conj_tac>>gs[EVERY_EL]>>strip_tac>>strip_tac>>pairarg_tac>>gs[]
+      >- (first_x_assum $ qspec_then ‘n’ assume_tac>>gs[])>>
+      last_x_assum $ qspec_then ‘n’ assume_tac>>gs[])>>
+  gs[CaseEq"option",CaseEq"prod"]>>rpt (pairarg_tac>>gs[])>>
+  gvs[wordPropsTheory.extract_labels_def]>>
+  Cases_on ‘l’>>gs[]>>
+  rename1 ‘comp _ _ l1 = (_, l1')’>>
+  Cases_on ‘l1'’>>gs[]>>
+  drule loop_to_word_comp_SND_LE>>strip_tac>>gs[]>>
+  qpat_x_assum ‘_= (_, l1)’ assume_tac>>
+  drule loop_to_word_comp_SND_LE>>strip_tac>>gs[]>>
+  Cases_on ‘l1’>>gs[]>>
+  drule comp_l_invariant>>gs[]>>
+  strip_tac>>gs[]>>
+  qpat_x_assum ‘_= (_, _, r')’ assume_tac>>
+  drule comp_l_invariant>>gs[]>>strip_tac>>
+  conj_tac>>gs[EVERY_EL]>>strip_tac>>strip_tac>>pairarg_tac>>gs[]
+  >- (last_x_assum $ qspec_then ‘n’ assume_tac>>gs[])>>
+  first_x_assum $ qspec_then ‘n’ assume_tac>>gs[]
+QED
+
+Theorem loop_to_word_comp_ALL_DISTINCT:
+  ∀ctxt prog l p r.
+    comp ctxt prog l = (p,r) ⇒
+    ALL_DISTINCT (extract_labels p)
+Proof
+  ho_match_mp_tac loop_to_wordTheory.comp_ind>>
+  rw[loop_to_wordTheory.comp_def]>>
+  gs[wordPropsTheory.extract_labels_def]
+  >- (pairarg_tac>>gs[]>>
+      pairarg_tac>>gs[]>>
+      rveq>>
+      gs[wordPropsTheory.extract_labels_def,
+         ALL_DISTINCT_APPEND]>>rpt strip_tac>>
+      drule loop_to_word_comp_extract_labels>>strip_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      qpat_x_assum ‘_= (_, l')’ assume_tac>>
+      drule loop_to_word_comp_extract_labels>>strip_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      gs[EVERY_MEM]>>
+      rpt (first_x_assum $ qspec_then ‘e’ assume_tac)>>gs[]>>
+      Cases_on ‘e’>>gs[])
+  >- (pairarg_tac>>gs[]>>
+      pairarg_tac>>gs[]>>
+      rveq>>
+      gs[wordPropsTheory.extract_labels_def,
+         ALL_DISTINCT_APPEND]>>rpt strip_tac>>
+      drule loop_to_word_comp_extract_labels>>strip_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      qpat_x_assum ‘_= (_, l')’ assume_tac>>
+      drule loop_to_word_comp_extract_labels>>strip_tac>>
+      drule loop_to_word_comp_SND_LE>>strip_tac>>
+      gs[EVERY_MEM]>>
+      rpt (first_x_assum $ qspec_then ‘e’ assume_tac)>>gs[]>>
+      Cases_on ‘e’>>gs[])>>
+  rename1 ‘_ = (q, r)’>>
+  gs[CaseEq"option", CaseEq"prod"]>>
+  rpt (pairarg_tac>>gs[])>>
+  gvs[wordPropsTheory.extract_labels_def]>>
+  Cases_on ‘l’>>gs[]>>
+  rename1 ‘comp _ _ l1 = (_, l1')’>>
+  Cases_on ‘l1'’>>gs[]>>
+  rename1 ‘comp _ _ l1 = (_, q', r')’>>
+  drule loop_to_word_comp_extract_labels>>strip_tac>>
+  drule loop_to_word_comp_SND_LE>>strip_tac>>
+  rename1 ‘_= (p1', l1)’>>
+  qpat_x_assum ‘_= (p1', l1)’ assume_tac>>
+  drule loop_to_word_comp_extract_labels>>strip_tac>>
+  drule loop_to_word_comp_SND_LE>>strip_tac>>
+  gs[]>>
+  Cases_on ‘l1’>>gs[]>>
+  gs[ALL_DISTINCT_APPEND, EVERY_MEM]>>rw[]
+  >- (last_x_assum $ qspec_then ‘(q, r)’ assume_tac>>gs[])
+  >- (first_x_assum $ qspec_then ‘(q, r)’ assume_tac>>gs[])
+  >- (last_x_assum $ qspec_then ‘(q', r')’ assume_tac>>gs[])
+  >- (first_x_assum $ qspec_then ‘(q', r')’ assume_tac>>gs[])>>
+  first_x_assum $ qspec_then ‘e’ assume_tac>>gs[]>>
+  first_x_assum $ qspec_then ‘e’ assume_tac>>gs[]>>
+  Cases_on ‘e’>>gs[]
+QED
+
+Theorem loop_to_word_comp_func_lab_pres:
+    comp_func n' params body = p ⇒
+    (∀n. n < LENGTH (extract_labels p) ⇒
+         (λ(l1,l2). l1 = n' ∧ l2 ≠ 0 ∧ l2 ≠ 1)
+         (EL n (extract_labels p))) ∧
+    ALL_DISTINCT (extract_labels p)
+Proof
+  strip_tac>>
+  gs[loop_to_wordTheory.comp_func_def]>>
+  qmatch_asmsub_abbrev_tac ‘FST cmp = _’>>
+  Cases_on ‘cmp’>>gs[]>>
+  drule loop_to_word_comp_extract_labels>>strip_tac>>
+  drule loop_to_word_comp_ALL_DISTINCT>>strip_tac>>
+  gs[]>>rpt strip_tac>>
+  gs[EVERY_EL]>>
+  first_x_assum $ qspec_then ‘n’ assume_tac>>gs[]>>
+  pairarg_tac>>gs[]
+QED
+
+Theorem loop_to_word_compile_prog_lab_pres:
+  loop_to_word$compile_prog prog = prog' ⇒
+  EVERY
+  (λ(n,m,p).
+     (let
+        labs = extract_labels p
+      in
+        EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) labs ∧
+        ALL_DISTINCT labs)) prog'
+Proof
+  strip_tac>>
+  gs[loop_to_wordTheory.compile_prog_def]>>
+  gs[EVERY_EL]>>ntac 2 strip_tac>>
+  pairarg_tac>>gs[]>>rveq>>gs[EL_MAP]>>
+  pairarg_tac>>gs[]>>
+  drule loop_to_word_comp_func_lab_pres>>rw[]
+QED
+
+(* first_name offset *)
+
+Theorem loop_to_word_compile_prog_FST_eq:
+  compile_prog prog = prog' ⇒
+  MAP FST prog' = MAP FST prog
+Proof
+  strip_tac>>gs[loop_to_wordTheory.compile_prog_def]>>
+  ‘LENGTH prog = LENGTH prog'’ by (rveq>>gs[LENGTH_MAP])>>
+  gs[MAP_EQ_EVERY2]>>gs[LIST_REL_EL_EQN]>>
+  strip_tac>>strip_tac>>gs[]>>rveq>>gs[EL_MAP]>>
+  pairarg_tac>>gs[]
+QED
+
+Theorem loop_to_word_compile_prog_lab_min:
+  compile_prog prog = prog' ∧
+  EVERY (λp. x ≤ FST p) prog ⇒
+  EVERY (λp. x ≤ FST p) prog'
+Proof
+  strip_tac>>
+  drule loop_to_word_compile_prog_FST_eq>>gs[GSYM EVERY_MAP]
+QED
+
+Theorem loop_to_word_compile_lab_min:
+  compile prog = prog' ∧
+  EVERY (λp. x ≤ FST p) prog ⇒
+  EVERY (λp. x ≤ FST p) prog'
+Proof
+  strip_tac>>
+  gs[loop_to_wordTheory.compile_def]>>
+  drule_then irule loop_to_word_compile_prog_lab_min>>
+  gs[]>>irule loop_removeProofTheory.loop_remove_comp_prog_lab_min>>
+  metis_tac[]
+QED
+
+(* inst_ok_less *)
+
+Theorem full_imp_inst_ok_less:
+  ∀c prog.
+    full_inst_ok_less c prog ⇒
+    every_inst (inst_ok_less c) prog
+Proof
+  recInduct wordPropsTheory.full_inst_ok_less_ind>>
+  rw[wordPropsTheory.full_inst_ok_less_def,
+     wordPropsTheory.inst_ok_less_def,
+     wordPropsTheory.every_inst_def]>>
+  Cases_on ‘ret’>-gs[]>>
+  rename1 ‘SOME x’>>PairCases_on ‘x’>>gs[]>>
+  Cases_on ‘handler’>-gs[]>>
+  rename1 ‘SOME x’>>PairCases_on ‘x’>>gs[]
+QED
+
+Theorem loop_to_word_comp_every_inst_ok_less:
+  ∀ctxt prog l.
+    byte_offset_ok c 0w ⇒
+    every_inst (inst_ok_less c) (FST (comp ctxt prog l))
+Proof
+  ho_match_mp_tac loop_to_wordTheory.comp_ind >>
+  rw[loop_to_wordTheory.comp_def,
+     wordPropsTheory.every_inst_def,
+     wordPropsTheory.inst_ok_less_def] >>
+  TRY (Cases_on ‘ret’>-gs[wordPropsTheory.every_inst_def]>>
+       rename1 ‘SOME x’>>PairCases_on ‘x’>>gs[]>>
+       Cases_on ‘handler’>-gs[wordPropsTheory.every_inst_def]>>
+       rename1 ‘SOME x’>>PairCases_on ‘x’)>>
+  gs[]>>rpt (pairarg_tac>>gs[])>>
+  gs[wordPropsTheory.every_inst_def]
+QED
+
+Theorem loop_to_word_comp_func_every_inst_ok_less:
+  comp_func n params body = p ∧
+  byte_offset_ok c 0w ⇒
+  every_inst (inst_ok_less c) p
+Proof
+  strip_tac>>gs[loop_to_wordTheory.comp_func_def]>>
+  rveq>>
+  drule_then irule loop_to_word_comp_every_inst_ok_less
+QED
+
+Theorem loop_to_word_compile_prog_every_inst_ok_less:
+  compile_prog lprog = wprog0 ∧
+  byte_offset_ok c 0w ⇒
+  EVERY (λ(n,m,p). every_inst (inst_ok_less c) p) wprog0
+Proof
+  strip_tac>>gs[loop_to_wordTheory.compile_prog_def]>>
+  rveq>>gs[EVERY_MAP, EVERY_EL]>>rpt strip_tac>>
+  pairarg_tac>>gs[]>>
+  pairarg_tac>>gs[]>>
+  drule_then irule loop_to_word_comp_func_every_inst_ok_less>>
+  gs[]
+QED
+
+Theorem loop_to_word_every_inst_ok_less:
+  compile lprog = wprog0 ∧
+  byte_offset_ok c 0w ⇒
+  EVERY (λ(n,m,p). every_inst (inst_ok_less c) p) wprog0
+Proof
+  strip_tac>>gs[loop_to_wordTheory.compile_def]>>
+  drule_then irule loop_to_word_compile_prog_every_inst_ok_less>>
+  gs[]
+QED
+
 val _ = export_theory();
diff --git a/pancake/proofs/pan_to_targetProofScript.sml b/pancake/proofs/pan_to_targetProofScript.sml
new file mode 100644
index 0000000000..8851646bbb
--- /dev/null
+++ b/pancake/proofs/pan_to_targetProofScript.sml
@@ -0,0 +1,225 @@
+(*
+
+composing semantics correctness from pan to target
+
+*)
+
+open preamble
+     backendProofTheory pan_to_wordProofTheory
+     pan_to_targetTheory
+
+val _ = new_theory "pan_to_targetProof";
+
+Overload stack_remove_prog_comp[local] = ``stack_remove$prog_comp``
+Overload stack_alloc_prog_comp[local] = ``stack_alloc$prog_comp``
+Overload stack_names_prog_comp[local] = ``stack_names$prog_comp``
+Overload word_to_word_compile[local] = ``word_to_word$compile``
+Overload word_to_stack_compile[local] = ``word_to_stack$compile``
+Overload stack_to_lab_compile[local] = ``stack_to_lab$compile``
+Overload pan_to_word_compile_prog[local] = ``pan_to_word$compile_prog
+``
+
+Theorem pan_to_lab_good_code_lemma:
+  compile c.stack_conf c.data_conf lim1 lim2 offs stack_prog = code ∧
+  compile asm_conf3 word_prog = (bm, wc, fs, stack_prog) ∧
+  word_to_word$compile word_conf asm_conf3 word_prog0 = (col, word_prog) ∧
+  compile_prog pan_prog = word_prog0 ∧
+  stack_to_labProof$labels_ok code ∧
+  all_enc_ok_pre conf code ⇒
+  lab_to_targetProof$good_code conf LN code
+Proof
+  (* start of 'good_code' proof for initial compilation *)
+  rw []
+  \\ qmatch_asmsub_abbrev_tac `stack_to_labProof$labels_ok lab_prog`
+  \\ fs[lab_to_targetProofTheory.good_code_def]
+  \\ CONJ_TAC >- fs[Abbr `lab_prog`, stack_to_labTheory.compile_def]
+  \\ CONJ_ASM1_TAC >- (
+    fs [stack_to_labProofTheory.labels_ok_def]
+    \\ qpat_x_assum `all_enc_ok_pre _ _` kall_tac
+    \\ first_x_assum (fn t => mp_tac t \\ match_mp_tac EVERY_MONOTONIC)
+    \\ simp[] \\ Cases \\ simp[]
+    \\ metis_tac [labPropsTheory.EVERY_sec_label_ok]
+  )
+  \\ CONJ_TAC >- (
+    fs [stack_to_labProofTheory.labels_ok_def]
+    \\ qmatch_asmsub_abbrev_tac `ALL_DISTINCT (MAP ff _)`
+    \\ `ff = Section_num` by
+      (simp[Abbr`ff`,FUN_EQ_THM]>>Cases>>simp[])
+    \\ fs [])
+  \\ CONJ_TAC >- (
+    fs [stack_to_labProofTheory.labels_ok_def]
+    \\ first_x_assum (fn t => mp_tac t \\ match_mp_tac EVERY_MONOTONIC
+      \\ simp[] \\ Cases \\ simp[] \\ NO_TAC)
+  )
+  \\ qpat_x_assum`Abbrev(lab_prog = _)` mp_tac
+  \\ simp[markerTheory.Abbrev_def]
+  \\disch_then (assume_tac o SYM)
+  \\ drule stack_to_labProofTheory.stack_to_lab_stack_good_handler_labels
+  \\ simp []
+  \\ disch_then match_mp_tac
+  \\ qmatch_asmsub_abbrev_tac ‘word_to_word$compile _ _ wprog’
+  \\ pop_assum $ (assume_tac o GSYM o REWRITE_RULE [markerTheory.Abbrev_def])
+  \\ drule pan_to_word_good_handlers
+  \\ disch_tac
+  \\ drule data_to_wordProofTheory.word_good_handlers_word_to_word
+  \\ disch_then (qspecl_then [‘word_conf’, ‘asm_conf3’] assume_tac)
+  \\ drule (INST_TYPE [beta|->alpha] word_to_stackProofTheory.word_to_stack_good_handler_labels)
+  \\ strip_tac
+  \\ pop_assum $ irule
+  \\ simp []
+  \\ qexists_tac ‘asm_conf3’>>gs[]
+QED
+
+Theorem word_to_stack_compile_FST:
+  word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ⇒
+  MAP FST p =
+  raise_stub_location::store_consts_stub_location::MAP FST wprog
+Proof
+  strip_tac>>gs[word_to_stackTheory.compile_def]>>
+  pairarg_tac>>gs[]>>rveq>>gs[]>>
+  drule_then irule word_to_stackProofTheory.MAP_FST_compile_word_to_stack
+QED
+
+Theorem pan_to_stack_first_ALL_DISTINCT:
+  pan_to_word_compile_prog pan_code = wprog0 ∧
+  word_to_word_compile c.word_to_word_conf mc.target.config wprog0 = (col,wprog) ∧
+  word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧
+  ALL_DISTINCT (MAP FST pan_code) ⇒
+  ALL_DISTINCT (MAP FST p)
+Proof
+  strip_tac>>drule pan_to_wordProofTheory.first_compile_prog_all_distinct>>
+  strip_tac>>
+  drule backendProofTheory.compile_to_word_conventions2>>strip_tac>>
+  gs[]>>
+  qpat_x_assum ‘MAP FST wprog = _’ $ assume_tac o GSYM>>gs[]>>
+  drule word_to_stack_compile_FST>>
+  strip_tac>>gs[]>>
+  drule pan_to_wordProofTheory.pan_to_word_compile_prog_lab_min>>
+  strip_tac>>
+  gs[GSYM EVERY_MAP]>>EVAL_TAC>>gs[EVERY_MEM]>>
+  rw[]>- (first_x_assum $ qspec_then ‘5’ assume_tac>>gs[])>>
+  first_x_assum $ qspec_then ‘6’ assume_tac>>gs[]
+QED
+
+Theorem pan_to_stack_compile_lab_pres:
+  pan_to_word$compile_prog pan_code = wprog0 ∧
+  word_to_word_compile c.word_to_word_conf mc.target.config wprog0 =(col,wprog) ∧
+  word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧
+  ALL_DISTINCT (MAP FST pan_code) ⇒
+  ALL_DISTINCT (MAP FST p) ∧
+  EVERY (λn. n ≠ 0 ∧ n ≠ 1 ∧ n ≠ 2 ∧ n ≠ gc_stub_location) (MAP FST p) ∧
+  EVERY
+  (λ(n,p).
+     (let
+        labs = extract_labels p
+      in
+        EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) labs ∧
+        ALL_DISTINCT labs)) p
+Proof
+  strip_tac>>
+  drule pan_to_wordProofTheory.pan_to_word_compile_lab_pres>>strip_tac>>
+  gs[]>>
+  drule backendProofTheory.compile_to_word_conventions2>>
+  strip_tac>>
+  drule pan_to_wordProofTheory.first_compile_prog_all_distinct>>
+  strip_tac>>gs[]>>
+  ‘EVERY
+   (λ(n,m,p).
+      (let
+         labs = extract_labels p
+       in
+         EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) labs ∧
+         ALL_DISTINCT labs)) wprog’
+    by (gs[EVERY2_EVERY]>>gs[EVERY_EL]>>ntac 2 strip_tac>>
+        ntac 3 (first_x_assum $ qspec_then ‘n’ assume_tac)>>
+        pairarg_tac>>gs[EL_ZIP, word_simpProofTheory.labels_rel_def]>>
+        pairarg_tac>>gs[EL_MAP]>>strip_tac>>strip_tac>>
+        ‘EL n (MAP FST wprog) = EL n (MAP FST wprog0)’ by rfs[]>>
+        gs[EL_MAP]>>
+        pairarg_tac>>gs[]>>
+        ‘(l1, l2) ∈ set (extract_labels p'')’
+          by (gs[MEM_SET_TO_LIST, SUBSET_DEF]>>
+              first_assum irule>>metis_tac[MEM_EL])>>
+        gs[MEM_EL]>>
+        first_x_assum $ qspec_then ‘n''''’ assume_tac>>
+        gs[]>>pairarg_tac>>gs[])>>
+  drule (INST_TYPE [beta|->alpha] word_to_stackProofTheory.word_to_stack_compile_lab_pres)>>
+  disch_then $ qspec_then ‘mc.target.config’ assume_tac>>
+  drule_all pan_to_stack_first_ALL_DISTINCT>>
+  strip_tac>>gs[]>>
+  strip_tac>>gs[backend_commonTheory.stack_num_stubs_def]>>
+  gs[backend_commonTheory.word_num_stubs_def,
+     wordLangTheory.store_consts_stub_location_def,
+     wordLangTheory.raise_stub_location_def,
+     stackLangTheory.gc_stub_location_def,
+     backend_commonTheory.stack_num_stubs_def]>>
+  drule pan_to_wordProofTheory.pan_to_word_compile_prog_lab_min>>
+  gs[GSYM EVERY_MAP, EVERY_MEM]>>ntac 3 strip_tac>>
+  first_x_assum $ qspec_then ‘n’ assume_tac>>gs[]
+QED
+
+Theorem pan_to_lab_labels_ok:
+  pan_to_word_compile_prog pan_code = wprog0 ∧
+  word_to_word_compile c.word_to_word_conf mc.target.config wprog0 = (col,wprog) ∧
+  word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧
+  stack_to_lab_compile c.stack_conf c.data_conf max_heap sp mc.target.config.addr_offset p = lprog ∧
+  ALL_DISTINCT (MAP FST pan_code) ⇒
+  labels_ok lprog
+Proof
+  strip_tac>>
+  qpat_x_assum ‘_ = lprog’ (assume_tac o GSYM)>>gs[]>>
+  irule stack_to_labProofTheory.stack_to_lab_compile_lab_pres>>
+  drule_all pan_to_stack_compile_lab_pres>>gs[]
+QED
+
+(** stack_to_lab$good_code **)
+
+Theorem word_to_stack_good_code_lemma:
+  word_to_word_compile c.word_to_word_conf mc.target.config
+          (pan_to_word_compile_prog pan_code) = (col,wprog) ∧
+  word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧
+  LENGTH mc.target.config.avoid_regs + 13 ≤ mc.target.config.reg_count ∧
+         (* from backend_config_ok c *)
+  ALL_DISTINCT (MAP FST pan_code) ⇒
+  good_code (mc.target.config.reg_count −
+           (LENGTH mc.target.config.avoid_regs + 3)) p
+Proof
+  gs[stack_to_labProofTheory.good_code_def]>>strip_tac>>
+  qmatch_asmsub_abbrev_tac ‘word_to_word_compile _ _ wprog0 = _’>>
+  qpat_x_assum ‘Abbrev (wprog0 = _)’ (assume_tac o GSYM o REWRITE_RULE [markerTheory.Abbrev_def])>>
+  drule_all pan_to_stack_compile_lab_pres>>strip_tac>>gs[]>>
+  drule backendProofTheory.compile_to_word_conventions2>>
+  strip_tac>>
+  drule pan_to_wordProofTheory.first_compile_prog_all_distinct>>
+  strip_tac>>gs[]>>
+  drule word_to_stack_compile_FST>>strip_tac>>
+  drule word_to_stackProofTheory.word_to_stack_stack_convs>>
+  gs[]>>impl_tac
+  >- (gs[EVERY_EL]>>
+      ntac 2 strip_tac>>
+      ntac 3 (first_x_assum $ qspec_then ‘n’ assume_tac)>>
+      gs[]>>
+      pairarg_tac>>gs[]>>
+      pairarg_tac>>gs[]>>simp[EL_MAP])>>
+  strip_tac>>gs[backend_commonTheory.stack_num_stubs_def]>>
+  gs[EVERY_EL]>>rpt strip_tac>>
+  pairarg_tac>>gs[EL_MAP]>>
+  qpat_x_assum ‘∀n. _ ⇒ alloc_arg _’ $ qspec_then ‘n’ assume_tac>>
+  gs[]>>
+
+  drule pan_to_word_compile_prog_lab_min>>
+  gs[GSYM EVERY_MAP]>>
+  qpat_x_assum ‘MAP FST _ = MAP FST _’ $ assume_tac o GSYM>>
+  gs[]>>
+  gs[GSYM EVERY_MAP, EVERY_MEM]>>strip_tac>>
+  ‘MEM k (MAP FST p)’
+    by (gs[MEM_MAP]>>gs[MEM_EL]>>gs[PULL_EXISTS]>>
+        first_assum $ irule_at (Pos last)>>gs[])>>
+  gs[backend_commonTheory.word_num_stubs_def,
+     wordLangTheory.store_consts_stub_location_def,
+     wordLangTheory.raise_stub_location_def,
+     backend_commonTheory.stack_num_stubs_def]>>
+  first_x_assum $ qspec_then ‘k’ assume_tac>>gs[]
+QED
+
+val _ = export_theory();
diff --git a/pancake/proofs/pan_to_wordProofScript.sml b/pancake/proofs/pan_to_wordProofScript.sml
index 53bb191e7e..9b6e5ccef4 100644
--- a/pancake/proofs/pan_to_wordProofScript.sml
+++ b/pancake/proofs/pan_to_wordProofScript.sml
@@ -723,5 +723,82 @@ Proof
   fs []
 QED
 
+(*** no_install/no_alloc/no_mt lemmas ***)
+
+Theorem pan_to_word_compile_prog_no_install_code:
+  compile_prog prog = prog' ⇒
+  no_install_code (fromAList prog')
+Proof
+  gs[compile_prog_def]>>strip_tac>>
+  metis_tac[loop_to_wordProofTheory.loop_compile_no_install_code]
+QED
+
+Theorem pan_to_word_compile_prog_no_alloc_code:
+  compile_prog prog = prog' ⇒
+  no_alloc_code (fromAList prog')
+Proof
+  gs[compile_prog_def]>>strip_tac>>
+  metis_tac[loop_to_wordProofTheory.loop_compile_no_alloc_code]
+QED
+
+Theorem pan_to_word_compile_prog_no_mt_code:
+  compile_prog prog = prog' ⇒
+  no_mt_code (fromAList prog')
+Proof
+  gs[compile_prog_def]>>strip_tac>>
+  metis_tac[loop_to_wordProofTheory.loop_compile_no_mt_code]
+QED
+
+(*** pan_to_word good_handlers ***)
+
+Theorem pan_to_word_good_handlers:
+  compile_prog prog = prog' ⇒
+  EVERY (λ(n,m,pp). good_handlers n pp) prog'
+Proof
+  gs[compile_prog_def,
+     loop_to_wordTheory.compile_def]>>
+  strip_tac>>
+  irule loop_to_wordProofTheory.loop_to_word_good_handlers>>metis_tac[]
+QED
+
+(* lab_pres *)
+
+Theorem pan_to_word_compile_lab_pres:
+  pan_to_word$compile_prog prog = prog' ⇒
+  EVERY
+  (λ(n,m,p).
+     (let
+        labs = extract_labels p
+      in
+        EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) labs ∧
+        ALL_DISTINCT labs)) prog'
+Proof
+  strip_tac>>gs[pan_to_wordTheory.compile_prog_def]>>
+  gs[loop_to_wordTheory.compile_def]>>
+  drule loop_to_word_compile_prog_lab_pres>>gs[]
+QED
+
+(* first_name offset : lab_min *)
+
+Theorem pan_to_word_compile_prog_lab_min:
+  compile_prog pprog = wprog ⇒
+  EVERY (λprog. 60 ≤ FST prog) wprog
+Proof
+  gs[pan_to_wordTheory.compile_prog_def]>>
+  strip_tac>>
+  drule_then irule loop_to_word_compile_lab_min>>
+  irule crep_to_loop_compile_prog_lab_min>>metis_tac[]
+QED
+
+(* inst_ok_less *)
+
+Theorem pan_to_word_every_inst_ok_less:
+  pan_to_word$compile_prog pan_code = wprog0 ∧
+  byte_offset_ok c 0w ⇒
+  EVERY (λ(n,m,p). every_inst (inst_ok_less c) p) wprog0
+Proof
+  gs[pan_to_wordTheory.compile_prog_def]>>strip_tac>>
+  drule_then irule loop_to_word_every_inst_ok_less>>gs[]
+QED
 
 val _ = export_theory();