Starting a run at the register channel

The two machines an instance describes – DescriptiveComplexity.wideData and DescriptiveComplexity.wideRegData – differ in one field, the channel, and it is read nowhere but in the initial tape: a step reads the transitions, the order and the positions and nothing else. So every run lemma of the library transfers by definition (wideRegData_step, wideRegData_reachesIn), and what has to be redone is the pair of statements at the two ends of a run.

They are the segment channel's own with two changes: the cell of x is wmRegSeg x, and only the elements that carry input have one. Where the segment channel says “every cell holds its element's symbol, every other address is blank”, the register channel says the same of the elements it writes for, and an address that is nobody's cell is blank as before.

theorem DescriptiveComplexity.wideRegData_step {A : Type} [FirstOrder.Language.wide.Structure A] (c c' : Config (WPoint A)) : (wideRegData A).Step c c' ↔ (wideData A).Step c c'

The two machines take the same steps: a step reads the transitions, the order and the positions, and the channel is none of those.

theorem DescriptiveComplexity.wideRegData_reachesIn {A : Type} [FirstOrder.Language.wide.Structure A] (n : ℕ) (c c' : Config (WPoint A)) : (wideRegData A).ReachesIn n c c' ↔ (wideData A).ReachesIn n c c'

And the same bounded runs.