Game0 is a simplification of the first game of *Lemmings Jr*. There is
only one lemming.

We give a sequence of formulas narrating the journey of a lemming from the lemming source to the lemming sink. It applies to the journey of the lemming chosen to dig even when other lemmings are present. For each formula we say where we expect it to come from.

As is conventional in situation calculus formalizations, is the
initial situation. The formula states that the lemming source will
open. This is inferred from a general fact about the start of lemming
games. Some lemming games have more than one source. However,
we may take it as an observation of the screen that there is
one lemming source in this game.

Let . We now have

This follows from (8).
It is a general fact about *Lemmings* that a lemming will fall out if
not all have fallen out. Calling one of them is allowable, but
we'll do this more precisely in a later version of these formulas.

Let

This is the next situation in which
is falling.

A simple chamber will be rectangular on the screen with walls at both
ends. We make a simple chamber in and can rely on persistence
to keep it a simple chamber in and beyond. This would be used in
planning to solve Game0. Alternatively, if we are actually playing Game0,
we can observe that is a simple chamber in . This requires
a mechanism for associating names with features of the picture and with
situations depicted on the screen.

Next we want

Let .

This is the point on immediately below the source. I suppose we should assert (and later infer) it exists before we name it.

Now we can have

We are now ready for

and consequently

with

Now that is down on the floor of , it will walk around
until the player turns it into a digger. The details of that,
while part of the ``biography'' of *l*0, do not
come into postulating

because this refers to an action of the player in designating
to be a digger. From it we get

The fact that is still in does come into inferring from

that

Now we need more geography, including the lower chamber . We need to say that is a simple chamber modified by putting the lemming sink at its right end. We also must say that every point of the floor of is above the ceiling of .

I am not satisfied with the suggestions given above for describing chamber types as modifications of basic types, so we will omit this for now. On the other hand, it is straightforward to say that the floor of is above the ceiling of . We have

and from it we get

and

We have used .

Similarly we want to infer that will fall to a point on , giving

Now we have two cases according to whether or . In either case we can show

.

I used instead of just , because we might want to quantify over . However, we haven't used this in the formulas given so far.

There are many more non-trivial matters that require careful consideration.

Mon Mar 2 16:21:50 PDT 1998