D18 Georg Meggle
Für T.G-4
+
: GG(P,A) GG(P,GG(P,A))
Da T.G4 bereits gezeigt, bleibt zu zeigen:
T.G4a: GG(P,GG(P,A)) GG(P,A)
Aus GG(P,GG(P,A)) nach D18.c GG
m
(P,GG(P,A)) bei bel. m 1; eben-
so mit D18.c und T.G5-1 GG
m
(P,GG
n
(P,A)) für bel. m,n 1. Daraus mit
L.G5 dann GG
m+n
(P,A) für bel. m,n 1 – also nach D18.c GG(P,A).
(T.G5-1 beweisbar mit T.G0-1 und T.G1-1.)
Für T.G-4
+*
: GW(P,A) GW(P,GW(P,A))
Da T.G-4
*
bereits gezeigt, nur noch die Umkehrung von T.G4* zu zeigen.
Das aber nach L.G1 trivial.
Für T.G5: A B ├ GG(P,A) GG(P,B)
Es gilt
TG1a: A B ├ G(X,A) G(X,B)
welches sich direkt aus RG und G1 ergibt. Und daher nach (GG.1) direkt
T.G5. T.G5 also analog aus T.G0 und T.G1.
Für T.G5*: A B ├