---

Step * of Lemma eq-Game_transitivity

∀G,H,K:Game.  (G ≡ H ⇒ H ≡ K ⇒ G ≡ K)
BY
{ (InstLemma `Game-induction` [⌜λ2G.∀H,K:Game.  (G ≡ H ⇒ H ≡ K ⇒ G ≡ K)⌝]⋅
   THEN Auto
   THEN skip{(RepeatFor 3 (ParallelOp -2) THEN ExRepD THEN D -4)}) }

1
1. g : Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ (∀H,K:Game.  (m ≡ H ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. g ≡ H
6. H ≡ K
⊢ g ≡ K

---

Latex:

---

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


By

---

Latex:
(InstLemma  `Game-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}G.\mforall{}H,K:Game.    (G  \mequiv{}  H  {}\mRightarrow{}  H  \mequiv{}  K  {}\mRightarrow{}  G  \mequiv{}  K)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  skip\{(RepeatFor  3  (ParallelOp  -2)  THEN  ExRepD  THEN  D  -4)\})

---

Home Index