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.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.

The loop element through the comparison's operations

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.

The loop element is the round's 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.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' ⋯

The comparison's machine run

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.