Reading one named register bit

The leaves of the element loops read single bits of the machine's registers at computed cells: a ρ-atom of an expansion sentence is one bit of VAL or MIRROR at the cell whose name marks match a tuple held in the control, a tag read is the same at a canonical cell. The trip is always the same: turn off the working-cell marker, scan up to the first cell whose tracks satisfy the name guard – unique by DescriptiveComplexity.Draw.eq_of_slotMark_name-style facts – take one step left reading the walked digit into the phase, and scan back down to the marker.

DescriptiveComplexity.Draw.Prog.reaches_readBit_pos and _neg are the two outcomes. The read changes nothing on the tape, so the two theorems mention one tape; the caller cases on the bit.

theorem DescriptiveComplexity.Draw.Prog.reaches_writeBit {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {t wk : W} (hnewk : wk ≠ t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) {NameG : (W → A) → Prop} {x₀ : I} (hname : NameG (PR.passTracksAt F.cell t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), NameG (PR.passTracksAt F.cell t rest m r) → r = F.cell x₀) {pStart pUp : P} {fc : Q → A} (hturn : ∀ (g : W → A), g wk = PR.one → PR.HasRight pStart fc g pUp fc g) (hup : ∀ (g : W → A), ¬NameG g → PR.HasRight pUp fc g pUp fc g) {b : Prop} {pW : P} (hwr : PR.HasLeft pUp fc (PR.passTracksAt F.cell t rest m (F.cell x₀)) pW fc (Function.update (PR.passTracksAt F.cell t rest m (F.cell x₀)) t (bitVal PR.zero PR.one b))) (hbackW : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pW fc g pW fc g) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt pStart fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt pW fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell t rest fun (y : I) => y = x₀ ∧ b ∨ y ≠ x₀ ∧ m y) (PR.syElt PR.blank) }

Writing one named register bit, the budget forgotten.

theorem DescriptiveComplexity.Draw.Prog.reaches_readBit_pos {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} (F : IxFile (Univ A R P K dd) I ile) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {t wk : W} (hnewk : wk ≠ t) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {rest : (Univ A R P K dd → Prop) → W → A} {m : I → Prop} {v : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (F.cell gbot)) (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) {NameG : (W → A) → Prop} {x₀ : I} (hname : NameG (PR.passTracksAt F.cell t rest m (F.cell x₀))) (huniq : ∀ (r : Univ A R P K dd → Prop), NameG (PR.passTracksAt F.cell t rest m r) → r = F.cell x₀) {pStart pUp pRy : P} {fc : Q → A} (hturn : ∀ (g : W → A), g wk = PR.one → PR.HasRight pStart fc g pUp fc g) (hup : ∀ (g : W → A), ¬NameG g → PR.HasRight pUp fc g pUp fc g) (hrd1 : ∀ (g : W → A), NameG g → g t = PR.one → PR.HasLeft pUp fc g pRy fc g) (hbackY : ∀ (g : W → A), g wk ≠ PR.one → PR.HasLeft pRy fc g pRy fc g) (hm : m x₀) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt pStart fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt pRy fc), head := Sum.inl v, tape := wideTape (PR.trackTapeAt F.cell t rest m) (PR.syElt PR.blank) }

Reading a set bit: the trip ends at the marker in the positive phase.