The inner gates, instantiated

The mirror of DescriptiveComplexity.Problems.Wide.DrawInstGate at the VAL register: one gate block per quantified level of a variable's pack, read off the round's register content instead of the mirror, its verdict conjoined into the level's polarity flag – one of the round's two – instead of the gates' single flag. The witness cells are the same (gateTagCell/gateECell are register-free), the control families are the same operations at the igateArgs pack, and the run is the same tag_run_iter with the read registers pointed at VAL.

The flag-riding lemmas are stated at a flag constrained to the round's two (hflag : flag = existGateC ∨ flag = allGateC), which is what makes every disequality against the machinery's written slots decidable.

noncomputable def DescriptiveComplexity.Draw.Data.igateTagFam {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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (st : TapeStD dt A R P) (flag : dt.CtlIx) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (vAdr : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (i : Fin (Fintype.card dt.X.Tag + 1)) : dt.CtlIx → A

The generated witness chain of a gate, at the pack.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.igateFam {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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (st : TapeStD dt A R P) (t : dt.X.Tag) (flag : dt.CtlIx) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (vAdr : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : Fin (dt.domNr t + 1)) : dt.CtlIx → A

The generated family of branch t's domain loop, at the pack.

Equations

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

The witness chain: read-back and decode

The domain payload at a generated state, and the leaf guards

The gate's machine run

The sub-fold: the sac invariant and the conjoining exit

The gates' flag rides, and the conjoining exit