diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
index 3d4fded15b..773521713f 100644
--- a/src/boss/prove_base_assumsScript.sml
+++ b/src/boss/prove_base_assumsScript.sml
@@ -296,16 +296,17 @@ val goals =
  60 |- (!P. Data_List_any P Data_List_nil <=> F) /\
        !P h t.
          Data_List_any P (Data_List_cons h t) <=> P h \/ Data_List_any P t,
- 61 |- Data_List_concat Data_List_nil = Data_List_nil /\
+ 61 |- (T <> F) /\ (F <> T)
+ 62 |- Data_List_concat Data_List_nil = Data_List_nil /\
        !h t.
          Data_List_concat (Data_List_cons h t) =
          Data_List_append h (Data_List_concat t),
- 62 |- Data_List_reverse Data_List_nil = Data_List_nil /\
+ 63 |- Data_List_reverse Data_List_nil = Data_List_nil /\
        !h t.
          Data_List_reverse (Data_List_cons h t) =
          Data_List_append (Data_List_reverse t)
            (Data_List_cons h Data_List_nil),
- 63 |- Data_List_unzip Data_List_nil =
+ 64 |- Data_List_unzip Data_List_nil =
        Data_Pair_comma Data_List_nil Data_List_nil /\
        !x l.
          Data_List_unzip (Data_List_cons x l) =
@@ -314,59 +315,59 @@ val goals =
               (Data_Pair_fst (Data_List_unzip l)))
            (Data_List_cons (Data_Pair_snd x)
               (Data_Pair_snd (Data_List_unzip l))),
- 64 |- Data_List_length Data_List_nil = Number_Natural_zero /\
+ 65 |- Data_List_length Data_List_nil = Number_Natural_zero /\
        !h t.
          Data_List_length (Data_List_cons h t) =
          Number_Natural_suc (Data_List_length t),
- 65 |- Number_Natural_factorial Number_Natural_zero =
+ 66 |- Number_Natural_factorial Number_Natural_zero =
        Number_Natural_bit1 Number_Natural_zero /\
        !n. Number_Natural_factorial (Number_Natural_suc n) =
            Number_Natural_times (Number_Natural_suc n)
              (Number_Natural_factorial n),
- 66 |- (Data_List_null Data_List_nil <=> T) /\
+ 67 |- (Data_List_null Data_List_nil <=> T) /\
        !h t. Data_List_null (Data_List_cons h t) <=> F,
- 67 |- (Number_Natural_even Number_Natural_zero <=> T) /\
+ 68 |- (Number_Natural_even Number_Natural_zero <=> T) /\
        !n. Number_Natural_even (Number_Natural_suc n) <=>
            ~Number_Natural_even n,
- 68 |- (Number_Natural_odd Number_Natural_zero <=> F) /\
+ 69 |- (Number_Natural_odd Number_Natural_zero <=> F) /\
        !n. Number_Natural_odd (Number_Natural_suc n) <=>
            ~Number_Natural_odd n,
- 69 |- Data_Unit_unit = @x. T,
- 70 |- Number_Natural_zero = Number_Natural_zero,
- 71 |- (?!x. F) <=> F,
- 72 |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b,
- 73 |- Data_Sum_left x = Data_Sum_left y <=> x = y,
- 74 |- Data_Sum_right x = Data_Sum_right y <=> x = y,
- 75 |- Function_id = Function_Combinator_s Function_const Function_const,
- 76 |- Relation_empty = (\x y. F),
- 77 |- Relation_universe = (\x y. T),
- 78 |- Number_Natural_bit1 =
+ 70 |- Data_Unit_unit = @x. T,
+ 71 |- Number_Natural_zero = Number_Natural_zero,
+ 72 |- (?!x. F) <=> F,
+ 73 |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b,
+ 74 |- Data_Sum_left x = Data_Sum_left y <=> x = y,
+ 75 |- Data_Sum_right x = Data_Sum_right y <=> x = y,
+ 76 |- Function_id = Function_Combinator_s Function_const Function_const,
+ 77 |- Relation_empty = (\x y. F),
+ 78 |- Relation_universe = (\x y. T),
+ 79 |- Number_Natural_bit1 =
        (\n.
             Number_Natural_plus n
               (Number_Natural_plus n (Number_Natural_suc Number_Natural_zero))),
- 79 |- Number_Natural_max = (\m n. if Number_Natural_less m n then n else m),
- 80 |- Number_Natural_min = (\m n. if Number_Natural_less m n then m else n),
- 81 |- Number_Natural_greater = (\m n. Number_Natural_less n m),
- 82 |- Number_Natural_greatereq = (\m n. Number_Natural_greater m n \/ m = n),
- 83 |- Number_Natural_less =
+ 80 |- Number_Natural_max = (\m n. if Number_Natural_less m n then n else m),
+ 81 |- Number_Natural_min = (\m n. if Number_Natural_less m n then m else n),
+ 82 |- Number_Natural_greater = (\m n. Number_Natural_less n m),
+ 83 |- Number_Natural_greatereq = (\m n. Number_Natural_greater m n \/ m = n),
+ 84 |- Number_Natural_less =
        (\m n. ?P. (!n. P (Number_Natural_suc n) ==> P n) /\ P m /\ ~P n),
- 84 |- Number_Natural_lesseq = (\m n. Number_Natural_less m n \/ m = n),
- 85 |- Relation_irreflexive = (\R. !x. ~R x x),
- 86 |- Relation_reflexive = (\R. !x. R x x),
- 87 |- Relation_transitive = (\R. !x y z. R x y /\ R y z ==> R x z),
- 88 |- Relation_wellFounded =
+ 85 |- Number_Natural_lesseq = (\m n. Number_Natural_less m n \/ m = n),
+ 86 |- Relation_irreflexive = (\R. !x. ~R x x),
+ 87 |- Relation_reflexive = (\R. !x. R x x),
+ 88 |- Relation_transitive = (\R. !x y z. R x y /\ R y z ==> R x z),
+ 89 |- Relation_wellFounded =
        (\R. !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b),
- 89 |- Relation_transitiveClosure =
+ 90 |- Relation_transitiveClosure =
        (\R a b.
             !P. (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==>
                 P a b),
- 90 |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y),
- 91 |- Relation_intersect = (\R1 R2 x y. R1 x y /\ R2 x y),
- 92 |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y),
- 93 |- Function_o = (\f g x. f (g x)),
- 94 |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x,
- 95 |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w,
- 96 |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w]: thm list
+ 91 |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y),
+ 92 |- Relation_intersect = (\R1 R2 x y. R1 x y /\ R2 x y),
+ 93 |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y),
+ 94 |- Function_o = (\f g x. f (g x)),
+ 95 |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x,
+ 96 |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w,
+ 97 |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w]: thm list
  *)
 
 val bool_cases = hd(amatch``(x = T) \/ _``);
@@ -1085,13 +1086,18 @@ val th60 = store_thm
 val concat_nil = hd(amatch``Data_List_concat Data_List_nil``);
 val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
 
+(* |- (T <> F) /\ (F <> T) *)
+val th61 = store_thm
+  ("th61",  el 61 goals |> concl,
+  PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]);
+
 (* |- Data_List_concat Data_List_nil = Data_List_nil /\
       !h t.
           Data_List_concat (Data_List_cons h t) =
           Data_List_append h (Data_List_concat t)
  *)
-val th61 = store_thm
-  ("th61", el 61 goals |> concl,
+val th62 = store_thm
+  ("th62", el 62 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC concat_nil
   \\ MATCH_ACCEPT_TAC concat_cons);
 
@@ -1104,8 +1110,8 @@ val reverse_cons = hd(amatch``Data_List_reverse (Data_List_cons _ _)``);
           Data_List_append (Data_List_reverse t)
             (Data_List_cons h Data_List_nil)
  *)
-val th62 = store_thm
-  ("th62", el 62 goals |> concl,
+val th63 = store_thm
+  ("th63", el 63 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC reverse_nil
   \\ MATCH_ACCEPT_TAC reverse_cons);
 
@@ -1123,8 +1129,8 @@ val unzip_cons = hd(amatch``Data_List_unzip (Data_List_cons _ _)``);
             (Data_List_cons (Data_Pair_snd x)
                (Data_Pair_snd (Data_List_unzip l)))
  *)
-val th63 = store_thm
-  ("th63", el 63 goals |> concl,
+val th64 = store_thm
+  ("th64", el 64 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC unzip_nil
   \\ PURE_REWRITE_TAC[unzip_cons]
   \\ rpt gen_tac
@@ -1139,8 +1145,8 @@ val length_cons = hd(amatch``Data_List_length (Data_List_cons _ _)``);
           Data_List_length (Data_List_cons h t) =
           Number_Natural_suc (Data_List_length t)
  *)
-val th64 = store_thm
-  ("th64", el 64 goals |> concl,
+val th65 = store_thm
+  ("th65", el 65 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC length_nil
   \\ MATCH_ACCEPT_TAC length_cons);
 
@@ -1154,8 +1160,8 @@ val fact_suc = hd(amatch``Number_Natural_factorial (Number_Natural_suc _)``);
           Number_Natural_times (Number_Natural_suc n)
             (Number_Natural_factorial n)
  *)
-val th65 = store_thm
-  ("th65", el 65 goals |> concl,
+val th66 = store_thm
+  ("th66", el 66 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC fact_zero
   \\ MATCH_ACCEPT_TAC fact_suc);
 
@@ -1165,8 +1171,8 @@ val null_cons = hd(amatch``Data_List_null (Data_List_cons _ _)``);
 (* |- (Data_List_null Data_List_nil <=> T) /\
       !h t. Data_List_null (Data_List_cons h t) <=> F
  *)
-val th66 = store_thm
-  ("th66", el 66 goals |> concl,
+val th67 = store_thm
+  ("th67", el 67 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO null_nil)
   \\ MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL null_cons)));
 
@@ -1176,8 +1182,8 @@ val even_cons = hd(amatch``Number_Natural_even (Number_Natural_suc _)``);
 (* |- (Number_Natural_even Number_Natural_zero <=> T) /\
       !n. Number_Natural_even (Number_Natural_suc n) <=> ~Number_Natural_even n
  *)
-val th67 = store_thm
-  ("th67", el 67 goals |> concl,
+val th68 = store_thm
+  ("th68", el 68 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQT_INTRO even_nil)
   \\ MATCH_ACCEPT_TAC even_cons);
 
@@ -1187,28 +1193,28 @@ val odd_cons = hd(amatch``Number_Natural_odd (Number_Natural_suc _)``);
 (* |- (Number_Natural_odd Number_Natural_zero <=> F) /\
       !n. Number_Natural_odd (Number_Natural_suc n) <=> ~Number_Natural_odd n
  *)
-val th68 = store_thm
-  ("th68", el 68 goals |> concl,
+val th69 = store_thm
+  ("th69", el 69 goals |> concl,
   conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO odd_nil)
   \\ MATCH_ACCEPT_TAC odd_cons);
 
 val one_thm = hd(amatch``_ = Data_Unit_unit``);
 
 (* |- Data_Unit_unit = @x. T *)
-val th69 = store_thm
-  ("th69", el 69 goals |> concl,
+val th70 = store_thm
+  ("th70", el 70 goals |> concl,
   PURE_ONCE_REWRITE_TAC[one_thm] \\ REFL_TAC);
 
 (* |- Number_Natural_zero = Number_Natural_zero *)
-val th70 = store_thm
-  ("th70", el 70 goals |> concl,
+val th71 = store_thm
+  ("th71", el 71 goals |> concl,
   REFL_TAC);
 
 val exists_simp = hd(amatch “(?x. t) <=> t”);
 
 (* |- (?!x. F) <=> F *)
-val th71 = store_thm
-  ("th71", el 71 goals |> concl,
+val th72 = store_thm
+  ("th72", el 72 goals |> concl,
   PURE_REWRITE_TAC [BETA_RULE (SPEC “\x:'a. F” ex_unique_thm)] \\
   PURE_REWRITE_TAC [SPEC “F” exists_simp, F_and] \\
   REFL_TAC);
@@ -1216,32 +1222,32 @@ val th71 = store_thm
 val comma_11 = hd(amatch``Data_Pair_comma _ _ = Data_Pair_comma _ _``);
 
 (* |- Data_Pair_comma x y = Data_Pair_comma a b <=> x = a /\ y = b *)
-val th72 = store_thm
-  ("th72", el 72 goals |> concl,
+val th73 = store_thm
+  ("th73", el 73 goals |> concl,
   MATCH_ACCEPT_TAC comma_11);
 
 (* |- Data_Sum_left x = Data_Sum_left y <=> x = y *)
-val th73 = store_thm
-  ("th73", el 73 goals |> concl,
+val th74 = store_thm
+  ("th74", el 74 goals |> concl,
   MATCH_ACCEPT_TAC left_11);
 
 (* |- Data_Sum_right x = Data_Sum_right y <=> x = y *)
-val th74 = store_thm
-  ("th74", el 74 goals |> concl,
+val th75 = store_thm
+  ("th75", el 75 goals |> concl,
   MATCH_ACCEPT_TAC right_11);
 
 val skk = hd(amatch``Function_Combinator_s _ _ = Function_id``);
 
 (* |- Function_id = Function_Combinator_s Function_const Function_const *)
-val th75 = store_thm
-  ("th75", el 75 goals |> concl,
+val th76 = store_thm
+  ("th76", el 76 goals |> concl,
   PURE_REWRITE_TAC[skk] \\ REFL_TAC);
 
 val empty_thm = hd(amatch``Relation_empty _ _``);
 
 (* |- Relation_empty = (\x y. F) *)
-val th76 = store_thm
-  ("th76", el 76 goals |> concl,
+val th77 = store_thm
+  ("th77", el 77 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,EQF_INTRO (SPEC_ALL empty_thm)]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1249,8 +1255,8 @@ val th76 = store_thm
 val universe_thm = hd(amatch``Relation_universe _ _``);
 
 (* |- Relation_universe = (\x y. T) *)
-val th77 = store_thm
-  ("th77", el 77 goals |> concl,
+val th78 = store_thm
+  ("th78", el 78 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,EQT_INTRO(SPEC_ALL universe_thm)]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1271,8 +1277,8 @@ val num_less_ind = hd(amatch``(!x. _ ==> _) ==> !n. P (n:Number_Natural_natural)
            Number_Natural_plus n
              (Number_Natural_plus n (Number_Natural_suc Number_Natural_zero)))
  *)
-val th78 = store_thm
-  ("th78", el 78 goals |> concl,
+val th79 = store_thm
+  ("th79", el 79 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,bit1_thm,plus_suc]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ gen_tac
@@ -1291,8 +1297,8 @@ val if_id   = hd(amatch``if _ then x else x``);
 val less_or_eq   = hd(amatch``Number_Natural_lesseq _ _ <=> (Number_Natural_less _ _) \/ _``);
 
 (* |- Number_Natural_max = (\m n. if Number_Natural_less m n then n else m) *)
-val th79 = store_thm
-  ("th79", el 79 goals |> concl,
+val th80 = store_thm
+  ("th80", el 80 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,max_thm,less_or_eq]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac
@@ -1307,8 +1313,8 @@ val th79 = store_thm
 val min_thm = hd(amatch``Number_Natural_min _ _ = COND _ _ _``);
 
 (* |- Number_Natural_min = (\m n. if Number_Natural_less m n then m else n) *)
-val th80 = store_thm
-  ("th80", el 80 goals |> concl,
+val th81 = store_thm
+  ("th81", el 81 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,min_thm,less_or_eq]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac
@@ -1323,8 +1329,8 @@ val th80 = store_thm
 val greater_thm   = hd(amatch``Number_Natural_greater _ _ = _``);
 
 (* |- Number_Natural_greater = (\m n. Number_Natural_less n m) *)
-val th81 = store_thm
-  ("th81", el 81 goals |> concl,
+val th82 = store_thm
+  ("th82", el 82 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,greater_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1332,8 +1338,8 @@ val th81 = store_thm
 val greatereq_thm = hd(amatch``Number_Natural_greatereq _ _``);
 
 (* |- Number_Natural_greatereq = (\m n. Number_Natural_greater m n \/ m = n) *)
-val th82 = store_thm
-  ("th82", el 82 goals |> concl,
+val th83 = store_thm
+  ("th83", el 83 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,greatereq_thm,less_or_eq,greater_thm]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac
@@ -1361,8 +1367,8 @@ val F_IMP2 = store_thm
 (* |- Number_Natural_less =
       (\m n. ?P. (!n. P (Number_Natural_suc n) ==> P n) /\ P m /\ ~P n)
  *)
-val th83 = store_thm
-  ("th83", el 83 goals |> concl,
+val th84 = store_thm
+  ("th84", el 84 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm]
   \\ qx_genl_tac[`a`,`b`]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
@@ -1421,8 +1427,8 @@ val th83 = store_thm
   \\ PURE_REWRITE_TAC[F_imp]);
 
 (* |- Number_Natural_lesseq = (\m n. Number_Natural_less m n \/ m = n) *)
-val th84 = store_thm
-  ("th84", el 84 goals |> concl,
+val th85 = store_thm
+  ("th85", el 85 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,less_or_eq]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1430,8 +1436,8 @@ val th84 = store_thm
 val irreflexive_thm = hd(amatch``Relation_irreflexive _ = _``);
 
 (* |- Relation_irreflexive = (\R. !x. ~R x x) *)
-val th85 = store_thm
-  ("th85", el 85 goals |> concl,
+val th86 = store_thm
+  ("th86", el 86 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm, irreflexive_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac
@@ -1440,8 +1446,8 @@ val th85 = store_thm
 val reflexive_thm = hd(amatch``Relation_reflexive _ = _``);
 
 (* |- Relation_reflexive = (\R. !x. R x x) *)
-val th86 = store_thm
-  ("th86", el 86 goals |> concl,
+val th87 = store_thm
+  ("th87", el 87 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm, reflexive_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1449,8 +1455,8 @@ val th86 = store_thm
 val transitive_thm = hd(amatch``Relation_transitive s <=> _``);
 
 (* |- Relation_transitive = (\R. !x y z. R x y /\ R y z ==> R x z) *)
-val th87 = store_thm
-  ("th87", el 87 goals |> concl,
+val th88 = store_thm
+  ("th88", el 88 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,transitive_thm]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ gen_tac \\ REFL_TAC);
@@ -1460,8 +1466,8 @@ val wellFounded_thm = hd(amatch``Relation_wellFounded r <=> !p. (?x. _) ==> _``)
 (* |- Relation_wellFounded =
       (\R. !B. (?w. B w) ==> ?min. B min /\ !b. R b min ==> ~B b)
  *)
-val th88 = store_thm
-  ("th88", el 88 goals |> concl,
+val th89 = store_thm
+  ("th89", el 89 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm]
   \\ PURE_REWRITE_TAC[wellFounded_thm]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
@@ -1477,8 +1483,8 @@ val subrelation_thm  = hd(amatch``Relation_subrelation x s <=> !x y. _``);
            !P. (!x y. R x y ==> P x y) /\ (!x y z. P x y /\ P y z ==> P x z) ==>
                P a b)
  *)
-val th89 = store_thm
-  ("th89", el 89 goals |> concl,
+val th90 = store_thm
+  ("th90", el 90 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm]
   \\ PURE_REWRITE_TAC[tc_def,bigIntersect_thm,mem_fromPred]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
@@ -1491,8 +1497,8 @@ val th89 = store_thm
   \\ REFL_TAC);
 
 (* |- Relation_subrelation = (\R1 R2. !x y. R1 x y ==> R2 x y) *)
-val th90 = store_thm
-  ("th90", el 90 goals |> concl,
+val th91 = store_thm
+  ("th91", el 91 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,subrelation_thm]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1505,15 +1511,15 @@ val mem_union = hd(amatch``Set_member _ (Set_union _ _) <=> _``);
 val mem_toSet = hd(amatch``Set_member _ (Relation_toSet _)``);
 
 (* |- Relation_intersect = (\R1 R2 x y. R1 x y /\ R2 x y) *)
-val th91 = store_thm
-  ("th91", el 91 goals |> concl,
+val th92 = store_thm
+  ("th92", el 92 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,intersect_thm,fromSet_thm,mem_inter,mem_toSet]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
 
 (* |- Relation_union = (\R1 R2 x y. R1 x y \/ R2 x y) *)
-val th92 = store_thm
-  ("th92", el 92 goals |> concl,
+val th93 = store_thm
+  ("th93", el 93 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,union_thm,fromSet_thm,mem_union,mem_toSet]
   \\ CONV_TAC(DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
@@ -1521,15 +1527,15 @@ val th92 = store_thm
 val o_thm = hd(amatch``(Function_o _ _) _ = _``);
 
 (* |- Function_o = (\f g x. f (g x)) *)
-val th93 = store_thm
-  ("th93", el 93 goals |> concl,
+val th94 = store_thm
+  ("th94", el 94 goals |> concl,
   PURE_REWRITE_TAC[GSYM fun_eq_thm,o_thm]
   \\ CONV_TAC (DEPTH_CONV BETA_CONV)
   \\ rpt gen_tac \\ REFL_TAC);
 
 (* |- (!x. P x ==> Q x) ==> (?x. P x) ==> ?x'. Q x' *)
-val th94 = store_thm
-  ("th94", el 94 goals |> concl,
+val th95 = store_thm
+  ("th95", el 95 goals |> concl,
   rpt strip_tac
   \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
   \\ qexists_tac`x`
@@ -1544,16 +1550,16 @@ val th94' = store_thm
  *)
 
 (* |- (x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w *)
-val th95 = store_thm
-  ("th95", el 95 goals |> concl,
+val th96 = store_thm
+  ("th96", el 96 goals |> concl,
    rpt strip_tac
   \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
   \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
   \\ first_assum ACCEPT_TAC);
 
 (* |- (x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w *)
-val th96 = store_thm
-  ("th96", el 96 goals |> concl,
+val th97 = store_thm
+  ("th97", el 97 goals |> concl,
   rpt strip_tac
   \\ first_x_assum(fn th => first_x_assum (assume_tac o MATCH_MP th))
   \\ TRY (disj1_tac >> first_assum ACCEPT_TAC)
@@ -1590,7 +1596,7 @@ val th89 = store_thm
  *)
 
 (* Now raise an error if the above th96 is not the last one *)
-val _ = if List.length goals <> 96 then
+val _ = if List.length goals <> 97 then
             (raise ERR "-" "assumptions changed")
         else ();
 
@@ -1629,8 +1635,7 @@ val LET_RAND = store_thm("LET_RAND", concl boolTheory.LET_RAND,
   \\ REFL_TAC)
 
 (* |- (T <=/=> F) /\ (F <=/=> T) *)
-val BOOL_EQ_DISTINCT = store_thm("BOOL_EQ_DISTINCT", concl boolTheory.BOOL_EQ_DISTINCT,
-  PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]);
+val BOOL_EQ_DISTINCT = th61;
 
 (* |- (!t1 t2. (if T then t1 else t2) = t1) /\
       !t1 t2. (if F then t1 else t2) = t2
diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
index 84a465bb0d..e728fddbe0 100644
--- a/src/list/src/listScript.sml
+++ b/src/list/src/listScript.sml
@@ -4734,6 +4734,16 @@ val EL_LENGTH_dropWhile_REVERSE = Q.store_thm("EL_LENGTH_dropWhile_REVERSE",
    >> fs [NOT_EVERY, dropWhile_APPEND_EXISTS, arithmeticTheory.ADD1])
 end
 
+Theorem dropWhile_id:
+ (dropWhile P ls = ls) <=> NULL ls \/ ~P(HD ls)
+Proof
+  Cases_on`ls` \\ rw[dropWhile_def, NULL]
+  \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`dropWhile P l`
+  \\ Q.SPECL_THEN[`P`,`l`]mp_tac LENGTH_dropWhile_LESS_EQ
+  \\ simp[]
+QED
+
 val IMP_EVERY_LUPDATE = store_thm("IMP_EVERY_LUPDATE",
   “!xs h i. P h /\ EVERY P xs ==> EVERY P (LUPDATE h i xs)”,
   Induct THEN fs [LUPDATE_def] THEN REPEAT STRIP_TAC
diff --git a/src/list/src/numposrepScript.sml b/src/list/src/numposrepScript.sml
index 3446fa2dd1..2b5d8bcff3 100644
--- a/src/list/src/numposrepScript.sml
+++ b/src/list/src/numposrepScript.sml
@@ -422,4 +422,88 @@ val l2n_11 = Q.store_thm("l2n_11",
         \\ NTAC 2 (POP_ASSUM SUBST1_TAC)
         \\ FULL_SIMP_TAC (srw_ss()) [l2n_APPEND]]);
 
+Theorem BITWISE_l2n_2:
+  LENGTH l1 = LENGTH l2 ==>
+  BITWISE (LENGTH l1) op (l2n 2 l1) (l2n 2 l2) =
+  l2n 2 (MAP2 (\x y. bool_to_bit $ op (ODD x) (ODD y)) l1 l2)
+Proof
+  Q.ID_SPEC_TAC`l2`
+  \\ Induct_on`l1`
+  \\ simp[BITWISE_EVAL]
+  >- simp[BITWISE_def, l2n_def]
+  \\ Q.X_GEN_TAC`b`
+  \\ Cases \\ fs[BITWISE_EVAL]
+  \\ strip_tac
+  \\ fs[l2n_def]
+  \\ simp[SBIT_def, ODD_ADD, ODD_MULT, GSYM bool_to_bit_def]
+QED
+
+Theorem l2n_2_neg:
+  !ls.
+  EVERY ($> 2) ls ==>
+  l2n 2 (MAP (\x. 1 - x) ls) = 2 ** LENGTH ls - SUC (l2n 2 ls)
+Proof
+  Induct
+  \\ rw[l2n_def]
+  \\ fs[EXP, ADD1]
+  \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
+  \\ Q.SPECL_THEN[`ls`,`2`]mp_tac l2n_lt
+  \\ simp[]
+QED
+
+Theorem l2n_max:
+  0 < b ==>
+  !ls. (l2n b ls = b ** (LENGTH ls) - 1) <=>
+       (EVERY ((=) (b - 1) o flip $MOD b) ls)
+Proof
+  strip_tac
+  \\ Induct
+  \\ rw[l2n_def]
+  \\ rw[EXP]
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`b * l + a`
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`b ** n`
+  \\ fs[EQ_IMP_THM]
+  \\ conj_tac
+  >- (
+    strip_tac
+    \\ Cases_on`n=0` \\ fs[] >- (fs[Abbr`n`] \\ rw[])
+    \\ `0 < b * b ** n` by simp[]
+    \\ `a + b * l + 1 = b * b ** n` by simp[]
+    \\ `(b * b ** n) DIV b = b ** n` by simp[MULT_TO_DIV]
+    \\ `(b * l + (a + 1)) DIV b = b ** n` by fs[]
+    \\ `(b * l) MOD b = 0` by simp[]
+    \\ `(b * l + (a + 1)) DIV b = (b * l) DIV b + (a + 1) DIV b`
+    by ( irule ADD_DIV_RWT \\ simp[] )
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `(a + 1) DIV b = if a = b - 1 then 1 else 0`
+    by (
+      rw[]
+      \\ `a + 1 < b` suffices_by rw[DIV_EQ_0]
+      \\ simp[Abbr`a`]
+      \\ `h MOD b < b - 1` suffices_by simp[]
+      \\ `h MOD b < b` by simp[]
+      \\ fs[] )
+    \\ `b * l DIV b = l` by simp[MULT_TO_DIV]
+    \\ pop_assum SUBST_ALL_TAC
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `l < b ** n` by ( map_every Q.UNABBREV_TAC[`l`,`n`]
+                         \\ irule l2n_lt \\ simp[] )
+    \\ Cases_on`a = b - 1` \\ fs[] )
+  \\ strip_tac
+  \\ rewrite_tac[LEFT_SUB_DISTRIB]
+  \\ Q.PAT_X_ASSUM`_ = a`(SUBST1_TAC o SYM)
+  \\ fs[SUB_LEFT_ADD] \\ rw[]
+  \\ Cases_on`n=0` \\ fs[]
+  \\ `b ** n <= b ** 0` by simp[]
+  \\ fs[EXP_BASE_LE_IFF]
+QED
+
+Theorem l2n_PAD_RIGHT_0[simp]:
+  0 < b ==> l2n b (PAD_RIGHT 0 h ls) = l2n b ls
+Proof
+  Induct_on`ls` \\ rw[l2n_def, PAD_RIGHT, l2n_eq_0, EVERY_GENLIST]
+  \\ fs[PAD_RIGHT, l2n_APPEND]
+  \\ fs[l2n_eq_0, EVERY_GENLIST]
+QED
+
 val _ = export_theory()
diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 124bea3e0f..6a3de4d876 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -8,7 +8,7 @@ open HolKernel Parse boolLib BasicProvers;
 open numLib metisLib simpLib combinTheory arithmeticTheory prim_recTheory
      pred_setTheory listTheory pairTheory markerLib TotalDefn;
 
-local open listSimps pred_setSimps in end;
+local open listSimps pred_setSimps dep_rewrite in end;
 
 val FILTER_APPEND = FILTER_APPEND_DISTRIB
 val REVERSE = REVERSE_SNOC_DEF
@@ -3189,6 +3189,201 @@ Proof
   \\ Cases_on`q` \\ fs[ADD1]
 QED
 
+Theorem chunks_append_divides:
+  !n l1 l2.
+    0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
+    chunks n (l1 ++ l2) = chunks n l1 ++ chunks n l2
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[dividesTheory.divides_def, PULL_EXISTS]
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q=0` \\ fs[] \\ rfs[]
+  \\ IF_CASES_TAC
+  >- ( Cases_on`q` \\ fs[ADD1, LEFT_ADD_DISTRIB] \\ fs[LESS_OR_EQ] )
+  \\ simp[DROP_APPEND, TAKE_APPEND]
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`lhs = _`
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q = 1` \\ fs[]
+  >- (
+    simp[Abbr`lhs`]
+    \\ fs[NOT_LESS_EQUAL]
+    \\ simp[DROP_LENGTH_TOO_LONG])
+  \\ simp[Abbr`lhs`]
+  \\ `n - n * q = 0` by simp[]
+  \\ simp[]
+  \\ first_x_assum irule
+  \\ simp[NULL_EQ]
+  \\ qexists_tac`q - 1`
+  \\ simp[]
+QED
+
+Theorem chunks_length[simp]:
+  chunks (LENGTH ls) ls = [ls]
+Proof
+  rw[Once chunks_def]
+QED
+
+Theorem chunks_not_nil[simp]:
+  !n ls. chunks n ls <> []
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def]
+QED
+
+Theorem LENGTH_chunks:
+  !n ls. 0 < n /\ ~NULL ls ==>
+    LENGTH (chunks n ls) =
+    LENGTH ls DIV n + (bool_to_bit $ ~divides n (LENGTH ls))
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def, dividesTheory.DIV_EQUAL_0, bool_to_bit_def,
+        dividesTheory.divides_def]
+  \\ fs[LESS_OR_EQ, ADD1, NULL_EQ, bool_to_bit_def] \\ rfs[]
+  \\ rw[]
+  \\ fs[dividesTheory.divides_def, dividesTheory.SUB_DIV]
+  \\ rfs[]
+  >- (
+    Cases_on`LENGTH ls DIV n = 0` >- rfs[dividesTheory.DIV_EQUAL_0]
+    \\ simp[] )
+  >- (
+    Cases_on`q` \\ fs[MULT_SUC]
+    \\ Q.MATCH_ASMSUB_RENAME_TAC`n + n * p`
+    \\ first_x_assum(Q.SPEC_THEN`2 + p`mp_tac)
+    \\ simp[LEFT_ADD_DISTRIB] )
+  >- (
+    first_x_assum(Q.SPEC_THEN`PRE q`mp_tac)
+    \\ Cases_on`q` \\ fs[MULT_SUC] )
+  \\ Cases_on`q` \\ fs[MULT_SUC]
+  \\ simp[ADD_DIV_RWT]
+QED
+
+Theorem EL_chunks:
+  !k ls n.
+  n < LENGTH (chunks k ls) /\ 0 < k /\ ~NULL ls ==>
+  EL n (chunks k ls) = TAKE k (DROP (n * k) ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[NULL_EQ]
+  \\ Q.PAT_X_ASSUM`_ < LENGTH _ `mp_tac
+  \\ rw[Once chunks_def] \\ fs[]
+  \\ rw[Once chunks_def]
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`EL m _`
+  \\ Cases_on`m` \\ fs[]
+  \\ pop_assum mp_tac
+  \\ dep_rewrite.DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ simp[NULL_EQ]
+  \\ strip_tac
+  \\ dep_rewrite.DEP_REWRITE_TAC[DROP_DROP]
+  \\ simp[MULT_SUC]
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`k + k * m <= _`
+  \\ `k * m <= LENGTH ls - k` suffices_by simp[]
+  \\ `m <= (LENGTH ls - k) DIV k` suffices_by simp[X_LE_DIV]
+  \\ fs[bool_to_bit_def]
+  \\ pop_assum mp_tac \\ rw[]
+QED
+
+Theorem chunks_MAP:
+  !n ls. chunks n (MAP f ls) = MAP (MAP f) (chunks n ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  \\ fs[]
+  \\ simp[GSYM MAP_DROP]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ simp[MAP_TAKE]
+QED
+
+Theorem chunks_ZIP:
+  !n ls l2. LENGTH ls = LENGTH l2 ==>
+  chunks n (ZIP (ls, l2)) = MAP ZIP (ZIP (chunks n ls, chunks n l2))
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- ( rw[Once chunks_def] \\ rw[Once chunks_def] )
+  >- rw[Once chunks_def]
+  \\ fs[]
+  \\ simp[GSYM ZIP_DROP]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ CONV_TAC(PATH_CONV"rrrr"(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ simp[ZIP_TAKE]
+QED
+
+Theorem chunks_TAKE:
+  !n ls m. divides n m /\ 0 < m ==>
+    chunks n (TAKE m ls) = TAKE (m DIV n) (chunks n ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ rw[]
+  >- (
+    rw[Once chunks_def] \\ fs[LENGTH_TAKE_EQ]
+    \\ fs[dividesTheory.divides_def]
+    \\ BasicProvers.VAR_EQ_TAC
+    \\ Q.MATCH_GOALSUB_RENAME_TAC`n * m`
+    \\ fs[ZERO_LESS_MULT]
+    \\ `n <= n * m` by simp[LE_MULT_CANCEL_LBARE]
+    \\ dep_rewrite.DEP_REWRITE_TAC[TAKE_LENGTH_TOO_LONG]
+    \\ simp[MULT_DIV] )
+  >- fs[dividesTheory.divides_def]
+  \\ fs[]
+  \\ simp[Once chunks_def, LENGTH_TAKE_EQ]
+  \\ `n <= m` by (
+    rfs[dividesTheory.divides_def] \\ rw[]
+    \\ fs[ZERO_LESS_MULT] )
+  \\ IF_CASES_TAC
+  >- (
+    pop_assum mp_tac \\ rw[]
+    \\ `m = n` by fs[] \\ rw[] )
+  \\ fs[TAKE_TAKE, DROP_TAKE]
+  \\ first_x_assum(Q.SPEC_THEN`m - n`mp_tac)
+  \\ simp[]
+  \\ impl_keep_tac >- (
+    fs[dividesTheory.divides_def]
+    \\ qexists_tac`q - 1`
+    \\ simp[LEFT_SUB_DISTRIB] )
+  \\ rw[]
+  \\ `m DIV n <> 0` by fs[dividesTheory.DIV_EQUAL_0]
+  \\ Cases_on`m DIV n` \\ fs[TAKE_TAKE_MIN]
+  \\ `MIN n m = n` by fs[MIN_DEF] \\ rw[]
+  \\ simp[dividesTheory.SUB_DIV]
+QED
+
+Definition chunks_tr_aux_def:
+  chunks_tr_aux n ls acc =
+    if LENGTH ls <= SUC n then REVERSE $ ls :: acc
+    else chunks_tr_aux n (DROP (SUC n) ls) (TAKE (SUC n) ls :: acc)
+Termination
+  WF_REL_TAC`measure $ LENGTH o FST o SND`
+  \\ rw[LENGTH_DROP]
+End
+
+Definition chunks_tr_def:
+  chunks_tr n ls = if n = 0 then [ls] else chunks_tr_aux (n - 1) ls []
+End
+
+Theorem chunks_tr_aux_thm:
+  !n ls acc.
+    chunks_tr_aux n ls acc =
+    REVERSE acc ++ chunks (SUC n) ls
+Proof
+  HO_MATCH_MP_TAC chunks_tr_aux_ind
+  \\ rw[]
+  \\ rw[Once chunks_tr_aux_def]
+  >- rw[Once chunks_def]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ rw[]
+QED
+
+Theorem chunks_tr_thm:
+  chunks_tr = chunks
+Proof
+  simp[FUN_EQ_THM, chunks_tr_def]
+  \\ Cases \\ rw[chunks_tr_aux_thm]
+QED
+
 (*---------------------------------------------------------------------------*)
 (* Various lemmas from the CakeML project https://cakeml.org                 *)
 (*---------------------------------------------------------------------------*)
@@ -3588,6 +3783,26 @@ Proof
 QED
 (* END more lemmas of IS_SUFFIX *)
 
+Theorem IS_SUFFIX_dropWhile:
+  IS_SUFFIX ls (dropWhile P ls)
+Proof
+  Induct_on`ls`
+  \\ rw[IS_SUFFIX_CONS]
+QED
+
+Theorem LENGTH_dropWhile_id:
+  (LENGTH (dropWhile P ls) = LENGTH ls) <=> (dropWhile P ls = ls)
+Proof
+  rw[EQ_IMP_THM]
+  \\ rw[dropWhile_id]
+  \\ Cases_on`ls` \\ fs[]
+  \\ strip_tac \\ fs[]
+  \\ `IS_SUFFIX t (dropWhile P t)` by simp[IS_SUFFIX_dropWhile]
+  \\ fs[IS_SUFFIX_APPEND]
+  \\ `LENGTH t = LENGTH l + LENGTH (dropWhile P t)` by metis_tac[LENGTH_APPEND]
+  \\ fs[]
+QED
+
 Theorem nub_GENLIST:
   nub (GENLIST f n) =
     MAP f (FILTER (\i. !j. (i < j) /\ (j < n) ==> f i <> f j) (COUNT_LIST n))
diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml
index 7d17c753b9..0d2a7c4223 100644
--- a/src/n-bit/wordsScript.sml
+++ b/src/n-bit/wordsScript.sml
@@ -5060,6 +5060,176 @@ QED
 Theorem CARD_WORD = CARD_CART_UNIV |> INST_TYPE [alpha |-> bool]
                                    |> SIMP_RULE bool_ss [CARD_BOOL,FINITE_BOOL]
 
+Theorem MEM_w2l_less:
+  1 < b /\ MEM x (w2l b w) ==> x < b
+Proof
+  Cases_on`w`
+  \\ rw[w2l_def]
+  \\ rpt $ pop_assum mp_tac
+  \\ map_every qid_spec_tac [`x`,`n`,`b`]
+  \\ recInduct n2l_ind
+  \\ rw[]
+  \\ pop_assum mp_tac
+  \\ rw[Once n2l_def]
+  >- ( irule MOD_LESS \\ gs[] )
+  \\ first_x_assum irule
+  \\ gs[DIV_LT_X]
+  \\ Cases_on`b` \\ gs[MULT]
+QED
+
+Theorem l2w_PAD_RIGHT_0[simp]:
+  0 < b ==> l2w b (PAD_RIGHT 0 h ls) = l2w b ls
+Proof
+  rw[l2w_def]
+QED
+
+Theorem word_and_lsl_eq_0:
+  w2n w1 < 2 ** n ==> w1 && w2 << n = 0w
+Proof
+  Cases_on`w1` \\ Cases_on`w2`
+  \\ rw[word_and_n2w, word_lsl_n2w]
+  \\ drule BITWISE_AND_SHIFT_EQ_0
+  \\ simp[]
+QED
+
+(* -------------------------------------------------------------------------
+    Theorems about word_{to,from}_bin_list
+   ------------------------------------------------------------------------- *)
+
+Theorem LENGTH_word_to_bin_list_bound:
+  LENGTH (word_to_bin_list (w:'a word)) <= (dimindex (:'a))
+Proof
+  rw[word_to_bin_list_def, w2l_def, LENGTH_n2l]
+  \\ Cases_on`w` \\ simp[]
+  \\ fs[dimword_def, GSYM LESS_EQ, LOG2_def, logrootTheory.LT_EXP_LOG]
+QED
+
+Theorem word_from_bin_list_ror:
+  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
+  ==>
+  word_ror (word_from_bin_list ls : 'a word) x =
+  word_from_bin_list (DROP x ls ++ TAKE x ls)
+Proof
+  rw[word_from_bin_list_def, l2w_def]
+  \\ Cases_on`x = 0` \\ gs[SHIFT_ZERO]
+  \\ rw[word_ror_n2w, l2n_APPEND]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ qspecl_then[`x`,`ls`](mp_tac o SYM) listTheory.TAKE_DROP
+  \\ disch_then(SUBST1_TAC o Q.AP_TERM`l2n 2`)
+  \\ rewrite_tac[l2n_APPEND]
+  \\ simp[]
+  \\ qmatch_goalsub_abbrev_tac`BITS _ _ (2 ** x * ld + lt)`
+  \\ qspecl_then[`x - 1`,`0`,`ld`,`lt`]mp_tac BITS_SUM2
+  \\ simp[ADD1]
+  \\ disch_then kall_tac
+  \\ qspecl_then[`x-1`,`lt`]mp_tac BITS_ZEROL
+  \\ simp[ADD1]
+  \\ impl_keep_tac
+  >- (
+    qspecl_then[`TAKE x ls`,`2`]mp_tac l2n_lt
+    \\ simp[] )
+  \\ simp[]
+  \\ disch_then kall_tac
+  \\ simp_tac std_ss [Once ADD_COMM, SimpRHS]
+  \\ qmatch_goalsub_abbrev_tac`BITS h x`
+  \\ qspecl_then[`h`,`x`,`ld`,`lt`]mp_tac BITS_SUM
+  \\ simp[] \\ disch_then kall_tac
+  \\ DEP_REWRITE_TAC[BITS_ZERO4]
+  \\ simp[Abbr`h`]
+  \\ DEP_REWRITE_TAC[BITS_ZEROL]
+  \\ qspecl_then[`DROP x ls`,`2`]mp_tac l2n_lt
+  \\ simp[ADD1]
+QED
+
+Theorem word_from_bin_list_rol:
+  x < dimindex(:'a) /\ LENGTH ls = dimindex(:'a)
+  ==>
+  word_rol (word_from_bin_list ls : 'a word) x =
+  word_from_bin_list (LASTN x ls ++ BUTLASTN x ls)
+Proof
+  rw[word_rol_def]
+  \\ Cases_on`x=0`
+  >- (
+    rw[rich_listTheory.LASTN, rich_listTheory.BUTLASTN]
+    \\ ONCE_REWRITE_TAC[GSYM ROR_MOD]
+    \\ rw[SHIFT_ZERO] )
+  \\ DEP_REWRITE_TAC[word_from_bin_list_ror]
+  \\ simp[rich_listTheory.LASTN_DROP, rich_listTheory.BUTLASTN_TAKE]
+QED
+
+Theorem word_from_bin_list_and:
+  LENGTH l1 = dimindex(:'a) /\
+  LENGTH l2 = dimindex(:'a)
+  ==>
+  word_from_bin_list l1 && word_from_bin_list l2 : 'a word =
+  word_from_bin_list (MAP2 (\x y. bool_to_bit $ (ODD x /\ ODD y)) l1 l2)
+Proof
+  rw[word_from_bin_list_def, l2w_def, word_and_n2w]
+  \\ qmatch_goalsub_abbrev_tac`BITWISE n`
+  \\ qmatch_goalsub_abbrev_tac`a MOD d = b MOD d`
+  \\ `d = 2 ** n`
+  by simp[Abbr`d`, Abbr`n`, dimword_def]
+  \\ `a < d` by (
+    pop_assum SUBST1_TAC
+    \\ qunabbrev_tac`a`
+    \\ irule BITWISE_LT_2EXP )
+  \\ `b < d`
+  by (
+    qunabbrev_tac`b`
+    \\ qmatch_goalsub_abbrev_tac`l2n 2 ls`
+    \\ `n = LENGTH ls` by simp[Abbr`ls`]
+    \\ qunabbrev_tac`d`
+    \\ qpat_x_assum`_ = 2 ** _`SUBST1_TAC
+    \\ pop_assum SUBST1_TAC
+    \\ irule l2n_lt \\ simp[] )
+  \\ simp[]
+  \\ unabbrev_all_tac
+  \\ DEP_REWRITE_TAC[GSYM BITWISE_l2n_2]
+  \\ simp[]
+QED
+
+Theorem word_from_bin_list_not:
+  LENGTH ls = dimindex(:'a) /\ EVERY ($> 2) ls ==>
+  ~word_from_bin_list ls : 'a word =
+  word_from_bin_list (MAP (\x. 1 - x) ls)
+Proof
+  rw[word_from_bin_list_def, l2w_def]
+  \\ rewrite_tac[word_1comp_n2w]
+  \\ Cases_on`l2n 2 ls = dimword(:'a) - 1`
+  >- (
+    mp_then Any (qspec_then`ls`mp_tac)
+      l2n_max (SIMP_CONV(srw_ss())[]``0 < 2n`` |> EQT_ELIM)
+    \\ `dimword (:'a) = 2 ** LENGTH ls` by simp[dimword_def]
+    \\ first_assum (SUBST_ALL_TAC o SYM)
+    \\ pop_assum kall_tac
+    \\ pop_assum SUBST_ALL_TAC
+    \\ simp[ADD1, ZERO_LT_dimword]
+    \\ strip_tac
+    \\ qmatch_goalsub_abbrev_tac`A MOD N = 0`
+    \\ `A = 0` suffices_by rw[]
+    \\ rw[Abbr`A`, l2n_eq_0]
+    \\ gs[listTheory.EVERY_MAP, listTheory.EVERY_MEM]
+    \\ rw[]
+    \\ `2 > x` by simp[]
+    \\ `x < 2` by simp[]
+    \\ pop_assum mp_tac
+    \\ `x MOD 2 = 1` by simp[]
+    \\ rewrite_tac[NUMERAL_LESS_THM]
+    \\ strip_tac \\ fs[] )
+  \\ `SUC (l2n 2 ls) < dimword(:'a)`
+  by (
+    qspecl_then[`ls`,`2`]mp_tac l2n_lt
+    \\ gs[dimword_def] )
+  \\ qmatch_goalsub_abbrev_tac`_ = n2w $ l2n 2 l1`
+  \\ `l2n 2 l1 < dimword(:'a)`
+  by (
+    qspecl_then[`l1`,`2`]mp_tac l2n_lt
+    \\ gs[dimword_def, Abbr`l1`] )
+  \\ simp[Abbr`l1`]
+  \\ drule l2n_2_neg
+  \\ simp[dimword_def]
+QED
+
 (* -------------------------------------------------------------------------
     Create a few word sizes
    ------------------------------------------------------------------------- *)
diff --git a/src/num/extra_theories/bitScript.sml b/src/num/extra_theories/bitScript.sml
index 8ff867a02a..3302624813 100644
--- a/src/num/extra_theories/bitScript.sml
+++ b/src/num/extra_theories/bitScript.sml
@@ -381,6 +381,12 @@ val NOT_MOD2_LEM2 = Q.store_thm("NOT_MOD2_LEM2",
 val ODD_MOD2_LEM = Q.store_thm("ODD_MOD2_LEM",
    `!n. ODD n = ((n MOD 2) = 1)`, RW_TAC arith_ss [ODD_EVEN, MOD_2])
 
+Theorem ODD_MOD_2[simp]:
+  ODD (x MOD 2) = ODD x
+Proof
+  RW_TAC arith_ss [ODD_MOD2_LEM]
+QED
+
 (* ------------------------------------------------------------------------- *)
 
 val DIV_MULT_THM = Q.store_thm("DIV_MULT_THM",
@@ -1520,4 +1526,55 @@ Proof
   simp_tac std_ss []
 QED
 
+Theorem BITWISE_COMM:
+  (!m. m <= n ==> op (BIT m x) (BIT m y) = op (BIT m y) (BIT m x))
+  ==> BITWISE n op x y = BITWISE n op y x
+Proof
+  Induct_on`n`
+  \\ SRW_TAC[][BITWISE_def]
+  \\ first_assum(Q.SPEC_THEN`n`mp_tac)
+  \\ impl_tac >- SRW_TAC[][]
+  \\ disch_then SUBST1_TAC
+  \\ simp[]
+  \\ first_x_assum irule
+  \\ SRW_TAC[][]
+  \\ first_x_assum irule
+  \\ simp[]
+QED
+
+Triviality BITWISE_AND_0_lemma:
+  BITWISE w $/\ x 0 = 0
+Proof
+  Q.ID_SPEC_TAC`x`
+  \\ Induct_on`w`
+  \\ SRW_TAC[][BITWISE_def, SBIT_def, BIT_ZERO]
+QED
+
+Theorem BITWISE_AND_0[simp]:
+  BITWISE w $/\ x 0 = 0 /\
+  BITWISE w $/\ 0 x = 0
+Proof
+  Q.SPECL_THEN[`$/\`,`0`,`x`,`w`]mp_tac(Q.GENL[`op`,`x`,`y`,`n`]BITWISE_COMM)
+  \\ impl_tac >- SRW_TAC[][BIT_ZERO]
+  \\ disch_then SUBST1_TAC
+  \\ SRW_TAC[][BITWISE_AND_0_lemma]
+QED
+
+Theorem BITWISE_AND_SHIFT_EQ_0:
+  !w x y n.
+  x < 2 ** n ==>
+  BITWISE w $/\ x (y * 2 ** n) = 0
+Proof
+  Induct \\ SRW_TAC[][BITWISE_def, SBIT_def]
+  \\ strip_tac
+  \\ Cases_on`w < n`
+  >- ( drule BIT_SHIFT_THM3 \\ simp[]
+       \\ Q.EXISTS_TAC`y` \\ simp[])
+  \\ FULL_SIMP_TAC(srw_ss())[NOT_LESS]
+  \\ drule TWOEXP_MONO2 \\ strip_tac
+  \\ `x < 2 ** w` by METIS_TAC[LESS_LESS_EQ_TRANS]
+  \\ drule NOT_BIT_GT_TWOEXP
+  \\ simp[]
+QED
+
 val _ = export_theory()
diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml
index 9ca58af265..5d7c49a333 100644
--- a/src/num/theories/arithmeticScript.sml
+++ b/src/num/theories/arithmeticScript.sml
@@ -224,6 +224,11 @@ val NRC = new_recursive_definition {
   def = “(NRC R 0 x y = (x = y)) /\
           (NRC R (SUC n) x y = ?z. R x z /\ NRC R n z y)”};
 
+val bool_to_bit_def = new_definition(
+  "bool_to_bit_def",
+  “bool_to_bit b = if b then 1 else 0”
+);
+
 val _ = overload_on ("RELPOW", “NRC”)
 val _ = overload_on ("NRC", “NRC”)
 
@@ -2962,6 +2967,19 @@ Proof
  >> PROVE_TAC []
 QED
 
+Theorem MOD_DIV_SAME[simp]:
+  0 < y ==> x MOD y DIV y = 0
+Proof
+  strip_tac
+  \\ Cases_on`y=1` \\ fs[DIV_1, MOD_1]
+  \\ `1 < y` by (
+    simp[ONE, SUC_LT]
+    \\ Cases_on`y` \\ fs[NOT_LESS_0, ONE]
+    \\ drule (NOT_LT_ZERO_EQ_ZERO |> GSYM |> SPEC_ALL |> iffRL |> CONTRAPOS)
+    \\ rw[] )
+  \\ rw[DIV_EQ_0, MOD_LESS]
+QED
+
 (* ------------------------------------------------------------------------ *)
 (* Some miscellaneous lemmas (from transc.ml)                               *)
 (* ------------------------------------------------------------------------ *)
@@ -4997,4 +5015,34 @@ val MOD_EXP = store_thm(
   `_ = (a * a ** m) MOD n` by rw[MOD_TIMES2] >>
   rw[EXP]);
 
+Theorem ODD_bool_to_bit[simp]:
+  ODD (bool_to_bit b) = b /\
+  ODD (1 - bool_to_bit b) = ~b
+Proof
+  rw[bool_to_bit_def, ODD, ONE, SUB_MONO_EQ, SUB_0]
+QED
+
+Theorem bool_to_bit_neq_add:
+  bool_to_bit (x <> y) =
+  (bool_to_bit x + bool_to_bit y) MOD 2
+Proof
+  reverse(rw[bool_to_bit_def, ADD_0, ADD])
+  >- (
+    rw[ONE, ADD] \\ rw[GSYM TWO, GSYM ONE]
+    \\ irule EQ_SYM
+    \\ irule (DIVMOD_ID |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL)
+    \\ rw[TWO, LESS_0] )
+  \\ irule EQ_SYM
+  \\ irule ONE_MOD
+  \\ rw[ONE, TWO, LESS_MONO, LESS_0]
+QED
+
+Theorem bool_to_bit_MOD_2[simp]:
+  bool_to_bit x MOD 2 = bool_to_bit x
+Proof
+  rw[bool_to_bit_def]
+  \\ irule ONE_MOD
+  \\ rw[ONE, TWO, LESS_MONO, LESS_0]
+QED
+
 val _ = export_theory()
diff --git a/src/num/theories/cv_compute/automation/cv_primScript.sml b/src/num/theories/cv_compute/automation/cv_primScript.sml
index 3df66869bc..eb7085391e 100644
--- a/src/num/theories/cv_compute/automation/cv_primScript.sml
+++ b/src/num/theories/cv_compute/automation/cv_primScript.sml
@@ -1239,9 +1239,6 @@ Proof
   \\ completeInduct_on ‘m’
   \\ simp [Once cv_word_and_loop_def]
   \\ Cases_on ‘m = 0’ \\ fs [wordsTheory.WORD_AND_CLAUSES]
-  >-
-   (qsuff_tac ‘!l n. BITWISE l $/\ 0 n = 0’ >- fs []
-    \\ Induct \\ fs [BITWISE])
   \\ gvs [PULL_FORALL,AND_IMP_INTRO] \\ rw []
   \\ Cases_on ‘l’ \\ gvs []
   \\ rename [‘n < 2 ** SUC l’]