38

Я . Vogel

Definition von ta und (a) i fiir i<Q{ta\ i, aea.

1 . a = a' + i=>ta= — l,{a)0 = a'.

Sei nun a = (pubc ein L-Term.

2 . с L'TQrm=>ta = tc, (a) i = (pub({c)i +1). Sei nun с kein L-Term.

3 . b = c = 0=^ta = u,{a)i = i+l. Sei nun b>0.

4 . b = b' + l=>ta = 0,(a)0 = C^a,{a){n-^l) = (pub'({a)n).

5 . 0^fb^M=>ra = tfe,(a)i = (pw((b)ï + l)(C^a).

6 . tb = u-\-l=>ta = ö,{a)0 = Ca,{a){n-\-l) = (pu{b){{a)n)0.

Diese Bachmann-Konstruktion übersetzen wir nach д. Leider wird aber nicht {{a)iy ={a^)i'^ gelten. Wir benutzen eine etwas gedrängte Schreibweise : x sei eine Funktion mit {i\i<Q{tx)} als Definitionsbereich und SxiSu+1 für alle i<Q{tx), Sc^u, txuu'\-l. Wir vereinbaren, daß Ausdrücke wie xl immer stillschweigend i < Q{tx) voraussetzen. Dann definieren wir die Funktion xp : = Ruxc mit tionsbereich {i\i<Q{t\p)} wie folgt.

Definition von Ruxc.

1 - tx= — l=>txp = 0,xpO = c,xp{n +1) = фи{хО)(xpn).

2 . OStxuu=>txp = tx,Wi = Фи{хг)с.

3 . tx = u-{-l=>t\p = 0,ipO = c,\p{n +1) = (pu(x(w^))0.

Definition von (a) und ta fiir аФО, aeä. L a = a'-\-l=^ta=-l,{a)0 = a'.

Sei nun a = (pubc L-Term.

2 . b = c = 0=>ta = u,{a)i = i+l.

3 . с L-Term, -ic^a=>ta = tc, (a) i = фиЬ{{с) i + 1).

4 . {a) : = Ки(Ь) (Ca), ta : = t(a) sonst.

Ziel von Abschnitt 4 ist zu zeigen, daß (a) für L-Terme a eine gegen a streng monoton wachsende Folge ist. Dazu einige Vorbereitungen.

Lemma 4.5. i < Q{ta), v < ta.

( i ) N,a = K,a,D,a = D,{a)i = 0. (ii) 0<i-^K^(a)i = K^auKJ:

Beim Beweis von Lemma 4.5 beachte man ta>0 und v<Sa (wegen ta^Sa). Wir führen die Induktion nach la nicht aus. Die charakteristischen Unterschiede zwischen N^a und D^a sind Gegenstand des nächsten Hüfssatzes. Dabei steht a<M-{-œ {aeä,MQd) für: es gibt beM mit a<b+l... + L