A program's run at the register channel

DescriptiveComplexity.Draw.Prog.wideAccept_prog turns a program's run into a yes-instance of DescriptiveComplexity.WideAccept, whose channel writes for every element. This file is the same statement at the register channel, where a program writes for the elements it marks and the file it is handed has one register per such element.

The marking is what a program says about its own channel: Prog.marked is a field, fun _ => True by default, and the two ends of a run read it. At the segment channel the program marks everything and the file is the ruler; at the register channel it marks its argument elements and the file lies in the working region (DescriptiveComplexity.wideRank_wmRegSeg_lt).

noncomputable def DescriptiveComplexity.Draw.Prog.initBackReg {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] (PR : Prog A R P Q W K dd) : (Univ A R P K dd → Prop) → W → A

The background at time zero, at the register channel: the mark of the element whose cell it is, for the elements the program writes for, and the blank at every other address.

Equations

• PR.initBackReg r s = if h : ∃ (x : DescriptiveComplexity.Draw.Univ A R P K dd), PR.marked x ∧ r = DescriptiveComplexity.wmRegSeg x then PR.mark h.choose s else PR.blank s