Nuprl Definition : Sudoku
Sudoku() ==
{s:square-board(9;{1..10-})|
(∀i,j,k:ℕ9. ((sudoku-cell(s;i;j) = sudoku-cell(s;i;k) ∈ ℤ) ⇒ (j = k ∈ ℤ)))
∧ (∀i,j,k:ℕ9. ((sudoku-cell(s;i;k) = sudoku-cell(s;j;k) ∈ ℤ) ⇒ (j = k ∈ ℤ)))
∧ (∀i,j,k,l:ℕ9.
((sudoku-cell(s;i;k) = sudoku-cell(s;j;l) ∈ ℤ)
⇒ ((i ÷ 3) = (j ÷ 3) ∈ ℤ)
⇒ ((k ÷ 3) = (l ÷ 3) ∈ ℤ)
⇒ ((i = j ∈ ℤ) ∧ (k = l ∈ ℤ))))}
Definitions occuring in Statement :
sudoku-cell: sudoku-cell(s;i;j),
square-board: square-board(n;T),
int_seg: {i..j-},
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
divide: n ÷ m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
square-board: square-board(n;T),
all: ∀x:A. B[x],
int_seg: {i..j-},
sudoku-cell: sudoku-cell(s;i;j),
implies: P ⇒ Q,
divide: n ÷ m,
natural_number: $n,
and: P ∧ Q,
equal: s = t ∈ T,
int: ℤ
FDL editor aliases :
Sudoku
Latex:
Sudoku() ==
\{s:square-board(9;\{1..10\msupminus{}\})|
(\mforall{}i,j,k:\mBbbN{}9. ((sudoku-cell(s;i;j) = sudoku-cell(s;i;k)) {}\mRightarrow{} (j = k)))
\mwedge{} (\mforall{}i,j,k:\mBbbN{}9. ((sudoku-cell(s;i;k) = sudoku-cell(s;j;k)) {}\mRightarrow{} (j = k)))
\mwedge{} (\mforall{}i,j,k,l:\mBbbN{}9.
((sudoku-cell(s;i;k) = sudoku-cell(s;j;l))
{}\mRightarrow{} ((i \mdiv{} 3) = (j \mdiv{} 3))
{}\mRightarrow{} ((k \mdiv{} 3) = (l \mdiv{} 3))
{}\mRightarrow{} ((i = j) \mwedge{} (k = l))))\}
Date html generated:
2016_05_15-PM-03_14_05
Last ObjectModification:
2015_09_23-AM-07_42_47
Theory : general
Home
Index