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.