```{

Another puzzle as described in Clifford A. Pickover's book
"Keys to Infinity" :

The following is a problem posted at the 2nd World Puzzle Championship in Brno,
Czech Republic. The logical labyrinth (below) was just one of many puzzles the

1, 2, 7,16, 5,19, 7, 8
10,17,23, 9,21,13, 6,23
15, 4,22,17,20, 4,18,22
19,17,11,24, 3,17, 8,19
12, 9, 7,14,23,18,12, 6
6, 5,23,14,10, 5, 2,23
8,20,10,11,19,18, 1,17
2,24,15,22,13, 4, 4,25

The goal is to find a path from the 1 (upper left) to the 25 (lower right)
such that the path contains exactly 25 squares. The allowable moves are up,
down, left and right, and the path may not repeat any numbers.

To obtain the solution, run the query

all Labyrinth()

}

local Map :< [0..7]->[0..7]->I =

[[ 1, 2, 7,16, 5,19, 7, 8],
[10,17,23, 9,21,13, 6,23],
[15, 4,22,17,20, 4,18,22],
[19,17,11,24, 3,17, 8,19],
[12, 9, 7,14,23,18,12, 6],
[ 6, 5,23,14,10, 5, 2,23],
[ 8,20,10,11,19,18, 1,17],
[ 2,24,15,22,13, 4, 4,25]]

local Board = [0..24]->I

pred Labyrinth() iff
pos:.Board &

//Initialize the array to keep the track of visited numbers, we start at number 1
pos := [1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0] &

//Current position is at (0,0), calculate the rest of the steps starting at step 1
Labyrinth1(pos,0,0,1) &

// Print the resulting array
Print(pos)

local pred Labyrinth1(pos:.Board,row:<I,col:<I,step:<I)  iff
if step < 25 then
Move(row,col,newrow,newcol) &

// Validate the number at the position is not visited yet:

~Map(newrow,newcol) in pos &

// Put the number into our array of visited numbers

pos(step) := Map(newrow,newcol) &

// Continue with the next move

Labyrinth1(pos,newrow,newcol,step+1)
end

local pred Move(row:<I,col:<I,newrow:>I,newcol:>I) iff

//  Given a position row,col (marked 'x'), we can
//  move to four different places:
//
//  +---+---+---+---+
//  |   |   |   |   |
//  +---+---+---+---+
//  |   | 1 |   |   |
//  +---+---+---+---+
//  | 4 | x | 2 |   |
//  +---+---+---+---+
//  |   | 3 |   |   |
//  +---+---+---+---+
//  |   |   |   |   |
//  +---+---+---+---+

newcol =  col     & newrow = row - 1 | // 1
newcol =  col + 1 & newrow = row     | // 2
newcol =  col     & newrow = row + 1 | // 3
newcol =  col - 1 & newrow = row       // 4

```