The opening's walk at the register channel #
The opening of a handed program leaves the marker, walks up to the file, steps
onto its first register, turns, comes home, guesses, and enters the evaluation.
What it asks of the instance is four addresses and five order facts
(DescriptiveComplexity.Draw.Data.reachesIn_openingHanded), and at this
channel they are all forced:
- the marker is the empty address, and the walk's first step is its increment;
- the file's first register is the singleton of the element the reduction
marks below the argument tags (
DescriptiveComplexity.wmRegSeg_least), so the address the walk stops on is that singleton's predecessor; - the walk reaches it as long as the singleton is not itself the second address – which it is not, there being an argument element above the marked one.
So the whole geometry follows from the marking, and this file derives it.