---

Step * 1 of Lemma Sudoku-size_wf


1. P : SudokuPuzzle()
⊢ Σ(Σ(||sudoku-allowed(P;i;j)|| | j < 9) | i < 9) ∈ ℕ
BY
{ MemTypeCD }

1
1. P : SudokuPuzzle()
⊢ Σ(Σ(||sudoku-allowed(P;i;j)|| | j < 9) | i < 9) ∈ ℤ

2
.....set predicate..... 
1. P : SudokuPuzzle()
⊢ 0 ≤ Σ(Σ(||sudoku-allowed(P;i;j)|| | j < 9) | i < 9)

3
.....wf..... 
1. P : SudokuPuzzle()
2. i : ℤ
⊢ 0 ≤ i ∈ Type

---

Latex:

---

Latex:

1.  P  :  SudokuPuzzle()
\mvdash{}  \mSigma{}(\mSigma{}(||sudoku-allowed(P;i;j)||  |  j  <  9)  |  i  <  9)  \mmember{}  \mBbbN{}


By

---

Latex:
MemTypeCD

---

Home Index