---

Step * 2 of Lemma sg-reachable_self


1. g : SimpleGame
2. x : Pos(g)
3. 0 < 1
4. seq-cons(x;seq-nil())[0] = x ∈ Pos(g)
5. seq-cons(x;seq-nil())[1 - 1] = x ∈ Pos(g)
6. ∀i:ℕ. ((2 * i) + 1 < 1 ⇒ (↓Legal1(seq-cons(x;seq-nil())[2 * i];seq-cons(x;seq-nil())[(2 * i) + 1])))
7. i : ℕ+
8. 2 * i < 1
⊢ ↓Legal2(seq-cons(x;seq-nil())[(2 * i) - 1];seq-cons(x;seq-nil())[2 * i])
BY
{ ((Assert 2 ≤ (2 * i) BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  SimpleGame
2.  x  :  Pos(g)
3.  0  <  1
4.  seq-cons(x;seq-nil())[0]  =  x
5.  seq-cons(x;seq-nil())[1  -  1]  =  x
6.  \mforall{}i:\mBbbN{}
          ((2  *  i)  +  1  <  1  {}\mRightarrow{}  (\mdownarrow{}Legal1(seq-cons(x;seq-nil())[2  *  i];seq-cons(x;seq-nil())[(2  *  i)  +  1])))
7.  i  :  \mBbbN{}\msupplus{}
8.  2  *  i  <  1
\mvdash{}  \mdownarrow{}Legal2(seq-cons(x;seq-nil())[(2  *  i)  -  1];seq-cons(x;seq-nil())[2  *  i])


By

---

Latex:
((Assert  2  \mleq{}  (2  *  i)  BY  Auto)  THEN  Auto)

---

Home Index