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.

theorem DescriptiveComplexity.Draw.Data.exists_openingWalkReg {L : FirstOrder.Language} {dt : Data L} {A R' P' : Type} [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] [Finite A] [Finite R'] [Finite P'] [Finite dt.KIx] (h : IsLinOrd WMLe) {botE : Univ A R' P' dt.KIx dt.dd} (hbotm : WMHasInp botE) (hleast : ∀ (y : Univ A R' P' dt.KIx dt.dd), WMHasInp y → WMLe botE y) (habove : ∃ (z : Univ A R' P' dt.KIx dt.dd), WMLt WMLe botE z) : ∃ (v₁ : Univ A R' P' dt.KIx dt.dd → Prop) (x : Univ A R' P' dt.KIx dt.dd → Prop) (y' : Univ A R' P' dt.KIx dt.dd → Prop), WMIncr WMLe (fun (x : Univ A R' P' dt.KIx dt.dd) => False) v₁ ∧ WMSetLe WMLe v₁ x ∧ WMIncr WMLe x (wmRegSeg botE) ∧ WMIncr WMLe (wmRegSeg botE) y' ∧ WMSetLe WMLe (fun (x : Univ A R' P' dt.KIx dt.dd) => False) (wmRegSeg botE)

The opening's walk exists: the marker's increment, the address the walk stops on, the file's first register and its own increment, with the five order facts the opening asks of them.

The one thing the instance has to bring is an element above the one the channel marks below the argument tags – any argument element will do – which is what makes the file's first register more than one step above the marker.