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