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