---

Step * 1 2 of Lemma Sudoku-size_wf

.....set predicate..... 
1. P : SudokuPuzzle()
⊢ 0 ≤ Σ(Σ(||sudoku-allowed(P;i;j)|| | j < 9) | i < 9)
BY
{ RepeatFor 2 ((BLemma `non_neg_sum` THEN Auto)) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  P  :  SudokuPuzzle()
\mvdash{}  0  \mleq{}  \mSigma{}(\mSigma{}(||sudoku-allowed(P;i;j)||  |  j  <  9)  |  i  <  9)


By

---

Latex:
RepeatFor  2  ((BLemma  `non\_neg\_sum`  THEN  Auto))

---

Home Index