The inner gates at an arbitrary file #
The mirror of DescriptiveComplexity.Problems.Wide.DrawIxGate 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. The registers the trips go to are the gates' own
(DescriptiveComplexity.Draw.Data.ixGateTagCell/ixGateECell), so only the
families, the guards and the run are restated here.
noncomputable def
DescriptiveComplexity.Draw.Data.ixIGateLeafP
{L : FirstOrder.Language}
{A R P : Type}
[LinearOrder A]
[L.IsRelational]
[L.Structure A]
(dt : Data L)
{I : Type}
(b : Fin dt.ko ⊕ Fin dt.ki)
(st : TapeSt dt A R P I)
(t : dt.X.Tag)
(hnt : (dt.domPk t).n ≤ dt.eDim)
{elt : I → Univ A R P dt.KIx dt.dd}
(zero one : A)
(v : Fin dt.eDim → A)
:
An inner gate's leaf at the file, over the wide valuation: the tag's domain sentence at the decoded assignment of the block value the VAL marks' address holds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.Data.ixIGateTagFam
{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}
(F : LaidFile dt A R P I)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero : A}
(hhas : F.toLayout.HasName zero)
(one : A)
(b : Fin dt.ko ⊕ Fin dt.ki)
(st : TapeSt dt A R P I)
(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.
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.Data.ixIGateFam
{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}
(F : LaidFile dt A R P I)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero : A}
(hhas : F.toLayout.HasName zero)
(one : A)
(b : Fin dt.ko ⊕ Fin dt.ki)
(st : TapeSt dt A R P I)
(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.