diff --git a/Manual/Description/theories.smd b/Manual/Description/theories.smd
index 3cec2cd044..7812ce00f1 100644
--- a/Manual/Description/theories.smd
+++ b/Manual/Description/theories.smd
@@ -4696,10 +4696,12 @@ alternate recursive presentation.
    ##thm FDIFF_FUPDATE
 ```
 
-There is one last, even more specialised, instance of `DRESTRICT` called `FMINUS`:
+There are two, even more specialised, instances of `DRESTRICT`
+called `FMINUS` and `FINTER`:
 
 ```repl
    ##thm FMINUS_def
+   ##thm FINTER_def
 ```
 
 **Union and sub-maps.**
diff --git a/src/finite_maps/finite_mapScript.sml b/src/finite_maps/finite_mapScript.sml
index 2b19635bbe..5557f5cac8 100644
--- a/src/finite_maps/finite_mapScript.sml
+++ b/src/finite_maps/finite_mapScript.sml
@@ -3569,6 +3569,37 @@ Definition FMINUS_def:
   FMINUS fm1 fm2 = FDIFF fm1 (FDOM fm2)
 End
 
+Theorem FLOOKUP_FMINUS:
+  FLOOKUP (FMINUS f1 f2) k =
+  case FLOOKUP f2 k of
+    NONE => FLOOKUP f1 k
+  | SOME v => NONE
+Proof
+  rw[FMINUS_def, FDIFF_def, FLOOKUP_DRESTRICT] >>
+  Cases_on ‘FLOOKUP f2 k’ >> gvs[FLOOKUP_DEF]
+QED
+
+(* ----------------------------------------------------------------------
+    FINTER : ('a |-> 'b) -> ('a |-> 'c) -> ('a |-> 'b)
+
+    Keeps the entries of the first map whose keys are in the domain of
+    the second map.
+  ----------------------------------------------------------------------- *)
+
+Definition FINTER_def:
+  FINTER f1 f2 = DRESTRICT f1 (FDOM f2)
+End
+
+Theorem FLOOKUP_FINTER:
+  FLOOKUP (FINTER f1 f2) k =
+  case FLOOKUP f2 k of
+    NONE => NONE
+  | SOME v => FLOOKUP f1 k
+Proof
+  rw[FINTER_def, FLOOKUP_DRESTRICT] >>
+  Cases_on ‘FLOOKUP f2 k’ >> gvs[FLOOKUP_DEF]
+QED
+
 
 Theorem FMERGE_WITH_KEY_FUNION_ALT:
   FMERGE_WITH_KEY f (FUNION m1 m2) m3 =
@@ -3920,7 +3951,7 @@ QED
 Theorem FLOOKUP_SIMP =
   [FLOOKUP_EMPTY, FLOOKUP_UPDATE, FDIFF_def, FLOOKUP_FMAP_MAP2,
    FLOOKUP_DRESTRICT, FLOOKUP_FDIFF, FLOOKUP_FUNION, FLOOKUP_FUN_FMAP,
-   FLOOKUP_FMAP_MAP2, FLOOKUP_FMERGE]
+   FLOOKUP_FMAP_MAP2, FLOOKUP_FMERGE, FLOOKUP_FMINUS, FLOOKUP_FINTER]
   |> map SPEC_ALL |> LIST_CONJ;
 
 (*---------------------------------------------------------------------------*)
diff --git a/src/num/theories/cv_compute/automation/cv_string_fmapScript.sml b/src/num/theories/cv_compute/automation/cv_string_fmapScript.sml
index 6891673839..06ebb1b862 100644
--- a/src/num/theories/cv_compute/automation/cv_string_fmapScript.sml
+++ b/src/num/theories/cv_compute/automation/cv_string_fmapScript.sml
@@ -4,7 +4,7 @@
 Theory cv_string_fmap
 Ancestors
   cv cv_type arithmetic words cv_rep cv_prim pair list option sum
-  alist indexedLists rich_list sptree finite_set cv_std
+  alist indexedLists rich_list sptree finite_set sorting cv_std
 Libs
   dep_rewrite cv_typeLib cv_repLib cv_transLib
 
@@ -82,7 +82,9 @@ Definition st_del_nil_def[simp]:
 End
 
 Definition mk_Branch_def:
-  mk_Branch x t1 t2 = if t1 = Nothing then t2 else Branch x t1 t2
+  mk_Branch c Nothing t2 = t2 ∧
+  mk_Branch c (Just x) t2 = Branch c (Just x) t2 ∧
+  mk_Branch c (Branch a b d) t2 = Branch c (Branch a b d) t2
 End
 
 Definition st_del_cons_def:
@@ -119,6 +121,88 @@ Definition st_union_def:
       Branch c1 (st_union t1 u1) (st_union t2 u2)
 End
 
+Definition st_inter_def:
+  st_inter Nothing t = Nothing ∧
+  st_inter t Nothing = Nothing ∧
+  st_inter (Just x) (Just y) = Just x ∧
+  st_inter (Just x) (Branch c t1 t2) = st_inter (Just x) t2 ∧
+  st_inter (Branch c t1 t2) (Just x) = st_inter t2 (Just x) ∧
+  st_inter (Branch c1 t1 t2) (Branch c2 u1 u2) =
+    if ORD c1 < ORD c2 then
+      st_inter t2 (Branch c2 u1 u2)
+    else if ORD c2 < ORD c1 then
+      st_inter (Branch c1 t1 t2) u2
+    else
+      mk_Branch c1 (st_inter t1 u1) (st_inter t2 u2)
+End
+
+Definition st_minus_def:
+  st_minus Nothing t = Nothing ∧
+  st_minus t Nothing = t ∧
+  st_minus (Just x) (Just y) = Nothing ∧
+  st_minus (Just x) (Branch c t1 t2) = st_minus (Just x) t2 ∧
+  st_minus (Branch c t1 t2) (Just x) = Branch c t1 (st_minus t2 (Just x)) ∧
+  st_minus (Branch c1 t1 t2) (Branch c2 u1 u2) =
+    if ORD c1 < ORD c2 then
+      Branch c1 t1 (st_minus t2 (Branch c2 u1 u2))
+    else if ORD c2 < ORD c1 then
+      st_minus (Branch c1 t1 t2) u2
+    else
+      mk_Branch c1 (st_minus t1 u1) (st_minus t2 u2)
+End
+
+Definition st_card_def:
+  st_card Nothing = 0:num ∧
+  st_card (Just x) = 1 ∧
+  st_card (Branch c t1 t2) = st_card t1 + st_card t2
+End
+
+Definition st_submap_def:
+  st_submap Nothing u = T ∧
+  st_submap (Just x) Nothing = F ∧
+  st_submap (Branch c t1 t2) Nothing = F ∧
+  st_submap (Just x) (Just y) = (x = y) ∧
+  st_submap (Just x) (Branch c u1 u2) = st_submap (Just x) u2 ∧
+  st_submap (Branch c t1 t2) (Just y) = F ∧
+  st_submap (Branch c1 t1 t2) (Branch c2 u1 u2) =
+    if ORD c1 < ORD c2 then F
+    else if ORD c2 < ORD c1 then st_submap (Branch c1 t1 t2) u2
+    else st_submap t1 u1 ∧ st_submap t2 u2
+End
+
+Definition st_lex_def:
+  st_lex t = (case st_get_nil t of
+              | NONE => st_branches t
+              | SOME v => ("",v) :: st_branches t) ∧
+  st_branches Nothing = [] ∧
+  st_branches (Just x) = [] ∧
+  st_branches (Branch c t1 t2) =
+    MAP (λ(k,v). (STRING c k, v)) (st_lex t1) ++ st_branches t2
+Termination
+  WF_REL_TAC ‘measure (λx. case x of
+                           | INL t => str_trie_size (K 0) t * 2 + 1
+                           | INR t => str_trie_size (K 0) t * 2)’
+End
+
+Definition st_lex_acc_def:
+  st_lex_acc t rp acc =
+    (case st_get_nil t of
+     | NONE => st_branches_acc t rp acc
+     | SOME v => (REVERSE rp, v) :: st_branches_acc t rp acc) ∧
+  st_branches_acc Nothing rp acc = acc ∧
+  st_branches_acc (Just x) rp acc = acc ∧
+  st_branches_acc (Branch c t1 t2) rp acc =
+    st_lex_acc t1 (c::rp) (st_branches_acc t2 rp acc)
+Termination
+  WF_REL_TAC ‘measure (λx. case x of
+                           | INL (t,rp,acc) => str_trie_size (K 0) t * 2 + 1
+                           | INR (t,rp,acc) => str_trie_size (K 0) t * 2)’
+End
+
+Definition st_to_list_def:
+  st_to_list t = st_lex_acc t [] []
+End
+
 (* verification *)
 
 Definition st_flat_def:
@@ -439,12 +523,18 @@ Proof
   Cases_on`t'` \\ gvs[]
 QED
 
+Theorem mk_Branch_thm:
+  mk_Branch c t1 t2 = if t1 = Nothing then t2 else Branch c t1 t2
+Proof
+  Cases_on ‘t1’ \\ gvs [mk_Branch_def]
+QED
+
 Theorem st_sorted_mk_Branch:
   st_sorted (mk_Branch c t1 t2) ⇔
     st_sorted t1 ∧ st_sorted t2 ∧
     (t1 ≠ Nothing ⇒ ∀c' t1' t2'. t2 = Branch c' t1' t2' ⇒ c < c')
 Proof
-  rw [mk_Branch_def, st_sorted_def] \\ rw [] \\ eq_tac \\ rw []
+  rw [mk_Branch_thm, st_sorted_def] \\ rw [] \\ eq_tac \\ rw []
 QED
 
 Theorem st_del_cons_not_Branch_Nothing:
@@ -452,7 +542,7 @@ Theorem st_del_cons_not_Branch_Nothing:
     st_del_cons t x xs ≠ Branch c Nothing rest
 Proof
   Induct \\ rw [st_del_cons_def, st_sorted_def]
-  \\ gvs [mk_Branch_def, AllCaseEqs()]
+  \\ gvs [mk_Branch_thm, AllCaseEqs()]
   \\ gvs[stringTheory.char_gt_def, stringTheory.char_lt_def]
   \\ `ORD c = ORD x` by gvs[]
   \\ gvs[stringTheory.ORD_11]
@@ -471,7 +561,7 @@ Proof
   \\ BasicProvers.TOP_CASE_TAC \\ gvs[]
   \\ gvs[stringTheory.char_lt_def, stringTheory.char_gt_def]
   \\ rw[] \\ gvs[]
-  \\ gvs[mk_Branch_def, AllCaseEqs(), st_sorted_def]
+  \\ gvs[mk_Branch_thm, AllCaseEqs(), st_sorted_def]
   \\ Cases_on`s` \\ gvs[stringTheory.char_lt_def]
 QED
 
@@ -497,7 +587,7 @@ QED
 Theorem st_get_nil_mk_Branch[simp]:
   ∀c t1 t2. st_get_nil (mk_Branch c t1 t2) = st_get_nil t2
 Proof
-  rw [mk_Branch_def, st_get_nil_def]
+  rw [mk_Branch_thm, st_get_nil_def]
 QED
 
 Theorem st_get_cons_mk_Branch:
@@ -506,14 +596,14 @@ Theorem st_get_cons_mk_Branch:
     if t1 = Nothing then st_get_cons t2 x xs
     else st_get_cons (Branch c t1 t2) x xs
 Proof
-  rw [mk_Branch_def]
+  rw [mk_Branch_thm]
 QED
 
 Theorem st_get_nil_st_del_cons[simp]:
   ∀t x xs. st_get_nil (st_del_cons t x xs) = st_get_nil t
 Proof
   Induct \\ rw [st_del_cons_def, st_get_nil_def]
-  \\ gvs [st_get_nil_def, mk_Branch_def]
+  \\ gvs [st_get_nil_def, mk_Branch_thm]
 QED
 
 Theorem st_get_cons_st_del_cons:
@@ -690,6 +780,417 @@ Proof
   \\ rw [] \\ gvs [option_case_id]
 QED
 
+Theorem st_inter_Just_left[local]:
+  ∀u x. st_inter (Just x) u =
+        case st_get_nil u of
+        | NONE => Nothing
+        | SOME _ => Just x
+Proof
+  Induct \\ gvs [st_inter_def]
+QED
+
+Theorem st_inter_Just_right[local]:
+  ∀t x. st_inter t (Just x) =
+        case st_get_nil t of
+        | NONE => Nothing
+        | SOME y => Just y
+Proof
+  Induct \\ gvs [st_inter_def]
+QED
+
+Theorem st_inter_Branch_le[local]:
+  ∀t u c' t1 t2.
+    st_sorted t ∧ st_inter t u = Branch c' t1 t2 ⇒
+    ∃d s1 s2. t = Branch d s1 s2 ∧ ORD d ≤ ORD c'
+Proof
+  ho_match_mp_tac st_inter_ind \\ rpt strip_tac
+  \\ gvs [st_inter_def, st_inter_Just_left, st_inter_Just_right, AllCaseEqs()]
+  \\ gvs [st_sorted_def, mk_Branch_thm, AllCaseEqs()]
+  \\ gvs [stringTheory.char_lt_def]
+QED
+
+Theorem st_sorted_st_inter[simp]:
+  ∀t u.
+    st_sorted t ∧ st_sorted u ⇒
+    st_sorted (st_inter t u)
+Proof
+  ho_match_mp_tac st_inter_ind \\ rpt strip_tac
+  \\ gvs [st_inter_def, st_inter_Just_left, st_inter_Just_right, AllCaseEqs()]
+  \\ gvs [st_sorted_def]
+  \\ rw [st_sorted_mk_Branch]
+  \\ drule_all st_inter_Branch_le
+  \\ rw [] \\ gvs [stringTheory.char_lt_def]
+QED
+
+Theorem st_get_nil_st_inter:
+  ∀t u.
+    st_get_nil (st_inter t u) =
+    case st_get_nil u of
+    | NONE => NONE
+    | SOME _ => st_get_nil t
+Proof
+  ho_match_mp_tac st_inter_ind \\ rw [st_inter_def]
+  \\ CASE_TAC \\ gvs []
+QED
+
+Theorem st_get_st_inter:
+  ∀t1 t2 n.
+    st_sorted t1 ∧ st_sorted t2 ⇒
+    st_get (st_inter t1 t2) n =
+    case st_get t2 n of
+    | NONE => NONE
+    | SOME _ => st_get t1 n
+Proof
+  ho_match_mp_tac st_inter_ind \\ rpt strip_tac
+  \\ Cases_on ‘n’
+  \\ gvs [st_inter_def, st_get_def, st_get_nil_st_inter, option_case_id,
+          st_inter_Just_left, st_inter_Just_right]
+  \\ gvs [st_sorted_def]
+  >- (rpt CASE_TAC \\ gvs [st_get_def])
+  >- (rpt CASE_TAC \\ gvs [st_get_def])
+  >- (rpt CASE_TAC \\ gvs [st_get_def])
+  \\ rename [‘st_get_cons (if ORD c1 < ORD c2 then _ else _) h s’]
+  \\ Cases_on ‘ORD c1 < ORD c2’ \\ gvs []
+  >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
+      \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
+  \\ Cases_on ‘ORD c2 < ORD c1’ \\ gvs []
+  >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
+      \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
+  \\ ‘c1 = c2’ by gvs [GSYM stringTheory.ORD_11] \\ gvs []
+  \\ rename [‘st_get_cons (mk_Branch c (st_inter l1 r1) (st_inter l2 r2)) h s’]
+  \\ qpat_x_assum ‘∀n. st_get (st_inter l2 r2) n = _’
+       (qspec_then ‘STRING h s’ mp_tac)
+  \\ qpat_x_assum ‘∀n. st_get (st_inter l1 r1) n = _’
+       (qspec_then ‘s’ mp_tac)
+  \\ gvs [st_get_cons_mk_Branch, st_get_def,
+          stringTheory.char_lt_def, stringTheory.char_gt_def]
+  \\ rw [] \\ gvs []
+  \\ ‘st_get_cons l2 h s = NONE’ by
+       (irule st_get_cons_sorted_lt
+        \\ gvs [stringTheory.char_lt_def] \\ rw [] \\ res_tac \\ gvs [])
+  \\ gvs [] \\ rpt CASE_TAC \\ gvs []
+QED
+
+Theorem st_minus_Just_left[local]:
+  ∀u x. st_minus (Just x) u =
+        case st_get_nil u of
+        | NONE => Just x
+        | SOME _ => Nothing
+Proof
+  Induct \\ gvs [st_minus_def]
+QED
+
+Theorem st_minus_Branch_le[local]:
+  ∀t u c' t1 t2.
+    st_sorted t ∧ st_minus t u = Branch c' t1 t2 ⇒
+    ∃d s1 s2. t = Branch d s1 s2 ∧ ORD d ≤ ORD c'
+Proof
+  ho_match_mp_tac st_minus_ind \\ rpt strip_tac
+  \\ gvs [st_minus_def, st_minus_Just_left, AllCaseEqs()]
+  \\ gvs [st_sorted_def, mk_Branch_thm, AllCaseEqs()]
+  \\ gvs [stringTheory.char_lt_def]
+QED
+
+Theorem st_sorted_st_minus[simp]:
+  ∀t u.
+    st_sorted t ∧ st_sorted u ⇒
+    st_sorted (st_minus t u)
+Proof
+  ho_match_mp_tac st_minus_ind \\ rpt strip_tac
+  \\ gvs [st_minus_def, st_minus_Just_left, AllCaseEqs()]
+  \\ gvs [st_sorted_def]
+  \\ rw [st_sorted_mk_Branch, st_sorted_def]
+  \\ drule_all st_minus_Branch_le
+  \\ rw [] \\ gvs [stringTheory.char_lt_def]
+QED
+
+Theorem st_get_nil_st_minus:
+  ∀t u.
+    st_get_nil (st_minus t u) =
+    case st_get_nil u of
+    | NONE => st_get_nil t
+    | SOME _ => NONE
+Proof
+  ho_match_mp_tac st_minus_ind \\ rw [st_minus_def]
+  \\ CASE_TAC \\ gvs []
+QED
+
+Theorem st_get_st_minus:
+  ∀t1 t2 n.
+    st_sorted t1 ∧ st_sorted t2 ⇒
+    st_get (st_minus t1 t2) n =
+    case st_get t2 n of
+    | NONE => st_get t1 n
+    | SOME _ => NONE
+Proof
+  ho_match_mp_tac st_minus_ind \\ rpt strip_tac
+  \\ Cases_on ‘n’
+  \\ gvs [st_minus_def, st_get_def, st_get_nil_st_minus, option_case_id,
+          st_minus_Just_left]
+  \\ gvs [st_sorted_def]
+  >- (rpt CASE_TAC \\ gvs [st_get_def])
+  >- (rpt CASE_TAC \\ gvs [st_get_def])
+  >- (rename [‘st_get_cons (st_minus u (Just x)) h s’]
+      \\ first_x_assum (qspec_then ‘STRING h s’ mp_tac)
+      \\ gvs [st_get_def])
+  \\ rename [‘st_get_cons (if ORD c1 < ORD c2 then _ else _) h s’]
+  \\ Cases_on ‘ORD c1 < ORD c2’ \\ gvs []
+  >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
+      \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
+  \\ Cases_on ‘ORD c2 < ORD c1’ \\ gvs []
+  >- (first_x_assum (qspec_then ‘STRING h s’ mp_tac)
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
+      \\ rw [] \\ gvs [] \\ rpt CASE_TAC \\ gvs [])
+  \\ ‘c1 = c2’ by gvs [GSYM stringTheory.ORD_11] \\ gvs []
+  \\ rename [‘st_get_cons (mk_Branch c (st_minus l1 r1) (st_minus l2 r2)) h s’]
+  \\ qpat_x_assum ‘∀n. st_get (st_minus l2 r2) n = _’
+       (qspec_then ‘STRING h s’ mp_tac)
+  \\ qpat_x_assum ‘∀n. st_get (st_minus l1 r1) n = _’
+       (qspec_then ‘s’ mp_tac)
+  \\ gvs [st_get_cons_mk_Branch, st_get_def,
+          stringTheory.char_lt_def, stringTheory.char_gt_def]
+  \\ rw [] \\ gvs []
+  \\ ‘st_get_cons l2 h s = NONE’ by
+       (irule st_get_cons_sorted_lt
+        \\ gvs [stringTheory.char_lt_def] \\ rw [] \\ res_tac \\ gvs [])
+  \\ gvs [] \\ rpt CASE_TAC \\ gvs []
+QED
+
+Theorem st_card_st_flat[local]:
+  ∀t. st_card t = LENGTH (st_flat t)
+Proof
+  Induct \\ gvs [st_card_def, st_flat_def]
+QED
+
+Theorem MEM_st_flat_lt[local]:
+  ∀t c k v.
+    st_sorted t ∧ (∀d t1 t2. t = Branch d t1 t2 ⇒ c < d) ∧
+    MEM (k,v) (st_flat t) ⇒
+    k = [] ∨ ∃d k'. k = STRING d k' ∧ c < d
+Proof
+  Induct \\ gvs [st_flat_def, st_sorted_def, MEM_MAP, EXISTS_PROD]
+  \\ rw [] \\ gvs []
+  \\ last_x_assum drule_all \\ rw [] \\ gvs [stringTheory.char_lt_def]
+QED
+
+Theorem MAP_FST_MAP_CONS[local]:
+  MAP FST (MAP (λ(k,v). (STRING c k,v)) l) = MAP (STRING c) (MAP FST l)
+Proof
+  gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
+QED
+
+Theorem ALL_DISTINCT_st_flat[local]:
+  ∀t. st_sorted t ⇒ ALL_DISTINCT (MAP FST (st_flat t))
+Proof
+  Induct \\ gvs [st_flat_def, st_sorted_def]
+  \\ rw [MAP_FST_MAP_CONS, ALL_DISTINCT_APPEND]
+  >- (irule ALL_DISTINCT_MAP_INJ \\ gvs [])
+  \\ gvs [MEM_MAP] \\ rw []
+  \\ CCONTR_TAC \\ gvs [MEM_MAP, EXISTS_PROD]
+  \\ drule MEM_st_flat_lt \\ disch_then drule \\ gvs []
+  \\ Cases_on ‘y’ \\ gvs []
+  \\ first_assum $ irule_at Any \\ gvs [stringTheory.char_lt_def]
+QED
+
+Theorem st_submap_thm:
+  ∀t u.
+    st_sorted t ∧ st_sorted u ⇒
+    (st_submap t u ⇔ ∀k v. st_get t k = SOME v ⇒ st_get u k = SOME v)
+Proof
+  ho_match_mp_tac st_submap_ind \\ rpt strip_tac
+  \\ gvs [st_submap_def, st_get_def, st_sorted_def]
+  >- (qexists_tac ‘[]’ \\ gvs [st_get_def])
+  >- (irule st_sorted_not_Nothing_get \\ gvs [st_sorted_def])
+  >- (eq_tac \\ rw [] \\ gvs [st_get_def]
+      \\ first_x_assum (qspecl_then [‘[]’,‘x’] mp_tac) \\ gvs [st_get_def])
+  >- (eq_tac \\ rw [] \\ Cases_on ‘k’ \\ gvs [st_get_def]
+      \\ first_x_assum (qspecl_then [‘[]’,‘v’] mp_tac) \\ gvs [st_get_def])
+  >- (rename [‘Branch c l1 l2’]
+      \\ qspec_then ‘l1’ mp_tac st_sorted_not_Nothing_get \\ gvs [] \\ rw []
+      \\ qexists_tac ‘STRING c k’ \\ qexists_tac ‘v’
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def])
+  \\ rename [‘st_get (Branch c1 l1 l2) _ = SOME _ ⇒
+              st_get (Branch c2 r1 r2) _ = SOME _’]
+  \\ Cases_on ‘ORD c1 < ORD c2’ \\ gvs []
+  >- (qspec_then ‘l1’ mp_tac st_sorted_not_Nothing_get \\ gvs [] \\ rw []
+      \\ qexists_tac ‘STRING c1 k’ \\ qexists_tac ‘v’
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def])
+  \\ Cases_on ‘ORD c2 < ORD c1’ \\ gvs []
+  >- (‘∀k v. st_get (Branch c1 l1 l2) k = SOME v ⇒
+             st_get (Branch c2 r1 r2) k = st_get r2 k’ by
+        (Cases \\ gvs [st_get_def, stringTheory.char_lt_def,
+                       stringTheory.char_gt_def]
+         \\ rw [] \\ gvs [])
+      \\ eq_tac \\ rw [] \\ res_tac \\ gvs [])
+  \\ ‘c1 = c2’ by gvs [GSYM stringTheory.ORD_11] \\ gvs []
+  \\ ‘∀h rest. st_get_cons l2 h rest ≠ NONE ⇒ ORD c1 < ORD h’ by
+       (rpt strip_tac \\ CCONTR_TAC
+        \\ qspecl_then [‘l2’,‘h’,‘rest’] mp_tac st_get_cons_sorted_lt
+        \\ gvs [] \\ rw [] \\ gvs [stringTheory.char_lt_def])
+  \\ eq_tac \\ rw []
+  >- (Cases_on ‘k’
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
+      >- (qpat_x_assum ‘∀k v. st_get l2 k = _ ⇒ _’
+            (qspecl_then [‘[]’,‘v’] mp_tac) \\ gvs [st_get_def])
+      \\ rw []
+      >- (qpat_x_assum ‘∀k v. st_get l2 k = _ ⇒ _’
+            (qspecl_then [‘STRING h t’,‘v’] mp_tac) \\ gvs [st_get_def])
+      \\ qpat_x_assum ‘∀k v. st_get l1 k = _ ⇒ _’
+           (qspecl_then [‘t’,‘v’] mp_tac) \\ gvs [st_get_def])
+  >- (first_x_assum (qspecl_then [‘STRING c1 k’,‘v’] mp_tac)
+      \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def])
+  \\ Cases_on ‘k’
+  >- (first_x_assum (qspecl_then [‘[]’,‘v’] mp_tac) \\ gvs [st_get_def])
+  \\ ‘ORD c1 < ORD h’ by
+       (qpat_x_assum ‘∀h rest. st_get_cons l2 h rest ≠ NONE ⇒ _’
+          (qspecl_then [‘h’,‘t’] mp_tac) \\ gvs [st_get_def])
+  \\ first_x_assum (qspecl_then [‘STRING h t’,‘v’] mp_tac)
+  \\ gvs [st_get_def, stringTheory.char_lt_def, stringTheory.char_gt_def]
+QED
+
+Theorem MEM_alookup[local]:
+  ∀l x. MEM x (MAP FST l) ⇔ ALOOKUP l x ≠ NONE
+Proof
+  gvs [ALOOKUP_NONE]
+QED
+
+Theorem ALOOKUP_MAP_STRING[local]:
+  ALOOKUP (MAP (λ(k,v). (STRING c k,v)) l) (STRING d rest) =
+    (if c = d then ALOOKUP l rest else NONE) ∧
+  ALOOKUP (MAP (λ(k,v). (STRING c k,v)) l) "" = NONE
+Proof
+  Induct_on ‘l’ \\ gvs [] \\ Cases \\ gvs [] \\ rw []
+QED
+
+Theorem ALOOKUP_st_lex:
+  (∀t:'a str_trie. st_sorted t ⇒ ∀k. ALOOKUP (st_lex t) k = st_get t k) ∧
+  (∀t:'a str_trie. st_sorted t ⇒
+     ∀k. ALOOKUP (st_branches t) k = if k = "" then NONE else st_get t k)
+Proof
+  ho_match_mp_tac st_lex_ind \\ rw [st_lex_def, st_get_def, st_sorted_def]
+  \\ Cases_on ‘k’
+  \\ gvs [ALOOKUP_APPEND, ALOOKUP_MAP_STRING, st_get_def]
+  \\ TRY (CASE_TAC \\ gvs [st_get_def] \\ NO_TAC)
+  \\ ‘∀d rest. ORD d ≤ ORD c ⇒ st_get_cons t' d rest = NONE’ by
+       (rw [] \\ irule st_get_cons_sorted_lt \\ gvs [] \\ rw []
+        \\ res_tac \\ gvs [stringTheory.char_lt_def])
+  \\ Cases_on ‘c = h’
+  \\ gvs [stringTheory.char_lt_def, stringTheory.char_gt_def]
+  >- (CASE_TAC \\ gvs [])
+  \\ rw [] \\ gvs []
+  \\ ‘ORD h = ORD c’ by DECIDE_TAC \\ gvs [stringTheory.ORD_11]
+QED
+
+Theorem st_lex_acc_thm[local]:
+  (∀t:'a str_trie rp acc. st_lex_acc t rp acc =
+     MAP (λ(k,v). (REVERSE rp ++ k, v)) (st_lex t) ++ acc) ∧
+  (∀t:'a str_trie rp acc. st_branches_acc t rp acc =
+     MAP (λ(k,v). (REVERSE rp ++ k, v)) (st_branches t) ++ acc)
+Proof
+  ho_match_mp_tac st_lex_acc_ind
+  \\ rw [st_lex_acc_def, st_lex_def]
+  \\ gvs [MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD]
+  \\ CASE_TAC \\ gvs []
+QED
+
+Theorem st_to_list_thm:
+  st_to_list t = st_lex t
+Proof
+  gvs [st_to_list_def, st_lex_acc_thm, pairTheory.ELIM_UNCURRY]
+QED
+
+Theorem MEM_st_lex[local]:
+  ∀t k. st_sorted t ⇒
+    (MEM k (MAP FST (st_lex t)) ⇔ st_get t k ≠ NONE) ∧
+    (MEM k (MAP FST (st_branches t)) ⇔ k ≠ "" ∧ st_get t k ≠ NONE)
+Proof
+  rw [MEM_alookup] \\ gvs [ALOOKUP_st_lex] \\ rw [] \\ gvs []
+QED
+
+Theorem transitive_string_lt[local]:
+  transitive string_lt
+Proof
+  gvs [relationTheory.transitive_def]
+  \\ metis_tac [stringTheory.string_lt_trans]
+QED
+
+Theorem SORTED_MAP_STRING[local]:
+  ∀l. SORTED string_lt (MAP (STRING c) l) ⇔ SORTED string_lt l
+Proof
+  Induct \\ gvs [] \\ Cases_on ‘l’
+  \\ gvs [SORTED_DEF, stringTheory.string_lt_def, stringTheory.char_lt_def]
+QED
+
+Theorem SORTED_st_lex:
+  (∀t:'a str_trie. st_sorted t ⇒ SORTED string_lt (MAP FST (st_lex t))) ∧
+  (∀t:'a str_trie. st_sorted t ⇒ SORTED string_lt (MAP FST (st_branches t)))
+Proof
+  ho_match_mp_tac st_lex_ind \\ rw [st_lex_def, st_sorted_def]
+  \\ gvs [SORTED_APPEND, transitive_string_lt, MAP_FST_MAP_CONS,
+          SORTED_MAP_STRING]
+  >- (CASE_TAC \\ gvs [SORTED_EQ, transitive_string_lt] \\ rw []
+      \\ ‘y ≠ ""’ by (qspecl_then [‘t’,‘y’] mp_tac MEM_st_lex \\ gvs [])
+      \\ Cases_on ‘y’ \\ gvs [stringTheory.string_lt_def])
+  \\ ‘∀d rest. ORD d ≤ ORD c ⇒ st_get_cons t' d rest = NONE’ by
+       (rw [] \\ irule st_get_cons_sorted_lt \\ gvs [] \\ rw []
+        \\ res_tac \\ gvs [stringTheory.char_lt_def])
+  \\ ‘∀y. MEM y (MAP FST (st_branches t')) ⇒
+          ∃d k2. y = STRING d k2 ∧ char_lt c d’ by
+       (rw [] \\ qspecl_then [‘t'’,‘y’] mp_tac MEM_st_lex \\ gvs [] \\ rw []
+        \\ Cases_on ‘y’ \\ gvs []
+        \\ CCONTR_TAC \\ gvs [st_get_def, stringTheory.char_lt_def]
+        \\ ‘ORD h ≤ ORD c’ by DECIDE_TAC \\ res_tac \\ gvs [])
+  \\ rw [] \\ gvs [MEM_MAP] \\ res_tac
+  \\ gvs [stringTheory.string_lt_def]
+QED
+
+Theorem ALOOKUP_eq_NONE[local]:
+  ∀l k v k'. SORTED string_lt (MAP FST ((k,v)::l)) ∧ ¬string_lt k k' ⇒
+             ALOOKUP l k' = NONE
+Proof
+  rw [] \\ gvs [SORTED_EQ, transitive_string_lt]
+  \\ CCONTR_TAC \\ gvs [GSYM MEM_alookup]
+  \\ first_x_assum drule \\ gvs []
+QED
+
+Theorem sorted_alist_unique[local]:
+  ∀l1 l2. SORTED string_lt (MAP FST l1) ∧ SORTED string_lt (MAP FST l2) ∧
+          ALOOKUP l1 = ALOOKUP l2 ⇒ l1 = l2
+Proof
+  Induct \\ Cases_on ‘l2’ \\ gvs [] \\ strip_tac
+  >- (Cases_on ‘h’ \\ gvs [FUN_EQ_THM]
+      \\ first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs [])
+  >- (rw [] \\ Cases_on ‘h’ \\ gvs [FUN_EQ_THM]
+      \\ first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs [])
+  \\ Cases_on ‘h’ \\ Cases_on ‘h'’ \\ strip_tac \\ gvs []
+  \\ ‘q' = q’ by
+       (CCONTR_TAC
+        \\ ‘string_lt q' q ∨ string_lt q q'’ by
+             metis_tac [stringTheory.string_lt_cases]
+        \\ gvs [FUN_EQ_THM]
+        >- (first_x_assum (qspec_then ‘q'’ mp_tac) \\ gvs []
+            \\ qspecl_then [‘t’,‘q’,‘r’,‘q'’] mp_tac ALOOKUP_eq_NONE
+            \\ impl_tac
+            >- (gvs [] \\ metis_tac [stringTheory.string_lt_antisym])
+            \\ gvs [])
+        \\ first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs []
+        \\ qspecl_then [‘l1’,‘q'’,‘r'’,‘q’] mp_tac ALOOKUP_eq_NONE
+        \\ impl_tac >- (gvs [] \\ metis_tac [stringTheory.string_lt_antisym])
+        \\ gvs [])
+  \\ gvs [FUN_EQ_THM]
+  \\ ‘r' = r’ by (first_x_assum (qspec_then ‘q’ mp_tac) \\ gvs [])
+  \\ gvs []
+  \\ first_x_assum irule
+  \\ gvs [SORTED_EQ, transitive_string_lt] \\ rw []
+  \\ Cases_on ‘q = x’ \\ gvs []
+  >- (Cases_on ‘ALOOKUP l1 q’ \\ Cases_on ‘ALOOKUP t q’ \\ gvs [MEM_alookup]
+      \\ metis_tac [stringTheory.string_lt_nonrefl, optionTheory.NOT_SOME_NONE])
+  \\ first_x_assum (qspec_then ‘x’ mp_tac) \\ gvs []
+QED
+
 val _ = cv_trans st_get_nil_def;
 val _ = cv_trans st_get_def;
 val _ = cv_trans st_make_def;
@@ -717,6 +1218,44 @@ val _ = cv_trans_rec st_union_def
    \\ qspec_then ‘cv_snd y’ assume_tac cv_size_cv_fst_cv_snd
    \\ gvs []);
 
+val _ = cv_trans_rec st_inter_def
+  (WF_REL_TAC ‘measure $ λ(x,y). cv_size x + cv_size y’
+   \\ cv_termination_tac
+   \\ rename [‘cv_size (cv_snd (cv_snd x)) + (cv_size (cv_snd (cv_snd y)) + 5)’]
+   \\ qspec_then ‘x’ assume_tac cv_size_cv_fst_cv_snd
+   \\ qspec_then ‘y’ assume_tac cv_size_cv_fst_cv_snd
+   \\ qspec_then ‘cv_snd x’ assume_tac cv_size_cv_fst_cv_snd
+   \\ qspec_then ‘cv_snd y’ assume_tac cv_size_cv_fst_cv_snd
+   \\ gvs []);
+
+val _ = cv_trans st_card_def;
+val _ = cv_trans st_submap_def;
+
+val st_lex_acc_pre_def = cv_trans_pre_rec "" st_lex_acc_def
+  (WF_REL_TAC ‘measure (λx. case x of
+                            | INL (cv,rp,acc) => cv_size cv * 2 + 1
+                            | INR (cv,rp,acc) => cv_size cv * 2)’
+   \\ cv_termination_tac);
+
+Theorem st_lex_acc_pre[cv_pre]:
+  (∀t:'a str_trie rp acc. st_lex_acc_pre t rp acc) ∧
+  (∀t:'a str_trie rp acc. st_branches_acc_pre t rp acc)
+Proof
+  ho_match_mp_tac st_lex_acc_ind \\ rw [] \\ simp [Once st_lex_acc_pre_def]
+QED
+
+val _ = cv_trans st_to_list_def;
+
+val _ = cv_trans_rec st_minus_def
+  (WF_REL_TAC ‘measure $ λ(x,y). cv_size x + cv_size y’
+   \\ cv_termination_tac
+   \\ rename [‘cv_size (cv_snd (cv_snd x)) + (cv_size (cv_snd (cv_snd y)) + 5)’]
+   \\ qspec_then ‘x’ assume_tac cv_size_cv_fst_cv_snd
+   \\ qspec_then ‘y’ assume_tac cv_size_cv_fst_cv_snd
+   \\ qspec_then ‘cv_snd x’ assume_tac cv_size_cv_fst_cv_snd
+   \\ qspec_then ‘cv_snd y’ assume_tac cv_size_cv_fst_cv_snd
+   \\ gvs []);
+
 (*----------------------------------------------------------*
    string |-> 'a
  *----------------------------------------------------------*)
@@ -783,13 +1322,10 @@ Proof
 QED
 
 Theorem cv_rep_string_DOMSUB[cv_rep]:
-  from_to f t ⇒
   from_string_fmap f (m \\ k) =
   cv_st_del (from_string_fmap f m) (from_list from_char k)
 Proof
-  rw[from_string_fmap_def]
-  \\ drule (GSYM (theorem "cv_st_del_thm" |> DISCH_ALL))
-  \\ simp [] \\ disch_then kall_tac
+  gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_del_thm"]
   \\ AP_TERM_TAC
   \\ simp [st_del_st_sets, st_del_Nothing]
   \\ irule st_sets_eq \\ fs [finite_mapTheory.FLOOKUP_SIMP, FUN_EQ_THM]
@@ -810,3 +1346,138 @@ Proof
   \\ gvs [st_get_st_sets, st_get_Nothing, st_sorted_def, option_case_id,
           finite_mapTheory.FLOOKUP_FUNION]
 QED
+
+Theorem cv_rep_string_FINTER[cv_rep]:
+  from_string_fmap f (FINTER m1 m2) =
+  cv_st_inter (from_string_fmap f m1) (from_string_fmap g m2)
+Proof
+  gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_inter_thm"]
+  \\ AP_TERM_TAC
+  \\ irule st_sorted_st_get_eq
+  \\ irule_at Any st_sorted_st_inter
+  \\ rw [st_sorted_st_sets, st_sorted_def]
+  \\ DEP_REWRITE_TAC [st_get_st_inter]
+  \\ gvs [st_get_st_sets, st_get_Nothing, st_sorted_def, option_case_id,
+          finite_mapTheory.FLOOKUP_FINTER]
+QED
+
+Theorem cv_rep_string_FMINUS[cv_rep]:
+  from_string_fmap f (FMINUS m1 m2) =
+  cv_st_minus (from_string_fmap f m1) (from_string_fmap g m2)
+Proof
+  gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_minus_thm"]
+  \\ AP_TERM_TAC
+  \\ irule st_sorted_st_get_eq
+  \\ irule_at Any st_sorted_st_minus
+  \\ rw [st_sorted_st_sets, st_sorted_def]
+  \\ DEP_REWRITE_TAC [st_get_st_minus]
+  \\ gvs [st_get_st_sets, st_get_Nothing, st_sorted_def, option_case_id,
+          finite_mapTheory.FLOOKUP_FMINUS]
+QED
+
+Theorem cv_rep_string_FCARD[cv_rep]:
+  Num (FCARD m) = cv_st_card (from_string_fmap f m)
+Proof
+  gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_card_thm"]
+  \\ qmatch_goalsub_abbrev_tac ‘st_card t’
+  \\ ‘st_sorted t’ by gvs [Abbr‘t’]
+  \\ ‘ALOOKUP (st_flat t) = FLOOKUP m’ by
+       (gvs [FUN_EQ_THM] \\ rw []
+        \\ DEP_REWRITE_TAC [ALOOKUP_st_flat]
+        \\ gvs [Abbr‘t’, st_get_st_sets]
+        \\ CASE_TAC \\ gvs [])
+  \\ ‘∀x. MEM x (MAP FST (st_flat t)) ⇔ ALOOKUP (st_flat t) x ≠ NONE’ by
+       gvs [ALOOKUP_NONE]
+  \\ ‘FDOM m = set (MAP FST (st_flat t))’ by
+       (gvs [pred_setTheory.EXTENSION]
+        \\ gvs [finite_mapTheory.FLOOKUP_DEF] \\ rw [])
+  \\ gvs [st_card_st_flat, finite_mapTheory.FCARD_DEF]
+  \\ DEP_REWRITE_TAC [ALL_DISTINCT_CARD_LIST_TO_SET]
+  \\ gvs [ALL_DISTINCT_st_flat]
+QED
+
+val submap_lemma = cv_rep_for [] “st_submap t u” |> DISCH_ALL;
+
+Theorem cv_rep_string_SUBMAP[cv_rep]:
+  from_to f_a t_a ⇒
+  cv_rep T (cv_st_submap (from_string_fmap f_a m1) (from_string_fmap f_a m2))
+        b2c (m1 ⊑ m2)
+Proof
+  qsuff_tac ‘m1 ⊑ m2 ⇔ st_submap (st_sets Nothing (fmap_to_alist m1))
+                                 (st_sets Nothing (fmap_to_alist m2))’
+  >- (simp [from_string_fmap_def]
+      \\ mp_tac (submap_lemma |> Q.GENL [‘t’,‘u’]
+                   |> Q.SPECL [‘st_sets Nothing (fmap_to_alist m1)’,
+                               ‘st_sets Nothing (fmap_to_alist m2)’])
+      \\ fs [])
+  \\ DEP_REWRITE_TAC [st_submap_thm]
+  \\ gvs [st_get_st_sets, option_case_id, finite_mapTheory.SUBMAP_FLOOKUP_EQN]
+QED
+
+(* the entries of a finite map, listed in increasing order of the keys *)
+Definition fmap_to_sorted_list_def:
+  fmap_to_sorted_list m =
+    @l. ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l)
+End
+
+Theorem fmap_to_sorted_list_eq:
+  ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l) ⇒
+  fmap_to_sorted_list m = l
+Proof
+  rw [fmap_to_sorted_list_def] \\ SELECT_ELIM_TAC \\ rw []
+  >- (qexists_tac ‘l’ \\ gvs [])
+  \\ irule sorted_alist_unique \\ gvs []
+QED
+
+Theorem fmap_to_sorted_list_thm:
+  ALOOKUP (fmap_to_sorted_list m) = FLOOKUP m ∧
+  SORTED string_lt (MAP FST (fmap_to_sorted_list m))
+Proof
+  ‘∃l. ALOOKUP l = FLOOKUP m ∧ SORTED string_lt (MAP FST l)’ by
+    (qexists_tac ‘st_lex (st_sets Nothing (fmap_to_alist m))’
+     \\ qmatch_goalsub_abbrev_tac ‘st_lex t’
+     \\ ‘st_sorted t’ by gvs [Abbr‘t’]
+     \\ conj_tac
+     >- (gvs [FUN_EQ_THM] \\ rw []
+         \\ DEP_REWRITE_TAC [ALOOKUP_st_lex] \\ gvs [Abbr‘t’, st_get_st_sets]
+         \\ CASE_TAC \\ gvs [])
+     \\ irule (CONJUNCT1 SORTED_st_lex) \\ gvs [])
+  \\ gvs [fmap_to_sorted_list_def] \\ SELECT_ELIM_TAC \\ rw []
+  \\ metis_tac []
+QED
+
+Theorem LENGTH_fmap_to_sorted_list:
+  LENGTH (fmap_to_sorted_list m) = FCARD m
+Proof
+  strip_assume_tac fmap_to_sorted_list_thm
+  \\ ‘ALL_DISTINCT (MAP FST (fmap_to_sorted_list m))’ by
+       (qspec_then ‘string_lt’ mp_tac (GEN_ALL SORTED_ALL_DISTINCT)
+        \\ impl_tac
+        >- gvs [transitive_string_lt, relationTheory.irreflexive_def,
+                stringTheory.string_lt_nonrefl]
+        \\ disch_then irule \\ gvs [])
+  \\ ‘FDOM m = set (MAP FST (fmap_to_sorted_list m))’ by
+       (‘∀x. MEM x (MAP FST (fmap_to_sorted_list m)) ⇔
+             ALOOKUP (fmap_to_sorted_list m) x ≠ NONE’ by gvs [ALOOKUP_NONE]
+        \\ gvs [pred_setTheory.EXTENSION]
+        \\ gvs [finite_mapTheory.FLOOKUP_DEF] \\ rw [])
+  \\ gvs [finite_mapTheory.FCARD_DEF]
+  \\ DEP_REWRITE_TAC [ALL_DISTINCT_CARD_LIST_TO_SET] \\ gvs []
+QED
+
+Theorem cv_rep_string_fmap_to_sorted_list[cv_rep]:
+  from_list (from_pair (from_list from_char) f) (fmap_to_sorted_list m) =
+  cv_st_to_list (from_string_fmap f m)
+Proof
+  gvs [from_string_fmap_def, GSYM $ fetch "-" "cv_st_to_list_thm"]
+  \\ AP_TERM_TAC
+  \\ gvs [st_to_list_thm]
+  \\ irule fmap_to_sorted_list_eq
+  \\ qmatch_goalsub_abbrev_tac ‘st_lex t’
+  \\ ‘st_sorted t’ by gvs [Abbr‘t’]
+  \\ conj_tac
+  >- (gvs [FUN_EQ_THM] \\ rw []
+      \\ DEP_REWRITE_TAC [ALOOKUP_st_lex] \\ gvs [Abbr‘t’, st_get_st_sets]
+      \\ CASE_TAC \\ gvs [])
+  \\ irule (CONJUNCT1 SORTED_st_lex) \\ gvs []
+QED
diff --git a/tools/Holmake/tests/rebuild_cachekey/subdir/baseScript.sml b/tools/Holmake/tests/rebuild_cachekey/subdir/baseScript.sml
index 8cc4789310..7832c12d0f 100644
--- a/tools/Holmake/tests/rebuild_cachekey/subdir/baseScript.sml
+++ b/tools/Holmake/tests/rebuild_cachekey/subdir/baseScript.sml
@@ -1,3 +1,4 @@
 Theory base[bare]
 Ancestors bool
 Theorem base_thm = TRUTH
+Theorem base_thm2 = TRUTH