# The Mysterious Lock of Monte Carlo

## Chapters 8 and 13 from [The Lady or the Tiger]

Here is a [calculational solution] to this problem. This puzzle was also published as Weekly Puzzle 32: The Lock on The Weekly Puzzles. In this solution I will use that version.

## Representation

We use the following abbreviations for statements about combinations:
```  O.x == "x opens the lock"
N.x == "x is neutral"
J.x == "x jams the lock"
```
x and y represent combinations; a combination is a non-empty digit sequence. p and q represent (possibly empty) digit sequences. We also introduce the following notations for sequences:
```  p = q == "p and q contain the same digits in the same order"
<p> = "the sequence that is the reverse of p"
```
So for example <1233> = 3321.

The crucial notation that we introduce is:

```  [x] = "the combination to which x is related"
```
In terms of the machines in Chapters 9 through 13 in [The Lady or the Tiger], [x] is the output of the machine for input x.

## Solution

Using these notations we can represent the five properties as follows:
``` (A)  [2x2] = x
(B)  [1x] = 2[x]
(C)  [5x] = <[x]>
(D)  [9x] = [x][x]
(E1) N.x => J.[x]
(E2) J.x => N.[x]
```
We are also given that
``` (Z)  exactly one of O.x, N.x, and J.x is true
```
One consequence of this (see my discussion of [Trilemmas]) is:
``` (Z1) O.x == N.x == J.x
```
All these properties hold for all combinations x.

The problem is now to find the shortest x for which O.x.

### Step 1

For any combination x:
```   O.x
==   "(Z1)"
N.x == J.x
==   "logic, working towards (E1) and (E2)"
(N.x => J.x) /\ (J.x => N.x)
<=   "(E1); (E2)"
[x] = x
```
So any combination that is related to itself will open the lock.

### Intermezzo: operations

Properties (A)-(D) allow us to simplify values of form [...]. But it is easy to see that they only work for values of the form [m2x2], where x is an arbitrary combination, and m is a (possibly empty) sequence of 1s, 5s, and 9s. For reasons that will become clear in a moment, we call each of those digits an 'operation digit'; n stands for an arbitrary operation digit. m is an 'operation sequence', i.e., a (possibly empty) sequence of operation digits.

Because expressions of the form [m2x2] occur often, we introduce a special notation:

```  m.x = [m2x2]
```
We use a function-application notation here, with a reason. Let's compute 1.x:
```   1.x
=    "definition of ."
[12x2]
=    "(B)"
2[2x2]
=    "(A)"
2x
```
When we do this also for 5 and 9, we get
``` (B') 1.x = 2x
(C') 5.x = <x>
(D') 9.x = xx
```
So we see that these digits are operations: 1 prepends a 2, 5 reverses, and 9 duplicates a digit sequence.

We can also combine operations:

``` (*)  n.(m.x) = nm.x
```
We prove this only for n=1; the other proofs are similar.
```   1.(m.x)
=    "(B')"
2(m.x)
=    "definition of ."
2[m2x2]
=    "(B) from right to left"
[1m2x2]
=    "definition of ."
1m.x
```
To give a simple example, it is easy to compute that
```   51.78
=    "(*) from right to left"
5.(1.78)
=    "(B')"
5.278
=    "(C')"
872
```
In the next step we will perform a similar situation, but then from bottom to top.

### Step 2

Armed with the knowledge about operations, we continue our quest for a self-related combination.
```   [x] = x
<=   "write x as m2y2"
(Em,y| x = m2y2: [m2y2] = m2y2)
```
Now we would like to write m2y2 as an operation on m and y. Since we know that we have a duplication operation, it seems that m2m2 is easier to rewrite. Therefore we calculate:
```   m2m2
=    "(D') from right to left"
9.m2
=    "definition of <...>, to put the 2 up front"
9.<2<m>>
=    "(C') from right to left"
9.(5.2<m>)
=    "(B') from right to left"
9.(5.(1.<m>))
=    "(C') from right to left"
9.(5.(1.(5.m)))
=    "(*), three times"
9515.m
=    "definition of ."
[95152m2]
```
With this we can continue our earlier calculation:
```   (Em,y| x = m2y2: [m2y2] = m2y2)
<=   "take y:=m"
(Em| x = m2m2: [m2m2] = m2m2)
==   "proof above"
(Em| x = m2m2: [m2m2] = [95152m2])
<=   "Leibniz' rule"
(Em| x = m2m2: m2m2 = 95152m2)
==   "remove 2m2 at the end"
(Em| x = m2m2: m = 9515)
==   "one-point rule"
x = 9515295152
```
Summarizing the complete calculation, we proved
```  (Ax| x = 9515295152: O.x)
```
or equivalently O.9515295152. And this is a combination that opens the lock. I also believe this to be the shortest one, but have not been able to prove that.

## Post Scriptum

It was only after I wrote the above, and contacted Tim Edmonds of The Weekly Puzzles about this solution, that I saw his. It turned out that there is a shorter combination; here is a calculational explanation.

Because of (Z) we know that a combination opens the lock iff it is not neutral and also doesn't jam it. In other words,

``` (Z2) O.x == !J.x /\ !N.x
```
(This is another consequence of (Z): see [Trilemmas].) This allows us to prove a statement of the form O.x as follows:
```   O.x
==   "(Z2)"
!J.x /\ !N.x
<=   "(E1) and (E2) from right to left"
!N.[x] /\ !J.[x]
==   "(Z2) from right to left"
O.[x]
```
Applying this to the combination that we already found, and abbreviating m = 9515, we get
```   O.m2m2                            --- already proved above
==   "(D') from right to left"
O.(9.m2)
==   "definition of ."
O.[92m22]
=>   "the property we've just proven"
O.92m22
```
So 92951522 is also a working combination, and it is shorter that the one I (and Smullyan) found. Again, I cannot prove that it is the shortest.
This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page.
```Changes to calc/tlott-8-and-13.html:

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
* Move from CVS to darcs: do not show the CVS date anymore.

Thu Feb  7 19:43:35 MET 2002  marnix
* Updated all files to use the m4 template

Wed Sep  5 21:20:00 MEST 2001  marnix
* Made explicit that last changed date is in GMT

Wed Sep  5 21:08:51 MEST 2001  marnix
* Now 'last changed' is on its own line

Wed Sep  5 10:10:47 MEST 2001  marnix
* Added date last changed

Wed Sep  5 08:50:24 MEST 2001  marnix
* Initial revision
```