Step
*
1
3
of Lemma
Sudoku-size_wf
.....wf..... 
1. P : SudokuPuzzle()
2. i : ℤ
⊢ 0 ≤ i ∈ Type
BY
{ Auto }
Latex:
Latex:
.....wf..... 
1.  P  :  SudokuPuzzle()
2.  i  :  \mBbbZ{}
\mvdash{}  0  \mleq{}  i  \mmember{}  Type
By
Latex:
Auto
Home
Index