eleven wrote:RedEd, please can you formulate another trivial proof to make Denis a believer this time also ?

OK.

Definition: an a/b/b/a pattern in a solution grid is anything isomorphic to that shown below:

- Code: Select all
` . . . | . `

a . . | b

b . . | a

---------+---

. . . | .

Fact: if a solution grid (

not necessarily unique) contains an

a/b/b/a pattern on four unclued cells, C, then C=b/a/a/b is also a solution.

Theorem: if a puzzle-in-progress (

that does not necessarily have a unique solution) has pencilmarks as shown below

on four unclued cells then the bottom right value resolves to '3':

- Code: Select all
` . . . | . `

1 . . | 2

2 . . | 13

---------+---

. . . | .

Proof: suppose to the contrary the bottom right value resolves to '1'. Then (vacuously) the solution grid contains the

1/2/2/1 pattern on four unclued cells, C. So, by the Fact above, C=2/1/1/2 is also a solution. But wait! - the pencilmarks do not allow that other solution - contradiction.