Nuprl Lemma : sudoku-cell_wf

[s:square-board(9;{1..10-})]. ∀[i,j:ℕ9].  (sudoku-cell(s;i;j) ∈ {1..10-})


Proof




Definitions occuring in Statement :  sudoku-cell: sudoku-cell(s;i;j) square-board: square-board(n;T) int_seg: {i..j-} uall: [x:A]. B[x] member: t ∈ T natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T sudoku-cell: sudoku-cell(s;i;j) nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop:
Lemmas referenced :  board-cell_wf int_seg_wf false_wf le_wf square-board_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesis dependent_set_memberEquality independent_pairFormation lambdaFormation hypothesisEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[s:square-board(9;\{1..10\msupminus{}\})].  \mforall{}[i,j:\mBbbN{}9].    (sudoku-cell(s;i;j)  \mmember{}  \{1..10\msupminus{}\})



Date html generated: 2016_05_15-PM-03_14_04
Last ObjectModification: 2015_12_27-PM-01_02_07

Theory : general


Home Index