Nuprl Definition : SudokuSolution
SudokuSolution(s;P) == ∀i,j:ℕ9. (sudoku-cell(s;i;j) ∈ sudoku-allowed(P;i;j))
Definitions occuring in Statement :
sudoku-allowed: sudoku-allowed(P;i;j),
sudoku-cell: sudoku-cell(s;i;j),
l_member: (x ∈ l),
int_seg: {i..j-},
all: ∀x:A. B[x],
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
l_member: (x ∈ l),
sudoku-cell: sudoku-cell(s;i;j),
sudoku-allowed: sudoku-allowed(P;i;j),
int_seg: {i..j-},
natural_number: $n
FDL editor aliases :
SudokuSolution
Latex:
SudokuSolution(s;P) == \mforall{}i,j:\mBbbN{}9. (sudoku-cell(s;i;j) \mmember{} sudoku-allowed(P;i;j))
Date html generated:
2016_05_15-PM-03_14_16
Last ObjectModification:
2015_09_23-AM-07_42_48
Theory : general
Home
Index