---

Step * 3 of Lemma Game-minus_functionality


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)
BY
{ ((Assert ∃j:right-indices(G1). right-move(G2;i) ≡ right-move(G1;j) BY (D -2 THEN Auto)) THEN D -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(G2)
7. j : right-indices(G1)
8. right-move(G2;i) ≡ right-move(G1;j)
⊢ ∃j:left-indices(-(G1)). left-move(-(G2);i) ≡ left-move(-(G1);j)

---

Latex:

---

Latex:

1.  G1  :  Game
2.  \mforall{}m:Game
          ((left-option\{i:l\}(G1;m)  \mvee{}  right-option\{i:l\}(G1;m))  {}\mRightarrow{}  (\mforall{}G2:Game.  (m  \mequiv{}  G2  {}\mRightarrow{}  -(m)  \mequiv{}  -(G2))))
3.  G2  :  Game
4.  \mforall{}m:Game.  ((left-option\{i:l\}(G2;m)  \mvee{}  right-option\{i:l\}(G2;m))  {}\mRightarrow{}  G1  \mequiv{}  m  {}\mRightarrow{}  -(G1)  \mequiv{}  -(m))
5.  G1  \mequiv{}  G2
6.  i  :  right-indices(G2)
\mvdash{}  \mexists{}j:left-indices(-(G1)).  left-move(-(G2);i)  \mequiv{}  left-move(-(G1);j)


By

---

Latex:
((Assert  \mexists{}j:right-indices(G1).  right-move(G2;i)  \mequiv{}  right-move(G1;j)  BY  (D  -2  THEN  Auto))  THEN  D  -1)

---

Home Index