---

Step * 1 1 of Lemma Sudoku-induction


1. P : SudokuPuzzle() ⟶ ℙ
2. F : ∀p:SudokuPuzzle(). ((∀q:SudokuPuzzle(). P[q] supposing Sudoku-size(q) < Sudoku-size(p)) ⇒ P[p])
3. p : SudokuPuzzle()
⊢ fix((λG,p. (F p G))) p ∈ P[p]
BY
{ ((Assert ⌜∀n:ℕ. ∀p:SudokuPuzzle().  ((Sudoku-size(p) ≤ n) ⇒ (fix((λG,p. (F p G))) p ∈ P[p]))⌝⋅
   THENM (InstHyp [⌜Sudoku-size(p)⌝;⌜p⌝] (-1)⋅ THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto
   THEN UnrollLoopsOnce
   THEN Fold `member` 0
   THEN Auto
   THEN FunExt
   THEN Auto') }

---

Latex:

---

Latex:

1.  P  :  SudokuPuzzle()  {}\mrightarrow{}  \mBbbP{}
2.  F  :  \mforall{}p:SudokuPuzzle()
                  ((\mforall{}q:SudokuPuzzle().  P[q]  supposing  Sudoku-size(q)  <  Sudoku-size(p))  {}\mRightarrow{}  P[p])
3.  p  :  SudokuPuzzle()
\mvdash{}  fix((\mlambda{}G,p.  (F  p  G)))  p  \mmember{}  P[p]


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}p:SudokuPuzzle().    ((Sudoku-size(p)  \mleq{}  n)  {}\mRightarrow{}  (fix((\mlambda{}G,p.  (F  p  G)))  p  \mmember{}  P[p]))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}Sudoku-size(p)\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto
  THEN  UnrollLoopsOnce
  THEN  Fold  `member`  0
  THEN  Auto
  THEN  FunExt
  THEN  Auto')

---

Home Index