ABSTRACT
Unfortunately, the proofs of these apparently sim ple statem ents require a detailed study of the way in which the formulas r# arise under the repeated applications of the substitution map sub. Assum e, for instance, that a for mula r0 of the endsequent (not yet containing y 0) gives rise, further up, to a side formula rj which itself, still further up, gives rise to another side for mula r2 . If r0 = Q x0 Qxj Q x2 w0 then
r0 = Qx0 Qx 1Qx 2 w0 ri = su b(x0,s 0 1 Q x, Qx2 w0) = Q y, Q y2 w , r2 = sub(yj,S[ | Q y2 w ,) = Q z2 w 2
r0* = Qx0 Qx 1Qx 2 w0 r ,# = su b (x0,h1l( s0) | Q x j Q x 2w0) = Q y 1’ Q y2’ w 1’ r2# = su b (y i’ ,h 1)( s 1) | Q y2’ w 1’) = Q z2’ w 2’ .
