Reversible Optionen ersetzen

• wenn G = (G^L, G^R) mit x∈G^L so daß y∈x^R und y≤G,

  dann G $\approx$ G' = (G^L $\setminus$ {x}∪y^L, G^R)

• Idee: falls G→_Lx, dann x→_Ry, ist für R besser als G

• Beispiel, mit: * = {0 | 0},↑ = {0 | *} (Name: Up)

  G = {↑ | ↑}, x = ↑, y = *, aus y≤G folgt G $\approx$ {0 | ↑}, ist Nf.

• Beweis: Strategie für zweiten in G' - G
  • für z∈y^L: z$\triangleleft$ y≤G, (z als unnütze L-Option in G)
  • (G' - G)→_R(G' - x)→_L(G' - y). Jetzt R nicht in - y, sondern in G', zu →_R(p - y)≥(p - G)$\triangleright$ 0
• Implementierung?