---

Step * 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()
⊢ P[p]
BY
{ UseWitness ⌜fix((λG,p. (F p G))) p⌝⋅ }

1
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]

---

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{}  P[p]


By

---

Latex:
UseWitness  \mkleeneopen{}fix((\mlambda{}G,p.  (F  p  G)))  p\mkleeneclose{}\mcdot{}

---

Home Index