The comparison atoms, instantiated

The first semantic instantiation: the element loop's run at the comparison pack DescriptiveComplexity.Draw.Data.cmpArgs. The enumeration is the lexicographic order on the narrow tuples, the generated family of DescriptiveComplexity.Draw.elemFam carries the loop element and the three bookkeeping flags, and the two inductions this file contributes are the loop's two invariants:

• the loop element is the round's tuple (DescriptiveComplexity.Draw.Data.readLv_cmpFam), so the name guards stop at the padded cell of the enumerated tuple and the read bits are the two block values' membership bits there;
• the flags fold the strict prefix (DescriptiveComplexity.Draw.Data.cmpFlags_cmpFam): agreement so far, a difference seen, and the first difference's verdict, over the tuples strictly below the round's.

DescriptiveComplexity.Draw.Data.cmp_run is the machine run; the final control's verdict bit is characterized against the two tracks' padded bits (DescriptiveComplexity.Draw.Data.ctlBit_avC_cmp_exit), which is the form DescriptiveComplexity.Problems.Wide.DrawCmp turns into the equality and order atoms.

The register a level reads, and its backing

noncomputable def DescriptiveComplexity.Draw.Data.lvSet {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (st : TapeSt dt A R P I) (v : dt.VarIx) (j : Fin (dt.nOf v)) : I → Prop

The register set a level's track holds: the working address for a free level, the VAL register for a quantified one – the contents behind DescriptiveComplexity.Draw.Data.lvTrack.

Equations

• dt.lvSet st v j = if ↑j < dt.arOf v then st.mir else st.val

theorem DescriptiveComplexity.Draw.Data.back_lvTrack {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (RF : LaidFile dt A R P I) (zero one : A) (st : TapeSt dt A R P I) (v : dt.VarIx) (j : Fin (dt.nOf v)) (r : Univ A R P dt.KIx dt.dd → Prop) : dt.ixBack RF.toLayout zero one ⋯ st r (dt.lvTrack v j) = bitVal zero one (bitAtOf RF.cell (dt.lvSet st v j) r)

A level's track is backed by its register set.

theorem DescriptiveComplexity.Draw.Data.back_lvTrackD {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] (F : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) (zero one : A) (st : TapeStD dt A R P) (v : dt.VarIx) (j : Fin (dt.nOf v)) (r : Univ A R P dt.KIx dt.dd → Prop) : dt.back F.cell zero one ⋯ st r (dt.lvTrack v j) = bitVal zero one (bitAtOf F.cell (dt.lvSet st v j) r)

A level's track is backed by its register set, at the elementwise file: the same statement read at DescriptiveComplexity.Draw.Data.back, which is what a space-bounded program's files say.

theorem DescriptiveComplexity.Draw.Data.lvSet_congr {L : FirstOrder.Language} (dt : Data L) {A R P I : Type} (vi : dt.VarIx) {st st' : TapeSt dt A R P I} (hmir : st.mir = st'.mir) (hval : st.val = st'.val) (j : Fin (dt.nOf vi)) : dt.lvSet st vi j = dt.lvSet st' vi j

A level's register set depends on the mirror and VAL alone – which is what lets everything read through it be transported between states that share those two registers.

theorem DescriptiveComplexity.Draw.Data.wk_ne_lvTrack {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (j : Fin (dt.nOf v)) : Slot.wk ≠ dt.lvTrack v j

The marker slot is not a level's track.

theorem DescriptiveComplexity.Draw.Data.reg_ne_lvTrack {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (j : Fin (dt.nOf v)) : Slot.reg ≠ dt.lvTrack v j

The register mark is not a level's track.

The loop element through the comparison's operations

theorem DescriptiveComplexity.Draw.Data.readLv_cmpInit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (f : dt.CtlIx → A) : dt.readLv (dt.cmpInit zero one f) = dt.readLv f

The loop element rides along cmpInit.

theorem DescriptiveComplexity.Draw.Data.readLv_setCtl_cmpRdC {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hnf : 2 ≤ dt.nfDim) (k : Fin 2) (b : Prop) (f : dt.CtlIx → A) : dt.readLv (dt.setCtl zero one (dt.cmpRdC hnf k) b f) = dt.readLv f

The loop element rides along a read's store.

theorem DescriptiveComplexity.Draw.Data.readLv_advLvN {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f : dt.CtlIx → A) : dt.readLv (dt.advLvN f) = tupNext (dt.readLv f)

The loop element after an advance is the next tuple.

The comparison's generated family

noncomputable def DescriptiveComplexity.Draw.Data.cmpSet {L : FirstOrder.Language} {dt : Data L} {A R P I : Type} (vi : dt.VarIx) (j₁ j₂ : Fin (dt.nOf vi)) (st : TapeSt dt A R P I) : Fin 2 → I → Prop

The two register sets a comparison reads: the level's register per paired read.

Equations

• DescriptiveComplexity.Draw.Data.cmpSet vi j₁ j₂ st k = if k = 0 then dt.lvSet st vi j₁ else dt.lvSet st vi j₂

noncomputable def DescriptiveComplexity.Draw.Data.cmpCell {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (RF : LaidFile dt A R P I) (zero : A) (hhas : RF.toLayout.HasName zero) (vi : dt.VarIx) (j₁ j₂ : Fin (dt.nOf vi)) (b : Lex (Fin dt.dd0 → A)) (k : Fin 2) : I

The cell of a comparison's round: the padded cell of the round's tuple, in the read's block.

Equations

• DescriptiveComplexity.Draw.Data.cmpCell RF zero hhas vi j₁ j₂ b k = RF.toLayout.reg hhas (if k = 0 then dt.lvBlk vi j₁ else dt.lvBlk vi j₂) (ofLex b)

noncomputable def DescriptiveComplexity.Draw.Data.cmpFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] (zero one : A) (hhas : RF.toLayout.HasName zero) (vi : dt.VarIx) (av : Fin dt.natMax) (hnf : 2 ≤ dt.nfDim) (isEq : Bool) (j₁ j₂ : Fin (dt.nOf vi)) (st : TapeSt dt A R P I) (vAdr : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (b : Lex (Fin dt.dd0 → A)) (j : Fin 3) : dt.CtlIx → A

The comparison's generated family, at its pack.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.cmpFam_congr_scratch {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] {zero one : A} {hhas : RF.toLayout.HasName zero} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} {st : TapeSt dt A R P I} {vAdr : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeSt dt A R P I} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : I), vAdr = RF.cell u) (f₀ : dt.CtlIx → A) (b : Lex (Fin dt.dd0 → A)) (j : Fin 3) : cmpFam RF zero one hhas vi av hnf isEq j₁ j₂ st vAdr f₀ b j = cmpFam RF zero one hhas vi av hnf isEq j₁ j₂ st' vAdr f₀ b j

A comparison is blind to the two scratch registers: it reads the levels' register sets, which are the mirror and VAL (DescriptiveComplexity.Draw.Data.lvSet), and its background at the working cell alone.

theorem DescriptiveComplexity.Draw.Data.back_cmpSet {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} {st : TapeSt dt A R P I} (k : Fin 2) (r : Univ A R P dt.KIx dt.dd → Prop) : dt.ixBack RF.toLayout zero one ⋯ st r ((dt.cmpArgs zero one vi av hnf isEq j₁ j₂).rdTrack k) = bitVal zero one (bitAtOf RF.cell (cmpSet vi j₁ j₂ st k) r)

The read tracks are backed by the register sets.

theorem DescriptiveComplexity.Draw.Data.wk_ne_cmp_rdTrack {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} (k : Fin 2) : Slot.wk ≠ (dt.cmpArgs zero one vi av hnf isEq j₁ j₂).rdTrack k

The marker slot is no read track.

theorem DescriptiveComplexity.Draw.Data.reg_ne_cmp_rdTrack {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} (k : Fin 2) : Slot.reg ≠ (dt.cmpArgs zero one vi av hnf isEq j₁ j₂).rdTrack k

The register mark is no read track.

The loop element is the round's tuple

theorem DescriptiveComplexity.Draw.Data.readLv_cmp_setFlag {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} (k : Fin 2) (bb : Bool) (q : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.readLv ((dt.cmpArgs zero one vi av hnf isEq j₁ j₂).setFlag k bb q g) = dt.readLv q

The loop element rides along a stored read.

theorem DescriptiveComplexity.Draw.Data.readLv_cmp_init {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} (q : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.readLv ((dt.cmpArgs zero one vi av hnf isEq j₁ j₂).initEl q g) = botTup

The loop starts at the least tuple.

theorem DescriptiveComplexity.Draw.Data.readLv_cmp_adv {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} (q : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.readLv ((dt.cmpArgs zero one vi av hnf isEq j₁ j₂).advEl q g) = tupNext (dt.readLv q)

An advance steps the tuple.

theorem DescriptiveComplexity.Draw.Data.readLv_cmp_chain {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} (bit : Fin 2 → Prop) (base : dt.CtlIx → A) (g : dt.SlotIx → A) (n : ℕ) : dt.readLv (chainSt bit (fun (j' : Fin 2) (b : Bool) (q' : dt.CtlIx → A) => (dt.cmpArgs zero one vi av hnf isEq j₁ j₂).setFlag j' b q' g) base n) = dt.readLv base

The loop element rides along a whole round's reads.

theorem DescriptiveComplexity.Draw.Data.ofLex_eq_tupNext_of_covers {A : Type} [LinearOrder A] [Finite A] {D : ℕ} {w z : Lex (Fin D → A)} (hwz : w < z) (hnb : ∀ (c : Lex (Fin D → A)), ¬(w < c ∧ c < z)) : ofLex z = tupNext (ofLex w)

A cover in the lexicographic order steps to the next tuple.

theorem DescriptiveComplexity.Draw.Data.ofLex_eq_botTup_of_bot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {D : ℕ} {z : Lex (Fin D → A)} (hz : ∀ (b : Lex (Fin D → A)), z ≤ b) : ofLex z = botTup

The bottom of the lexicographic order is the least tuple.

theorem DescriptiveComplexity.Draw.Data.readLv_cmpFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] {zero one : A} {hhas : RF.toLayout.HasName zero} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} {st : TapeSt dt A R P I} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (f₀ : dt.CtlIx → A) (b : Lex (Fin dt.dd0 → A)) (j : Fin 3) : dt.readLv (cmpFam RF zero one hhas vi av hnf isEq j₁ j₂ st vAdr f₀ b j) = ofLex b

The loop element is the round's tuple, at every stage of the family.

The flags fold the strict prefix

def DescriptiveComplexity.Draw.Data.CmpAgr {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (RF : LaidFile dt A R P I) (zero : A) (hhas : RF.toLayout.HasName zero) (vi : dt.VarIx) (j₁ j₂ : Fin (dt.nOf vi)) (st : TapeSt dt A R P I) (b : Lex (Fin dt.dd0 → A)) : Prop

The two blocks agree at a tuple: the two reads' bits coincide.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.Draw.Data.CmpFst {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] {I : Type} (RF : LaidFile dt A R P I) (zero : A) (hhas : RF.toLayout.HasName zero) (vi : dt.VarIx) (j₁ j₂ : Fin (dt.nOf vi)) (st : TapeSt dt A R P I) (b : Lex (Fin dt.dd0 → A)) : Prop

The first difference is at this tuple, the second block holding it: everything below agrees, and here only the second block holds the cell.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.cmp_chain_apply_ne {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} {bit : Fin 2 → Prop} {base : dt.CtlIx → A} {g : dt.SlotIx → A} {q : dt.CtlIx} (hq : ∀ (k : Fin 2), q ≠ dt.cmpRdC hnf k) (n : ℕ) : chainSt bit (fun (j' : Fin 2) (b : Bool) (q' : dt.CtlIx → A) => (dt.cmpArgs zero one vi av hnf isEq j₁ j₂).setFlag j' b q' g) base n q = base q

A slot off the paired reads rides along the whole chain.

theorem DescriptiveComplexity.Draw.Data.ctlBit_chain_setCtl {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) {nr : ℕ} (slotOf : Fin nr → dt.CtlIx) (hinj : ∀ (j j' : Fin nr), slotOf j = slotOf j' → j = j') (bit : Fin nr → Prop) (base : dt.CtlIx → A) (n : ℕ) (j : Fin nr) : ↑j < n → (dt.ctlBit one (chainSt bit (fun (j' : Fin nr) (b : Bool) (q' : dt.CtlIx → A) => dt.setCtl zero one (slotOf j') (b = true) q') base n) (slotOf j) ↔ bit j)

A stored-read chain reads back, slot by slot: the chain writing each read into its own control slot delivers every bit already written.

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmp_chain_rd {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} (hzo : zero ≠ one) {bit : Fin 2 → Prop} {base : dt.CtlIx → A} {g : dt.SlotIx → A} (k : Fin 2) : dt.ctlBit one (chainSt bit (fun (j' : Fin 2) (b : Bool) (q' : dt.CtlIx → A) => (dt.cmpArgs zero one vi av hnf isEq j₁ j₂).setFlag j' b q' g) base 2) (dt.cmpRdC hnf k) ↔ bit k

The whole chain's stored reads: the two bits of the round.

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmp_advEl {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {zero one : A} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} {q : dt.CtlIx} (hq : ∀ (j : Fin dt.dd0), q ≠ dt.lvC j) (f : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.ctlBit one ((dt.cmpArgs zero one vi av hnf isEq j₁ j₂).advEl f g) q ↔ dt.ctlBit one (dt.cmpFold zero one hnf f) q

A control slot off the loop variables rides along an advance, showing the fold's value.

theorem DescriptiveComplexity.Draw.Data.cmpFlags_cmpFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] {zero one : A} {hhas : RF.toLayout.HasName zero} {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} {st : TapeSt dt A R P I} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (f₀ : dt.CtlIx → A) (b : Lex (Fin dt.dd0 → A)) : (dt.ctlBit one (cmpFam RF zero one hhas vi av hnf isEq j₁ j₂ st vAdr f₀ b 0) dt.cmpAccC ↔ ∀ u < b, CmpAgr RF zero hhas vi j₁ j₂ st u) ∧ (dt.ctlBit one (cmpFam RF zero one hhas vi av hnf isEq j₁ j₂ st vAdr f₀ b 0) dt.cmpDecC ↔ ∃ u < b, ¬CmpAgr RF zero hhas vi j₁ j₂ st u) ∧ (dt.ctlBit one (cmpFam RF zero one hhas vi av hnf isEq j₁ j₂ st vAdr f₀ b 0) dt.cmpValC ↔ ∃ u < b, CmpFst RF zero hhas vi j₁ j₂ st u)

The flags fold the strict prefix: at every round's entry, the three bookkeeping bits are agreement everywhere below, a difference seen below, and a first difference below with the second block holding it.

The greatest tuple

noncomputable def DescriptiveComplexity.Draw.Data.topTup {D : ℕ} {B : Type} [LinearOrder B] [Finite B] [Nonempty B] : Fin D → B

The last tuple: every coordinate the greatest element.

Equations

• DescriptiveComplexity.Draw.Data.topTup x✝ = Finset.univ.max' ⋯

theorem DescriptiveComplexity.Draw.Data.le_topTup {D : ℕ} {B : Type} [LinearOrder B] [Finite B] [Nonempty B] (p : Fin D) (a : B) : a ≤ topTup p

Every element is below the last tuple's coordinates.

theorem DescriptiveComplexity.Draw.Data.isMaxTup_topTup {D : ℕ} {B : Type} [LinearOrder B] [Finite B] [Nonempty B] : IsMaxTup topTup

The last tuple is exhausted.

The comparison's machine run

theorem DescriptiveComplexity.Draw.Data.cmp_reachesIn {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] (hhasP : RF.toLayout.HasName PR.zero) (hsepP : RF.toLayout.NameSep PR.zero ⋯) (vi : dt.VarIx) (av : Fin dt.natMax) (hnf : 2 ≤ dt.nfDim) (isEq : Bool) (j₁ j₂ : Fin (dt.nOf vi)) {emb : ElemPh 2 → P} {exitPh : P} {rEmb : (i : ElemSite 2) → ElemSh 2 i → R} [Finite dt.KIx] (hrules : ∀ (i : ElemSite 2) (ρ : ElemSh 2 i), PR.rules (rEmb i ρ) = elemRule PR.one Slot.wk Slot.reg emb (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).rdTrack (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).MatchOf (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).setFlag (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).initEl (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).advEl (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd RF.le) {gbot : I} (hbot : ∀ (y : I), RF.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeSt dt A R P I} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (f₀ : dt.CtlIx → A) (w : ℕ) (hcost : ∀ (b : Lex (Fin dt.dd0 → A)) (k : Fin 2), 2 * (wideRank (RF.cell (cmpCell RF PR.zero hhasP vi j₁ j₂ b k)) - wideRank v) + 2 ≤ w) : (wideData (Univ A R P dt.KIx dt.dd)).ReachesIn ((2 + (w + 2) * 2) * (Nat.card (Lex (Fin dt.dd0 → A)) + 1) + 1) { state := Sum.inr (PR.stElt (emb ElemPh.e0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.mir (dt.ixBack RF.toLayout PR.zero PR.one ⋯ st) st.mir) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh ((dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt (cmpFam RF PR.zero PR.one hhasP vi av hnf isEq j₁ j₂ st v f₀ (toLex topTup) (Fin.last 2)) (dt.ixBack RF.toLayout PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.mir (dt.ixBack RF.toLayout PR.zero PR.one ⋯ st) st.mir) (PR.syElt PR.blank) }

The comparison atom's machine run, on a clock: from the loop's entry checkpoint at the marker to the exit phase one cell to its right, the control carrying the whole enumeration's fold, two read trips paid per tuple.

theorem DescriptiveComplexity.Draw.Data.cmp_run {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] (hhasP : RF.toLayout.HasName PR.zero) (hsepP : RF.toLayout.NameSep PR.zero ⋯) (vi : dt.VarIx) (av : Fin dt.natMax) (hnf : 2 ≤ dt.nfDim) (isEq : Bool) (j₁ j₂ : Fin (dt.nOf vi)) {emb : ElemPh 2 → P} {exitPh : P} {rEmb : (i : ElemSite 2) → ElemSh 2 i → R} [Finite dt.KIx] (hrules : ∀ (i : ElemSite 2) (ρ : ElemSh 2 i), PR.rules (rEmb i ρ) = elemRule PR.one Slot.wk Slot.reg emb (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).rdTrack (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).MatchOf (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).setFlag (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).initEl (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).advEl (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt (dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd RF.le) {gbot : I} (hbot : ∀ (y : I), RF.le gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {st : TapeSt dt A R P I} (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (emb ElemPh.e0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell Slot.mir (dt.ixBack RF.toLayout PR.zero PR.one ⋯ st) st.mir) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh ((dt.cmpArgs PR.zero PR.one vi av hnf isEq j₁ j₂).exitSt (cmpFam RF PR.zero PR.one hhasP vi av hnf isEq j₁ j₂ st v f₀ (toLex topTup) (Fin.last 2)) (dt.ixBack RF.toLayout PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell Slot.mir (dt.ixBack RF.toLayout PR.zero PR.one ⋯ st) st.mir) (PR.syElt PR.blank) }

The comparison atom's machine run, the budget forgotten.

The verdict, characterized

theorem DescriptiveComplexity.Draw.Data.ctlBit_avC_cmp_exit {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {I : Type} (RF : LaidFile dt A R P I) [Nonempty A] {vi : dt.VarIx} {av : Fin dt.natMax} (hnf : 2 ≤ dt.nfDim) {isEq : Bool} {j₁ j₂ : Fin (dt.nOf vi)} {st : TapeSt dt A R P I} {vAdr : Univ A R P dt.KIx dt.dd → Prop} {zero one : A} {hhas : RF.toLayout.HasName zero} (hzo : zero ≠ one) (f₀ : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.ctlBit one ((dt.cmpArgs zero one vi av hnf isEq j₁ j₂).exitSt (cmpFam RF zero one hhas vi av hnf isEq j₁ j₂ st vAdr f₀ (toLex topTup) (Fin.last 2)) g) (dt.avC av) ↔ if isEq = true then ∀ (u : Lex (Fin dt.dd0 → A)), CmpAgr RF zero hhas vi j₁ j₂ st u else (∀ (u : Lex (Fin dt.dd0 → A)), CmpAgr RF zero hhas vi j₁ j₂ st u) ∨ ∃ (u : Lex (Fin dt.dd0 → A)), CmpFst RF zero hhas vi j₁ j₂ st u

The verdict the exit control carries: agreement everywhere for an equality atom; agreement everywhere or a first difference the second block's, for an order atom. This is exactly the shape DescriptiveComplexity.Draw.Data.encMap_eq_iff_padBits and DescriptiveComplexity.Draw.Data.encOrder_le_iff_padBits decide against the two registers' contents.