diff --git a/examples/lambda/barendregt/boehmScript.sml b/examples/lambda/barendregt/boehmScript.sml
index 46d91ff1d7..2a1a0d0333 100644
--- a/examples/lambda/barendregt/boehmScript.sml
+++ b/examples/lambda/barendregt/boehmScript.sml
@@ -12,7 +12,7 @@ open optionTheory arithmeticTheory pred_setTheory listTheory rich_listTheory
 open binderLib nomsetTheory termTheory appFOLDLTheory chap2Theory chap3Theory
      head_reductionTheory standardisationTheory solvableTheory reductionEval;
 
-open horeductionTheory takahashiTheory;
+open horeductionTheory takahashiS3Theory;
 
 val _ = new_theory "boehm";
 
@@ -20,6 +20,409 @@ val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"];
 
 val o_DEF = combinTheory.o_DEF;
 
+(*---------------------------------------------------------------------------*
+ *  Boehm tree
+ *---------------------------------------------------------------------------*)
+
+(* The type of Boehm tree:
+
+   For each ltree node, ‘NONE’ represents {\bot} (for unsolvable terms), while
+  ‘SOME (vs,y)’ represents ‘LAMl vs (VAR y)’. This separation of vs and y has
+   at least two advantages:
+
+   1. ‘set vs’ is the set of binding variables (BV) at that ltree node.
+   2. ‘LAMl vs (VAR y)’ can be easily "expanded" (w.r.t. eta reduction) into terms
+      such as ‘LAMl (vs ++ [z0;z1]) t’ (with two extra children ‘z0’ and ‘z1’)
+      without changing the head variable (VAR y).
+ *)
+Type boehm_tree[pp] = “:(string list # string) option ltree”
+
+(* Definition 10.1.9 [1, p.221] (Effective Boehm tree)
+
+   NOTE: The setup of ‘X UNION FV M’ when calling ‘FRESH_list’ guarentees that
+   the generated Boehm tree is "correct" no matter what X is supplied.
+
+   The word "correct" means that the binding lists of each node in the generated
+   Boehm tree do not capture free variables in the children nodes. Thus, if we
+   further translate each node from ‘string list # string’ to ‘num # num’ w.r.t.
+   de Bruijn encodings, the resulting Boehm tree should be unique for all X.
+
+   2024 UPDATE: Now BT_generator takes (X,M) where X is the initial X. Then,
+   for each generating children, the created fresh binding list ‘vs’ at current
+   level must be added into X for the next level. This is because the children
+   terms may contain free variables in ‘vs’, which was bound (thus not included
+   in FV M). When choosing binding variables for the next level, ‘vs’ must be
+   avoided too, for a "correct" generation.            -- Chun Tian, 4 gen 2024
+ *)
+Definition BT_generator_def :
+    BT_generator (X,M) =
+      if solvable M then
+         let M0 = principle_hnf M;
+              n = LAMl_size M0;
+             vs = FRESH_list n (X UNION FV M);
+             M1 = principle_hnf (M0 @* (MAP VAR vs));
+             Ms = hnf_children M1;
+              l = MAP ($, (X UNION set vs)) Ms;
+              y = hnf_headvar M1;
+              h = (vs,y)
+         in
+            (SOME h, fromList l)
+      else
+            (NONE  , LNIL)
+End
+
+Definition BT_def :
+    BT = ltree_unfold BT_generator
+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
+    rw [pairTheory.CURRY_DEF]
+QED
+
+(* This is the meaning of Boehm tree nodes, ‘fromNote’ translated from BT nodes
+   to lambda terms in form of ‘SOME (LAMl vs (VAR y))’ or ‘NONE’.
+ *)
+Definition fromNode_def :
+    fromNode = OPTION_MAP (\(vs,y). LAMl vs (VAR y))
+End
+
+(* Boehm tree of a single (free) variable ‘VAR s’ *)
+Definition BT_VAR_def :
+    BT_VAR s :boehm_tree = Branch (SOME (NIL,s)) LNIL
+End
+
+(* Remarks 10.1.3 (iii) [1, p.216]: unsolvable terms all have the same Boehm
+   tree (‘bot’). The following overloaded ‘bot’ may be returned by
+  ‘THE (ltree_lookup A p)’ when looking up a terminal node of the Boehm tree.
+ *)
+Overload bot = “Branch NONE (LNIL :boehm_tree llist)”
+
+(* Another form of ‘bot’, usually returned by “THE (ltree_el A p)”. *)
+Overload bot = “(NONE :(string list # string) option, SOME 0)”
+
+(* Unicode name: "base" *)
+val _ = Unicode.unicode_version {u = UTF8.chr 0x22A5, tmnm = "bot"};
+val _ = TeX_notation {hol = "bot", TeX = ("\\ensuremath{\\bot}", 1)};
+
+(* some easy theorems about Boehm trees of unsolvable terms *)
+Theorem BT_of_unsolvables :
+    !X M. unsolvable M ==> BTe X M = bot
+Proof
+    rw [BT_def, BT_generator_def, ltree_unfold, ltree_map]
+QED
+
+Theorem BT_of_unsolvables_EQ :
+    !X M N. unsolvable M /\ unsolvable N ==> BTe X M = BTe X N
+Proof
+    rw [BT_of_unsolvables]
+QED
+
+Theorem BT_finite_branching :
+    !X M. finite_branching (BTe X M)
+Proof
+    rpt GEN_TAC
+ >> irule finite_branching_coind'
+ >> Q.EXISTS_TAC ‘\b. ?X M. b = BTe X M’
+ >> rw [] >- (qexistsl_tac [‘X’, ‘M’] >> rw [])
+ (* stage work *)
+ >> qabbrev_tac ‘A = BTe X M’
+ >> qabbrev_tac ‘a = ltree_node A’
+ >> qabbrev_tac ‘ts = ltree_children A’
+ >> qexistsl_tac [‘a’, ‘ts’]
+ (* A = Branch a ts *)
+ >> CONJ_TAC >- rw [Abbr ‘a’, Abbr ‘ts’]
+ (* LFINITE ts *)
+ >> CONJ_TAC
+ >- rw [Abbr ‘A’, Abbr ‘ts’, BT_def, BT_generator_def, Once ltree_unfold,
+        LFINITE_fromList]
+ >> qabbrev_tac ‘P = \b. ?X M. b = BTe X M’
+ >> rw [Abbr ‘A’, Abbr ‘ts’, BT_def, BT_generator_def, Once ltree_unfold]
+ >> 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 ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
+ >> rename1 ‘MEM N (hnf_children M1)’
+ >> qexistsl_tac [‘X UNION set vs’, ‘N’] >> rw [BT_def]
+QED
+
+(* Given a hnf ‘M0’ and a shared binding variable list ‘vs’
+
+   hnf_tac adds the following abbreviation and new assumptions:
+
+   Abbrev (M1 = principle_hnf (M0 @* MAP VAR (TAKE (LAMl_size M0) vs)))
+   M0 = LAMl (TAKE (LAMl_size M0) vs) (VAR y @* args)
+   M1 = VAR y @* args
+
+   where the names "M1", "y" and "args" can be chosen from inputs.
+ *)
+fun hnf_tac (M0, vs, M1, y, args) = let
+ val n = “LAMl_size ^M0” in
+    qabbrev_tac ‘^M1 = principle_hnf (^M0 @* MAP VAR (TAKE ^n ^vs))’
+ >> Know ‘?^y ^args. ^M0 = LAMl (TAKE ^n ^vs) (VAR ^y @* ^args)’
+ >- (irule (iffLR hnf_cases_shared) >> rw [])
+ >> STRIP_TAC
+ >> Know ‘^M1 = VAR ^y @* ^args’
+ >- (qunabbrev_tac ‘^M1’ \\
+     Q.PAT_ASSUM ‘^M0 = LAMl (TAKE ^n ^vs) (VAR ^y @* ^args)’
+        (fn th => REWRITE_TAC [Once th]) \\
+     MATCH_MP_TAC principle_hnf_beta_reduce >> rw [hnf_appstar])
+ >> DISCH_TAC
+end;
+
+(* Proposition 10.1.6 [1, p.219] (beta-equivalent terms have the same Boehm tree)
+
+   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
+ *)
+Theorem lameq_BT_cong :
+    !X M N. FINITE X /\ FV M UNION FV N SUBSET X ==>
+            M == N ==> BTe X M = BTe X N
+Proof
+    RW_TAC std_ss []
+ >> reverse (Cases_on ‘solvable M’)
+ >- (‘unsolvable N’ by METIS_TAC [lameq_solvable_cong] \\
+     rw [BT_of_unsolvables])
+ >> ‘solvable N’ by METIS_TAC [lameq_solvable_cong]
+ (* applying ltree_bisimulation *)
+ >> rw [ltree_bisimulation]
+ (* NOTE: ‘solvable P /\ solvable Q’ cannot be added into the next relation *)
+ >> Q.EXISTS_TAC ‘\x y. ?P Q Y. FINITE Y /\ FV P UNION FV Q SUBSET Y /\
+                                P == Q /\ x = BTe Y P /\ y = BTe Y Q’
+ >> BETA_TAC
+ >> CONJ_TAC >- (qexistsl_tac [‘M’, ‘N’, ‘X’] >> rw [])
+ (* stage work *)
+ >> qx_genl_tac [‘a1’, ‘ts1’, ‘a2’, ‘ts2’] >> STRIP_TAC
+ >> qabbrev_tac ‘P0 = principle_hnf P’
+ >> 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 ‘P1 = principle_hnf (P0 @* MAP VAR vs)’
+ >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs')’
+ >> qabbrev_tac ‘Ps = hnf_children P1’
+ >> qabbrev_tac ‘Qs = hnf_children Q1’
+ >> qabbrev_tac ‘y  = hnf_headvar P1’
+ >> qabbrev_tac ‘y' = hnf_headvar Q1’
+ (* applying ltree_unfold *)
+ >> Q.PAT_X_ASSUM ‘_ = BTe Y Q’ MP_TAC
+ >> simp [BT_def, Once ltree_unfold, BT_generator_def]
+ >> Q.PAT_X_ASSUM ‘_ = BTe Y P’ MP_TAC
+ >> simp [BT_def, Once ltree_unfold, BT_generator_def]
+ >> NTAC 2 STRIP_TAC
+ (* easy case: unsolvable P (and Q) *)
+ >> reverse (Cases_on ‘solvable P’)
+ >- (‘unsolvable Q’ by PROVE_TAC [lameq_solvable_cong] >> fs [] \\
+     rw [llist_rel_def, LLENGTH_MAP])
+ (* 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 [])
+ >> DISCH_THEN (fs o wrap)
+ >> Know ‘n = n' /\ vs = vs'’
+ >- (reverse CONJ_ASM1_TAC >- rw [Abbr ‘vs’, Abbr ‘vs'’] \\
+     qunabbrevl_tac [‘n’, ‘n'’, ‘P0’, ‘Q0’] \\
+     MATCH_MP_TAC lameq_principle_hnf_size_eq' >> art [])
+ (* clean up now duplicated abbreviations: n' and vs' *)
+ >> qunabbrevl_tac [‘n'’, ‘vs'’]
+ >> DISCH_THEN (rfs o wrap o GSYM)
+ (* 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 [])
+ >> DISCH_THEN (rfs o wrap o GSYM)
+ >> qunabbrevl_tac [‘y’, ‘y'’]
+ (* applying lameq_principle_hnf_thm' *)
+ >> MP_TAC (Q.SPECL [‘Y’, ‘P’, ‘Q’, ‘P0’, ‘Q0’, ‘n’, ‘vs’, ‘P1’, ‘Q1’]
+                     lameq_principle_hnf_thm') >> simp []
+ >> rw [llist_rel_def, LLENGTH_MAP, EL_MAP]
+ >> Cases_on ‘i < LENGTH Ps’ >> fs [LNTH_fromList, EL_MAP]
+ >> Q.PAT_X_ASSUM ‘(Y UNION set vs,EL i Ps) = z’  (ONCE_REWRITE_TAC o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘(Y UNION set vs,EL i Qs) = z'’ (ONCE_REWRITE_TAC o wrap o SYM)
+ >> qexistsl_tac [‘EL i Ps’, ‘EL i Qs’, ‘Y UNION set vs’] >> simp []
+ (* preparing for hnf_children_FV_SUBSET
+
+    Here, once again, we need to get suitable explicit forms of P0 and Q0,
+    to show that, P1 and Q1 are absfree hnf.
+  *)
+ >> ‘hnf P0 /\ hnf Q0’ by PROVE_TAC [hnf_principle_hnf, solvable_iff_has_hnf]
+ >> qabbrev_tac ‘n = LAMl_size Q0’
+ >> ‘ALL_DISTINCT vs /\ LENGTH vs = n /\ DISJOINT (set vs) Y’
+      by rw [Abbr ‘vs’, FRESH_list_def]
+ >> Know ‘DISJOINT (set vs) (FV P0)’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+     Q.EXISTS_TAC ‘Y’ >> art [] \\
+     MATCH_MP_TAC SUBSET_TRANS \\
+     Q.EXISTS_TAC ‘FV P’ >> art [] \\
+     qunabbrev_tac ‘P0’ \\
+     MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ >> Know ‘DISJOINT (set vs) (FV Q0)’
+ >- (MATCH_MP_TAC DISJOINT_SUBSET \\
+     Q.EXISTS_TAC ‘Y’ >> art [] \\
+     MATCH_MP_TAC SUBSET_TRANS \\
+     Q.EXISTS_TAC ‘FV Q’ >> art [] \\
+     qunabbrev_tac ‘Q0’ \\
+     MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [])
+ >> DISCH_TAC
+ (* NOTE: the next two hnf_tac will refine P1 and Q1 *)
+ >> qunabbrevl_tac [‘P1’, ‘Q1’]
+ >> hnf_tac (“P0 :term”, “vs :string list”,
+             “P1 :term”, “y  :string”, “args :term list”)
+ >> hnf_tac (“Q0 :term”, “vs :string list”,
+             “Q1 :term”, “y' :string”, “args' :term list”)
+ >> ‘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 *)
+ >> qunabbrevl_tac [‘P1’, ‘Q1’]
+ >> qabbrev_tac ‘P1 = principle_hnf (P0 @* MAP VAR vs)’
+ >> qabbrev_tac ‘Q1 = principle_hnf (Q0 @* MAP VAR vs)’
+ (* applying hnf_children_FV_SUBSET *)
+ >> CONJ_TAC
+ >| [ (* goal 1 (of 2) *)
+      Know ‘!i. i < LENGTH Ps ==> FV (EL i Ps) SUBSET FV P1’
+      >- (MATCH_MP_TAC hnf_children_FV_SUBSET >> rw [Abbr ‘Ps’, hnf_appstar]) \\
+      DISCH_TAC \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV P1’ \\
+      CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV P0 UNION set vs’ \\
+      CONJ_TAC >- simp [FV_LAMl] \\
+      Suff ‘FV P0 SUBSET Y’ >- SET_TAC [] \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV P’ \\
+      reverse CONJ_TAC >- art [] (* FV P SUBSET Y *) \\
+      qunabbrev_tac ‘P0’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [],
+      (* goal 2 (of 2) *)
+      Know ‘!i. i < LENGTH Qs ==> FV (EL i Qs) SUBSET FV Q1’
+      >- (MATCH_MP_TAC hnf_children_FV_SUBSET >> rw [Abbr ‘Qs’, hnf_appstar]) \\
+      DISCH_TAC \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV Q1’ \\
+      CONJ_TAC >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV Q0 UNION set vs’ \\
+      CONJ_TAC >- simp [FV_LAMl] \\
+      Suff ‘FV Q0 SUBSET Y’ >- SET_TAC [] \\
+      MATCH_MP_TAC SUBSET_TRANS >> Q.EXISTS_TAC ‘FV Q’ \\
+      reverse CONJ_TAC >- art [] (* FV Q SUBSET Y *) \\
+      qunabbrev_tac ‘Q0’ >> MATCH_MP_TAC principle_hnf_FV_SUBSET' >> art [] ]
+QED
+
+(*---------------------------------------------------------------------------*
+ *  subterm
+ *---------------------------------------------------------------------------*)
+
+(* Definition 10.1.13 (iii), ‘subterm’ is the main device connecting Boehm trees
+   to Boehm transformations (below).
+
+  ‘subterm X M p’ returns (Y,N) where Y is X enriched with all binding variables
+   up to p, and N is the actual subterm.
+
+   NOTE: Similarily with BT_generator, the setup of ‘X UNION FV M’ guarentees
+   the correctness of ‘subterm X M’ for whatever X provided, including {}.
+
+   Also, in the recursive call of substerm, ‘X UNION set vs’ is used instead of
+   just ‘X’, because ‘vs’ may be free variables in some Ms.
+ *)
+Definition subterm_def :
+    subterm X M []      = SOME (X,M :term) /\
+    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);
+            M1 = principle_hnf (M0 @* (MAP VAR vs));
+            Ms = hnf_children M1;
+             m = LENGTH Ms
+        in
+            if x < m then subterm (X UNION set vs) (EL x Ms) xs else NONE
+    else
+        NONE
+End
+
+(* This assumes ‘subterm X M p <> NONE’ *)
+Overload subterm' = “\X M p. SND (THE (subterm X M p))”
+
+(* |- !X M. subterm X M [] = SOME M *)
+Theorem subterm_NIL[simp] = cj 1 subterm_def
+
+(* 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 ==>
+            BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p)
+Proof
+    Induct_on ‘p’
+ >- rw [subterm_def, ltree_lookup_def]
+ >> 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 ‘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]
+ >> simp [Once ltree_unfold, BT_generator_def]
+ >> DISCH_TAC
+ >> simp [LNTH_fromList, EL_MAP]
+ >> Q.PAT_X_ASSUM ‘h::p IN ltree_paths (BTe X M)’ MP_TAC
+ >> POP_ORW
+ >> rw [ltree_paths_def, ltree_lookup_def, LNTH_fromList, GSYM BT_def, EL_MAP]
+QED
+
+(* NOTE: In the above theorem, when the antecedents hold, i.e.
+
+         p IN ltree_paths (BTe X M) /\ subterm X M p = NONE
+
+   Then ‘subterm' X M (FRONT p)’ must be an unsolvable term. This result can be
+   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) ==>
+           (subterm X M p = NONE <=>
+            p <> [] /\ unsolvable (subterm' X M (FRONT p)))
+Proof
+    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 ‘M1 = principle_hnf (M0 @* (MAP VAR vs))’
+ >> qabbrev_tac ‘Ms = hnf_children M1’
+ >> reverse (Cases_on ‘solvable M’)
+ >- (rw [] >> Suff ‘p = []’ >- rw [subterm_NIL] \\
+     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 []
+ (* stage work, now M is solvable *)
+ >> Cases_on ‘p = []’
+ >- (rw [subterm_NIL] \\
+     Q.PAT_X_ASSUM ‘[h] IN ltree_paths (BTe X M)’ MP_TAC \\
+     simp [BT_def, Once ltree_unfold, BT_generator_def, ltree_paths_def,
+           ltree_lookup_def, LNTH_fromList] \\
+     Cases_on ‘h < LENGTH Ms’ >> simp [])
+ (* now: p <> [] *)
+ >> Know ‘h < LENGTH Ms’
+ >- (Q.PAT_X_ASSUM ‘h::p IN ltree_paths (BTe X M)’ MP_TAC \\
+     simp [BT_def, Once ltree_unfold, BT_generator_def, ltree_paths_def,
+           ltree_lookup_def, LNTH_fromList] \\
+     Cases_on ‘h < LENGTH Ms’ >> simp [])
+ >> RW_TAC std_ss [FRONT_DEF]
+ (* stage work *)
+ >> qabbrev_tac ‘N = EL h Ms’
+ >> Know ‘subterm X M (h::FRONT p) = subterm (X UNION set vs) N (FRONT p)’
+ >- rw [subterm_def]
+ >> Rewr'
+ >> FULL_SIMP_TAC std_ss []
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ (* p IN ltree_paths (BTe X N) *)
+ >> Q.PAT_X_ASSUM ‘h::p IN ltree_paths (BTe X M)’ MP_TAC
+ >> rw [BT_def, Once ltree_unfold, BT_generator_def, ltree_paths_def,
+        ltree_lookup_def, LNTH_fromList, EL_MAP]
+QED
+
 (*---------------------------------------------------------------------------*
  *  Equivalent terms
  *---------------------------------------------------------------------------*)
@@ -57,16 +460,20 @@ Definition equivalent_def :
            ~solvable M /\ ~solvable N
 End
 
-Theorem equivalent_comm :
-    !M N. equivalent M N <=> equivalent N M
+Theorem equivalent_symmetric :
+    symmetric equivalent
 Proof
-    RW_TAC std_ss [equivalent_def, Once MAX_COMM, Once UNION_COMM]
- >- (rename1 ‘y2 = y3 /\ n1 + m3 = n3 + m2 <=> y = y1 /\ n + m1 = n1 + m’ \\
-    ‘n3 = n’ by rw [Abbr ‘n3’, Abbr ‘n’] >> gs [] \\
-     EQ_TAC >> rw [])
- >>  METIS_TAC []
+    RW_TAC std_ss [symmetric_def, equivalent_def, Once MAX_COMM, Once UNION_COMM]
+ >> reverse (Cases_on ‘solvable x /\ solvable y’) >- fs []
+ >> simp []
+ >> rename1 ‘y1 = y2 /\ m1 + n = m + n1 <=> y3 = y4 /\ m3 + n1 = m2 + n3’
+ >> ‘n3 = n’ by rw [Abbr ‘n3’, Abbr ‘n’] >> gs []
+ >> EQ_TAC >> rw []
 QED
 
+(* |- !x y. equivalent x y <=> equivalent y x *)
+Theorem equivalent_comm = REWRITE_RULE [symmetric_def] equivalent_symmetric
+
 Theorem equivalent_of_solvables :
     !M N. solvable M /\ solvable N ==>
          (equivalent M N <=>
@@ -115,29 +522,6 @@ Proof
  >> METIS_TAC []
 QED
 
-(* Given a hnf ‘M0’ and a shared binding variable list ‘vs’
-
-   hnf_tac adds the following abbreviation and new assumptions:
-
-   Abbrev (M1 = principle_hnf (M0 @* MAP VAR (TAKE (LAMl_size M0) vs)))
-   M0 = LAMl (TAKE (LAMl_size M0) vs) (VAR y @* args)
-   M1 = VAR y @* args
-
-   where the names "M1", "y" and "args" can be chosen from inputs.
- *)
-fun hnf_tac (M0,vs,M1,y,args) = let val n = “LAMl_size ^M0” in
-    qabbrev_tac ‘^M1 = principle_hnf (^M0 @* MAP VAR (TAKE ^n ^vs))’
- >> Know ‘?^y ^args. ^M0 = LAMl (TAKE ^n ^vs) (VAR ^y @* ^args)’
- >- (irule (iffLR hnf_cases_shared) >> rw [])
- >> STRIP_TAC
- >> Know ‘^M1 = VAR ^y @* ^args’
- >- (qunabbrev_tac ‘^M1’ \\
-     Q.PAT_ASSUM ‘^M0 = LAMl (TAKE ^n ^vs) (VAR ^y @* ^args)’
-        (fn th => REWRITE_TAC [Once th]) \\
-     MATCH_MP_TAC principle_hnf_beta_reduce >> rw [hnf_appstar])
- >> DISCH_TAC
-end;
-
 (* The following combined tactic is useful after:
 
    RW_TAC std_ss [equivalent_of_solvables, principle_hnf_reduce]
@@ -167,8 +551,8 @@ val equivalent_tac =
  >> Q.PAT_X_ASSUM ‘N0 = _’ ASSUME_TAC
  >> Q.PAT_X_ASSUM ‘M1 = _’ ASSUME_TAC
  >> Q.PAT_X_ASSUM ‘N1 = _’ ASSUME_TAC
- >> ‘VAR y1 = y’  by rw [Abbr ‘y’ , hnf_head_absfree]
- >> ‘VAR y2 = y'’ by rw [Abbr ‘y'’, hnf_head_absfree];
+ >> ‘VAR y1 = y’  by rw [Abbr ‘y’ , absfree_hnf_head]
+ >> ‘VAR y2 = y'’ by rw [Abbr ‘y'’, absfree_hnf_head];
 
 (* From [1, p.238]. This concerte example shows that dB encoding is not easy in
    defining this "concept": the literal encoding of inner head variables are not
@@ -219,7 +603,7 @@ Proof
  >> METIS_TAC []
 QED
 
-Theorem equivalent_unsolvables :
+Theorem equivalent_of_unsolvables :
     !M N. unsolvable M /\ unsolvable N ==> equivalent M N
 Proof
     rw [equivalent_def]
@@ -229,7 +613,15 @@ QED
  *  Boehm transformations
  *---------------------------------------------------------------------------*)
 
-(* Definition 10.3.3 (i) *)
+(* Definition 10.3.2 [1, p.246] *)
+val _ = set_fixity "is_substitution_instance_of" (Infixr 490);
+
+(* NOTE: ‘(DOM phi) SUBSET (FV M)’ is not necessary *)
+Definition is_substitution_instance_of :
+    N is_substitution_instance_of M <=> ?phi. N = M ISUB phi
+End
+
+(* Definition 10.3.3 (i) [1, p.246] *)
 Type transform[pp] = “:(term -> term) list”
 
 (* Definition 10.3.3 (ii) *)
@@ -560,7 +952,7 @@ Proof
 QED
 
 (* Lemma 10.3.6 (i) [1, p.247] *)
-Theorem Boehm_transform_is_ready_exists :
+Theorem Boehm_transform_exists_lemma1 :
     !M. ?pi. Boehm_transform pi /\ is_ready (apply pi M)
 Proof
     Q.X_GEN_TAC ‘M’
@@ -666,8 +1058,7 @@ Proof
              Know ‘(FEMPTY |++ L) ' (EL n (FRONT Z)) = EL n args'’
              >- (FIRST_X_ASSUM MATCH_MP_TAC >> art []) >> Rewr' \\
              Suff ‘z # EL n args’
-             >- (DISCH_TAC \\
-                 CCONTR_TAC >> fs [] >> METIS_TAC [SUBSET_DEF]) \\
+             >- (DISCH_TAC >> CCONTR_TAC >> fs [] >> METIS_TAC [SUBSET_DEF]) \\
              CCONTR_TAC >> fs [] \\
              Q.PAT_X_ASSUM ‘DISJOINT (set Z) X’ MP_TAC \\
              rw [DISJOINT_ALT, Abbr ‘X’] \\
@@ -693,8 +1084,7 @@ Proof
      Know ‘DISJOINT (set Z) (BIGUNION (IMAGE FV (set args')))’
      >- (MATCH_MP_TAC DISJOINT_SUBSET \\
          Q.EXISTS_TAC ‘X’ >> rw [Abbr ‘X’]) \\
-     rw [DISJOINT_ALT] \\
-     FIRST_X_ASSUM irule >> art [] \\
+     rw [DISJOINT_ALT] >> FIRST_X_ASSUM irule >> art [] \\
      Q.EXISTS_TAC ‘EL n args'’ >> rw [MEM_EL] \\
      Q.EXISTS_TAC ‘n’ >> art [])
  >> DISCH_TAC
@@ -705,6 +1095,7 @@ Proof
      reverse CONJ_TAC
      >- (rw [Abbr ‘p1’, Abbr ‘xs’, MAP_MAP_o, GSYM MAP_REVERSE]) \\
      MATCH_MP_TAC Boehm_transform_APPEND >> rw [Abbr ‘p2’, Abbr ‘p3’])
+ (* applying is_ready_alt *)
  >> simp [is_ready_alt]
  >> DISJ2_TAC
  >> qexistsl_tac [‘a’, ‘args'’]
@@ -723,7 +1114,7 @@ Proof
      CONJ_TAC >- art [] \\
      qunabbrev_tac ‘M0’ \\
      MATCH_MP_TAC lameq_SYM \\
-     MATCH_MP_TAC lameq_principle_hnf' >> art [])
+     MATCH_MP_TAC lameq_principle_hnf_reduce' >> art [])
  >> ONCE_REWRITE_TAC [Boehm_apply_APPEND]
  >> MATCH_MP_TAC lameq_TRANS
  >> Q.EXISTS_TAC ‘apply (p3 ++ p2) M1’
@@ -887,8 +1278,7 @@ Proof
       Q.EXISTS_TAC ‘apply p3 (VAR a @* MAP VAR bs)’ \\
       CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> art []) \\
       rw [Abbr ‘p3’] \\
-      MATCH_MP_TAC lameq_TRANS \\
-      Q.EXISTS_TAC ‘f2 P’ \\
+      MATCH_MP_TAC lameq_TRANS >> Q.EXISTS_TAC ‘f2 P’ \\
       reverse CONJ_TAC >- rw [] \\
       MATCH_MP_TAC solving_transform_lameq >> rw [Abbr ‘f2’],
       (* goal 2 (of 2) *)
@@ -988,7 +1378,7 @@ Proof
        Q.EXISTS_TAC ‘apply (p1 ++ p0) N0’ \\
        CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf >> art [GSYM solvable_iff_has_hnf]) \\
+                    MATCH_MP_TAC lameq_principle_hnf_reduce >> art [GSYM solvable_iff_has_hnf]) \\
     (* eliminating p0 *)
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
@@ -1026,7 +1416,7 @@ Proof
        CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘M0’ \\
                     MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf >> art [GSYM solvable_iff_has_hnf]) \\
+                    MATCH_MP_TAC lameq_principle_hnf_reduce >> art [GSYM solvable_iff_has_hnf]) \\
     (* eliminating p0 *)
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
@@ -1115,7 +1505,7 @@ Proof
        Q.EXISTS_TAC ‘apply (pi ++ p0) M0’ \\
        CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘M0’ >> MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf \\
+                    MATCH_MP_TAC lameq_principle_hnf_reduce \\
                     ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
@@ -1128,7 +1518,7 @@ Proof
        Q.EXISTS_TAC ‘apply (pi ++ p0) N0’ \\
        CONJ_TAC >- (MATCH_MP_TAC lameq_apply_cong >> POP_ASSUM (REWRITE_TAC o wrap) \\
                     qunabbrev_tac ‘N0’ >> MATCH_MP_TAC lameq_SYM \\
-                    MATCH_MP_TAC lameq_principle_hnf \\
+                    MATCH_MP_TAC lameq_principle_hnf_reduce \\
                     ASM_REWRITE_TAC [GSYM solvable_iff_has_hnf]) \\
        REWRITE_TAC [Boehm_apply_APPEND] \\
        MATCH_MP_TAC lameq_TRANS \\
diff --git a/examples/lambda/barendregt/chap3Script.sml b/examples/lambda/barendregt/chap3Script.sml
index 759cfa7169..5d295c27cc 100644
--- a/examples/lambda/barendregt/chap3Script.sml
+++ b/examples/lambda/barendregt/chap3Script.sml
@@ -186,6 +186,16 @@ val ccbeta_rwt = store_thm(
     FULL_SIMP_TAC (srw_ss()) []
   ]);
 
+Theorem ccbeta_LAMl_rwt :
+    !vs M N. LAMl vs M -b-> N <=> ?M'. N = LAMl vs M' /\ M -b-> M'
+Proof
+    Induct_on ‘vs’
+ >> rw [ccbeta_rwt] (* only one goal left *)
+ >> EQ_TAC >> rw []
+ >- (Q.EXISTS_TAC ‘M'’ >> art [])
+ >> Q.EXISTS_TAC ‘LAMl vs M'’ >> rw []
+QED
+
 val beta_normal_form_bnf = store_thm(
   "beta_normal_form_bnf",
   ``normal_form beta = bnf``,
@@ -689,6 +699,7 @@ val ccbeta_lameq = store_thm(
   "ccbeta_lameq",
   ``!M N. M -b-> N ==> M == N``,
   SRW_TAC [][lameq_betaconversion, EQC_R]);
+
 val betastar_lameq = store_thm(
   "betastar_lameq",
   ``!M N. M -b->* N ==> M == N``,
@@ -1578,6 +1589,11 @@ val betastar_eq_cong = store_thm(
   ``bnf N ==> M -b->* M' ==> (M -b->* N  <=> M' -b->* N)``,
   METIS_TAC [bnf_triangle, RTC_CASES_RTC_TWICE]);
 
+(* |- !x y z. x -b->* y /\ y -b->* z ==> x -b->* z *)
+Theorem betastar_TRANS =
+        RTC_TRANSITIVE |> Q.ISPEC ‘compat_closure beta’
+                       |> REWRITE_RULE [transitive_def]
+
 val _ = export_theory();
 val _ = html_theory "chap3";
 
diff --git a/examples/lambda/barendregt/head_reductionScript.sml b/examples/lambda/barendregt/head_reductionScript.sml
index a1f372ca80..12e4b4ab33 100644
--- a/examples/lambda/barendregt/head_reductionScript.sml
+++ b/examples/lambda/barendregt/head_reductionScript.sml
@@ -39,6 +39,9 @@ val hreduce1_FV = store_thm(
   ``∀M N. M -h-> N ⇒ ∀v. v ∈ FV N ⇒ v ∈ FV M``,
   METIS_TAC [SUBSET_DEF, hreduce_ccbeta, cc_beta_FV_SUBSET]);
 
+(* |- !M N. M -h-> N ==> FV N SUBSET FV M *)
+Theorem hreduce1_FV_SUBSET = hreduce1_FV |> REWRITE_RULE [GSYM SUBSET_DEF]
+
 Theorem hreduces_FV :
     ∀M N. M -h->* N ⇒ v ∈ FV N ⇒ v ∈ FV M
 Proof
@@ -985,12 +988,60 @@ Proof
           (tail (pcons x r q) = tail (drop i p))’ >- art []
  >> simp []
  >> DISCH_THEN (fs o wrap)
- >> ‘nth_label i p = g i’ by (rw [Abbr ‘p’, nth_label_pgenerate])
- >> ‘!i. el i p = f i’    by (rw [Abbr ‘p’, el_pgenerate])
+ >> ‘nth_label i p = g i’ by rw [Abbr ‘p’, nth_label_pgenerate]
+ >> ‘!i. el i p = f i’    by rw [Abbr ‘p’, el_pgenerate]
  >> ASM_REWRITE_TAC [GSYM ADD1]
  >> Q.EXISTS_TAC ‘SUC i’ >> REWRITE_TAC []
 QED
 
+(* This theorem guarentees the one-one mapping between the list and the path *)
+Theorem finite_head_reduction_path_to_list_11 :
+    !M p. (p = head_reduction_path M) /\ finite p ==>
+          ?l. l <> [] /\ (HD l = M) /\ hnf (LAST l) /\
+             (LENGTH l = THE (length p)) /\
+             (!i. i < LENGTH l ==> (EL i l = el i (head_reduction_path M))) /\
+              !i. SUC i < LENGTH l ==> EL i l -h-> EL (SUC i) l
+Proof
+    RW_TAC std_ss []
+ >> qabbrev_tac ‘p = head_reduction_path M’
+ >> ‘?n. length p = SOME n’ by METIS_TAC [finite_length]
+ >> Cases_on ‘n’ >- fs [length_never_zero]
+ >> rename1 ‘length p = SOME (SUC n)’
+ >> Q.EXISTS_TAC ‘GENLIST (\i. el i p) (SUC n)’ >> simp []
+ >> STRONG_CONJ_TAC >- rw [NOT_NIL_EQ_LENGTH_NOT_0] >> DISCH_TAC
+ >> CONJ_TAC >- rw [GSYM EL, Abbr ‘p’, head_reduction_path_def]
+ >> CONJ_TAC (* hnf *)
+ >- (qabbrev_tac ‘l = GENLIST (\i. el i p) (SUC n)’ \\
+     rw [Abbr ‘l’, LAST_EL] \\
+     Suff ‘el n p = last p’ >- rw [Abbr ‘p’, head_reduction_path_def] \\
+     rw [finite_last_el])
+ >> rw [head_reduce1_def]
+ >> ‘i IN PL p /\ i + 1 IN PL p’ by rw [PL_def]
+ >> qabbrev_tac ‘q = drop i p’
+ >> ‘el i p = first q’ by rw [Abbr ‘q’] >> POP_ORW
+ >> Know ‘el i (tail p) = first (tail q)’
+ >- (rw [Abbr ‘q’, REWRITE_RULE [ADD1] el_def])
+ >> Rewr'
+ >> Know ‘is_head_reduction q’
+ >- (qunabbrev_tac ‘q’ \\
+     irule finite_is_head_reduction_drop \\
+     rw [Abbr ‘p’, head_reduction_path_def])
+ >> DISCH_TAC
+ (* perform case analysis *)
+ >> ‘(?x. q = stopped_at x) \/ ?x r xs. q = pcons x r xs’ by METIS_TAC [path_cases]
+ >- (Know ‘PL q = IMAGE (\n. n - i) (PL p)’
+     >- rw [Abbr ‘q’, PL_drop] \\
+    ‘PL p = count (SUC n)’ by rw [PL_def, count_def] >> POP_ORW \\
+     POP_ORW (* q = stopped_at x *) \\
+     simp [PL_stopped_at] \\
+     Suff ‘IMAGE (\n. n - i) (count (SUC n)) <> {0}’ >- METIS_TAC [] \\
+     rw [Once EXTENSION] \\
+     Q.EXISTS_TAC ‘n - i’ >> rw [] \\
+     Q.EXISTS_TAC ‘n’ >> rw [])
+ >> fs [is_head_reduction_thm]
+ >> Q.EXISTS_TAC ‘r’ >> art []
+QED
+
 Theorem finite_head_reduction_path_to_list :
     !M. finite (head_reduction_path M) <=>
         ?l. l <> [] /\ (HD l = M) /\ hnf (LAST l) /\
@@ -999,40 +1050,8 @@ Proof
     Q.X_GEN_TAC ‘M’
  >> qabbrev_tac ‘p = head_reduction_path M’
  >> EQ_TAC >> rpt STRIP_TAC
- >- (‘?n. length p = SOME n’ by METIS_TAC [finite_length] \\
-     Cases_on ‘n’ >- fs [length_never_zero] \\
-     rename1 ‘length p = SOME (SUC n)’ \\
-     Q.EXISTS_TAC ‘GENLIST (\i. el i p) (SUC n)’ >> simp [] \\
-     STRONG_CONJ_TAC >- rw [NOT_NIL_EQ_LENGTH_NOT_0] >> DISCH_TAC \\
-     CONJ_TAC >- rw [GSYM EL, Abbr ‘p’, head_reduction_path_def] \\
-     CONJ_TAC (* hnf *)
-     >- (qabbrev_tac ‘l = GENLIST (\i. el i p) (SUC n)’ \\
-         rw [Abbr ‘l’, LAST_EL] \\
-         Suff ‘el n p = last p’ >- rw [Abbr ‘p’, head_reduction_path_def] \\
-         rw [finite_last_el]) \\
-     rw [head_reduce1_def] \\
-    ‘i IN PL p /\ i + 1 IN PL p’ by rw [PL_def] \\
-     qabbrev_tac ‘q = drop i p’ \\
-    ‘el i p = first q’ by rw [Abbr ‘q’] >> POP_ORW \\
-     Know ‘el i (tail p) = first (tail q)’
-     >- (rw [Abbr ‘q’, REWRITE_RULE [ADD1] el_def]) >> Rewr' \\
-     Know ‘is_head_reduction q’
-     >- (qunabbrev_tac ‘q’ \\
-         irule finite_is_head_reduction_drop \\
-         rw [Abbr ‘p’, head_reduction_path_def]) >> DISCH_TAC \\
-  (* perform case analysis *)
-    ‘(?x. q = stopped_at x) \/ ?x r xs. q = pcons x r xs’ by METIS_TAC [path_cases]
-     >- (Know ‘PL q = IMAGE (\n. n - i) (PL p)’
-         >- rw [Abbr ‘q’, PL_drop] \\
-        ‘PL p = count (SUC n)’ by rw [PL_def, count_def] >> POP_ORW \\
-         POP_ORW (* q = stopped_at x *) \\
-         simp [PL_stopped_at] \\
-         Suff ‘IMAGE (\n. n - i) (count (SUC n)) <> {0}’ >- METIS_TAC [] \\
-         rw [Once EXTENSION] \\
-         Q.EXISTS_TAC ‘n - i’ >> rw [] \\
-         Q.EXISTS_TAC ‘n’ >> art []) \\
-     fs [is_head_reduction_thm] \\
-     Q.EXISTS_TAC ‘r’ >> art [])
+ >- (MP_TAC (Q.SPECL [‘M’, ‘p’] finite_head_reduction_path_to_list_11) \\
+     rw [] >> Q.EXISTS_TAC ‘l’ >> rw [])
  (* stage work *)
  >> qabbrev_tac ‘len = LENGTH l’
  >> ‘0 < len /\ len <> 0’ by rw [Abbr ‘len’, GSYM NOT_NIL_EQ_LENGTH_NOT_0]
@@ -1200,7 +1219,7 @@ QED
 
 Overload hnf_headvar = “\t. THE_VAR (hnf_head t)”
 
-(* hnf_children retrives the ‘args’ part of an abs-free hnf (VAR y @* args) *)
+(* hnf_children retrives the ‘args’ part of absfree hnf *)
 Definition hnf_children_def :
     hnf_children t = if is_comb t then
                         SNOC (rand t) (hnf_children (rator t))
@@ -1255,7 +1274,25 @@ Proof
  >> rw [hnf_children_appstar, hnf_head_appstar]
 QED
 
-Theorem hnf_head_absfree :
+Theorem hnf_children_FV_SUBSET :
+    !M Ms. hnf M /\ ~is_abs M /\ (Ms = hnf_children M) ==>
+           !i. i < LENGTH Ms ==> FV (EL i Ms) SUBSET FV M
+Proof
+    rpt STRIP_TAC
+ >> ‘M = hnf_head M @* hnf_children M’ by PROVE_TAC [absfree_hnf_thm]
+ >> POP_ORW
+ >> Q.PAT_X_ASSUM ‘Ms = hnf_children M’ (fs o wrap)
+ >> qabbrev_tac ‘Ms = hnf_children M’
+ >> simp [FV_appstar]
+ >> MATCH_MP_TAC SUBSET_TRANS
+ >> Q.EXISTS_TAC ‘BIGUNION (IMAGE FV (set Ms))’
+ >> simp []
+ >> rw [SUBSET_DEF, IN_BIGUNION_IMAGE]
+ >> Q.EXISTS_TAC ‘EL i Ms’ >> rw [MEM_EL]
+ >> Q.EXISTS_TAC ‘i’ >> rw []
+QED
+
+Theorem absfree_hnf_head :
     !y args. hnf_head (VAR y @* args) = VAR y
 Proof
     rpt GEN_TAC
diff --git a/examples/lambda/barendregt/solvableScript.sml b/examples/lambda/barendregt/solvableScript.sml
index 272e37cbc8..86657898f8 100644
--- a/examples/lambda/barendregt/solvableScript.sml
+++ b/examples/lambda/barendregt/solvableScript.sml
@@ -1,16 +1,16 @@
 (*---------------------------------------------------------------------------*
- * solvableScript.sml (or chap8_3): Theory of Solvable Lambda Terms          *
+ * solvableScript.sml (or chap8_3): solvable terms (and principle hnfs)      *
  *---------------------------------------------------------------------------*)
 
 open HolKernel Parse boolLib bossLib;
 
 (* core theories *)
 open arithmeticTheory pred_setTheory listTheory rich_listTheory sortingTheory
-     finite_mapTheory pathTheory hurdUtils;
+     finite_mapTheory pathTheory relationTheory hurdUtils;
 
 (* lambda theories *)
 open binderLib nomsetTheory termTheory appFOLDLTheory chap2Theory chap3Theory
-     reductionEval standardisationTheory head_reductionTheory;
+     reductionEval standardisationTheory head_reductionTheory horeductionTheory;
 
 val _ = new_theory "solvable";
 
@@ -626,17 +626,61 @@ Proof
  >> MATCH_MP_TAC lameq_appstar_cong >> rw [lameq_K]
 QED
 
+(*---------------------------------------------------------------------------*
+ *  Principle Head Normal Forms (principle_hnf)
+ *---------------------------------------------------------------------------*)
+
 (* Definition 8.3.20 [1, p.177]
 
-   A term may have several hnf's, e.g. if any of its hnf can still do beta
-   reductions, after such reductions the term is still an hnf by definition.
-   The (unique) terminating term of head reduction path is called "principle"
-   hnf, which is used for defining Boehm trees.
+   A term may have many different hnf's. For example, if any hnf can still do
+   beta reductions, after reductions the hnf is still an hnf of the original term.
+
+   For solvable terms, there is a unique terminating hnf as the last element of
+   head reduction path, which is called "principle" hnf.
  *)
 Definition principle_hnf_def :
     principle_hnf = last o head_reduction_path
 End
 
+(* principle hnf has less (or equal) free variables
+
+   NOTE: this theorem depends on finite_head_reduction_path_to_list_11 and
+         hreduce1_FV.
+ *)
+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 *)
+ >> 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 []
+QED
+
+(* |- !M. solvable M ==> FV (principle_hnf M) SUBSET FV M *)
+Theorem principle_hnf_FV_SUBSET' =
+        principle_hnf_FV_SUBSET |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
+
 Theorem hnf_principle_hnf :
     !M. has_hnf M ==> hnf (principle_hnf M)
 Proof
@@ -920,7 +964,7 @@ Proof
  >> MATCH_MP_TAC lameq_solvable_cong_lemma >> art []
 QED
 
-Theorem lameq_principle_hnf :
+Theorem lameq_principle_hnf_reduce :
     !M. has_hnf M ==> principle_hnf M == M
 Proof
     rpt STRIP_TAC
@@ -936,8 +980,263 @@ Proof
 QED
 
 (* |- !M. solvable M ==> principle_hnf M == M *)
-Theorem lameq_principle_hnf' =
-        REWRITE_RULE [GSYM solvable_iff_has_hnf] lameq_principle_hnf
+Theorem lameq_principle_hnf_reduce' =
+        lameq_principle_hnf_reduce |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
+
+Theorem hnf_ccbeta_appstar_rwt[local] :
+    !y Ms N. VAR y @* Ms -b-> N /\ Ms <> [] ==>
+             ?Ns. N = VAR y @* Ns /\ LENGTH Ns = LENGTH Ms /\
+                  !i. i < LENGTH Ms ==> EL i Ms -b->* EL i Ns
+Proof
+    Q.X_GEN_TAC ‘y’
+ >> Induct_on ‘Ms’ using SNOC_INDUCT >> rw []
+ >> fs [ccbeta_rwt] (* 2 subgoals *)
+ >- (Cases_on ‘Ms = []’ >> fs [ccbeta_rwt] \\
+     Q.PAT_X_ASSUM ‘!N. P’ (MP_TAC o (Q.SPEC ‘M'’)) \\
+     RW_TAC std_ss [] \\
+     Q.EXISTS_TAC ‘SNOC x Ns’ >> rw [] \\
+    ‘i = LENGTH Ms \/ i < LENGTH Ms’ by rw []
+     >- (rw [EL_LENGTH_SNOC] \\
+         Q.PAT_X_ASSUM ‘LENGTH Ns = LENGTH Ms’ (REWRITE_TAC o wrap o SYM) \\
+         rw [EL_LENGTH_SNOC]) \\
+     rw [EL_SNOC])
+ (* stage work *)
+ >> Cases_on ‘Ms = []’ >> fs []
+ >- (Q.EXISTS_TAC ‘[N']’ >> rw [])
+ >> Q.EXISTS_TAC ‘SNOC N' Ms’
+ >> rw [appstar_SNOC]
+ >> ‘i = LENGTH Ms \/ i < LENGTH Ms’ by rw []
+ >- (rw [EL_LENGTH_SNOC])
+ >> rw [EL_SNOC]
+QED
+
+Theorem hnf_ccbeta_cases[local] :
+    !Ms. LAMl vs (VAR y @* Ms) -b-> N ==>
+         ?Ns. N = LAMl vs (VAR y @* Ns) /\
+              LENGTH Ns = LENGTH Ms /\
+              !i. i < LENGTH Ms ==> EL i Ms -b->* EL i Ns
+Proof
+    rw [ccbeta_LAMl_rwt]
+ >> Suff ‘?Ns. M' = VAR y @* Ns /\ LENGTH Ns = LENGTH Ms /\
+              !i. i < LENGTH Ms ==> EL i Ms -b->* EL i Ns’
+ >- (STRIP_TAC >> Q.EXISTS_TAC ‘Ns’ >> rw [])
+ >> MATCH_MP_TAC hnf_ccbeta_appstar_rwt
+ >> Cases_on ‘Ms = []’ >> fs [ccbeta_rwt]
+QED
+
+(* Lemma 8.3.16 [1, p.176] *)
+Theorem hnf_betastar_cases :
+    !vs y Ms N. LAMl vs (VAR y @* Ms) -b->* N ==>
+                ?Ns. N = LAMl vs (VAR y @* Ns) /\
+                     LENGTH Ns = LENGTH Ms /\
+                     !i. i < LENGTH Ms ==> EL i Ms -b->* EL i Ns
+Proof
+    NTAC 2 GEN_TAC
+ >> Suff ‘!M N. M -b->* N ==>
+               !Ms. M = LAMl vs (VAR y @* Ms) ==>
+                   ?Ns. N = LAMl vs (VAR y @* Ns) /\
+                        LENGTH Ns = LENGTH Ms /\
+                        !i. i < LENGTH Ms ==> EL i Ms -b->* EL i Ns’
+ >- METIS_TAC []
+ >> HO_MATCH_MP_TAC RTC_INDUCT >> rw []
+ >> Know ‘?Ns. M' = LAMl vs (VAR y @* Ns) /\
+               LENGTH Ns = LENGTH Ms /\
+               !i. i < LENGTH Ms ==> EL i Ms -b->* EL i Ns’
+ >- (irule hnf_ccbeta_cases >> art [])
+ >> STRIP_TAC
+ >> Q.PAT_X_ASSUM ‘!Ms. M' = LAMl vs (VAR y @* Ms) ==> P’
+      (MP_TAC o (Q.SPEC ‘Ns’))
+ >> RW_TAC std_ss [] (* this asserts Ns' *)
+ >> Q.EXISTS_TAC ‘Ns'’ >> rw []
+ >> MATCH_MP_TAC betastar_TRANS
+ >> Q.EXISTS_TAC ‘EL i Ns’ >> rw []
+QED
+
+(* Corollary 8.3.17 (ii) [1, p.176] (inner part) *)
+Theorem lameq_principle_hnf_lemma :
+    !X M N. FINITE X /\ FV M SUBSET X /\ FV N SUBSET X /\
+            hnf M /\ hnf N /\ M == N
+        ==> LAMl_size M = LAMl_size N /\
+            let n = LAMl_size M;
+                vs = FRESH_list n X;
+                M1 = principle_hnf (M @* MAP VAR vs);
+                N1 = principle_hnf (N @* MAP VAR vs)
+            in
+                hnf_headvar M1 = hnf_headvar N1 /\
+                LENGTH (hnf_children M1) = LENGTH (hnf_children N1) /\
+                !i. i < LENGTH (hnf_children M1) ==>
+                    EL i (hnf_children M1) == EL i (hnf_children N1)
+Proof
+    rpt GEN_TAC >> STRIP_TAC
+ (* at the beginning, we don't know if n = n' *)
+ >> qabbrev_tac ‘n  = LAMl_size M’
+ >> qabbrev_tac ‘n' = LAMl_size N’
+ (* applying hnf_cases_shared *)
+ >> qabbrev_tac ‘vs = FRESH_list (MAX n n') X’
+ >> ‘ALL_DISTINCT vs /\ DISJOINT (set vs) X /\ LENGTH vs = MAX n n'’
+      by rw [FRESH_list_def, Abbr ‘vs’]
+ >> Know ‘?y args. M = 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’ >> fs [])
+ >> STRIP_TAC
+ >> Know ‘?y' args'. N = 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’ >> fs [])
+ >> STRIP_TAC
+ >> qabbrev_tac ‘vs1 = TAKE n vs’
+ >> qabbrev_tac ‘vs2 = TAKE n' vs’
+ >> ‘n = LENGTH vs1 /\ n' = LENGTH vs2’ by rw [Abbr ‘n’, Abbr ‘n'’]
+ (* applying lameq_CR *)
+ >> ‘?Z. M -b->* Z /\ N -b->* Z’ by METIS_TAC [lameq_CR]
+ (* applying hnf_betastar_cases *)
+ >> ‘?Ns. Z = LAMl vs1 (VAR y @* Ns) /\ LENGTH Ns = LENGTH args /\
+          !i. i < LENGTH args ==> EL i args -b->* EL i Ns’
+       by METIS_TAC [hnf_betastar_cases]
+ >> ‘?Ns'. Z = LAMl vs2 (VAR y' @* Ns') /\ LENGTH Ns' = LENGTH args' /\
+          !i. i < LENGTH args' ==> EL i args' -b->* EL i Ns'’
+       by METIS_TAC [hnf_betastar_cases]
+ (* eliminate n' once we know n = n' *)
+ >> STRONG_CONJ_TAC >- METIS_TAC [LAMl_size_hnf]
+ >> DISCH_THEN (REV_FULL_SIMP_TAC std_ss o wrap o SYM)
+ >> qunabbrevl_tac [‘vs1’, ‘vs2’]
+ >> ‘TAKE n vs = vs’ by METIS_TAC [TAKE_LENGTH_ID]
+ >> POP_ASSUM (REV_FULL_SIMP_TAC std_ss o wrap)
+ (* eliminiate LETs in the goal *)
+ >> simp []
+ (* applying principle_hnf_beta_reduce *)
+ >> Know ‘principle_hnf (LAMl vs (VAR y @* args) @* MAP VAR vs) = VAR y @* args’
+ >- (MATCH_MP_TAC principle_hnf_beta_reduce >> rw [hnf_appstar])
+ >> Rewr'
+ >> Know ‘principle_hnf (LAMl vs (VAR y' @* args') @* MAP VAR vs) = VAR y' @* args'’
+ >- (MATCH_MP_TAC principle_hnf_beta_reduce >> rw [hnf_appstar])
+ >> Rewr'
+ >> simp [hnf_head_hnf, hnf_children_hnf]
+ >> Q.PAT_X_ASSUM ‘M = LAMl vs _’ K_TAC
+ >> Q.PAT_X_ASSUM ‘N = LAMl vs _’ K_TAC
+ >> gs [LAMl_eq_rewrite]
+ >> Q.PAT_X_ASSUM ‘y = y'’ (fs o wrap o SYM)
+ >> Q.PAT_X_ASSUM ‘Ns = Ns'’ (fs o wrap o SYM)
+ >> NTAC 2 (Q.PAT_X_ASSUM ‘_ = LENGTH args’ K_TAC)
+ >> Q.PAT_X_ASSUM ‘Z = _’ K_TAC
+ >> rpt STRIP_TAC
+ (* applying lameq_TRANS and betastar_lameq *)
+ >> MATCH_MP_TAC lameq_TRANS
+ >> Q.EXISTS_TAC ‘EL i Ns’
+ >> CONJ_TAC >- (MATCH_MP_TAC betastar_lameq >> rw [])
+ >> MATCH_MP_TAC lameq_SYM
+ >> MATCH_MP_TAC betastar_lameq >> rw []
+QED
+
+Theorem lameq_principle_hnf_size_eq :
+    !M N. has_hnf M /\ has_hnf N /\ M == N ==>
+          LAMl_size (principle_hnf M) = LAMl_size (principle_hnf N)
+Proof
+    rpt STRIP_TAC
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ >> qabbrev_tac ‘N0 = principle_hnf N’
+ >> 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_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\
+     MATCH_MP_TAC lameq_SYM \\
+     qunabbrev_tac ‘N0’ \\
+     MATCH_MP_TAC lameq_principle_hnf_reduce >> art [])
+ >> DISCH_TAC
+ >> ‘hnf M0 /\ hnf N0’ by METIS_TAC [hnf_principle_hnf]
+ >> qabbrev_tac ‘X = FV M0 UNION FV N0’
+ >> MP_TAC (Q.SPECL [‘X’, ‘M0’, ‘N0’] lameq_principle_hnf_lemma)
+ >> rw [Abbr ‘X’]
+QED
+
+(* |- !M N.
+        solvable M /\ solvable N /\ M == N ==>
+        LAMl_size (principle_hnf M) = LAMl_size (principle_hnf N)
+ *)
+Theorem lameq_principle_hnf_size_eq' =
+        lameq_principle_hnf_size_eq |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
+
+Theorem lameq_principle_hnf_headvar_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 /\
+         M0 = principle_hnf M /\ N0 = principle_hnf N /\
+         n = LAMl_size M0 /\ vs = FRESH_list n X /\
+         M1 = principle_hnf (M0 @* MAP VAR vs) /\
+         N1 = principle_hnf (N0 @* MAP VAR vs)
+     ==> hnf_headvar M1 = hnf_headvar N1
+Proof
+    RW_TAC std_ss [UNION_SUBSET]
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ >> qabbrev_tac ‘N0 = principle_hnf N’
+ >> qabbrev_tac ‘n = LAMl_size M0’
+ >> qabbrev_tac ‘vs = FRESH_list n X’
+ >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
+ >> qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vs)’
+ >> 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_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\
+     MATCH_MP_TAC lameq_SYM \\
+     qunabbrev_tac ‘N0’ \\
+     MATCH_MP_TAC lameq_principle_hnf_reduce >> art [])
+ >> DISCH_TAC
+ >> ‘hnf M0 /\ hnf N0’ by METIS_TAC [hnf_principle_hnf]
+ (* applying lameq_principle_hnf_lemma *)
+ >> MP_TAC (Q.SPECL [‘X’, ‘M0’, ‘N0’] lameq_principle_hnf_lemma)
+ >> Suff ‘FV M0 SUBSET X /\ FV N0 SUBSET X’ >- rw []
+ (* applying principle_hnf_FV_SUBSET *)
+ >> 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]
+
+(* Corollary 8.3.17 (ii) [1, p.176] (outer part) *)
+Theorem lameq_principle_hnf_thm :
+    !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 /\
+         M0 = principle_hnf M /\ N0 = principle_hnf N /\
+         n = LAMl_size M0 /\ vs = FRESH_list n X /\
+         M1 = principle_hnf (M0 @* MAP VAR vs) /\
+         N1 = principle_hnf (N0 @* MAP VAR vs)
+     ==> LAMl_size M0 = LAMl_size N0 /\
+         hnf_headvar M1 = hnf_headvar N1 /\
+         LENGTH (hnf_children M1) = LENGTH (hnf_children N1) /\
+         !i. i < LENGTH (hnf_children M1) ==>
+             EL i (hnf_children M1) == EL i (hnf_children N1)
+Proof
+    rpt GEN_TAC >> STRIP_TAC
+ >> NTAC 6 POP_ORW
+ >> qabbrev_tac ‘M0 = principle_hnf M’
+ >> qabbrev_tac ‘N0 = principle_hnf N’
+ >> qabbrev_tac ‘n = LAMl_size M0’
+ >> qabbrev_tac ‘vs = FRESH_list n X’
+ >> qabbrev_tac ‘M1 = principle_hnf (M0 @* MAP VAR vs)’
+ >> qabbrev_tac ‘N1 = principle_hnf (N0 @* MAP VAR vs)’
+ >> 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_TRANS >> Q.EXISTS_TAC ‘N’ >> art [] \\
+     MATCH_MP_TAC lameq_SYM \\
+     qunabbrev_tac ‘N0’ \\
+     MATCH_MP_TAC lameq_principle_hnf_reduce >> art [])
+ >> DISCH_TAC
+ >> ‘hnf M0 /\ hnf N0’ by METIS_TAC [hnf_principle_hnf]
+ (* applying lameq_principle_hnf_lemma *)
+ >> MP_TAC (Q.SPECL [‘X’, ‘M0’, ‘N0’] lameq_principle_hnf_lemma)
+ >> Suff ‘FV M0 SUBSET X /\ FV N0 SUBSET X’ >- rw []
+ (* applying principle_hnf_FV_SUBSET *)
+ >> METIS_TAC [principle_hnf_FV_SUBSET, SUBSET_TRANS, UNION_SUBSET]
+QED
+
+Theorem lameq_principle_hnf_thm' =
+        lameq_principle_hnf_thm |> REWRITE_RULE [GSYM solvable_iff_has_hnf]
 
 val _ = export_theory ();
 val _ = html_theory "solvable";
diff --git a/examples/lambda/basics/appFOLDLScript.sml b/examples/lambda/basics/appFOLDLScript.sml
index 75cf17543a..a039ceee98 100644
--- a/examples/lambda/basics/appFOLDLScript.sml
+++ b/examples/lambda/basics/appFOLDLScript.sml
@@ -332,6 +332,12 @@ Proof
     rw [FOLDR_SNOC]
 QED
 
+Theorem LAMl_eq_rewrite[simp] :
+    LAMl vs t1 = LAMl vs t2 <=> t1 = t2
+Proof
+    Induct_on ‘vs’ >> rw [LAM_eq_thm]
+QED
+
 (*---------------------------------------------------------------------------*
  *  funpow for lambda terms (using arithmeticTheory.FUNPOW)
  *---------------------------------------------------------------------------*)
diff --git a/src/coalgebras/ltreeScript.sml b/src/coalgebras/ltreeScript.sml
index f70d709627..74f9c52c9b 100644
--- a/src/coalgebras/ltreeScript.sml
+++ b/src/coalgebras/ltreeScript.sml
@@ -8,9 +8,10 @@
   Note that this tree data structure allows for both infinite depth
   and infinite breadth.
 *)
-open HolKernel Parse boolLib bossLib term_tactic;
+open HolKernel Parse boolLib bossLib;
+
 open arithmeticTheory listTheory llistTheory alistTheory optionTheory;
-open mp_then pred_setTheory relationTheory pairTheory combinTheory;
+open pred_setTheory relationTheory pairTheory combinTheory hurdUtils;
 
 val _ = new_theory "ltree";
 
@@ -700,50 +701,65 @@ Proof
  >> EQ_TAC >> rw []
 QED
 
-Definition ltree_finite_branching_def :
-    ltree_finite_branching = ltree_every (\a ts. LFINITE ts)
+Definition finite_branching_def :
+    finite_branching = ltree_every (\a ts. LFINITE ts)
 End
 
-Theorem ltree_finite_branching_rules :
-    !a ts. EVERY ltree_finite_branching ts ==>
-           ltree_finite_branching (Branch a (fromList ts))
+Theorem finite_branching_rules :
+    !a ts. EVERY finite_branching ts ==>
+           finite_branching (Branch a (fromList ts))
 Proof
-    rw [ltree_finite_branching_def, EVERY_MEM]
+    rw [finite_branching_def, EVERY_MEM]
  >> qabbrev_tac ‘P = \(a :'a) (ts :'a ltree llist). LFINITE ts’
  >> rw [Once ltree_every_cases]
  >- rw [Abbr ‘P’, LFINITE_fromList]
  >> rw [every_fromList_EVERY, EVERY_MEM]
 QED
 
+(* The "primed" version uses ‘every’ (and ‘LFINITE’) instead of ‘EVERY’ *)
+Theorem finite_branching_rules' :
+    !a ts. LFINITE ts /\ every finite_branching ts ==>
+           finite_branching (Branch a ts)
+Proof
+    rw [finite_branching_def]
+QED
+
 Theorem ltree_finite_imp_finite_branching :
-    !t. ltree_finite t ==> ltree_finite_branching t
+    !t. ltree_finite t ==> finite_branching t
 Proof
     HO_MATCH_MP_TAC ltree_finite_ind
- >> rw [ltree_finite_branching_rules]
+ >> rw [finite_branching_rules]
 QED
 
 (* cf. ltree_cases *)
-Theorem ltree_finite_branching_cases :
-    !t. ltree_finite_branching t <=>
-        ?a ts. t = Branch a (fromList ts) /\ EVERY ltree_finite_branching ts
+Theorem finite_branching_cases :
+    !t. finite_branching t <=>
+        ?a ts. t = Branch a (fromList ts) /\ EVERY finite_branching ts
 Proof
-    rw [ltree_finite_branching_def, Once ltree_every_cases]
+    rw [finite_branching_def, Once ltree_every_cases]
  >> EQ_TAC >> rw [LFINITE_fromList, every_fromList_EVERY]
  >> ‘?l. ts = fromList l’ by METIS_TAC [LFINITE_IMP_fromList]
  >> fs [every_fromList_EVERY]
 QED
 
+Theorem finite_branching_cases' :
+    !t. finite_branching t <=>
+        ?a ts. t = Branch a ts /\ LFINITE ts /\ every finite_branching ts
+Proof
+    rw [finite_branching_def, Once ltree_every_cases]
+QED
+
 (* |- (!a0. P a0 ==> ?a ts. a0 = Branch a ts /\ LFINITE ts /\ every P ts) ==>
-      !a0. P a0 ==> ltree_finite_branching a0
+      !a0. P a0 ==> finite_branching a0
  *)
 val lemma = ltree_every_coind
          |> (Q.SPEC ‘\(a :'a) (ts :'a ltree llist). LFINITE ts’)
          |> (Q.SPEC ‘P’) |> BETA_RULE
-         |> REWRITE_RULE [GSYM ltree_finite_branching_def];
+         |> REWRITE_RULE [GSYM finite_branching_def];
 
-Theorem ltree_finite_branching_coind :
+Theorem finite_branching_coind :
     !P. (!t. P t ==> ?a ts. t = Branch a (fromList ts) /\ EVERY P ts) ==>
-         !t. P t ==> ltree_finite_branching t
+         !t. P t ==> finite_branching t
 Proof
     NTAC 2 STRIP_TAC
  >> MATCH_MP_TAC lemma
@@ -754,11 +770,18 @@ Proof
  >> rw [LFINITE_fromList, every_fromList_EVERY]
 QED
 
-Theorem ltree_finite_branching_rewrite[simp] :
-    ltree_finite_branching (Branch a ts) <=>
-    LFINITE ts /\ every ltree_finite_branching ts
+Theorem finite_branching_coind' :
+    !P. (!t. P t ==> ?a ts. t = Branch a ts /\ LFINITE ts /\ every P ts) ==>
+         !t. P t ==> finite_branching t
+Proof
+    NTAC 2 STRIP_TAC
+ >> MATCH_MP_TAC lemma >> rw []
+QED
+
+Theorem finite_branching_rewrite[simp] :
+    finite_branching (Branch a ts) <=> LFINITE ts /\ every finite_branching ts
 Proof
-    SIMP_TAC std_ss [ltree_finite_branching_cases]
+    SIMP_TAC std_ss [finite_branching_cases]
  >> EQ_TAC >> rw []
  >- rw [LFINITE_fromList]
  >- rw [every_fromList_EVERY]
@@ -766,6 +789,103 @@ Proof
  >> fs [every_fromList_EVERY]
 QED
 
+(*---------------------------------------------------------------------------*
+ *  More ltree operators
+ *---------------------------------------------------------------------------*)
+
+Definition ltree_node_def[simp] :
+    ltree_node (Branch a ts) = a
+End
+
+Definition ltree_children_def[simp] :
+    ltree_children (Branch a ts) = ts
+End
+
+Theorem ltree_node_children_reduce[simp] :
+    Branch (ltree_node t) (ltree_children t) = t
+Proof
+   ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
+ >> rw []
+QED
+
+Definition ltree_paths_def :
+    ltree_paths t = {p | ltree_lookup t p <> NONE}
+End
+
+Theorem IN_ltree_lookup :
+    !p t. p IN ltree_paths t <=> ltree_lookup t p <> NONE
+Proof
+    rw [ltree_paths_def]
+QED
+
+Theorem NIL_IN_ltree_paths[simp] :
+    [] IN ltree_paths t
+Proof
+    rw [ltree_paths_def, ltree_lookup_def]
+QED
+
+Theorem ltree_paths_inclusive :
+    !l1 l2 t. l1 <<= l2 /\ l2 IN ltree_paths t ==> l1 IN ltree_paths t
+Proof
+    Induct_on ‘l1’
+ >> rw [] (* only one goal left *)
+ >> Cases_on ‘l2’ >> fs []
+ >> rename1 ‘l1 <<= l2’
+ >> Q.PAT_X_ASSUM ‘h = h'’ K_TAC
+ >> rename1 ‘h::l1 IN ltree_paths t’
+ >> POP_ASSUM MP_TAC
+ >> ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
+ >> POP_ORW
+ >> simp [ltree_paths_def, ltree_lookup_def]
+ >> Cases_on ‘LNTH h ts’ >> rw []
+ >> fs [GSYM IN_ltree_lookup]
+ >> FIRST_X_ASSUM MATCH_MP_TAC
+ >> Q.EXISTS_TAC ‘l2’ >> rw []
+QED
+
+Theorem ltree_el :
+    ltree_el t [] = SOME (ltree_node t,LLENGTH (ltree_children t)) /\
+    ltree_el t (n::ns) =
+      case LNTH n (ltree_children t) of
+        NONE => NONE
+      | SOME a => ltree_el a ns
+Proof
+   ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
+ >> simp [ltree_el_def]
+QED
+
+Theorem ltree_lookup :
+    ltree_lookup t [] = SOME t /\
+    ltree_lookup t (n::ns) =
+      case LNTH n (ltree_children t) of
+        NONE => NONE
+      | SOME a => ltree_lookup a ns
+Proof
+   ‘?a ts. t = Branch a ts’ by METIS_TAC [ltree_cases]
+ >> simp [ltree_lookup_def]
+QED
+
+Theorem ltree_lookup_iff_ltree_el[local] :
+    !p t. ltree_lookup t p <> NONE <=> ltree_el t p <> NONE
+Proof
+    Induct_on ‘p’
+ >- rw [ltree_lookup, ltree_el]
+ >> rw [Once ltree_lookup, Once ltree_el]
+ >> Cases_on ‘LNTH h (ltree_children t)’ >> fs []
+QED
+
+Theorem ltree_paths_alt :
+    !t. ltree_paths A = {p | ltree_el A p <> NONE}
+Proof
+    rw [ltree_paths_def, Once EXTENSION, ltree_lookup_iff_ltree_el]
+QED
+
+Theorem ltree_el_valid :
+    !p t. p IN ltree_paths t ==> ltree_el t p <> NONE
+Proof
+    rw [ltree_paths_alt]
+QED
+
 (*---------------------------------------------------------------------------*
  *  Rose tree is a finite variant of ltree, defined inductively.
  *---------------------------------------------------------------------------*)
diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
index 46c59d6e34..1a2b941914 100644
--- a/src/list/src/listScript.sml
+++ b/src/list/src/listScript.sml
@@ -2719,7 +2719,6 @@ val f_REVERSE_lemma = TAC_PROOF (([],
       (GEN (“x:('a)list”) (BETA_RULE (AP_THM x (“REVERSE (x:('a)list)”))))))),
       ASM_REWRITE_TAC[]]);
 
-
 val SNOC_Axiom_old = prove(
   “!(e:'b) (f:'b -> ('a -> (('a)list -> 'b))).
         ?! fn1.
@@ -2766,6 +2765,13 @@ val SNOC_Axiom = store_thm(
 val SNOC_INDUCT = save_thm("SNOC_INDUCT", prove_induction_thm SNOC_Axiom_old);
 val SNOC_CASES =  save_thm("SNOC_CASES", hd (prove_cases_thm SNOC_INDUCT));
 
+(* cf. rich_listTheory.IS_PREFIX_SNOC *)
+Theorem isPREFIX_SNOC[simp] :
+    l <<= SNOC x l
+Proof
+    Induct_on ‘l’ >> rw [SNOC, isPREFIX]
+QED
+
 (*--------------------------------------------------------------*)
 (* List generator                                               *)
 (*  GENLIST f n = [f 0;...; f(n-1)]                             *)