ABSTRACT
The idea of this transformation is quite simple: apply rep(z,s | - ) to every formula in every sequent of H - and hope that the result is the desired H# . In order to leave the other formulas of the endsequent unchanged, a first requirement evidently will be that z is not free in the formulas of M (nor, in the second case, in u ) . Further, I w ill need that rep(z,s | rep(x,z) | v)) becomes r e p ( x ,s |v ) . And I will also need that instances of Q -ru les within H remain such instances:
If Qy w is principal formula w ith a side formula rep(y ,t | w ) , y / z , thenthese formulas are transformed into Qy rep(z,s | w) and rep(z,s | rep(y ,t | w ) ) . But the latter should be usable as a side formula again, and so it should be of the form rep (y , h^(Z} s)(t) |r e p (z ,s |w ) ) .
