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 l0, 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.