What we've shown

(1) We define a set of reductions, using 
reduces, onereduces (SN0.thy) and cutReduces (CutRed.thy)

  cutReduces_Der "cutReduces (Der seq rule dtl) dtn = 
    (rule = cut & dtl ~= [] & ~ isUnf dtn &
    (c8red (Der seq rule dtl) dtn | nparRed (Der seq rule dtl) dtn) & 
    (Der seq rule dtl) ~= dtn)"
    
  cutReduces_Unf "cutReduces (Unf seq) dtn = False"

  c8red_def "c8red dt dtn == conclPT dtn = conclPT dt &
	    allPT wfb dtn & allPT (frb rls) dtn & c8redP dt dtn"

  nparRed_def "nparRed dt dtn == conclPT dtn = conclPT dt &
	    allPT wfb dtn & allPT (frb rls) dtn & nparRedP dt dtn"

  nparRedP' "nparRedP (Der seq rule dtl) dtn = (rule = cut & (ALL dts.
    isSubt dtn dts & isCut dts --> 
      isSubt (Der seq cut dtl) dts & Der seq cut dtl ~= dts |
	cutForm (Der seq cut dtl) = cutForm dts & 
	(dts, Der seq cut dtl) : LRPorder))"

    "nparRedP (Unf seq) dtn = False"

  c8redP_def "c8redP dt dtn == (ALL dts.
    isSubt dtn dts & botRule dts = cut --> 
      (isSubt dt dts & dt ~= dts) |
      size (cutForm dts) < size (cutForm dt))"

A strongly normalizable proof tree is defined (in SN0.thy)
in terms of the above.

Thus the above defines the set of reductions to which our
proof of strong normalization, in SN2.thy, applies.

(2) In RP.thy, we have defined functions mLP and mRP which are used in 
principal reductions.
We have shown that the results makeCutLP and makeCutRP,
used in the cut-elimination proof, can be replaced by stronger
results makeCutmLP and makeCutmRP, which specify that the functions 
mLP and mRP are used to obtain the replacement trees.

(3) In NP.thy, we have shown that, under certain conditions,
the reductions obtained by using mLP and mRP satisfy the predicate
cutReduces.

(4) In NP.thy we have enhanced the results allLP and allLRP 
(by allLPm and allLRPm) to show that the results allLP and allLRP
can be achieved by reductions which use mLP and mRP and which also
satisfy cutReduces (except for the identity reduction).