The round flags and the pass's pack, at an arbitrary file

DescriptiveComplexity.Problems.Wide.DrawRoundSem read at a coarse file: the flags' semantic readings, the pass they jointly deliver, the valuation and the semantic pack built from it, and the leaf's two readings.

The flags along the VAL loop, without quantified levels

theorem DescriptiveComplexity.Draw.Data.ixCtlBit_flag_varFM_of_nIn_zero {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] {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)) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeSt dt A R P I} {ι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)} (hzo : PR.zero ≠ PR.one) (hn0 : dt.nIn vi = 0) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (v : Univ A R P dt.KIx dt.dd → Prop) (fG : dt.CtlIx → A) (a : ιV) : dt.ctlBit PR.one (ixVarFM F hinj hhasP heltP vi st v mV semOf fG a) q

Without quantified levels the two flags are constant along the VAL loop: the entry seeded them True, the inner-gates thread is empty, and no fold update writes a flag.

theorem DescriptiveComplexity.Draw.Data.ixCtlBit_roundFX_pass_iff {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] {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)) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {st : TapeSt dt A R P I} {ι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)} (hzo : PR.zero ≠ PR.one) {q : dt.CtlIx} (hq : q = dt.existGateC ∨ q = dt.allGateC) (v : Univ A R P dt.KIx dt.dd → Prop) (fG : dt.CtlIx → A) (a : ιV) : dt.ctlBit PR.one (ixRoundFX F hinj hhasP heltP vi st v mV semOf (ixVarFM F hinj hhasP heltP vi st v mV semOf fG a) a) q ↔ ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = q → dt.ixIGPassP F PR.zero PR.one vi (dt.ixRoundSt st (mV a)) ℓ

A round flag at the round's exit reads as the per-polarity pass: every quantified level of the flag's polarity holds an encoding-shaped, one-hot, domain-satisfying block value. The capstone's hEx/hAll.

theorem DescriptiveComplexity.Draw.Data.ixRoundPass_of_polarities {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {vi : dt.VarIx} {zero one : A} {stV : TapeSt dt A R P I} (hEx : ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.existGateC → dt.ixIGPassP F zero one vi stV ℓ) (hAl : ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.allGateC → dt.ixIGPassP F zero one vi stV ℓ) (ℓ : Fin (dt.nIn vi)) : dt.ixIGPassP F zero one vi stV ℓ

The two polarity readings deliver the full pass: every level's flag is one of the two. The capstone's hPass.

The pack, built from the pass

noncomputable def DescriptiveComplexity.Draw.Data.ixPassW {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (zero one : A) (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (j : Fin (dt.nOf vi)) : dt.X.Map A

The valuation a passing round holds: the gated address's points at the free levels, the points the pass's encodings choose at the quantified ones.

Equations

• dt.ixPassW F zero one hpassEnc vi stV hp mbW j = if h : ↑j < dt.arOf vi then mbW ⟨↑j, h⟩ else Exists.choose ⋯

theorem DescriptiveComplexity.Draw.Data.ixPassW_hENC {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk (ixAddr elt stV.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (j : Fin (dt.nOf vi)) : wmBlk (ixAddr elt (dt.lvSet stV vi j)) (Tag.arg (toLex (dt.lvBlk vi j))) = encMap dt.ly zero one (dt.ixPassW F zero one hpassEnc vi stV hp mbW j)

The master encoding fact of a passing round: every level's block – the working address's at the free levels, the round register's at the quantified ones – encodes the valuation's point. The capstone's hENC, and DescriptiveComplexity.Draw.Data.ixMkKindSem's input.

noncomputable def DescriptiveComplexity.Draw.Data.ixPassSem {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), wmBlk (ixAddr elt stV.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (mbW ℓ)) (b : Fin (dt.natOf vi)) : dt.IxKindSem zero one vi stV elt (dt.kindOf vi b)

The semantic pack of a passing round, constructed: the capstone's semOf, with hsem definitional.

Equations

• dt.ixPassSem F hpassEnc vi stV hp mbW hmb b = dt.ixMkKindSem zero one vi stV (dt.ixPassW F zero one hpassEnc vi stV hp mbW) ⋯ (dt.kindOf vi b)

The stage tracks at the composed target

theorem DescriptiveComplexity.Draw.Data.ixAddr_ixStageTgt_iff {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) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] {zero : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (st : TapeSt dt A R P I) (n : ℕ) (x : Univ A R P dt.KIx dt.dd) : ixAddr elt (dt.ixStageTgt F hhas vi ts st n) x ↔ ∃ (ℓ : Fin (dt.d.B.arity iv)) (b : Lex (Fin dt.dd0 → A)), ↑ℓ < n ∧ x = dt.stageXD zero iv ℓ b ∧ ixAddr elt (dt.lvSet st vi (ts ℓ)) (dt.stageXS zero vi iv ts ℓ b)

The composed TARGET's address, in closed form: the coarse file's DescriptiveComplexity.Draw.Data.ixStageTgt read as a set of elements is the elementwise closed form – the destination cells are the elements the destination registers stand for, and the source bits are read at the source registers' elements.

theorem DescriptiveComplexity.Draw.Data.ixWmBlk_stageTgtD_eq_encMap {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) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (vi : dt.VarIx) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (stV : TapeSt dt A R P I) {p : Fin (dt.d.B.arity iv) → dt.X.Map A} (hsrc : ∀ (ℓ : Fin (dt.d.B.arity iv)), wmBlk (ixAddr elt (dt.lvSet stV vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (p ℓ)) (ℓ : Fin (dt.d.B.arity iv)) : wmBlk (ixAddr elt (dt.ixStageTgt F hhas vi ts stV (dt.d.B.arity iv))) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))) = encMap dt.ly zero one (p ℓ)

The composed TARGET's argument blocks are the sources': after all copy loops, block ℓ of TARGET is the position's source block – the copy is faithful on the padded cells, and an encoding holds no others.

theorem DescriptiveComplexity.Draw.Data.ixAddr_ixStageTgt_eq_tupAddr {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) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (vi : dt.VarIx) (iv : dt.d.B.ι) (ha : dt.d.B.arity iv ≤ dt.ko) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) (stV : TapeSt dt A R P I) {p : Fin (dt.d.B.arity iv) → dt.X.Map A} (hsrc : ∀ (ℓ : Fin (dt.d.B.arity iv)), wmBlk (ixAddr elt (dt.lvSet stV vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (p ℓ)) : ixAddr elt (dt.ixStageTgt F hhas vi ts stV (dt.d.B.arity iv)) = tupAddr dt.ly zero one ha p

The composed TARGET is the canonical address of the points it names: its blocks below the arity are their encodings and it marks nothing else, which is tupAddr_of_blocks. This is what lets a dictionary be asked for at canonical addresses alone – and so lets one be read off an arbitrary set of marked addresses, which is what a backward reading of a run has to do.

theorem DescriptiveComplexity.Draw.Data.ixOld_stage_of_dict {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) {elt : I → Univ A R P dt.KIx dt.dd} (hinj : Function.Injective elt) [Nonempty A] [L.Structure A] {zero one : A} (hhas : F.toLayout.HasName zero) (helt : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b c) = dt.blkElt b (pad zero c)) (vi : dt.VarIx) (iv : dt.d.B.ι) (ha : dt.d.B.arity iv ≤ dt.ko) (σ : dt.d.B.Assignment (dt.X.Map A)) (stV : TapeSt dt A R P I) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (x : Fin (dt.d.B.arity iv) → dt.X.Map A), Below (tupAddr dt.ly zero one ha x) → (stV.old iv (tupAddr dt.ly zero one ha x) ↔ σ iv x)) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)) {p : Fin (dt.d.B.arity iv) → dt.X.Map A} (hsrc : ∀ (ℓ : Fin (dt.d.B.arity iv)), wmBlk (ixAddr elt (dt.lvSet stV vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (p ℓ)) (hbelow : Below (ixAddr elt (dt.ixStageTgt F hhas vi ts stV (dt.d.B.arity iv)))) : stV.old iv (ixAddr elt (dt.ixStageTgt F hhas vi ts stV (dt.d.B.arity iv))) ↔ σ iv p

A stage track reads the dictionary at the composed target, asking for the dictionary at canonical addresses only: the target is the canonical address of the points it names (ixAddr_ixStageTgt_eq_tupAddr), so what a run has to know about its stage tracks is one bit per tuple, not one per address. Forwards that is weaker than asking for the dictionary at every address, and the guess supplies it just the same; backwards it is the difference between a dictionary that can be read off a run and one that cannot.

The leaf, read at the round's register

theorem DescriptiveComplexity.Draw.Data.ixRoundPass_iff_split_gen {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) {q : dt.CtlIx} {bpol : Bool} (hqiff : ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = q ↔ dt.polOf vi (dt.arOf vi + ↑ℓ) = bpol) : (∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = q → dt.ixIGPassP F zero one vi stV ℓ) ↔ ∀ (j : Fin (dt.nOf vi)), dt.arOf vi ≤ ↑j → dt.polOf vi ↑j = bpol → IsEnc dt.ly zero one (ixBlk (argIn dt.ko) (ixAddr elt stV.val) ⟨↑j, ⋯⟩)

A per-polarity pass is the split's gate clause, reindexed from the quantified levels to the pack's indices.

theorem DescriptiveComplexity.Draw.Data.ixLevelVal_encMap {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (mbW ℓ)) (j : Fin (dt.nOf vi)) : dt.levelVal vi mb (ixBlk (argIn dt.ko) (ixAddr elt stV.val)) j = encMap dt.ly zero one (dt.ixPassW F zero one hpassEnc vi stV hp mbW j)

The valuation the leaf decodes is the pass's: every level's block of the leaf's reading encodes ixPassW's point.

theorem DescriptiveComplexity.Draw.Data.ixLeafP_pass_iff {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) [LinearOrder (dt.X.Map A)] (hzo : zero ≠ one) (vi : dt.VarIx) (stV : TapeSt dt A R P I) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (mbW ℓ)) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ) : dt.leafP zero one vi σ mb (ixBlk (argIn dt.ko) (ixAddr elt stV.val)) ↔ qfValue (dt.matOf vi) fun (atm : ((dt.X.E.sum FirstOrder.Language.order).sum dt.d.B.lang).BoundedFormula Empty (dt.nOf vi)) => (matAtom? atm).elim False (MatAtom.holds σ (dt.ixPassW F zero one hpassEnc vi stV hp mbW))

The leaf at a passing round is the matrix's value at the pass's points – the capstone's hPsPass, with Ps the gated matrix DescriptiveComplexity.Draw.Data.leafP.

theorem DescriptiveComplexity.Draw.Data.ixLeafP_fail_iff {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) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] {zero one : A} (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) [LinearOrder (dt.X.Map A)] (vi : dt.VarIx) (stV : TapeSt dt A R P I) (σ : dt.d.B.Assignment (dt.X.Map A)) (mb : Fin dt.ko → (Fin dt.dd → A) → Prop) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), mb (Fin.castLE ⋯ ℓ) = encMap dt.ly zero one (mbW ℓ)) (hEA : ¬((∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.existGateC → dt.ixIGPassP F zero one vi stV ℓ) ∧ ∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.allGateC → dt.ixIGPassP F zero one vi stV ℓ)) : (∀ (ℓ : Fin (dt.nIn vi)), dt.igFlag vi ℓ = dt.existGateC → dt.ixIGPassP F zero one vi stV ℓ) ↔ dt.leafP zero one vi σ mb (ixBlk (argIn dt.ko) (ixAddr elt stV.val))

The leaf at a failing round is the ∃-clause alone – the capstone's hPsFail: the ∀-clause's implication is vacuous when the two readings do not both hold.