---

Step * 1 1 of Lemma Sudoku-size_wf


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

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index