---

Step * of Lemma Sudoku-size_wf

∀[P:SudokuPuzzle()]. (Sudoku-size(P) ∈ ℕ)
BY
{ ProveWfLemma }

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

---

Latex:

---

Latex:
\mforall{}[P:SudokuPuzzle()].  (Sudoku-size(P)  \mmember{}  \mBbbN{})


By

---

Latex:
ProveWfLemma

---

Home Index