132 3 Der Redehandlungskalkul
Als nachstes soil gezeigt werden, dass RGF(S) fur keine Sequenz S leer ist, dass also
jede Sequenz irgendwie fortgesetzt werden kann.
Theorem 3-2. RGF ist fur keine Sequenz leer
Wenn S ∈ SEQ, dann ist RGF(S) ≠ 0.
Beweis: Sei S ∈ SEQ. Nun gilt, dass rxo^l ∈ GTERM. Also ist nach Definition 3-16 S и
{(Dom(S), rAlso x0 = x0∣)} ∈ IEF(S). Also ist S и {(Dom(S), rAlso x0 = x0∣)} ∈
RGF(S) ≠ 0. ■
Theorem 3-3. Die Elemente von RGF(S) sind Fortsetzungen von S um genau einen Satz
Wenn S ∈ SEQ und S' ∈ RGF(S), dann gibt es Ξ ∈ PERF und Γ ∈ GFORM, so dass S' = S
и {(Dom(S), rΞ γ∣)}.
Beweis: Sei S ∈ SEQ und S' ∈ RGF(S). Dann ist S' ∈ AF(S) oder S' ∈ SEF(S) oder S'
∈ SBF(S) oder S' ∈ KEF(S) oder S' ∈ KBF(S) oder S' ∈ BEF(S) oder S' ∈ BBF(S)
oder S' ∈ AEF(S) oder S' ∈ ABF(S) oder S' ∈ NEF(S) oder S' ∈ NBF(S) oder S' ∈
UEF(S) oder S' ∈ UBF(S) oder S' ∈ PEF(S) oder S' ∈ PBF(S) oder S' ∈ IEF(S) oder
S' ∈ IBF(S).
Sei S' ∈ AF(S). Dann gibt es gemaβ Definition 3-1 Γ ∈ GFORM, so dass S' = S и
{(Dom(S), rSei Γ∣)}. Dann ist S'Dom(S) = rSei Γl und damit gibt es Ξ ∈ PERF und Γ ∈
GFORM, so dass S' = S и {(Dom(S), rΞ Γ∣)}.
Sei S' ∈ SEF(S) oder S' ∈ SBF(S) oder S' ∈ KEF(S) oder S' ∈ KBF(S) oder S' ∈
BEF(S) oder S' ∈ BBF(S) oder S' ∈ AEF(S) oder S' ∈ ABF(S) oder S' ∈ NEF(S) oder
S' ∈ NBF(S) oder S' ∈ UEF(S) oder S' ∈ UBF(S) oder S' ∈ PEF(S) oder S' ∈ PBF(S)
oder S' ∈ IEF(S) oder S' ∈ IBF(S). Dann gibt es gemaβ Definition 3-2 bis Definition
3-17 jeweils Γ ∈ GFORM, so dass S' = S и {(Dom(S), rAlso Γ∣)}. Dann ist S'Dom(S) =
rAlso Γπ und damit gibt es abermals Ξ ∈ PERF und Γ ∈ GFORM, so dass S' = S и
{(Dom(S), rΞ Γ∣)}. ■
Theorem 3-4. RGF-Fortsetzungen von Sequenzen sind genau um eins mdchtiger als die Aus-
gangssequenz
Wenn S ∈ SEQ und S' ∈ RGF(S), dann Dom(S') = Dom(S)+1.
Beweis: Sei S ∈ SEQ und S' ∈ RGF(S). Dann gibt es mit Theorem 3-3 Ξ ∈ PERF und Γ
∈ GFORM, so dass S' = S и {(Dom(S), rΞ Γ∣)} und damit Dom(S') = Dom(S)+1. ■