Step
*
of Lemma
SudokuSolution_wf
∀[s:Sudoku()]. ∀[P:SudokuPuzzle()].  (SudokuSolution(s;P) ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[s:Sudoku()].  \mforall{}[P:SudokuPuzzle()].    (SudokuSolution(s;P)  \mmember{}  \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index