One variable's verdict at an arbitrary file #
DescriptiveComplexity.Problems.Wide.DrawVerdict read at a coarse file: the
machinery's exit bit as the alternating prefix over the leaf, and its
specialization at a fixed-point variable and at the output.
noncomputable def
DescriptiveComplexity.Draw.Data.ixMirBlk
{L : FirstOrder.Language}
(dt : Data L)
{A R P I : Type}
{elt : I → Univ A R P dt.KIx dt.dd}
(st : TapeSt dt A R P I)
:
The working address's outer blocks, as the valuation the free levels of a pack read: the mirror's block at each outer index.
Equations
- dt.ixMirBlk st k = DescriptiveComplexity.wmBlk (DescriptiveComplexity.ixAddr elt st.mir) (DescriptiveComplexity.Draw.Tag.arg (toLex (Sum.inl k)))
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixMirBlk_of_mir
{L : FirstOrder.Language}
{dt : Data L}
{A R P I : Type}
{elt : I → Univ A R P dt.KIx dt.dd}
{st st' : TapeSt dt A R P I}
(h : st.mir = st'.mir)
:
The address's blocks depend on the mirror alone.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixAccVerdict_leafP
{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}
(F : LaidFile dt A R P I)
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(hhasP : F.toLayout.HasName PR.zero)
(heltP :
∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c))
(hix : IsLinOrd F.le)
(hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1)
{Use : I → Prop}
(hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
(hpassEnc :
∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)),
dt.ixIGPassP F PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ)))))
[LinearOrder (dt.X.Map A)]
(vi : dt.VarIx)
(st : TapeSt dt A R P I)
{v : Univ A R P dt.KIx dt.dd → Prop}
{ιV : Type}
[LinearOrder ιV]
[Finite ιV]
(mV : ιV → I → Prop)
(semOf :
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ) →
(b : Fin (dt.natOf vi)) → dt.IxKindSem PR.zero PR.one vi (dt.ixRoundSt st (mV a)) elt (dt.kindOf vi b))
(hlin : IsLinOrd WMLe)
(hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
{a₀ aT : ιV}
(hbotV : ∀ (a : ιV), a₀ ≤ a)
(hmV0 : mV a₀ = fun (x : I) => False)
(hUse : ∀ (a : ιV) (u : I), mV a u → Use u)
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a'))
(hKin :
∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j)
(hTop :
∀ (u : Univ A R P dt.KIx dt.dd),
dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u)
(σ : dt.d.B.Assignment (dt.X.Map A))
(mbW : Fin (dt.arOf vi) → dt.X.Map A)
(hmb : ∀ (ℓ : Fin (dt.arOf vi)), dt.ixMirBlk st (Fin.castLE ⋯ ℓ) = encMap dt.ly PR.zero PR.one (mbW ℓ))
{Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop}
(hdict :
∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A),
Below (tupAddr dt.ly PR.zero PR.one ⋯ x) → (st.old iv (tupAddr dt.ly PR.zero PR.one ⋯ x) ↔ σ iv x))
(hbelow :
∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)),
Below
(ixAddr elt
(dt.ixStageTgt F hhasP vi ts
(have __src := dt.ixRoundSt st (mV a);
{ mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old,
new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })
(dt.d.B.arity iv))))
(hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q)
(hsem :
∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ)
(b : Fin (dt.natOf vi)), semOf a hp b = dt.ixPassSem F hpassEnc vi (dt.ixRoundSt st (mV a)) hp mbW ⋯ b)
(fG : dt.CtlIx → A)
:
dt.accVerdict PR.one (dt.polOf vi)
((dt.varArgsOf PR.zero PR.one vi).postFold
(ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG aT) aT)
(dt.ixBack F.toLayout PR.zero PR.one ⋯ (dt.ixRoundSt st (mV aT)) v)) ↔ altQuantFrom (dt.polOf vi) (dt.leafP PR.zero PR.one vi σ (dt.ixMirBlk st)) 0
(ixBlk (argIn dt.ko) (ixAddr elt (mV aT)))
The machinery's verdict is the prefix over the leaf: every abstract
input of DescriptiveComplexity.Draw.Data.ixAccVerdict_varFM_qfValue
discharged – the flags by
DescriptiveComplexity.Draw.Data.ixCtlBit_roundFX_pass_iff, the pass by
DescriptiveComplexity.Draw.Data.ixRoundPass_of_polarities, the valuation
and its pack by DescriptiveComplexity.Draw.Data.ixPassW, the stage reads
by DescriptiveComplexity.Draw.Data.ixOld_stage_of_dict, and the two
leaf readings by DescriptiveComplexity.Draw.Data.ixLeafP_pass_iff /
DescriptiveComplexity.Draw.Data.ixLeafP_fail_iff.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixAccVerdict_next
{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}
(F : LaidFile dt A R P I)
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(hhasP : F.toLayout.HasName PR.zero)
(heltP :
∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c))
(hix : IsLinOrd F.le)
(hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1)
{Use : I → Prop}
(hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
(hpassEnc :
∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)),
dt.ixIGPassP F PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ)))))
[LinearOrder (dt.X.Map A)]
(st : TapeSt dt A R P I)
{v : Univ A R P dt.KIx dt.dd → Prop}
{ιV : Type}
[LinearOrder ιV]
[Finite ιV]
(mV : ιV → I → Prop)
(i : dt.d.B.ι)
(semOf :
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn (some i))), dt.ixIGPassP F PR.zero PR.one (some i) (dt.ixRoundSt st (mV a)) ℓ) →
(b : Fin (dt.natOf (some i))) →
dt.IxKindSem PR.zero PR.one (some i) (dt.ixRoundSt st (mV a)) elt (dt.kindOf (some i) b))
(hlin : IsLinOrd WMLe)
(hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
{a₀ aT : ιV}
(hbotV : ∀ (a : ιV), a₀ ≤ a)
(hmV0 : mV a₀ = fun (x : I) => False)
(hUse : ∀ (a : ιV) (u : I), mV a u → Use u)
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a'))
(hKin :
∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j)
(hTop :
∀ (u : Univ A R P dt.KIx dt.dd),
dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u)
(σ : dt.d.B.Assignment (dt.X.Map A))
(mbW : Fin (dt.arOf (some i)) → dt.X.Map A)
(hmb : ∀ (ℓ : Fin (dt.arOf (some i))), dt.ixMirBlk st (Fin.castLE ⋯ ℓ) = encMap dt.ly PR.zero PR.one (mbW ℓ))
{Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop}
(hdict :
∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A),
Below (tupAddr dt.ly PR.zero PR.one ⋯ x) → (st.old iv (tupAddr dt.ly PR.zero PR.one ⋯ x) ↔ σ iv x))
(hbelow :
∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (some i))),
Below
(ixAddr elt
(dt.ixStageTgt F hhasP (some i) ts
(have __src := dt.ixRoundSt st (mV a);
{ mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old,
new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })
(dt.d.B.arity iv))))
(hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q)
(hsem :
∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (some i))), dt.ixIGPassP F PR.zero PR.one (some i) (dt.ixRoundSt st (mV a)) ℓ)
(b : Fin (dt.natOf (some i))), semOf a hp b = dt.ixPassSem F hpassEnc (some i) (dt.ixRoundSt st (mV a)) hp mbW ⋯ b)
(fG : dt.CtlIx → A)
:
The machinery's verdict at a fixed-point variable is one step of the
iteration at the points the working address's outer blocks encode: the
prefix of DescriptiveComplexity.Draw.Data.ixAccVerdict_leafP read through
DescriptiveComplexity.Draw.Data.altQuantFrom_leafP.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixAccVerdict_out
{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}
(F : LaidFile dt A R P I)
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(hhasP : F.toLayout.HasName PR.zero)
(heltP :
∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhasP b c) = dt.blkElt b (pad PR.zero c))
(hix : IsLinOrd F.le)
(hblkP : ∀ (u : I), F.blk u = tagBlk (elt u).1)
{Use : I → Prop}
(hmono : ∀ (u u' : I), WMLt F.le u u' ↔ WMLt WMLe (elt u) (elt u'))
(hup : ∀ (u : I) (x : Univ A R P dt.KIx dt.dd), Use u → WMLt WMLe (elt u) x → ∃ (u' : I), Use u' ∧ elt u' = x)
[Nonempty A]
[L.IsRelational]
[L.Structure A]
(hpassEnc :
∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)),
dt.ixIGPassP F PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ)))))
[LinearOrder (dt.X.Map A)]
(st : TapeSt dt A R P I)
{v : Univ A R P dt.KIx dt.dd → Prop}
{ιV : Type}
[LinearOrder ιV]
[Finite ιV]
(mV : ιV → I → Prop)
(semOf :
(a : ιV) →
(∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ) →
(b : Fin (dt.natOf none)) → dt.IxKindSem PR.zero PR.one none (dt.ixRoundSt st (mV a)) elt (dt.kindOf none b))
(hlin : IsLinOrd WMLe)
(hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y)
{a₀ aT : ιV}
(hbotV : ∀ (a : ιV), a₀ ≤ a)
(hmV0 : mV a₀ = fun (x : I) => False)
(hUse : ∀ (a : ιV) (u : I), mV a u → Use u)
(hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr F.le (mV a) (mV a'))
(hKin :
∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), ixAddr elt (mV a) (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j)
(hTop :
∀ (u : Univ A R P dt.KIx dt.dd),
dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (ixAddr elt (mV aT)) u)
(σ : dt.d.B.Assignment (dt.X.Map A))
{Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop}
(hdict :
∀ (iv : dt.d.B.ι) (x : Fin (dt.d.B.arity iv) → dt.X.Map A),
Below (tupAddr dt.ly PR.zero PR.one ⋯ x) → (st.old iv (tupAddr dt.ly PR.zero PR.one ⋯ x) ↔ σ iv x))
(hbelow :
∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf none)),
Below
(ixAddr elt
(dt.ixStageTgt F hhasP none ts
(have __src := dt.ixRoundSt st (mV a);
{ mir := __src.mir, tgt := __src.tgt, sav := ixMark elt v, val := __src.val, old := __src.old,
new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })
(dt.d.B.arity iv))))
(hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q)
(hsem :
∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn none)), dt.ixIGPassP F PR.zero PR.one none (dt.ixRoundSt st (mV a)) ℓ)
(b : Fin (dt.natOf none)),
semOf a hp b = dt.ixPassSem F hpassEnc none (dt.ixRoundSt st (mV a)) hp (fun (ℓ : Fin (dt.arOf none)) => ℓ.elim0) ⋯ b)
(fG : dt.CtlIx → A)
:
The machinery's verdict at the output variable is the output sentence
at the stage the tracks hold: the prefix of
DescriptiveComplexity.Draw.Data.ixAccVerdict_leafP read through
DescriptiveComplexity.Draw.Data.altQuantFrom_leafP_out. The output
variable is nullary, so the working address's outer blocks encode the empty
tuple and there is nothing to ask of them – which is why this is the one
verdict a reduction can take at the empty address.