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 THEN Auto)
   THEN With ⌜i⌝ 
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto
   THEN RepUR ``left-option right-option`` 0
   THEN Auto) }

1
1. Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m))  (∀H:Game. ((m H ∈ Game)  m ≡ H)))
3. Game
4. H ∈ Game
5. 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. Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m))  (∀H:Game. ((m H ∈ Game)  m ≡ H)))
3. Game
4. H ∈ Game
5. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
6. 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