Step
*
1
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 : ℕ
7. (2 * i) + 1 < 1
⊢ ↓Legal1(seq-cons(x;seq-nil())[2 * i];seq-cons(x;seq-nil())[(2 * i) + 1])
BY
{ ((Assert 0 ≤ (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. i : \mBbbN{}
7. (2 * i) + 1 < 1
\mvdash{} \mdownarrow{}Legal1(seq-cons(x;seq-nil())[2 * i];seq-cons(x;seq-nil())[(2 * i) + 1])
By
Latex:
((Assert 0 \mleq{} (2 * i) BY Auto) THEN Auto)
Home
Index