---

Step * of Lemma sudoku-cell_wf

∀[s:square-board(9;{1..10-})]. ∀[i,j:ℕ9].  (sudoku-cell(s;i;j) ∈ {1..10-})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[s:square-board(9;\{1..10\msupminus{}\})].  \mforall{}[i,j:\mBbbN{}9].    (sudoku-cell(s;i;j)  \mmember{}  \{1..10\msupminus{}\})


By

---

Latex:
ProveWfLemma

---

Home Index