more on readme

Author: Andrei Popescu

README.md

@@ -149,7 +149,9 @@ As discussed in Sect. 9 and App. G, we have automated the production of binding-
    * todo: the tactic for heuristic too. 
 
 
-### Mapping of the results from the main paper to Isabelle theorem names
+### Mapping of the results from the paper to Isabelle theorem names
+
+#### For the main paper 
 
 Prop 1 --> subsumed by Prop. 2 (also generated and proved automatically by the standard inductive definition)
 
@@ -175,6 +177,14 @@ Prop 21 --> theorem `strong_induct_reneqv` from ILC_Renaming_Equivalence.thy
 
 Thm 22 --> theorem `strong_iinduct` (in locale `IInduct`) from thys/Generic_Strong_Rule_Induction.thy. 
 
+#### For the appendix
+
+Thm. 29 --> just a recallection of the standard rule induction of the predicate generated by the rules. In isabelle the predicate is called `II` and is located in thys/Urban_Berghofer_Norrish_Rule_Induction.thy, in the locale `UBN_Components`, so the Isabelle is called `II.induct`.
+
+Thm. 33 --> this is infered from our Thm. 19 (theorem `strong_induct` in locale `Induct`) via a sublocale relationship: `UBN < UBN: Induct_simple` (the second `UBN` is just a label to avoid name clashes), which makes the theorem `strong_induct` available into the locale `UBN` 
+
+(NB: The Urban-Berghofer-Norrish result is formalized in an incremental sequence of locales that follows the same structere and naming as the locales for our main abstract results. `UBN` stands for the acronym of the author names.)
+