---

Step * of Lemma Sudoku-induction

No Annotations
∀P:SudokuPuzzle() ⟶ ℙ
  ((∀p:SudokuPuzzle(). ((∀q:SudokuPuzzle(). P[q] supposing Sudoku-size(q) < Sudoku-size(p)) ⇒ P[p]))
  ⇒ (∀p:SudokuPuzzle(). P[p]))
BY
{ (Auto THEN RenameVar `F' (-2)) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}P:SudokuPuzzle()  {}\mrightarrow{}  \mBbbP{}
    ((\mforall{}p:SudokuPuzzle()
            ((\mforall{}q:SudokuPuzzle().  P[q]  supposing  Sudoku-size(q)  <  Sudoku-size(p))  {}\mRightarrow{}  P[p]))
    {}\mRightarrow{}  (\mforall{}p:SudokuPuzzle().  P[p]))


By

---

Latex:
(Auto  THEN  RenameVar  `F'  (-2))

---

Home Index