---

Step * of Lemma eq-Game_weakening

∀G,H:Game.  ((G = H ∈ Game) ⇒ G ≡ H)
BY
{ (InstLemma `Game-induction` [⌜λ2G.∀H:Game. ((G = H ∈ Game) ⇒ G ≡ H)⌝]⋅
   THEN Auto
   THEN (D 0 THEN Auto)
   THEN D 0 With ⌜i⌝ 
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto
   THEN RepUR ``left-option right-option`` 0
   THEN Auto) }

1
1. g : Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ (∀H:Game. ((m = H ∈ Game) ⇒ m ≡ H)))
3. H : Game
4. g = H ∈ Game
5. i : left-indices(H)
⊢ (∃x:left-indices(g). (left-move(H;i) = left-move(g;x) ∈ Game))
∨ (∃x:right-indices(g). (left-move(H;i) = right-move(g;x) ∈ Game))

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

---

Latex:

---

Latex:
\mforall{}G,H:Game.    ((G  =  H)  {}\mRightarrow{}  G  \mequiv{}  H)


By

---

Latex:
(InstLemma  `Game-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}G.\mforall{}H:Game.  ((G  =  H)  {}\mRightarrow{}  G  \mequiv{}  H)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (D  0  THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{} 
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  RepUR  ``left-option  right-option``  0
  THEN  Auto)

---

Home Index