---

Step * of Lemma sudoku-allowed_wf

∀[P:SudokuPuzzle()]. ∀[i,j:ℕ9].  (sudoku-allowed(P;i;j) ∈ {1..10-} List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[P:SudokuPuzzle()].  \mforall{}[i,j:\mBbbN{}9].    (sudoku-allowed(P;i;j)  \mmember{}  \{1..10\msupminus{}\}  List)


By

---

Latex:
ProveWfLemma

---

Home Index