---

Step * of Lemma Game-minus_functionality

∀G1,G2:Game.  (G1 ≡ G2 ⇒ -(G1) ≡ -(G2))
BY
{ (RepeatFor 2 (((BLemma `Game-induction` THENA Auto) THEN RepeatFor 2 ((D 0 THENA Auto))))
   THEN Auto
   THEN D 0
   THEN Auto
   THEN Unfold `Game-minus` -1
   THEN RepUR ``left-indices right-indices mkGame Wsup`` -1
   THEN Folds ``left-indices right-indices`` (-1)) }

1
1. G1 : Game
2. ∀m:Game. ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀G2:Game. (m ≡ G2 ⇒ -(m) ≡ -(G2))))
3. G2 : Game
4. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ G1 ≡ m ⇒ -(G1) ≡ -(m))
5. G1 ≡ G2
6. i : right-indices(G1)
⊢ ∃j:left-indices(-(G2)). left-move(-(G1);i) ≡ left-move(-(G2);j)

2
1. G1 : Game
2. ∀m:Game. ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀G2:Game. (m ≡ G2 ⇒ -(m) ≡ -(G2))))
3. G2 : Game
4. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ G1 ≡ m ⇒ -(G1) ≡ -(m))
5. G1 ≡ G2
6. ∀i:left-indices(-(G1)). ∃j:left-indices(-(G2)). left-move(-(G1);i) ≡ left-move(-(G2);j)
7. i : left-indices(G1)
⊢ ∃j:right-indices(-(G2)). right-move(-(G1);i) ≡ right-move(-(G2);j)

3
1. G1 : Game
2. ∀m:Game. ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀G2:Game. (m ≡ G2 ⇒ -(m) ≡ -(G2))))
3. G2 : Game
4. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ G1 ≡ m ⇒ -(G1) ≡ -(m))
5. G1 ≡ G2
6. i : right-indices(G2)
⊢ ∃j:left-indices(-(G1)). left-move(-(G2);i) ≡ left-move(-(G1);j)

4
1. G1 : Game
2. ∀m:Game. ((left-option{i:l}(G1;m) ∨ right-option{i:l}(G1;m)) ⇒ (∀G2:Game. (m ≡ G2 ⇒ -(m) ≡ -(G2))))
3. G2 : Game
4. ∀m:Game. ((left-option{i:l}(G2;m) ∨ right-option{i:l}(G2;m)) ⇒ G1 ≡ m ⇒ -(G1) ≡ -(m))
5. G1 ≡ G2
6. ∀i:left-indices(-(G2)). ∃j:left-indices(-(G1)). left-move(-(G2);i) ≡ left-move(-(G1);j)
7. i : left-indices(G2)
⊢ ∃j:right-indices(-(G1)). right-move(-(G2);i) ≡ right-move(-(G1);j)

---

Latex:

---

Latex:
\mforall{}G1,G2:Game.    (G1  \mequiv{}  G2  {}\mRightarrow{}  -(G1)  \mequiv{}  -(G2))


By

---

Latex:
(RepeatFor  2  (((BLemma  `Game-induction`  THENA  Auto)  THEN  RepeatFor  2  ((D  0  THENA  Auto))))
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `Game-minus`  -1
  THEN  RepUR  ``left-indices  right-indices  mkGame  Wsup``  -1
  THEN  Folds  ``left-indices  right-indices``  (-1))

---

Home Index