From 55fc604a4ec317844b3f3305d181463a43dfd827 Mon Sep 17 00:00:00 2001
From: "Chun Tian (binghe)" <binghe.lisp@gmail.com>
Date: Wed, 14 Feb 2024 17:02:36 +1100
Subject: [PATCH] [lambda] Advanced properties of principle_hnf

---
 examples/lambda/barendregt/boehmScript.sml    | 202 +++++--
 examples/lambda/barendregt/chap2Script.sml    | 117 +++-
 .../barendregt/head_reductionScript.sml       | 381 ++++++++++++-
 examples/lambda/barendregt/solvableScript.sml | 507 ++++++++++++++++--
 examples/lambda/basics/appFOLDLScript.sml     |  13 +
 examples/lambda/basics/termScript.sml         |   3 +-
 6 files changed, 1128 insertions(+), 95 deletions(-)

diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
index 6b8a3014b9..52bfb0c75e 100644
--- a/examples/lambda/barendregt/boehmScript.sml
+++ b/examples/lambda/barendregt/boehmScript.sml
@@ -59,7 +59,7 @@ Definition BT_generator_def :
       if solvable M then
          let M0 = principle_hnf M;
               n = LAMl_size M0;
-             vs = FRESH_list n (X UNION FV M);
+             vs = FRESH_list n (X UNION FV M0);
              M1 = principle_hnf (M0 @* (MAP VAR vs));
              Ms = hnf_children M1;
               l = MAP ($, (X UNION set vs)) Ms;
@@ -77,7 +77,6 @@ End
 
 Overload BTe = “\X M. BT (X,M)”
 
-(* BTe is actually the Curry-ized version of BT *)
 Theorem BTe_def :
     !X M. BTe X M = CURRY BT X M
 Proof
@@ -122,6 +121,21 @@ Proof
     rw [BT_of_unsolvables]
 QED
 
+Theorem BT_of_principle_hnf :
+    !X M. solvable M ==> BTe X (principle_hnf M) = BTe X M
+Proof
+    reverse (RW_TAC std_ss [BT_def, BT_generator_def, ltree_unfold])
+ >- (Q.PAT_X_ASSUM ‘unsolvable M0’ MP_TAC >> simp [] \\
+     rw [Abbr ‘M0’, solvable_iff_has_hnf] \\
+     MATCH_MP_TAC hnf_has_hnf \\
+     MATCH_MP_TAC hnf_principle_hnf' >> art [])
+ >> ‘M0' = M0’ by rw [Abbr ‘M0'’, Abbr ‘M0’, principle_hnf_stable']
+ >> qunabbrev_tac ‘M0'’
+ >> POP_ASSUM (rfs o wrap)
+ >> ‘principle_hnf M0 = M0’ by rw [Abbr ‘M0’, principle_hnf_stable']
+ >> POP_ASSUM (rfs o wrap)
+QED
+
 Theorem BT_finite_branching :
     !X M. finite_branching (BTe X M)
 Proof
@@ -145,7 +159,7 @@ Proof
  >> rw [every_fromList_EVERY, LMAP_fromList, EVERY_MAP, Abbr ‘P’, EVERY_MEM]
  >> qabbrev_tac ‘M0 = principle_hnf M’
  >> qabbrev_tac ‘n = LAMl_size M0’
- >> qabbrev_tac ‘vs = FRESH_list n (X UNION FV M)’
+ >> qabbrev_tac ‘vs = FRESH_list n (X UNION FV M0)’
  >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
  >> rename1 ‘MEM N (hnf_children M1)’
  >> qexistsl_tac [‘X UNION set vs’, ‘N’] >> rw [BT_def]
@@ -180,7 +194,7 @@ end;
    NOTE: X is an sufficiently large finite set of names covering all FVs of
          M and N. The Boehm trees of M and N are generated with help of this set.
 
-   TODO: this theorem can be improved to an iff: M == N <=> BTe X M = BTe X N
+   NOTE2: this theorem can be improved to an iff: M == N <=> BTe X M = BTe X N
  *)
 Theorem lameq_BT_cong :
     !X M N. FINITE X /\ FV M UNION FV N SUBSET X ==>
@@ -204,8 +218,8 @@ Proof
  >> qabbrev_tac ‘Q0 = principle_hnf Q’
  >> qabbrev_tac ‘n  = LAMl_size P0’
  >> qabbrev_tac ‘n' = LAMl_size Q0’
- >> qabbrev_tac ‘vs = FRESH_list n (Y UNION FV P)’
- >> qabbrev_tac ‘vs' = FRESH_list n' (Y UNION FV Q)’
+ >> qabbrev_tac ‘vs = FRESH_list n  (Y UNION FV P0)’
+ >> qabbrev_tac ‘vs'= FRESH_list n' (Y UNION FV Q0)’
  >> qabbrev_tac ‘P1 = principle_hnf (P0 @* MAP VAR vs)’
  >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs')’
  >> qabbrev_tac ‘Ps = hnf_children P1’
@@ -225,8 +239,11 @@ Proof
  (* now both P and Q are solvable *)
  >> ‘solvable Q’ by PROVE_TAC [lameq_solvable_cong]
  (* clean up definitions of vs and vs' by using ‘FV M UNION FV N SUBSET X’ *)
- >> Know ‘Y UNION FV P = Y /\ Y UNION FV Q = Y’
- >- (Q.PAT_X_ASSUM ‘FV P UNION FV Q SUBSET Y’ MP_TAC >> SET_TAC [])
+ >> Know ‘Y UNION FV P0 = Y /\ Y UNION FV Q0 = Y’
+ >- (Q.PAT_X_ASSUM ‘FV P UNION FV Q SUBSET Y’ MP_TAC \\
+    ‘FV P0 SUBSET FV P’ by METIS_TAC [principle_hnf_FV_SUBSET'] \\
+    ‘FV Q0 SUBSET FV Q’ by METIS_TAC [principle_hnf_FV_SUBSET'] \\
+     NTAC 2 (POP_ASSUM MP_TAC) >> SET_TAC [])
  >> DISCH_THEN (fs o wrap)
  >> Know ‘n = n' /\ vs = vs'’
  >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
@@ -238,7 +255,7 @@ Proof
  (* proving y = y' *)
  >> STRONG_CONJ_TAC
  >- (MP_TAC (Q.SPECL [‘Y’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’]
-                     lameq_principle_hnf_headvar_eq') >> simp [])
+                     lameq_principle_hnf_head_eq') >> simp [])
  >> DISCH_THEN (rfs o wrap o GSYM)
  >> qunabbrevl_tac [‘y’, ‘y'’]
  (* applying lameq_principle_hnf_thm' *)
@@ -335,10 +352,10 @@ Definition subterm_def :
     subterm X M (x::xs) = if solvable M then
         let M0 = principle_hnf M;
              n = LAMl_size M0;
-            vs = FRESH_list n (X UNION FV M);
+             m = hnf_children_size M0;
+            vs = FRESH_list n (X UNION FV M0);
             M1 = principle_hnf (M0 @* (MAP VAR vs));
-            Ms = hnf_children M1;
-             m = LENGTH Ms
+            Ms = hnf_children M1
         in
             if x < m then subterm (X UNION set vs) (EL x Ms) xs else NONE
     else
@@ -347,13 +364,13 @@ End
 
 Theorem subterm_of_solvables :
     !X M x xs. solvable M ==>
-               subterm X M (x::xs) =
+      subterm X M (x::xs) =
         let M0 = principle_hnf M;
              n = LAMl_size M0;
-            vs = FRESH_list n (X UNION FV M);
+             m = hnf_children_size M0;
+            vs = FRESH_list n (X UNION FV M0);
             M1 = principle_hnf (M0 @* (MAP VAR vs));
-            Ms = hnf_children M1;
-             m = LENGTH Ms
+            Ms = hnf_children M1
         in
             if x < m then subterm (X UNION set vs) (EL x Ms) xs else NONE
 Proof
@@ -361,6 +378,47 @@ Proof
  >> rw [subterm_def]
 QED
 
+(* M0 is not needed if M is already an hnf *)
+Theorem subterm_of_hnf :
+    !X M x xs. FINITE X /\ hnf M ==>
+      subterm X M (x::xs) =
+        let  n = LAMl_size M;
+             m = hnf_children_size M;
+            vs = FRESH_list n (X UNION FV M);
+            M1 = principle_hnf (M @* (MAP VAR vs));
+            Ms = hnf_children M1
+        in
+            if x < m then subterm (X UNION set vs) (EL x Ms) xs else NONE
+Proof
+    rpt STRIP_TAC
+ >> ‘solvable M’ by PROVE_TAC [solvable_iff_has_hnf, hnf_has_hnf]
+ >> RW_TAC std_ss [subterm_of_solvables]
+ >> ‘M0 = M’ by rw [Abbr ‘M0’, principle_hnf_reduce]
+ >> POP_ASSUM (fn th => gs [Abbr ‘M0’, th])
+QED
+
+(* In the extreme case, M is a absfree hnf (i.e. VAR y @* args), and the
+   definition of subterm can be greatly simplified.
+ *)
+Theorem subterm_of_absfree_hnf :
+    !X M x xs. FINITE X /\ hnf M /\ ~is_abs M ==>
+      subterm X M (x::xs) =
+        let  m = hnf_children_size M;
+            Ms = hnf_children M
+        in
+            if x < m then subterm X (EL x Ms) xs else NONE
+Proof
+    rpt STRIP_TAC
+ >> ‘solvable M’ by PROVE_TAC [solvable_iff_has_hnf, hnf_has_hnf]
+ >> RW_TAC std_ss [subterm_of_solvables]
+ >> ‘?y args. M = VAR y @* args’ by PROVE_TAC [absfree_hnf_cases]
+ >> gs [Abbr ‘m’, Abbr ‘M0’, Abbr ‘Ms’, Abbr ‘n’, hnf_children_hnf, hnf_appstar]
+ >> ‘FINITE (X UNION FV (VAR y @* args))’ by rw []
+ >> POP_ASSUM (MP_TAC o (Q.SPEC ‘0’) o (MATCH_MP FRESH_list_def))
+ >> rw []
+ >> gs [Abbr ‘Ms'’, Abbr ‘M1’, hnf_children_hnf]
+QED
+
 (* NOTE: The uses of ‘subterm' X M p’ assumes ‘subterm X M p <> NONE’ *)
 Overload subterm' = “\X M p. SND (THE (subterm X M p))”
 
@@ -373,6 +431,26 @@ Proof
     rw [subterm_NIL]
 QED
 
+(* NOTE: This theorem is only possible when ‘vs = FRESH_list n (X UNION FV M0)’
+        (instead of ‘FV M’) in the definition of [subterm_def].
+ *)
+Theorem subterm_of_principle_hnf :
+    !X M p. solvable M /\ p <> [] ==> subterm X (principle_hnf M) p = subterm X M p
+Proof
+    rpt STRIP_TAC
+ >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
+ >> Cases_on ‘p’ >> fs []
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ >> ‘solvable M0’ by PROVE_TAC [solvable_principle_hnf]
+ >> RW_TAC std_ss [subterm_of_solvables]
+ >> ‘M0' = M0’ by rw [Abbr ‘M0'’, Abbr ‘M0’, principle_hnf_stable']
+ >> qunabbrev_tac ‘M0'’
+ >> POP_ASSUM (fs o wrap)
+ >> ‘vs' = vs’ by rw [Abbr ‘vs’, Abbr ‘vs'’]
+ >> POP_ASSUM (fs o wrap)
+ >> PROVE_TAC []
+QED
+
 (* Lemma 10.1.15 [1, p.222] *)
 Theorem BT_subterm_thm :
     !p X M. p IN ltree_paths (BTe X M) /\ subterm X M p <> NONE ==>
@@ -383,7 +461,7 @@ Proof
  >> rw [subterm_def, ltree_lookup]
  >> qabbrev_tac ‘M0 = principle_hnf M’
  >> qabbrev_tac ‘n = LAMl_size M0’
- >> qabbrev_tac ‘vs = FRESH_list n (X UNION FV M)’
+ >> qabbrev_tac ‘vs = FRESH_list n (X UNION FV M0)’
  >> qabbrev_tac ‘M1 = principle_hnf (M0 @* (MAP VAR vs))’
  >> qabbrev_tac ‘Ms = hnf_children M1’
  >> Know ‘BTe X M = ltree_unfold BT_generator (X,M)’ >- rw [BT_def]
@@ -403,15 +481,17 @@ QED
    even improved to an iff, as the present theorem shows.
  *)
 Theorem subterm_is_none_iff_parent_unsolvable :
-    !p X M. p IN ltree_paths (BTe X M) ==>
+    !p X M. FINITE X /\ p IN ltree_paths (BTe X M) ==>
            (subterm X M p = NONE <=>
             p <> [] /\ subterm X M (FRONT p) <> NONE /\
             unsolvable (subterm' X M (FRONT p)))
 Proof
-    Induct_on ‘p’ >> rw [subterm_def] (* 2 subgoals, only one left *)
+    Induct_on ‘p’
+ >> rw [subterm_def] (* 2 subgoals, only one left *)
  >> qabbrev_tac ‘M0 = principle_hnf M’
  >> qabbrev_tac ‘n = LAMl_size M0’
- >> qabbrev_tac ‘vs = FRESH_list n (X UNION FV M)’
+ >> qabbrev_tac ‘m = hnf_children_size M0’
+ >> qabbrev_tac ‘vs = FRESH_list n (X UNION FV M0)’
  >> qabbrev_tac ‘M1 = principle_hnf (M0 @* (MAP VAR vs))’
  >> qabbrev_tac ‘Ms = hnf_children M1’
  >> reverse (Cases_on ‘solvable M’)
@@ -419,6 +499,26 @@ Proof
      Q.PAT_X_ASSUM ‘h::p IN ltree_paths (BTe X M)’ MP_TAC \\
      simp [BT_of_unsolvables, ltree_paths_def, ltree_lookup_def])
  >> simp []
+ >> Know ‘m = LENGTH Ms’
+ >- (qunabbrev_tac ‘M1’ \\
+    ‘ALL_DISTINCT vs /\ LENGTH vs = n /\ DISJOINT (set vs) (X UNION FV M0)’
+       by (rw [Abbr ‘vs’, FRESH_list_def]) \\
+    ‘hnf M0’ by rw [hnf_principle_hnf', Abbr ‘M0’] \\
+     Know ‘?y args. M0 = LAMl (TAKE n vs) (VAR y @* args)’
+     >- (qunabbrev_tac ‘n’ >> irule (iffLR hnf_cases_shared) >> rw [] \\
+         MATCH_MP_TAC DISJOINT_SUBSET \\
+         Q.EXISTS_TAC ‘X UNION FV M0’ >> art [] \\
+         SET_TAC []) >> STRIP_TAC \\
+    ‘TAKE n vs = vs’ by rw [] \\
+     POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap) \\
+     qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’ \\
+     Know ‘M1 = VAR y @* args’
+     >- (qunabbrev_tac ‘M1’ >> POP_ORW \\
+         MATCH_MP_TAC principle_hnf_beta_reduce >> rw [hnf_appstar]) \\
+     qunabbrev_tac ‘Ms’ \\
+     Rewr' >> simp [hnf_children_hnf] \\
+     qunabbrev_tac ‘m’ >> simp [])
+ >> DISCH_TAC
  (* stage work, now M is solvable *)
  >> Cases_on ‘p = []’
  >- (rw [subterm_NIL] \\
@@ -447,7 +547,7 @@ Proof
 QED
 
 Theorem subterm_is_none_imp_parent_not :
-    !p X M. p IN ltree_paths (BTe X M) /\
+    !p X M. FINITE X /\ p IN ltree_paths (BTe X M) /\
             subterm X M p = NONE ==> subterm X M (FRONT p) <> NONE
 Proof
     METIS_TAC [subterm_is_none_iff_parent_unsolvable]
@@ -485,8 +585,11 @@ Proof
      Cases_on ‘p’ >> fs [subterm_def])
  >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
  >> RW_TAC std_ss [subterm_of_solvables]
- >> Know ‘X UNION FV M = X /\ X UNION FV N = X’
- >- (Q.PAT_X_ASSUM ‘FV M UNION FV N SUBSET X’ MP_TAC >> SET_TAC [])
+ >> Know ‘X UNION FV M0 = X /\ X UNION FV M0' = X’
+ >- (Q.PAT_X_ASSUM ‘FV M UNION FV N SUBSET X’ MP_TAC \\
+    ‘FV M0 SUBSET FV M’ by METIS_TAC [principle_hnf_FV_SUBSET'] \\
+    ‘FV M0' SUBSET FV N’ by METIS_TAC [principle_hnf_FV_SUBSET'] \\
+     NTAC 2 (POP_ASSUM MP_TAC) >> SET_TAC [])
  >> DISCH_THEN (fs o wrap)
  >> Know ‘n = n' /\ vs = vs'’
  >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
@@ -499,9 +602,6 @@ Proof
  >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘N’, ‘M0’, ‘M0'’, ‘n’, ‘vs’, ‘M1’, ‘M1'’]
                      lameq_principle_hnf_thm') >> simp []
  >> RW_TAC std_ss [Abbr ‘m’, Abbr ‘m'’]
- >> qabbrev_tac ‘m = LENGTH Ms'’
- >> Cases_on ‘h < m’ >> simp []
- >> Cases_on ‘p = []’ >> fs []
  (* preparing for hnf_children_FV_SUBSET
 
     Here, once again, we need to get suitable explicit forms of P0 and Q0,
@@ -510,7 +610,7 @@ Proof
  >> ‘hnf M0 /\ hnf M0'’ by PROVE_TAC [hnf_principle_hnf']
  >> qabbrev_tac ‘n = LAMl_size M0’
  >> ‘ALL_DISTINCT vs /\ LENGTH vs = n /\ DISJOINT (set vs) X’
-      by rw [Abbr ‘vs’, FRESH_list_def]
+       by rw [Abbr ‘vs’, FRESH_list_def]
  >> Know ‘DISJOINT (set vs) (FV M0)’
  >- (MATCH_MP_TAC DISJOINT_SUBSET \\
      Q.EXISTS_TAC ‘X’ >> art [] \\
@@ -540,7 +640,20 @@ Proof
  >> qunabbrevl_tac [‘M1’, ‘M1'’]
  >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
  >> qabbrev_tac ‘M1' = principle_hnf (M0' @* MAP VAR vs)’
- (* final stage *)
+ >> Know ‘LENGTH args = LENGTH Ms’
+ >- (qunabbrev_tac ‘Ms’ \\
+     Q.PAT_X_ASSUM ‘M1 = VAR y @* args’ (ONCE_REWRITE_TAC o wrap) \\
+     simp [hnf_children_hnf])
+ >> Rewr'
+ >> Know ‘LENGTH args' = LENGTH Ms'’
+ >- (qunabbrev_tac ‘Ms'’ \\
+     Q.PAT_X_ASSUM ‘M1' = VAR y' @* args'’ (ONCE_REWRITE_TAC o wrap) \\
+     simp [hnf_children_hnf])
+ >> Rewr'
+ >> qabbrev_tac ‘m = LENGTH Ms'’
+ >> Cases_on ‘h < m’ >> simp []
+ >> Cases_on ‘p = []’ >> fs []
+  (* final stage *)
  >> FIRST_X_ASSUM MATCH_MP_TAC >> simp []
  >> CONJ_TAC (* 2 subgoals *)
  >| [ (* goal 1 (of 2) *)
@@ -588,7 +701,12 @@ Proof
  >> Q.PAT_X_ASSUM ‘subterm X M (h::p) <> NONE’ MP_TAC
  >> RW_TAC std_ss [subterm_of_solvables]
  >> gs []
- >> Know ‘X UNION FV M = X /\ X UNION FV N = X’ >- ASM_SET_TAC []
+ >> Know ‘X UNION FV M0 = X /\ X UNION FV M0' = X’
+ >- (Q.PAT_X_ASSUM ‘FV M SUBSET X’ MP_TAC \\
+     Q.PAT_X_ASSUM ‘FV N SUBSET X’ MP_TAC \\
+    ‘FV M0 SUBSET FV M’ by METIS_TAC [principle_hnf_FV_SUBSET'] \\
+    ‘FV M0' SUBSET FV N’ by METIS_TAC [principle_hnf_FV_SUBSET'] \\
+     NTAC 2 (POP_ASSUM MP_TAC) >> SET_TAC [])
  >> DISCH_THEN (fs o wrap)
  >> Know ‘n = n' /\ vs = vs'’
  >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
@@ -601,8 +719,6 @@ Proof
  >> MP_TAC (Q.SPECL [‘X’, ‘M’, ‘N’, ‘M0’, ‘M0'’, ‘n’, ‘vs’, ‘M1’, ‘M1'’]
                      lameq_principle_hnf_thm') >> simp []
  >> RW_TAC std_ss [Abbr ‘m’, Abbr ‘m'’]
- >> qabbrev_tac ‘m = LENGTH Ms'’
- >> Cases_on ‘p = []’ >> fs []
  (* preparing for hnf_children_FV_SUBSET *)
  >> ‘hnf M0 /\ hnf M0'’ by PROVE_TAC [hnf_principle_hnf']
  >> qabbrev_tac ‘n = LAMl_size M0’
@@ -633,10 +749,22 @@ Proof
  >> Q.PAT_X_ASSUM ‘n = LAMl_size M0'’ (rfs o wrap o SYM)
  >> ‘TAKE n vs = vs’ by rw [TAKE_LENGTH_ID_rwt]
  >> POP_ASSUM (rfs o wrap)
- (* refine P1 and Q1 again for clear assumptions using them *)
+  (* refine P1 and Q1 again for clear assumptions using them *)
  >> qunabbrevl_tac [‘M1’, ‘M1'’]
  >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
  >> qabbrev_tac ‘M1' = principle_hnf (M0' @* MAP VAR vs)’
+ >> Know ‘LENGTH args = LENGTH Ms’
+ >- (qunabbrev_tac ‘Ms’ \\
+     Q.PAT_X_ASSUM ‘M1 = VAR y @* args’ (ONCE_REWRITE_TAC o wrap) \\
+     simp [hnf_children_hnf])
+ >> DISCH_TAC
+ >> Know ‘LENGTH args' = LENGTH Ms'’
+ >- (qunabbrev_tac ‘Ms'’ \\
+     Q.PAT_X_ASSUM ‘M1' = VAR y' @* args'’ (ONCE_REWRITE_TAC o wrap) \\
+     simp [hnf_children_hnf])
+ >> DISCH_TAC
+ >> qabbrev_tac ‘m = LENGTH Ms'’
+ >> Cases_on ‘p = []’ >> fs []
  (* final stage *)
  >> FIRST_X_ASSUM MATCH_MP_TAC >> simp []
  >> CONJ_TAC (* 2 subgoals *)
@@ -1268,7 +1396,7 @@ Proof
      CONJ_TAC >- art [] \\
      qunabbrev_tac ‘M0’ \\
      MATCH_MP_TAC lameq_SYM \\
-     MATCH_MP_TAC lameq_principle_hnf_reduce' >> art [])
+     MATCH_MP_TAC lameq_principle_hnf' >> art [])
  >> ONCE_REWRITE_TAC [Boehm_apply_APPEND]
  >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘apply (p3 ++ p2) M1’
@@ -1562,7 +1690,7 @@ Proof
        Q.EXISTS_TAC ‘apply (p1 ++ p0) N0’ \\
        CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf_reduce >> art [GSYM solvable_iff_has_hnf]) \\
+                    MATCH_MP_TAC lameq_principle_hnf >> art [GSYM solvable_iff_has_hnf]) \\
     (* eliminating p0 *)
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
@@ -1600,7 +1728,7 @@ Proof
        CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘M0’ \\
                     MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf_reduce >> art [GSYM solvable_iff_has_hnf]) \\
+                    MATCH_MP_TAC lameq_principle_hnf >> art [GSYM solvable_iff_has_hnf]) \\
     (* eliminating p0 *)
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
@@ -1688,7 +1816,7 @@ Proof
        Q.EXISTS_TAC ‘apply (pi ++ p0) M0’ \\
        CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘M0’ >> MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf_reduce \\
+                    MATCH_MP_TAC lameq_principle_hnf \\
                     ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
@@ -1701,7 +1829,7 @@ Proof
        Q.EXISTS_TAC ‘apply (pi ++ p0) N0’ \\
        CONJ_TAC >- (MATCH_MP_TAC Boehm_apply_lameq_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf_reduce \\
+                    MATCH_MP_TAC lameq_principle_hnf \\
                     ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
diff --git a/examples/lambda/barendregt/chap2Script.sml b/examples/lambda/barendregt/chap2Script.sml
index 723d20755c..b50c0c60da 100644
--- a/examples/lambda/barendregt/chap2Script.sml
+++ b/examples/lambda/barendregt/chap2Script.sml
@@ -5,7 +5,7 @@
 open HolKernel Parse boolLib bossLib;
 
 open pred_setTheory pred_setLib listTheory rich_listTheory finite_mapTheory
-     arithmeticTheory hurdUtils;
+     arithmeticTheory string_numTheory hurdUtils;
 
 open termTheory BasicProvers nomsetTheory binderLib appFOLDLTheory;
 
@@ -774,6 +774,24 @@ Proof
  >> SRW_TAC [][]
 QED
 
+Theorem term_cases_disjoint :
+    !t. ~(is_comb t /\ is_abs t) /\
+        ~(is_comb t /\ is_var t) /\
+        ~(is_abs t /\ is_var t)
+Proof
+    Q.X_GEN_TAC ‘t’
+ >> rpt CONJ_TAC
+ >| [ (* goal 1 (of 3) *)
+      Suff ‘is_abs t ==> ~is_comb t’ >- PROVE_TAC [] \\
+      rw [is_abs_cases] >> rw [],
+      (* goal 2 (of 3) *)
+      Suff ‘is_var t ==> ~is_comb t’ >- PROVE_TAC [] \\
+      rw [is_var_cases] >> rw [],
+      (* goal 3 (of 3) *)
+      Suff ‘is_abs t ==> ~is_var t’ >- PROVE_TAC [] \\
+      rw [is_abs_cases] >> rw [] ]
+QED
+
 Theorem term_laml_cases:
   ∀X. FINITE X ⇒
       ∀t. (∃s. t = VAR s) ∨ (∃M1 M2. t = M1 @@ M2) ∨
@@ -1155,7 +1173,7 @@ val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"}
 
 (* permutator [1, p.247] *)
 Definition permutator_def :
-    permutator n = let Z = FRESH_list (n + 1) {};
+    permutator n = let Z = GENLIST n2s (n + 1);
                        z = LAST Z;
                    in
                        LAMl Z (VAR z @* MAP VAR (FRONT Z))
@@ -1165,13 +1183,14 @@ Theorem closed_permutator :
     !n. closed (permutator n)
 Proof
     rw [closed_def, permutator_def, FV_LAMl]
- >> qabbrev_tac ‘Z = FRESH_list (n + 1) {}’
- >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’ by rw [FRESH_list_def, Abbr ‘Z’]
+ >> qabbrev_tac ‘Z = GENLIST n2s (n + 1)’
+ >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’
+       by (rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST])
  >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
  >> qabbrev_tac ‘z = LAST Z’
  >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL]
- >> Suff ‘FV (VAR z @* MAP VAR (FRONT Z)) SUBSET set Z’ >- SET_TAC []
- >> rw [FV_appstar, SUBSET_DEF, MEM_MAP] >- art []
+ >> Suff ‘{z} UNION set (FRONT Z) SUBSET set Z’ >- SET_TAC []
+ >> rw [SUBSET_DEF]
  >> rfs [MEM_FRONT_NOT_NIL]
 QED
 
@@ -1183,8 +1202,9 @@ Theorem permutator_thm :
 Proof
     RW_TAC std_ss [permutator_def]
  >> qabbrev_tac ‘n = LENGTH Ns’
- >> qabbrev_tac ‘Z = FRESH_list (n + 1) {}’
- >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’ by rw [FRESH_list_def, Abbr ‘Z’]
+ >> qabbrev_tac ‘Z = GENLIST n2s (n + 1)’
+ >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’
+       by (rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST])
  >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
  >> qabbrev_tac ‘z = LAST Z’
  >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL]
@@ -1338,6 +1358,87 @@ Proof
  >> rw [Abbr ‘y’, MEM_LAST_NOT_NIL]
 QED
 
+Definition selector_def :
+    selector i n = LAMl (GENLIST n2s n) (VAR (n2s i))
+End
+
+Theorem closed_selector :
+    !i n. i < n ==> closed (selector i n)
+Proof
+    rw [closed_def, selector_def, FV_LAMl]
+ >> POP_ASSUM MP_TAC >> rw [MEM_GENLIST]
+QED
+
+(* |- !i n. i < n ==> FV (selector i n) = {} *)
+Theorem FV_selector[simp] = REWRITE_RULE [closed_def] closed_selector
+
+Theorem selector_thm :
+    !i n Ns. i < n /\ LENGTH Ns = n ==> selector i n @* Ns == EL i Ns
+Proof
+    RW_TAC std_ss [selector_def]
+ >> qabbrev_tac ‘n = LENGTH Ns’
+ >> qabbrev_tac ‘Z = GENLIST n2s n’
+ >> ‘ALL_DISTINCT Z /\ LENGTH Z = n’ by rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST]
+ >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> qabbrev_tac ‘z = n2s i’
+ >> Know ‘MEM z Z’
+ >- (rw [Abbr ‘Z’, Abbr ‘z’, MEM_GENLIST] \\
+     Q.EXISTS_TAC ‘i’ >> art [])
+ >> DISCH_TAC
+ (* preparing for LAMl_ALPHA_ssub *)
+ >> qabbrev_tac
+     ‘Y = FRESH_list n (set Z UNION (BIGUNION (IMAGE FV (set Ns))))’
+ >> Know ‘FINITE (set Z UNION (BIGUNION (IMAGE FV (set Ns))))’
+ >- (rw [] >> rw [FINITE_FV])
+ >> DISCH_TAC
+ >> Know ‘ALL_DISTINCT Y /\
+          DISJOINT (set Y) (set Z UNION (BIGUNION (IMAGE FV (set Ns)))) /\
+          LENGTH Y = n’
+ >- (ASM_SIMP_TAC std_ss [FRESH_list_def, Abbr ‘Y’])
+ >> rw []
+ (* applying LAMl_ALPHA_ssub *)
+ >> Know ‘LAMl Z (VAR z) = LAMl Y ((FEMPTY |++ ZIP (Z,MAP VAR Y)) ' (VAR z))’
+ >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [] \\
+     Q.PAT_X_ASSUM ‘DISJOINT (set Z) (set Y)’ MP_TAC \\
+     rw [DISJOINT_ALT])
+ >> Rewr'
+ >> ‘Y <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> REWRITE_TAC [GSYM fromPairs_def]
+ >> qabbrev_tac ‘fm = fromPairs Z (MAP VAR Y)’
+ >> ‘FDOM fm = set Z’ by rw [FDOM_fromPairs, Abbr ‘fm’]
+ >> Know ‘fm ' (VAR z) = EL i (MAP VAR Y)’
+ >- (rw [ssub_thm] \\
+     Know ‘z = EL i Z’
+     >- (simp [Abbr ‘Z’, Abbr ‘z’] \\
+         fs [LENGTH_GENLIST, EL_GENLIST]) >> Rewr' \\
+     qunabbrev_tac ‘fm’ \\
+     MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw [])
+ >> Rewr'
+ (* stage work *)
+ >> qabbrev_tac ‘t = EL i (MAP VAR Y)’
+ >> Suff ‘EL i Ns = (FEMPTY |++ ZIP (Y,Ns)) ' t’
+ >- (Rewr' \\
+     MATCH_MP_TAC lameq_LAMl_appstar_ssub >> rw [] \\
+     ONCE_REWRITE_TAC [DISJOINT_SYM] \\
+     FIRST_X_ASSUM MATCH_MP_TAC \\
+     Q.EXISTS_TAC ‘x’ >> art [])
+ (* cleanup ‘fm’ *)
+ >> Q.PAT_X_ASSUM ‘FDOM fm = set Z’ K_TAC
+ >> qunabbrev_tac ‘fm’
+ (* stage work *)
+ >> REWRITE_TAC [Once EQ_SYM_EQ, GSYM fromPairs_def]
+ >> qabbrev_tac ‘fm = fromPairs Y Ns’
+ >> ‘FDOM fm = set Y’ by rw [Abbr ‘fm’, FDOM_fromPairs]
+ >> simp [Abbr ‘t’, EL_MAP]
+ >> Know ‘MEM (EL i Y) Y’
+ >- (rw [MEM_EL] \\
+     Q.EXISTS_TAC ‘i’ >> rw [])
+ >> Rewr
+ >> Q.PAT_X_ASSUM ‘FDOM fm = set Y’ K_TAC
+ >> simp [Abbr ‘fm’]
+ >> MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []
+QED
+
 (* ----------------------------------------------------------------------
     closed terms and closures of (open or closed) terms, leading into
     B's Chapter 2's section “Solvable and unsolvable terms” p41.
diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml
index f59523ffe1..8233b57d38 100644
--- a/examples/lambda/barendregt/head_reductionScript.sml
+++ b/examples/lambda/barendregt/head_reductionScript.sml
@@ -28,6 +28,14 @@ val _ = overload_on ("-h->", ``hreduce1``)
 val _ = set_fixity "-h->*" (Infix(NONASSOC, 450))
 val _ = overload_on ("-h->*", ``hreduce1^*``)
 
+Theorem hreduce_TRANS :
+    !M0 M1 M2. M0 -h->* M1 /\ M1 -h->* M2 ==> M0 -h->* M2
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)
+ >> Q.EXISTS_TAC ‘M1’ >> art []
+QED
+
 val hreduce_ccbeta = store_thm(
   "hreduce_ccbeta",
   ``∀M N. M -h-> N ⇒ M -β-> N``,
@@ -49,6 +57,14 @@ Proof
  >> METIS_TAC [relationTheory.RTC_RULES, hreduce1_FV]
 QED
 
+Theorem hreduce_FV_SUBSET :
+    !M N. M -h->* N ==> FV N SUBSET FV M
+Proof
+    rw [SUBSET_DEF]
+ >> irule hreduces_FV
+ >> Q.EXISTS_TAC ‘N’ >> art []
+QED
+
 val _ = temp_add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT,2)),
                        fixity = Infix(NONASSOC, 950),
                        paren_style = OnlyIfNecessary,
@@ -114,6 +130,69 @@ Proof
  >> fs [hreduce1_rules]
 QED
 
+Theorem hreduce1_LAMl :
+    !vs M1 M2. M1 -h-> M2 ==> LAMl vs M1 -h-> LAMl vs M2
+Proof
+    Induct_on ‘vs’ >> rw []
+ >> MATCH_MP_TAC hreduce1_LAM
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
+QED
+
+Theorem hreduce1_abs :
+    !M N. M -h-> N ==> is_abs M ==> is_abs N
+Proof
+    rw [Once hreduce1_cases] >> fs []
+QED
+
+Theorem hreduce_abs :
+    !M N. M -h->* N ==> is_abs M ==> is_abs N
+Proof
+    HO_MATCH_MP_TAC RTC_STRONG_INDUCT_RIGHT1
+ >> rw []
+ >> irule hreduce1_abs
+ >> Q.EXISTS_TAC ‘N’ >> art []
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
+QED
+
+(* NOTE: Initially M1 is an APP, eventually it may become a VAR, never be LAM
+
+   The antecedent ‘!M. M1 -h->* M /\ M -h-> M2 ==> ~is_abs M’ says that
+   only head reductions between M1 and M2 (excluded) must not be abstractions,
+   i.e. starting from M2 it can be abstractions.
+ *)
+Theorem hreduce_rules_appstar :
+    !M1 M2 Ns. ~is_abs M1 /\ (!M. M1 -h->* M /\ M -h-> M2 ==> ~is_abs M) /\
+               M1 -h->* M2 ==> M1 @* Ns -h->* M2 @* Ns
+Proof
+    rpt STRIP_TAC
+ >> Q.PAT_X_ASSUM ‘~is_abs M1’ MP_TAC
+ >> Q.PAT_X_ASSUM ‘!M. P’ MP_TAC
+ >> POP_ASSUM MP_TAC
+ >> Q.ID_SPEC_TAC ‘M2’
+ >> Q.ID_SPEC_TAC ‘M1’
+ >> HO_MATCH_MP_TAC RTC_STRONG_INDUCT_RIGHT1 >> rw []
+ >> rw [Once RTC_CASES2] >> DISJ2_TAC
+ >> Q.EXISTS_TAC ‘M2 @* Ns’
+ >> reverse CONJ_TAC
+ >- (MATCH_MP_TAC hreduce1_rules_appstar >> art [] \\
+     FIRST_X_ASSUM MATCH_MP_TAC >> art [])
+ >> FIRST_X_ASSUM irule >> rw []
+ >> CCONTR_TAC >> fs []
+ >> ‘is_abs M2’ by PROVE_TAC [hreduce1_abs]
+ >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
+ >> PROVE_TAC []
+QED
+
+(* slight weaker but more useful *)
+Theorem hreduce_rules_appstar' :
+    !M1 M2 Ns. ~is_abs M1 /\ ~is_abs M2 /\ M1 -h->* M2 ==> M1 @* Ns -h->* M2 @* Ns
+Proof
+    rpt STRIP_TAC
+ >> MATCH_MP_TAC hreduce_rules_appstar >> art []
+ >> rpt STRIP_TAC
+ >> PROVE_TAC [hreduce1_abs]
+QED
+
 Theorem hreduce1_gen_bvc_ind :
   !P f. (!x. FINITE (f x)) /\
         (!v M N x. v NOTIN f x ==> P (LAM v M @@ N) ([N/v] M) x) /\
@@ -190,6 +269,211 @@ Proof
     rw [substitutive_def, hreduce_substitutive]
 QED
 
+(* This nice and hard-to-prove theorem gives a precise explicit form for any
+   lambda term whose single-step head reduction is in the form of ‘LAMl vs t’.
+
+   NOTE: This proof is hard in the sense that some primitive theorems from
+   nomsetTheory are used. And ‘~is_abs t’ is necessary for the case vs = [].
+ *)
+Theorem hreduce1_LAMl_cases :
+    !M vs t. ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\
+             M -h-> LAMl vs t /\ ~is_abs t ==>
+        ?vs1 vs2 N. (vs = vs1 ++ vs2) /\ (M = LAMl vs1 N) /\ ~is_abs N /\
+                    N -h-> LAMl vs2 t
+Proof
+    HO_MATCH_MP_TAC simple_induction >> rw []
+ >> Cases_on ‘vs = []’
+ >- (Q.PAT_X_ASSUM ‘LAM v M -h-> LAMl vs t’ MP_TAC \\
+     rw [Once hreduce1_cases] >> fs [])
+ >> Cases_on ‘vs’ >> FULL_SIMP_TAC list_ss []
+ >> rename1 ‘LAM v M -h-> LAM h (LAMl vs t)’
+ >> Q.PAT_X_ASSUM ‘T’ K_TAC
+ >> Q.PAT_X_ASSUM ‘LAM v M -h-> _’ MP_TAC
+ >> rw [Once hreduce1_cases]
+ >> Q.PAT_X_ASSUM ‘LAM v M = LAM v' M1’ MP_TAC
+ >> rw [LAM_eq_thm]
+  (* v = v' *)
+ >- (fs [LAM_eq_thm] >| (* 4 subgoals *)
+     [ (* goal 1 (of 4) *)
+       Q.PAT_X_ASSUM ‘h = v’ (fs o wrap) \\
+      ‘FV M DELETE v = FV M’ by ASM_SET_TAC [] >> fs [] \\
+       Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs’, ‘t’])) >> rw [] \\
+       fs [FOLDR_APPEND] \\
+       qexistsl_tac [‘v::vs1’, ‘vs2’, ‘N’] >> rw [],
+       (* goal 2 (of 4) *)
+       fs [tpm_eqr, tpm_LAMl] \\
+       qabbrev_tac ‘vs' = listpm string_pmact [(h,v)] vs’ \\
+       qabbrev_tac ‘t' = tpm [(h,v)] t’ \\
+      ‘ALL_DISTINCT vs'’ by rw [ALL_DISTINCT_listpm, Abbr ‘vs'’] \\
+       Know ‘DISJOINT (set vs') (FV M)’
+       >- (rw [DISJOINT_ALT, Abbr ‘vs'’, MEM_listpm] \\
+           Cases_on ‘x = h’ >- art [] \\
+           Cases_on ‘x = v’ >- fs [] \\
+           Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M DELETE v)’ MP_TAC \\
+           rw [DISJOINT_ALT] >> fs [] \\
+           METIS_TAC []) >> DISCH_TAC \\
+       Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs'’, ‘t'’])) \\
+       Know ‘~is_abs t'’ >- rw [Abbr ‘t'’, is_abs_cases] >> rw [] \\
+       Know ‘vs = listpm string_pmact [(v,h)] (vs1 ++ vs2)’
+       >- (Q.PAT_X_ASSUM ‘_ = vs1 ++ vs2’ MP_TAC \\
+           NTAC 2 (rw [Once LIST_EQ_REWRITE]) \\
+           Know ‘EL x (vs1 ++ vs2) = swapstr h v (EL x vs)’
+           >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
+               FIRST_X_ASSUM MATCH_MP_TAC >> art []) >> Rewr' \\
+           simp []) >> Rewr' \\
+       qexistsl_tac [‘h::listpm string_pmact [(v,h)] vs1’,
+                     ‘listpm string_pmact [(v,h)] vs2’, ‘tpm [(v,h)] N’] \\
+       simp [listpm_APPENDlist] \\
+       reverse CONJ_TAC
+       >- (Know ‘LAMl (listpm string_pmact [(v,h)] vs2) t = tpm [(v,h)] (LAMl vs2 t')’
+           >- (rw [Abbr ‘t'’, tpm_LAMl] \\
+               rw [Once tpm_eqr, pmact_flip_args]) >> Rewr' \\
+           rw [tpm_hreduce]) \\
+       Know ‘LAMl (listpm string_pmact [(v,h)] vs1) (tpm [(v,h)] N) =
+             tpm [(v,h)] (LAMl vs1 N)’ >- rw [tpm_LAMl] >> Rewr' \\
+       simp [LAM_eq_thm, pmact_flip_args],
+       (* goal 3 (of 4) *)
+       Q.PAT_X_ASSUM ‘h = v’ (fs o wrap) \\
+       Q.PAT_X_ASSUM ‘T’ K_TAC \\
+       Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs’, ‘t’])) \\
+       Know ‘DISJOINT (set vs) (FV M)’
+       >- (Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M DELETE v)’ MP_TAC \\
+           rw [DISJOINT_ALT'] >> METIS_TAC []) \\
+       RW_TAC std_ss [] \\
+       qexistsl_tac [‘v::vs1’, ‘vs2’, ‘N’] >> rw [],
+       (* goal 4 (of 4) *)
+       METIS_TAC [] ])
+ (* v <> v' *)
+ >> fs [tpm_eql, LAM_eq_thm] (* another 4 subgoals, even harder *)
+ >| [ (* goal 1 (of 4) *)
+      Q.PAT_X_ASSUM ‘h = v'’ (fs o wrap o SYM) \\
+      Q.PAT_X_ASSUM ‘T’ K_TAC \\
+      Q.PAT_X_ASSUM ‘LAMl vs t = M2’ (fs o wrap o SYM) \\
+     ‘tpm [(v,h)] M1 -h-> tpm [(v,h)] (LAMl vs t)’ by rw [tpm_hreduce] \\
+      FULL_SIMP_TAC std_ss [tpm_LAMl] \\
+      qabbrev_tac ‘vs' = listpm string_pmact [(v,h)] vs’ \\
+      qabbrev_tac ‘t' = tpm [(v,h)] t’ \\
+     ‘ALL_DISTINCT vs'’ by rw [ALL_DISTINCT_listpm, Abbr ‘vs'’] \\
+     ‘~is_abs t'’ by rw [Abbr ‘t'’, is_abs_cases] \\
+      Know ‘DISJOINT (set vs') (FV (tpm [(v,h)] M1))’
+      >- (rw [DISJOINT_ALT', FV_tpm, Abbr ‘vs'’, MEM_listpm] \\
+          Cases_on ‘x = v’ >- rw [] \\
+          Cases_on ‘x = h’ >- fs [] \\
+          fs [] (* eliminate swapstr *) \\
+          Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV (tpm [(v,h)] M1) DELETE v)’ MP_TAC \\
+          rw [DISJOINT_ALT', MEM_listpm]) >> DISCH_TAC \\
+      Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs'’, ‘t'’])) \\
+      RW_TAC std_ss [] \\
+      fs [tpm_LAMl] \\
+      Know ‘vs = listpm string_pmact [(v,h)] (vs1 ++ vs2)’
+      >- (Q.PAT_X_ASSUM ‘_ = vs1 ++ vs2’ MP_TAC \\
+          NTAC 2 (rw [Once LIST_EQ_REWRITE]) \\
+          Know ‘EL x (vs1 ++ vs2) = swapstr h v (EL x vs)’
+          >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
+              FIRST_X_ASSUM MATCH_MP_TAC >> art []) >> Rewr' \\
+          simp []) >> Rewr' \\
+      qexistsl_tac [‘h::listpm string_pmact [(v,h)] vs1’,
+                    ‘listpm string_pmact [(v,h)] vs2’, ‘tpm [(v,h)] N’] \\
+      simp [listpm_APPENDlist] \\
+      reverse CONJ_TAC
+      >- (Know ‘LAMl (listpm string_pmact [(v,h)] vs2) t = tpm [(v,h)] (LAMl vs2 t')’
+          >- (rw [Abbr ‘t'’, tpm_LAMl] \\
+              rw [Once tpm_eqr, pmact_flip_args]) >> Rewr' \\
+          rw [tpm_hreduce]) \\
+      Know ‘LAMl (listpm string_pmact [(v,h)] vs1) (tpm [(v,h)] N) =
+            tpm [(v,h)] (LAMl vs1 N)’ >- rw [tpm_LAMl] \\
+      DISCH_THEN (fs o wrap) \\
+      simp [LAM_eq_thm, pmact_flip_args],
+      (* goal 2 (of 4): this is the most difficult subgoal... *)
+      fs [tpm_eqr, tpm_LAMl] \\
+      qabbrev_tac ‘vs' = listpm string_pmact [(h,v')] vs’ \\
+      qabbrev_tac ‘t' = tpm [(h,v')] t’ \\
+      Q.PAT_X_ASSUM ‘LAMl vs' t' = M2’ (fs o wrap o SYM) \\
+     ‘tpm [(v,v')] M1 -h-> tpm [(v,v')] (LAMl vs' t')’ by rw [tpm_hreduce] \\
+      FULL_SIMP_TAC std_ss [tpm_LAMl] \\
+      qabbrev_tac ‘vs'' = listpm string_pmact [(v,v')] vs'’ \\
+      qabbrev_tac ‘t'' = tpm [(v,v')] t'’ \\
+     ‘ALL_DISTINCT vs'’ by rw [ALL_DISTINCT_listpm, Abbr ‘vs'’] \\
+     ‘ALL_DISTINCT vs''’ by rw [ALL_DISTINCT_listpm, Abbr ‘vs''’] \\
+     ‘~is_abs t'’ by rw [Abbr ‘t'’, is_abs_cases] \\
+     ‘~is_abs t''’ by rw [Abbr ‘t''’, is_abs_cases] \\
+      Know ‘DISJOINT (set vs'') (FV (tpm [(v,v')] M1))’
+      >- (rw [DISJOINT_ALT', FV_tpm, Abbr ‘vs''’, MEM_listpm] \\
+          simp [Abbr ‘vs'’, MEM_listpm] \\
+          Cases_on ‘x = v'’ >- fs [] \\
+          Cases_on ‘x = v’ >> fs [] \\
+          Cases_on ‘x = h’ >> fs [] \\
+          Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV (tpm [(v,v')] M1) DELETE v)’ MP_TAC \\
+          rw [DISJOINT_ALT', MEM_listpm]) >> DISCH_TAC \\
+      Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs''’, ‘t''’])) \\
+      RW_TAC std_ss [] \\
+      qabbrev_tac ‘vs'' = listpm string_pmact [(v,v')] vs'’ \\
+      Know ‘vs = listpm string_pmact [(h,v')] vs'’
+      >- (rw [Once LIST_EQ_REWRITE, Abbr ‘vs'’]) >> Rewr' \\
+      Know ‘vs' = listpm string_pmact [(v,v')] vs''’
+      >- (rw [Once LIST_EQ_REWRITE, Abbr ‘vs''’]) >> Rewr' \\
+      Q.PAT_X_ASSUM ‘vs'' = vs1 ++ vs2’ (ONCE_REWRITE_TAC o wrap) \\
+      qunabbrev_tac ‘vs''’ \\
+      qexistsl_tac [‘h::listpm string_pmact [(h,v')] (listpm string_pmact [(v,v')] vs1)’,
+                    ‘listpm string_pmact [(h,v')] (listpm string_pmact [(v,v')] vs2)’,
+                    ‘tpm [(h,v')] (tpm [(v,v')] N)’] \\
+      simp [listpm_APPENDlist] \\
+      reverse CONJ_TAC
+      >- (qabbrev_tac ‘vs2' = listpm string_pmact [(v,v')] vs2’ \\
+          Know ‘LAMl (listpm string_pmact [(h,v')] vs2') t = tpm [(h,v')] (LAMl vs2' t')’
+          >- (rw [Abbr ‘t'’, tpm_LAMl]) >> Rewr' \\
+          rw [tpm_hreduce, Abbr ‘vs2'’] \\
+          Know ‘LAMl (listpm string_pmact [(v,v')] vs2) t' = tpm [(v,v')] (LAMl vs2 t'')’
+          >- (rw [Abbr ‘t''’, tpm_LAMl]) >> Rewr' \\
+          rw [tpm_hreduce]) \\
+      qabbrev_tac ‘vs1' = listpm string_pmact [(v,v')] vs1’ \\
+      qabbrev_tac ‘N' = tpm [(v,v')] N’ \\
+      Know ‘LAMl (listpm string_pmact [(h,v')] vs1') (tpm [(h,v')] N') =
+            tpm [(h,v')] (LAMl vs1' N')’ >- rw [tpm_LAMl] >> Rewr' \\
+      qunabbrevl_tac [‘vs1'’, ‘N'’] \\
+      Know ‘LAMl (listpm string_pmact [(v,v')] vs1) (tpm [(v,v')] N) =
+            tpm [(v,v')] (LAMl vs1 N)’ >- rw [tpm_LAMl] >> Rewr' \\
+      Cases_on ‘h = v’ >> fs [] \\
+      simp [LAM_eq_thm, pmact_flip_args] \\
+      Q.PAT_X_ASSUM ‘tpm [(v,v')] M1 = LAMl vs1 N’ (REWRITE_TAC o wrap o SYM) \\
+      rw [FV_tpm] \\
+   (* applying fresh_tpm_subst *)
+      simp [fresh_tpm_subst] \\
+      qabbrev_tac ‘M = [VAR h/v'] M1’ \\
+      Know ‘tpm [(h,v)] M = [VAR v/h] M’
+      >- (rw [Once pmact_flip_args] \\
+          MATCH_MP_TAC fresh_tpm_subst \\
+          rw [FV_SUB, Abbr ‘M’]) >> Rewr' \\
+      qunabbrev_tac ‘M’ \\
+   (* applying lemma15a *)
+      ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
+      MATCH_MP_TAC lemma15a >> art [],
+      (* goal 3 (of 4): conflicts of assumptions *)
+      METIS_TAC [],
+      (* goal 4 (of 4): cannot be harder than others *)
+      Q.PAT_X_ASSUM ‘h = v’ (fs o wrap) \\
+      Q.PAT_X_ASSUM ‘T’ K_TAC \\
+      fs [tpm_eqr, tpm_LAMl] \\
+      qabbrev_tac ‘vs' = listpm string_pmact [(v,v')] vs’ \\
+      qabbrev_tac ‘t' = tpm [(v,v')] t’ \\
+      Q.PAT_X_ASSUM ‘LAMl vs' t' = M2’ (fs o wrap o SYM) \\
+     ‘tpm [(v,v')] M1 -h-> tpm [(v,v')] (LAMl vs' t')’ by rw [tpm_hreduce] \\
+      FULL_SIMP_TAC std_ss [tpm_LAMl] \\
+      Know ‘listpm string_pmact [(v,v')] vs' = vs’
+      >- (rw [Once LIST_EQ_REWRITE, Abbr ‘vs'’]) >> DISCH_THEN (fs o wrap) \\
+      Know ‘tpm [(v,v')] t' = t’
+      >- (rw [Abbr ‘t'’]) >> DISCH_THEN (fs o wrap) \\
+      Know ‘DISJOINT (set vs) (FV (tpm [(v,v')] M1))’
+      >- (Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV (tpm [(v,v')] M1) DELETE v)’ MP_TAC \\
+          rw [DISJOINT_ALT', FV_tpm] \\
+          Cases_on ‘x = v’ >- fs [] \\
+          Cases_on ‘x = v'’ >> fs []) >> DISCH_TAC \\
+      Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs’, ‘t’])) \\
+      RW_TAC std_ss [] \\
+      qexistsl_tac [‘v::vs1’, ‘vs2’, ‘N’] \\
+      simp [listpm_APPENDlist] ]
+QED
+
 (* ----------------------------------------------------------------------
     Head normal form (hnf)
    ---------------------------------------------------------------------- *)
@@ -1392,11 +1676,10 @@ Proof
     Induct_on ‘vs’ >> rw []
 QED
 
-Theorem hnf_children_size_hnf[simp] :
-    hnf_children_size (LAMl vs (VAR y @* Ms)) = LENGTH Ms
+Theorem hnf_children_size_appstar[simp] :
+    hnf_children_size (VAR y @* Ms) = LENGTH Ms
 Proof
-    rw []
- >> Induct_on ‘Ms’ using SNOC_INDUCT >- rw []
+    Induct_on ‘Ms’ using SNOC_INDUCT >- rw []
  >> rw [appstar_SNOC]
 QED
 
@@ -1438,6 +1721,96 @@ Proof
  >> METIS_TAC []
 QED
 
+(*---------------------------------------------------------------------------*
+ *  hreduce, LAMl and appstar
+ *---------------------------------------------------------------------------*)
+
+Theorem hreduce_LAMl_appstar_lemma[local] :
+    !pi. ALL_DISTINCT (MAP FST pi) /\
+         EVERY (\e. DISJOINT (FV e) (set (MAP FST pi))) (MAP SND pi) ==>
+         LAMl (MAP FST pi) t @* MAP SND pi -h->* (FEMPTY |++ pi) ' t
+Proof
+    Induct_on ‘pi’
+ >> rw [FUPDATE_LIST_THM] (* only one goal left *)
+ (* cleanup antecedents of IH *)
+ >> Q.PAT_X_ASSUM
+     ‘_ ==> LAMl (MAP FST pi) t @* MAP SND pi -h->* (FEMPTY |++ pi) ' t’ MP_TAC
+ >> Know ‘EVERY (\e. DISJOINT (FV e) (set (MAP FST pi))) (MAP SND pi)’
+ >- (POP_ASSUM MP_TAC \\
+     rw [EVERY_MEM, MEM_MAP])
+ >> RW_TAC std_ss []
+ (* stage work *)
+ >> qabbrev_tac ‘vs = MAP FST pi’
+ >> qabbrev_tac ‘Ns = MAP SND pi’
+ >> simp [Once RTC_CASES1]
+ >> DISJ2_TAC
+ (* preparing for hreduce1_rules_appstar *)
+ >> qabbrev_tac ‘v = FST h’
+ >> qabbrev_tac ‘N = SND h’
+ >> Q.EXISTS_TAC ‘[N/v] (LAMl vs t) @* Ns’
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC hreduce1_rules_appstar >> simp [] \\
+     rw [Once hreduce1_cases] \\
+     qexistsl_tac [‘v’, ‘LAMl vs t’] >> rw [])
+ >> Know ‘[N/v] (LAMl vs t) @* Ns =
+          [N/v] (LAMl vs t @* Ns)’
+ >- (simp [appstar_SUB] \\
+     Suff ‘MAP [N/v] Ns = Ns’ >- rw [] \\
+     rw [LIST_EQ_REWRITE, EL_MAP] \\
+     MATCH_MP_TAC lemma14b \\
+     rename1 ‘i < LENGTH Ns’ \\
+     Q.PAT_X_ASSUM ‘EVERY (\e. DISJOINT (FV e) (set vs) /\ v # e) Ns’ MP_TAC \\
+     rw [EVERY_MEM] \\
+     POP_ASSUM (MP_TAC o (Q.SPEC ‘EL i Ns’)) \\
+     Suff ‘MEM (EL i Ns) Ns’ >- rw [] \\
+     rw [MEM_EL] >> Q.EXISTS_TAC ‘i’ >> art [])
+ >> Rewr'
+ >> ‘h = (v,N)’ by rw [Abbr ‘v’, Abbr ‘N’] >> POP_ORW
+ >> simp [FUPDATE_LIST_THM]
+ (* applying FUPDATE_FUPDATE_LIST_COMMUTES *)
+ >> Know ‘FEMPTY |+ (v,N) |++ pi = (FEMPTY |++ pi) |+ (v,N)’
+ >- (MATCH_MP_TAC FUPDATE_FUPDATE_LIST_COMMUTES >> rw [])
+ >> Rewr'
+ >> qabbrev_tac ‘fm = FEMPTY |++ pi’
+ >> ‘FDOM fm = set vs’ by rw [Abbr ‘fm’, FDOM_FUPDATE_LIST]
+ (* applying ssub_update_apply_SUBST' *)
+ >> Know ‘(fm |+ (v,N)) ' t = [fm ' N/v] (fm ' t)’
+ >- (MATCH_MP_TAC ssub_update_apply_SUBST' \\
+     rw [Once DISJOINT_SYM, MEM_EL, Abbr ‘fm’] \\
+     Know ‘(FEMPTY |++ pi) ' (EL n vs) = EL n Ns’
+     >- (MATCH_MP_TAC FUPDATE_LIST_APPLY_MEM \\
+        ‘LENGTH pi = LENGTH vs’ by rw [Abbr ‘vs’] \\
+         Q.EXISTS_TAC ‘n’ >> rw [] \\
+         Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\
+         rw [EL_ALL_DISTINCT_EL_EQ]) >> Rewr' \\
+     Q.PAT_X_ASSUM ‘EVERY (\e. DISJOINT (FV e) (set vs) /\ v # e) Ns’ MP_TAC \\
+     rw [EVERY_MEM] \\
+     POP_ASSUM (MP_TAC o (Q.SPEC ‘EL n Ns’)) \\
+     Suff ‘MEM (EL n Ns) Ns’ >- rw [] \\
+     rw [MEM_EL] >> Q.EXISTS_TAC ‘n’ >> art [] \\
+     Suff ‘LENGTH Ns = LENGTH vs’ >- rw [] \\
+     rw [Abbr ‘Ns’, Abbr ‘vs’])
+ >> Rewr'
+ >> Know ‘fm ' N = N’
+ >- (MATCH_MP_TAC ssub_14b >> rw [GSYM DISJOINT_DEF])
+ >> Rewr'
+ >> MATCH_MP_TAC hreduce_substitutive >> art []
+QED
+
+Theorem hreduce_LAMl_appstar :
+    !t xs Ns. ALL_DISTINCT xs /\ (LENGTH xs = LENGTH Ns) /\
+              EVERY (\e. DISJOINT (FV e) (set xs)) Ns
+          ==> LAMl xs t @* Ns -h->* (FEMPTY |++ ZIP (xs,Ns)) ' t
+Proof
+    RW_TAC std_ss []
+ >> qabbrev_tac ‘n = LENGTH xs’
+ >> qabbrev_tac ‘pi = ZIP (xs,Ns)’
+ >> ‘xs = MAP FST pi’ by rw [Abbr ‘pi’, MAP_ZIP]
+ >> ‘Ns = MAP SND pi’ by rw [Abbr ‘pi’, MAP_ZIP]
+ >> simp []
+ >> MATCH_MP_TAC hreduce_LAMl_appstar_lemma >> rw []
+QED
+
 val _ = export_theory()
 val _ = html_theory "head_reduction";
 
diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
index 90fa8ebd07..aa24f8a181 100644
--- a/examples/lambda/barendregt/solvableScript.sml
+++ b/examples/lambda/barendregt/solvableScript.sml
@@ -41,7 +41,6 @@ Proof
 QED
 
 val _ = reveal "Y"; (* from chap2Theory *)
-
 Theorem solvable_Y :
     solvable Y
 Proof
@@ -49,6 +48,7 @@ Proof
  >> Q.EXISTS_TAC ‘[K @@ I]’ >> simp []
  >> ASM_SIMP_TAC (betafy (srw_ss())) [YYf, Once YffYf, lameq_K]
 QED
+val _ = hide "Y";
 
 Theorem closure_VAR[simp] :
     closure (VAR x) = I
@@ -642,6 +642,69 @@ Definition principle_hnf_def :
     principle_hnf = last o head_reduction_path
 End
 
+(* NOTE: This theorem fully captures the characteristics of principle hnf *)
+Theorem principle_hnf_thm :
+    !M N. has_hnf M ==> (principle_hnf M = N <=> M -h->* N /\ hnf N)
+Proof
+    rw [corollary11_4_8]
+ >> qabbrev_tac ‘p = head_reduction_path M’
+ >> MP_TAC (Q.SPECL [‘M’, ‘p’] finite_head_reduction_path_to_list_11)
+ >> RW_TAC std_ss [principle_hnf_def]
+ >> simp [finite_last_el]
+ >> Q.PAT_X_ASSUM ‘LENGTH l = THE (length p)’ (ONCE_REWRITE_TAC o wrap o SYM)
+ >> qabbrev_tac ‘n = PRE (LENGTH l)’
+ >> ‘LENGTH l <> 0’ by rw [GSYM NOT_NIL_EQ_LENGTH_NOT_0]
+ >> ‘n < LENGTH l’ by rw [Abbr ‘n’]
+ >> Q.PAT_X_ASSUM ‘!i. i < LENGTH l ==> EL i l = el i p’ (fn th => rw [GSYM th])
+ (* now the path p is not needed *)
+ >> Q.PAT_X_ASSUM ‘finite p’ K_TAC
+ >> qunabbrev_tac ‘p’
+ (* easier direction first *)
+ >> EQ_TAC
+ >- (DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) \\
+     reverse CONJ_TAC
+     >- (Suff ‘EL n l = LAST l’ >- rw [] \\
+         rw [LAST_EL, Abbr ‘n’]) \\
+     POP_ASSUM MP_TAC \\
+     Q.SPEC_TAC (‘n’, ‘i’) \\
+     Induct_on ‘i’ >> rw [] \\
+     MATCH_MP_TAC hreduce_TRANS \\
+     Q.EXISTS_TAC ‘EL i l’ >> rw [])
+ (* stage work *)
+ >> rpt STRIP_TAC
+ >> qabbrev_tac ‘M = HD l’
+ (* now both ‘LAST l’ and ‘N’ is hnf, they must be the same, because a hnf has
+    no further head reductions, and we know N is in the head reduction path.
+
+    But first, we need to prove |- ?i. i < LENGTH l /\ N = EL i l, because
+    head reduction is deterministic, thus all reductions from ‘HD l’ must lie
+    in the list l.
+ *)
+ >> Know ‘!N0. M -h->* N0 ==> ?i. i < LENGTH l /\ N0 = EL i l’
+ >- (HO_MATCH_MP_TAC RTC_ALT_RIGHT_INDUCT >> rw []
+     >- (Q.EXISTS_TAC ‘0’ >> rw [Abbr ‘M’]) \\
+    ‘SUC i < LENGTH l \/ i = n’ by rw [Abbr ‘n’]
+     >- (‘EL i l -h-> EL (SUC i) l’ by PROVE_TAC [] \\
+         Q.EXISTS_TAC ‘SUC i’ >> art [] \\
+         PROVE_TAC [hreduce1_unique]) \\
+    ‘EL i l = LAST l’ by rw [LAST_EL, Abbr ‘n’] \\
+     METIS_TAC [hnf_def])
+ >> DISCH_THEN (MP_TAC o (Q.SPEC ‘N’))
+ >> RW_TAC std_ss []
+ >> ‘i = n \/ i < n \/ n < i’ by rw []
+ >| [ (* goal 1 (of 3) *)
+      rw [],
+      (* goal 2 (of 3) *)
+     ‘SUC i < LENGTH l’ by rw [Abbr ‘n’] \\
+     ‘EL i l -h-> EL (SUC i) l’ by PROVE_TAC [] \\
+      METIS_TAC [hnf_def],
+      (* goal 3 (of 3) *)
+      fs [Abbr ‘n’] ]
+QED
+
+Theorem principle_hnf_thm' =
+        principle_hnf_thm |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
+
 (* principle hnf has less (or equal) free variables
 
    NOTE: this theorem depends on finite_head_reduction_path_to_list_11 and
@@ -650,31 +713,20 @@ End
 Theorem principle_hnf_FV_SUBSET :
     !M. has_hnf M ==> FV (principle_hnf M) SUBSET FV M
 Proof
-    rw [corollary11_4_8]
- >> qabbrev_tac ‘p = head_reduction_path M’
- >> MP_TAC (Q.SPECL [‘M’, ‘p’] finite_head_reduction_path_to_list_11)
- >> rw [principle_hnf_def, combinTheory.o_DEF]
- >> simp [finite_last_el]
- >> Q.PAT_X_ASSUM ‘LENGTH l = _’ (ONCE_REWRITE_TAC o wrap o SYM)
- >> qabbrev_tac ‘n = PRE (LENGTH l)’
- >> ‘LENGTH l <> 0’ by rw [GSYM NOT_NIL_EQ_LENGTH_NOT_0]
- >> Know ‘el n p = EL n l’
- >- (ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
-     FIRST_X_ASSUM MATCH_MP_TAC >> rw [Abbr ‘n’])
- >> Rewr'
- >> REWRITE_TAC [GSYM EL]
- (* preparing for induction *)
- >> Suff ‘!j. j < LENGTH l ==> FV (EL j l) SUBSET FV (EL 0 l)’
- >- (DISCH_THEN MATCH_MP_TAC >> rw [Abbr ‘n’])
- >> Q.PAT_X_ASSUM ‘!i. i < LENGTH l ==> EL i l = el i p’ K_TAC
- >> Induct_on ‘j’
- >> RW_TAC std_ss [SUBSET_REFL] (* only one goal is left *)
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘N = principle_hnf M’
+ (* applying principle_hnf_thm *)
+ >> Know ‘principle_hnf M = N’ >- rw [Abbr ‘N’]
+ >> rw [principle_hnf_thm]
+ >> Q.PAT_X_ASSUM ‘M -h->* N’ MP_TAC
+ >> Q.ID_SPEC_TAC ‘N’
+ >> HO_MATCH_MP_TAC RTC_ALT_RIGHT_INDUCT >> rw []
+ >> rename1 ‘N0 -h-> N1’
  >> MATCH_MP_TAC SUBSET_TRANS
- >> Q.EXISTS_TAC ‘FV (EL j l)’
- >> reverse CONJ_TAC
- >- (FIRST_X_ASSUM MATCH_MP_TAC >> rw [])
- >> MATCH_MP_TAC hreduce1_FV_SUBSET
- >> FIRST_X_ASSUM MATCH_MP_TAC >> art []
+ >> Q.EXISTS_TAC ‘FV N0’ >> art []
+ >> rw [SUBSET_DEF]
+ >> irule hreduce1_FV
+ >> Q.EXISTS_TAC ‘N1’ >> art []
 QED
 
 (* |- !M. solvable M ==> FV (principle_hnf M) SUBSET FV M *)
@@ -691,7 +743,18 @@ QED
 
 (* |- !M. solvable M ==> hnf (principle_hnf M) *)
 Theorem hnf_principle_hnf' =
-   REWRITE_RULE [GSYM solvable_iff_has_hnf] hnf_principle_hnf
+    REWRITE_RULE [GSYM solvable_iff_has_hnf] hnf_principle_hnf
+
+Theorem solvable_principle_hnf :
+    !M. solvable M ==> solvable (principle_hnf M)
+Proof
+    rw [solvable_iff_has_hnf]
+ >> MATCH_MP_TAC hnf_has_hnf
+ >> MATCH_MP_TAC hnf_principle_hnf >> art []
+QED
+
+Theorem principle_hnf_has_hnf =
+    REWRITE_RULE [solvable_iff_has_hnf] solvable_principle_hnf
 
 Theorem principle_hnf_reduce[simp] :
     !M. hnf M ==> principle_hnf M = M
@@ -750,6 +813,16 @@ Proof
  >> rw [Abbr ‘q’, Abbr ‘p’, Once is_head_reduction_thm]
 QED
 
+(* NOTE: this useful theorem can be used to rewrite ‘principle_hnf M’ to
+  ‘principle_hnf N’, if one can prove ‘M -h->* N’. *)
+Theorem principle_hnf_hreduce :
+    !M N. M -h->* N ==> principle_hnf M = principle_hnf N
+Proof
+    HO_MATCH_MP_TAC RTC_INDUCT >> rw []
+ >> POP_ASSUM (ONCE_REWRITE_TAC o wrap o SYM)
+ >> MATCH_MP_TAC principle_hnf_hreduce1 >> art []
+QED
+
 Theorem principle_hnf_LAMl_appstar_lemma[local] :
     !t. hnf t /\
         ALL_DISTINCT (MAP FST pi) /\
@@ -758,9 +831,9 @@ Theorem principle_hnf_LAMl_appstar_lemma[local] :
        (!y. MEM y (MAP SND pi) ==> y # t) ==>
         principle_hnf (LAMl (MAP FST pi) t @* MAP VAR (MAP SND pi)) = tpm pi t
 Proof
-    Induct_on ‘pi’ (* using SNOC_INDUCT *)
+    Induct_on ‘pi’
  >- rw [principle_hnf_reduce]
- >> rw [] (* rw [FOLDR_SNOC, MAP_SNOC] *)
+ >> rw []
  >> Cases_on ‘h’ (* ‘x’ *) >> fs []
  >> qabbrev_tac ‘M = LAMl (MAP FST pi) t’
  >> ‘hnf M’ by rw [Abbr ‘M’, hnf_LAMl]
@@ -832,12 +905,12 @@ Proof
  >> FIRST_X_ASSUM MATCH_MP_TAC >> rw []
 QED
 
-(* ‘principle_hnf’ can be used to do final beta-reductions to make a hnf abs-free
+(* ‘principle_hnf’ can be used to do final beta-reductions for an abs-free hnf
 
    NOTE: to satisfy ‘DISJOINT (set xs) (set ys)’, one first get ‘LENGTH xs’
          without knowing ‘xs’ (e.g. by ‘LAMl_size’), then generate ‘ys’ by
-        ‘FRESH_list’, and then call ‘hnf_cases_genX’ using ‘ys’ as the excluded
-         list.
+        ‘FRESH_list’, and then call [hnf_cases_genX] using ‘ys’ as the new
+         excluded list.
  *)
 Theorem principle_hnf_LAMl_appstar :
     !t xs ys. hnf t /\
@@ -845,7 +918,7 @@ Theorem principle_hnf_LAMl_appstar :
               LENGTH xs = LENGTH ys /\
               DISJOINT (set xs) (set ys) /\
               DISJOINT (set ys) (FV t)
-          ==> principle_hnf (LAMl xs t @* (MAP VAR ys)) = tpm (ZIP (xs,ys)) t
+          ==> principle_hnf (LAMl xs t @* MAP VAR ys) = tpm (ZIP (xs,ys)) t
 Proof
     RW_TAC std_ss []
  >> qabbrev_tac ‘n = LENGTH xs’
@@ -876,7 +949,7 @@ Proof
 QED
 
 Theorem principle_hnf_beta_reduce :
-    !xs t. hnf t ==> principle_hnf (LAMl xs t @* (MAP VAR xs)) = t
+    !xs t. hnf t ==> principle_hnf (LAMl xs t @* MAP VAR xs) = t
 Proof
     Induct_on ‘xs’
  >> rw [principle_hnf_reduce]
@@ -890,6 +963,19 @@ Proof
  >> simp [Abbr ‘M’]
 QED
 
+Theorem hreduce_BETA :
+    !vs t. LAMl vs t @* MAP VAR vs -h->* t
+Proof
+    Induct_on ‘vs’
+ >> rw [Once RTC_CASES1] (* only 1 goal is left *)
+ >> DISJ2_TAC
+ >> qabbrev_tac ‘M = LAMl vs t’
+ >> Q.EXISTS_TAC ‘[VAR h/h] M @* MAP VAR vs’
+ >> reverse CONJ_TAC >- rw [Abbr ‘M’]
+ >> MATCH_MP_TAC hreduce1_rules_appstar
+ >> rw [hreduce1_BETA]
+QED
+
 (* Example 8.3.2 [1, p.171] *)
 Theorem unsolvable_Omega :
     unsolvable Omega
@@ -946,6 +1032,7 @@ Proof
  >> rw [lameq_SYM]
 QED
 
+(* NOTE: this proof has used first principles of solvable terms *)
 Theorem lameq_solvable_cong :
     !M N. M == N ==> (solvable M <=> solvable N)
 Proof
@@ -958,13 +1045,14 @@ Proof
     ‘FINITE (FV M UNION FV N)’ by rw [] \\
      simp [SET_TO_LIST_INV] >> SET_TAC [])
  >> STRIP_TAC
+ (* applying solvable_iff_LAMl *)
  >> ‘solvable M <=> solvable M0’ by (rw [Abbr ‘M0’]) >> POP_ORW
  >> ‘solvable N <=> solvable N0’ by (rw [Abbr ‘N0’]) >> POP_ORW
  >> ‘M0 == N0’ by (rw [Abbr ‘M0’, Abbr ‘N0’, lameq_LAMl_cong])
  >> MATCH_MP_TAC lameq_solvable_cong_lemma >> art []
 QED
 
-Theorem lameq_principle_hnf_reduce :
+Theorem lameq_principle_hnf :
     !M. has_hnf M ==> principle_hnf M == M
 Proof
     rpt STRIP_TAC
@@ -980,8 +1068,8 @@ Proof
 QED
 
 (* |- !M. solvable M ==> principle_hnf M == M *)
-Theorem lameq_principle_hnf_reduce' =
-        lameq_principle_hnf_reduce |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
+Theorem lameq_principle_hnf' =
+        lameq_principle_hnf |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
 
 Theorem hnf_ccbeta_appstar_rwt[local] :
     !y Ms N. VAR y @* Ms -b-> N /\ Ms <> [] ==>
@@ -1139,11 +1227,11 @@ Proof
  >> Know ‘M0 == N0’
  >- (MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘M’ \\
      CONJ_TAC >- (qunabbrev_tac ‘M0’ \\
-                  MATCH_MP_TAC lameq_principle_hnf_reduce >> art []) \\
+                  MATCH_MP_TAC lameq_principle_hnf >> art []) \\
      MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\
      MATCH_MP_TAC lameq_SYM \\
      qunabbrev_tac ‘N0’ \\
-     MATCH_MP_TAC lameq_principle_hnf_reduce >> art [])
+     MATCH_MP_TAC lameq_principle_hnf >> art [])
  >> DISCH_TAC
  >> ‘hnf M0 /\ hnf N0’ by METIS_TAC [hnf_principle_hnf]
  >> qabbrev_tac ‘X = FV M0 UNION FV N0’
@@ -1158,7 +1246,7 @@ QED
 Theorem lameq_principle_hnf_size_eq' =
         lameq_principle_hnf_size_eq |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
 
-Theorem lameq_principle_hnf_headvar_eq :
+Theorem lameq_principle_hnf_head_eq :
     !X M N M0 N0 n vs M1 N1.
          FINITE X /\ FV M UNION FV N SUBSET X /\
          has_hnf M /\ has_hnf N /\ M == N /\
@@ -1178,11 +1266,11 @@ Proof
  >> Know ‘M0 == N0’
  >- (MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘M’ \\
      CONJ_TAC >- (qunabbrev_tac ‘M0’ \\
-                  MATCH_MP_TAC lameq_principle_hnf_reduce >> art []) \\
+                  MATCH_MP_TAC lameq_principle_hnf >> art []) \\
      MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\
      MATCH_MP_TAC lameq_SYM \\
      qunabbrev_tac ‘N0’ \\
-     MATCH_MP_TAC lameq_principle_hnf_reduce >> art [])
+     MATCH_MP_TAC lameq_principle_hnf >> art [])
  >> DISCH_TAC
  >> ‘hnf M0 /\ hnf N0’ by METIS_TAC [hnf_principle_hnf]
  (* applying lameq_principle_hnf_lemma *)
@@ -1192,8 +1280,8 @@ Proof
  >> METIS_TAC [principle_hnf_FV_SUBSET, SUBSET_TRANS]
 QED
 
-Theorem lameq_principle_hnf_headvar_eq' =
-        lameq_principle_hnf_headvar_eq |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
+Theorem lameq_principle_hnf_head_eq' =
+        lameq_principle_hnf_head_eq |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
 
 (* Corollary 8.3.17 (ii) [1, p.176] (outer part) *)
 Theorem lameq_principle_hnf_thm :
@@ -1221,11 +1309,11 @@ Proof
  >> Know ‘M0 == N0’
  >- (MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘M’ \\
      CONJ_TAC >- (qunabbrev_tac ‘M0’ \\
-                  MATCH_MP_TAC lameq_principle_hnf_reduce >> art []) \\
+                  MATCH_MP_TAC lameq_principle_hnf >> art []) \\
      MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\
      MATCH_MP_TAC lameq_SYM \\
      qunabbrev_tac ‘N0’ \\
-     MATCH_MP_TAC lameq_principle_hnf_reduce >> art [])
+     MATCH_MP_TAC lameq_principle_hnf >> art [])
  >> DISCH_TAC
  >> ‘hnf M0 /\ hnf N0’ by METIS_TAC [hnf_principle_hnf]
  (* applying lameq_principle_hnf_lemma *)
@@ -1238,6 +1326,335 @@ QED
 Theorem lameq_principle_hnf_thm' =
         lameq_principle_hnf_thm |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
 
+(* NOTE: the difficulty of applying this theorem is to prove the antecedents *)
+Theorem principle_hnf_substitutive :
+    !M N v P. has_hnf M /\ has_hnf ([P/v] M) /\ has_hnf ([P/v] N) /\
+              principle_hnf M = N ==>
+              principle_hnf ([P/v] M) = principle_hnf ([P/v] N)
+Proof
+    rpt STRIP_TAC
+ >> POP_ASSUM MP_TAC
+ >> reverse (rw [principle_hnf_thm])
+ >- (MATCH_MP_TAC hnf_principle_hnf >> art [])
+ >> MATCH_MP_TAC hreduce_TRANS
+ >> Q.EXISTS_TAC ‘[P/v] N’
+ >> CONJ_TAC
+ >- (MATCH_MP_TAC hreduce_substitutive >> art [])
+ >> qabbrev_tac ‘M' = [P/v] M’
+ >> qabbrev_tac ‘N' = [P/v] N’
+ >> qabbrev_tac ‘Q = principle_hnf N'’
+ >> Know ‘principle_hnf N' = Q’ >- rw [Abbr ‘Q’]
+ >> rw [principle_hnf_thm]
+QED
+
+Theorem principle_hnf_substitutive_hnf :
+    !M N v P. has_hnf M /\ has_hnf ([P/v] M) /\ hnf ([P/v] N) /\
+              principle_hnf M = N ==>
+              principle_hnf ([P/v] M) = [P/v] N
+Proof
+    rpt STRIP_TAC
+ >> Know ‘principle_hnf ([P/v] M) = principle_hnf ([P/v] N)’
+ >- (MATCH_MP_TAC principle_hnf_substitutive >> art [] \\
+     MATCH_MP_TAC hnf_has_hnf >> art [])
+ >> Rewr'
+ >> MATCH_MP_TAC principle_hnf_reduce >> art []
+QED
+
+(* This is an important theroem, hard to prove.
+
+   To use this theorem, first one defines ‘M0 = principle_hnf M’ as abbreviation,
+   then define ‘n = LAMl_size M0’ and ‘vs = FRESH_list n (FV M)’ (or ‘FV M0’, or
+  ‘X UNION FV M0’, ‘X UNION FV M’), and this give us the needed antecedents:
+
+       ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\ LENGTH vs = n
+
+   Then use hnf_cases_shared to derive ‘M0 = LAMl vs (VAR y @* args)’ and then
+  ‘M1 = principle_hnf (M0 @* MAP VAR vs) = VAR y @* args’.
+
+   The conclusion is that ‘principle_hnf (M @* MAP VAR vs) = M1’.
+
+   Now ‘principle_hnf’ can be used to "denude" the outer LAMl of a solvable term.
+
+   An extra list of free variables ‘l’ may need to append after MAP VAR vs.
+ *)
+Theorem principle_hnf_denude_lemma[local] :
+    !M vs l y Ns. solvable M /\
+                  ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\
+                  M -h->* LAMl vs (VAR y @* Ns) ==>
+                  M @* MAP VAR vs @* MAP VAR l -h->* VAR y @* Ns @* MAP VAR l
+Proof
+    rpt STRIP_TAC
+ (* eliminating MAP VAR l *)
+ >> MATCH_MP_TAC hreduce_rules_appstar'
+ >> rw [is_abs_appstar]
+ >- (fs [] >> CCONTR_TAC >> fs [] \\
+    ‘is_abs (VAR y @* Ns)’ by PROVE_TAC [hreduce_abs] >> fs [])
+ (* now l is eliminated *)
+ >> NTAC 4 (POP_ASSUM MP_TAC)
+ >> Suff ‘!M M0. M -h->* M0 ==>
+                 solvable M ==>
+                   !vs t. ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\
+                          M0 = LAMl vs t /\ ~is_abs t ==>
+                          M @* MAP VAR vs -h->* t’
+ >- (rpt STRIP_TAC >> FIRST_X_ASSUM irule >> rw [])
+ >> HO_MATCH_MP_TAC RTC_STRONG_INDUCT_RIGHT1
+ >> rw [hreduce_BETA] (* only one goal is left *)
+ >> Q.PAT_X_ASSUM ‘solvable M ==> P’ MP_TAC
+ >> RW_TAC std_ss []
+ (* NOTE: this assumption is only possible with RTC_STRONG_INDUCT, etc. *)
+ >> Know ‘DISJOINT (set vs) (FV M0)’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+     Q.EXISTS_TAC ‘FV M’ >> art [] \\
+     MATCH_MP_TAC hreduce_FV_SUBSET >> art [])
+ >> DISCH_TAC
+ (* stage work.
+
+    Now we need to discuss the possible shapes of M0:
+
+    1. M0 := LAMl vs (P @@ Q), where P @@ Q -h-> t
+    2. M0 := LAMl vs1 (P @@ Q), where P @@ Q -h-> LAMl vs2 t, vs = vs1 ++ vs2
+
+    The first case is included in the second case.
+
+    Using IH, we have: M @* MAP VAR vs1 -h->* P @@ Q -h-> LAMl vs2 t (hnf)
+    Thus (using RTC transitivity): M @* MAP VAR vs1 -h->* LAMl vs2 t (hnf)
+
+    Since M @* MAP VAR vs = M @* MAP VAR vs1 @* MAP VAR vs2, the head reduction
+    process should proceed with the part ‘M @* MAP VAR vs1’ until arrive at
+   ‘P @@ Q’ (APP) without showing any LAM (otherwise it cannot be P @@ Q), and
+    then do it again to ‘LAMl vs2 t’, i.e.
+
+    M @* MAP VAR vs1 @* MAP VAR vs2 -h->* P @@ Q @* MAP VAR vs2
+                                    -h-> LAMl vs2 t @* MAP VAR vs2
+                                    -h->* t (QED)
+
+    The possible fact ‘hnf t’ is not used in the above reduction process.
+ *)
+ (* applying hreduce1_LAMl_cases *)
+ >> Know ‘ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M0) /\ M0 -h-> LAMl vs t /\ ~is_abs t’
+ >- art []
+ >> DISCH_THEN (STRIP_ASSUME_TAC o (MATCH_MP hreduce1_LAMl_cases))
+ (* stage work *)
+ >> Q.PAT_X_ASSUM ‘!vs t. P’ (MP_TAC o (Q.SPECL [‘vs1’, ‘N’]))
+ >> Know ‘ALL_DISTINCT vs1’
+ >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT vs’ MP_TAC \\
+     rw [ALL_DISTINCT_APPEND])
+ >> Know ‘DISJOINT (set vs1) (FV M)’
+ >- (Q.PAT_X_ASSUM ‘DISJOINT (set vs) (FV M)’ MP_TAC \\
+     rw [LIST_TO_SET_APPEND])
+ >> RW_TAC std_ss []
+ >> simp [appstar_APPEND]
+ >> MATCH_MP_TAC hreduce_TRANS
+ >> Q.EXISTS_TAC ‘LAMl vs2 t @* MAP VAR vs2’
+ >> reverse CONJ_TAC >- rw [hreduce_BETA]
+ >> rw [Once RTC_CASES2] >> DISJ2_TAC
+ >> Q.EXISTS_TAC ‘N @* MAP VAR vs2’
+ >> reverse CONJ_TAC
+ >- (MATCH_MP_TAC hreduce1_rules_appstar >> art [] \\
+     fs [is_comb_APP_EXISTS])
+ >> MATCH_MP_TAC hreduce_rules_appstar' >> art []
+ >> rw [is_abs_appstar]
+ >> CCONTR_TAC >> fs []
+ >> ‘is_abs N’ by PROVE_TAC [hreduce_abs]
+QED
+
+Theorem principle_hnf_denude_solvable :
+    !M vs l y args. solvable M /\
+       ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\
+       principle_hnf M = LAMl vs (VAR y @* args) ==>
+       solvable (M @* MAP VAR vs @* MAP VAR l)
+Proof
+    rpt GEN_TAC >> STRIP_TAC
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ (* applying principle_hnf_thm' *)
+ >> Know ‘principle_hnf M = M0’ >- rw [Abbr ‘M0’]
+ >> simp [principle_hnf_thm', hnf_appstar]
+ >> DISCH_TAC
+ >> ‘M0 == M’ by rw [lameq_principle_hnf', Abbr ‘M0’]
+ >> ‘M0 @* MAP VAR vs == VAR y @* args’ by rw []
+ >> ‘M0 @* MAP VAR vs == M @* MAP VAR vs’ by rw [lameq_appstar_cong]
+ >> Know ‘M @* MAP VAR vs @* MAP VAR l == VAR y @* args @* MAP VAR l’
+ >- (MATCH_MP_TAC lameq_appstar_cong \\
+     PROVE_TAC [lameq_SYM, lameq_TRANS])
+ >> DISCH_TAC
+ >> Suff ‘solvable (VAR y @* args @* MAP VAR l)’
+ >- PROVE_TAC [lameq_solvable_cong]
+ >> REWRITE_TAC [solvable_iff_has_hnf]
+ >> MATCH_MP_TAC hnf_has_hnf >> rw [hnf_appstar]
+QED
+
+Theorem principle_hnf_denude_thm :
+    !l M vs y args. solvable M /\
+       ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\
+       principle_hnf M = LAMl vs (VAR y @* args) ==>
+       principle_hnf (M @* MAP VAR vs @* MAP VAR l) = VAR y @* args @* MAP VAR l
+Proof
+    rpt GEN_TAC >> STRIP_TAC
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ (* applying principle_hnf_thm' *)
+ >> Know ‘principle_hnf M = M0’ >- rw [Abbr ‘M0’]
+ >> simp [principle_hnf_thm', hnf_appstar]
+ >> DISCH_TAC
+ >> Know ‘solvable (M @* MAP VAR vs @* MAP VAR l)’
+ >- (MATCH_MP_TAC principle_hnf_denude_solvable \\
+     qexistsl_tac [‘y’, ‘args’] \\
+     Q.PAT_X_ASSUM ‘M0 = _’ (ONCE_REWRITE_TAC o wrap o SYM) \\
+     rw [Abbr ‘M0’])
+ >> DISCH_TAC
+ (* applying again principle_hnf_thm' *)
+ >> simp [principle_hnf_thm', hnf_appstar]
+ (* now all ‘principle_hnf’ are eliminated, leaving only -h->* *)
+ >> MATCH_MP_TAC principle_hnf_denude_lemma >> art []
+QED
+
+(* |- !M vs y args.
+        solvable M /\ ALL_DISTINCT vs /\ DISJOINT (set vs) (FV M) /\
+        principle_hnf M = LAMl vs (VAR y @* args) ==>
+        principle_hnf (M @* MAP VAR vs) = VAR y @* args
+ *)
+Theorem principle_hnf_denude_thm' =
+        principle_hnf_denude_thm |> Q.SPEC ‘[]’ |> SIMP_RULE (srw_ss()) []
+
+Theorem principle_hnf_permutator_lemma[local] :
+    !vs Ns. ALL_DISTINCT vs /\ ~MEM y vs /\ LENGTH vs = LENGTH Ns /\
+            EVERY (\e. DISJOINT (FV e) (set (SNOC y vs))) (SNOC N Ns) ==>
+            LAMl vs (LAM y (VAR y @* MAP VAR vs)) @* Ns @@ N -h->* N @* Ns
+Proof
+    rpt STRIP_TAC
+ >> REWRITE_TAC [GSYM LAMl_SNOC, GSYM appstar_SNOC]
+ >> qabbrev_tac ‘vs' = SNOC y vs’
+ >> qabbrev_tac ‘Ns' = SNOC N Ns’
+ >> qabbrev_tac ‘t = VAR y @* MAP VAR vs’
+ >> Suff ‘N @* Ns = fromPairs vs' Ns' ' t’
+ >- (Rewr' >> REWRITE_TAC [fromPairs_def] \\
+     MATCH_MP_TAC hreduce_LAMl_appstar \\
+     rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC] \\
+     Q.PAT_X_ASSUM ‘EVERY _ (SNOC N Ns)’ MP_TAC \\
+     rw [EVERY_MEM, LIST_TO_SET_SNOC] \\ (* 2 subgoals, same tactics *)
+     METIS_TAC [])
+ >> ‘LENGTH vs' = LENGTH Ns'’ by rw [Abbr ‘vs'’, Abbr ‘Ns'’]
+ >> ‘y IN FDOM (fromPairs vs' Ns')’ by rw [FDOM_fromPairs, Abbr ‘vs'’]
+ >> simp [Abbr ‘t’, ssub_appstar]
+ >> Know ‘fromPairs vs' Ns' ' y = N’
+ >- (‘y = LAST vs'’ by rw [Abbr ‘vs'’, LAST_SNOC] >> POP_ORW \\
+     ‘vs' <> []’ by rw [Abbr ‘vs'’] \\
+     rw [LAST_EL] \\
+     qabbrev_tac ‘n = PRE (LENGTH Ns')’ \\
+     Know ‘fromPairs vs' Ns' ' (EL n vs') = EL n Ns'’
+     >- (MATCH_MP_TAC fromPairs_FAPPLY_EL \\
+         rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC, Abbr ‘n’]) >> Rewr' \\
+    ‘Ns' <> []’ by rw [Abbr ‘Ns'’] \\
+    ‘EL n Ns' = LAST Ns'’ by rw [LAST_EL, Abbr ‘n’] >> POP_ORW \\
+     rw [Abbr ‘Ns'’, LAST_SNOC])
+ >> Rewr'
+ >> Suff ‘MAP ($' (fromPairs vs' Ns')) (MAP VAR vs) = Ns’ >- rw []
+ >> rw [LIST_EQ_REWRITE]
+ >> rename1 ‘i < LENGTH Ns’
+ >> Know ‘EL i vs IN FDOM (fromPairs vs' Ns')’
+ >- (rw [FDOM_fromPairs] \\
+     rw [Abbr ‘vs'’, MEM_EL] \\
+     DISJ2_TAC >> Q.EXISTS_TAC ‘i’ >> art [])
+ >> rw [EL_MAP]
+ >> Know ‘EL i vs = EL i vs' /\ EL i Ns = EL i Ns'’
+ >- ASM_SIMP_TAC std_ss [EL_SNOC, Abbr ‘vs'’, Abbr ‘Ns'’]
+ >> rw []
+ >> MATCH_MP_TAC fromPairs_FAPPLY_EL
+ >> rw [Abbr ‘vs'’, Abbr ‘Ns'’, ALL_DISTINCT_SNOC]
+QED
+
+Theorem principle_hnf_permutator :
+    !n N Ns. hnf N /\ ~is_abs N /\ LENGTH Ns = n ==>
+             principle_hnf (permutator n @* Ns @@ N) = N @* Ns
+Proof
+    rpt STRIP_TAC
+ >> Know ‘solvable (permutator n @* Ns @@ N)’
+ >- (‘permutator n @* Ns @@ N == N @* Ns’
+       by PROVE_TAC [permutator_thm] \\
+     Suff ‘solvable (N @* Ns)’ >- PROVE_TAC [lameq_solvable_cong] \\
+     REWRITE_TAC [solvable_iff_has_hnf] \\
+     MATCH_MP_TAC hnf_has_hnf \\
+     rw [hnf_appstar])
+ >> DISCH_TAC
+ >> rw [principle_hnf_thm', hnf_appstar]
+ >> RW_TAC std_ss [permutator_def]
+ >> qabbrev_tac ‘n = LENGTH Ns’
+ >> ‘ALL_DISTINCT Z /\ LENGTH Z = n + 1’
+       by (rw [Abbr ‘Z’, ALL_DISTINCT_GENLIST])
+ >> ‘Z <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> ‘MEM z Z’ by rw [Abbr ‘z’, MEM_LAST_NOT_NIL]
+ >> qabbrev_tac ‘M = VAR z @* MAP VAR (FRONT Z)’
+ (* preparing for LAMl_ALPHA_ssub *)
+ >> qabbrev_tac ‘Y = FRESH_list (n + 1)
+                       (set Z UNION (FV N) UNION (BIGUNION (IMAGE FV (set Ns))))’
+ >> ‘FINITE (set Z UNION (FV N) UNION (BIGUNION (IMAGE FV (set Ns))))’
+       by (rw [] >> rw [FINITE_FV])
+ >> Know ‘ALL_DISTINCT Y /\
+          DISJOINT (set Y) (set Z UNION (FV N) UNION (BIGUNION (IMAGE FV (set Ns)))) /\
+          LENGTH Y = n + 1’
+ >- (ASM_SIMP_TAC std_ss [FRESH_list_def, Abbr ‘Y’])
+ >> rw [] (* this breaks all unions in the DISJOINT *)
+ (* applying LAMl_ALPHA_ssub *)
+ >> Know ‘LAMl Z M = LAMl Y ((FEMPTY |++ ZIP (Z,MAP VAR Y)) ' M)’
+ >- (MATCH_MP_TAC LAMl_ALPHA_ssub >> rw [DISJOINT_SYM] \\
+     Suff ‘FV M = set Z’ >- METIS_TAC [DISJOINT_SYM] \\
+     rw [Abbr ‘M’, FV_appstar] \\
+    ‘Z = SNOC (LAST Z) (FRONT Z)’ by PROVE_TAC [SNOC_LAST_FRONT] \\
+     POP_ORW \\
+     simp [LIST_TO_SET_SNOC] \\
+     rw [Once EXTENSION, MEM_MAP] \\
+     EQ_TAC >> rw [] >> fs [] \\
+     DISJ2_TAC \\
+     Q.EXISTS_TAC ‘FV (VAR x)’ >> rw [] \\
+     Q.EXISTS_TAC ‘VAR x’ >> rw [])
+ >> Rewr'
+ >> ‘Y <> []’ by rw [NOT_NIL_EQ_LENGTH_NOT_0]
+ >> REWRITE_TAC [GSYM fromPairs_def]
+ >> qabbrev_tac ‘fm = fromPairs Z (MAP VAR Y)’
+ >> ‘FDOM fm = set Z’ by rw [FDOM_fromPairs, Abbr ‘fm’]
+ >> qabbrev_tac ‘y = LAST Y’
+ (* postfix for LAMl_ALPHA_ssub *)
+ >> ‘!t. LAMl Y t = LAMl (SNOC y (FRONT Y)) t’
+       by (ASM_SIMP_TAC std_ss [Abbr ‘y’, SNOC_LAST_FRONT]) >> POP_ORW
+ >> REWRITE_TAC [LAMl_SNOC]
+ >> Know ‘fm ' M = VAR y @* MAP VAR (FRONT Y)’
+ >- (simp [Abbr ‘M’, ssub_appstar] \\
+     Know ‘fm ' z = VAR y’
+     >- (rw [Abbr ‘fm’, Abbr ‘z’, LAST_EL] \\
+         Know ‘fromPairs Z (MAP VAR Y) ' (EL (PRE (n + 1)) Z) =
+               EL (PRE (n + 1)) (MAP VAR Y)’
+         >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
+         rw [EL_MAP, Abbr ‘y’, LAST_EL]) >> Rewr' \\
+     Suff ‘MAP ($' fm) (MAP VAR (FRONT Z)) = MAP VAR (FRONT Y)’ >- rw [] \\
+     rw [LIST_EQ_REWRITE, LENGTH_FRONT] \\
+    ‘PRE (n + 1) = n’ by rw [] >> POP_ASSUM (fs o wrap) \\
+     rename1 ‘i < n’ \\
+     simp [EL_MAP, LENGTH_FRONT] \\
+     Know ‘MEM (EL i (FRONT Z)) Z’
+     >- (rw [MEM_EL] \\
+         Q.EXISTS_TAC ‘i’ >> rw [] \\
+         MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) \\
+     rw [Abbr ‘fm’] \\
+     Know ‘EL i (FRONT Z) = EL i Z’
+     >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\
+     Know ‘EL i (FRONT Y) = EL i Y’
+     >- (MATCH_MP_TAC EL_FRONT >> rw [LENGTH_FRONT, NULL_EQ]) >> Rewr' \\
+     Know ‘fromPairs Z (MAP VAR Y) ' (EL i Z) = EL i (MAP VAR Y)’
+     >- (MATCH_MP_TAC fromPairs_FAPPLY_EL >> rw []) >> Rewr' \\
+     rw [EL_MAP])
+ >> Rewr'
+ >> qabbrev_tac ‘vs = FRONT Y’
+ >> Know ‘ALL_DISTINCT vs /\ ~MEM y vs’
+ >- (Q.PAT_X_ASSUM ‘ALL_DISTINCT Y’ MP_TAC \\
+    ‘Y = SNOC y vs’ by METIS_TAC [SNOC_LAST_FRONT] >> POP_ORW \\
+     rw [ALL_DISTINCT_SNOC])
+ >> STRIP_TAC
+ >> MATCH_MP_TAC principle_hnf_permutator_lemma
+ >> ‘SNOC y vs = Y’ by METIS_TAC [SNOC_LAST_FRONT] >> POP_ORW
+ >> rw [EVERY_MEM, Abbr ‘vs’, LENGTH_FRONT] >- art []
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> Q.EXISTS_TAC ‘e’ >> art []
+QED
+
 val _ = export_theory ();
 val _ = html_theory "solvable";
 
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index 4a4ae1ef3d..68f2b0a425 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -183,6 +183,19 @@ Proof
  >> simp [LIST_TO_SET_SNOC] >> SET_TAC []
 QED
 
+(* A special case of FV_appstar *)
+Theorem FV_appstar_MAP_VAR[simp] :
+    FV (M @* MAP VAR vs) = FV M UNION set vs
+Proof
+    rw [FV_appstar]
+ >> Suff ‘BIGUNION (IMAGE FV (set (MAP VAR vs))) = set vs’ >- rw []
+ >> rw [Once EXTENSION, IN_BIGUNION_IMAGE]
+ >> reverse EQ_TAC >> rpt STRIP_TAC
+ >- (Q.EXISTS_TAC ‘VAR x’ >> rw [MEM_MAP])
+ >> rename1 ‘x IN FV t’
+ >> gs [MEM_MAP]
+QED
+
 (*---------------------------------------------------------------------------*
  *  LAMl (was in standardisationTheory)
  *---------------------------------------------------------------------------*)
diff --git a/examples/lambda/basics/termScript.sml b/examples/lambda/basics/termScript.sml
index 6d7144d665..4a7155919f 100644
--- a/examples/lambda/basics/termScript.sml
+++ b/examples/lambda/basics/termScript.sml
@@ -1053,7 +1053,8 @@ QED
 
 (* A combined version of ssub_update_apply_SUBST and ssub_SUBST *)
 Theorem ssub_update_apply_SUBST' :
-    !M. (!k. k IN FDOM fm ==> v # fm ' k) /\ v NOTIN FDOM fm /\
+    !M fm v N.
+       (!k. k IN FDOM fm ==> v # fm ' k) /\ v NOTIN FDOM fm /\
         DISJOINT (FDOM fm) (FV N) ==>
         (fm |+ (v,N)) ' M = [fm ' N/v] (fm ' M)
 Proof