---

Step * of Lemma Game-minus-minus

∀G:Game. -(-(G)) ≡ G
BY
{ (BLemma `Game-induction` THEN Auto) }

1
1. G : Game
2. ∀m:Game. ((left-option{i:l}(G;m) ∨ right-option{i:l}(G;m)) ⇒ -(-(m)) ≡ m)
⊢ -(-(G)) ≡ G

---

Latex:

---

Latex:
\mforall{}G:Game.  -(-(G))  \mequiv{}  G


By

---

Latex:
(BLemma  `Game-induction`  THEN  Auto)

---

Home Index