The two legs, joined at any program with the clocked rules

DescriptiveComplexity.Draw.Data.wideRegAccept_of_legs packages an opening and an evaluation as a yes-instance of DescriptiveComplexity.WideRegAccept, and DescriptiveComplexity.Draw.Data.reachesIn_openingReg runs the opening – both at an arbitrary program. This file joins them, at an arbitrary program too: the opening at the file the channel hands over, the evaluation at the same file, the guess writing an assignment's tracks inside the region it sweeps, and the clock met by the region's size, the evaluation's width and its rounds.

What the join reads of the program is only what a hypothesis can carry: its rules at named sites, its channel's marks, its constants and its accepting predicate. So the program a reduction emits and the padded one that buys the clock its room (RegChannelPad.lean) are both instances of one statement, and nothing here has to be proved twice.

noncomputable def DescriptiveComplexity.Draw.Data.regGatedSemP {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [LinearOrder A] [Nonempty A] [Finite A] [Finite dt.KIx] [L.Structure A] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [Finite (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [LinearOrder R'] [Finite R'] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] (PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd) (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {ιV : Type} (mV : ιV → dt.NexRegIx A R' (Option dt.KIx) → Prop) (w : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) (j : Fin dt.nv) (st : TapeSt dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R' (Option dt.KIx))) : dt.ixGatedAt (regLaid h hord) j st → (p : dt.IxScratch A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R' (Option dt.KIx))) → (a : ιV) → (∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP (regLaid h hord) PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) → (b : Fin (dt.natOf (dt.varAt j))) → dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) w ↑b) (dt.regElt A R' (Option dt.KIx)) (dt.kindOf (dt.varAt j) b)

The semantic packs a run of this evaluation is threaded by, pinned at the program: the packs are built once and for all (regGatedSem), and the only thing this adds is which program the gates they answer for belong to – which a term whose type mentions the program cannot leave to inference.

Equations

• DescriptiveComplexity.Draw.Data.regGatedSemP PR h hord mV = dt.regGatedSem h hord ⋯ mV

theorem DescriptiveComplexity.Draw.Data.wideRegAccept_regLaid_of_rules {L : FirstOrder.Language} {dt : Data L} {A R' : Type} [Fintype dt.SlotIx] [LinearOrder A] [Nonempty A] [Finite A] [Finite dt.KIx] [Nonempty dt.KIx] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] [LinearOrder (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [Finite (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF))] [LinearOrder R'] [Finite R'] [FirstOrder.Language.wide.Structure (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] [Finite (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)] {PR : Prog A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.CtlIx dt.SlotIx dt.KIx dt.dd} (hpl : Fintype.card (dt.CtlIx ⊕ dt.SlotIx) ≤ dt.dd) {bot : Option dt.KIx} (hE : NexEmitted PR bot) (hR : PR.table.Reads) (h : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {v' v₁ x y y' s₀ top : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop} (hvi₁ : WMIncr WMLe (fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) v₁) (hwalk : WMSetLe WMLe v₁ x) (hxy : WMIncr WMLe x y) (hyy' : WMIncr WMLe y y') (hyv : WMSetLe WMLe (fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) y) (hs₀ : WMIncr WMLe (fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) s₀) (hvi' : WMIncr WMLe (fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) v') (σ : dt.d.B.Assignment (dt.X.Map A)) (htop : WMSetLe WMLe s₀ top) (htopne : ∃ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), top z) (hexB : dt.exitG PR.one (PR.passTracksAt (regLaid h hord).cell Slot.mir (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (dt.nexEntrySt fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)) (fun (x : dt.RegIx) => False) fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)) (hexG : dt.exitG PR.one (PR.passTracksAt (regLaid h hord).cell Slot.mir (dt.ixBack (regLaid h hord).toLayout PR.zero PR.one ⋯ (have __src := dt.nexEntrySt fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False; { mir := __src.mir, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := dt.guessTracks PR.zero PR.one σ s₀ top, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp })) (fun (x : dt.RegIx) => False) fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)) {e₀ : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (he₀ : ∀ (y : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe e₀ y) (harg : ∀ (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), WMHasInp (Tag.arg (toLex b), padTup PR.zero c)) (hargall : ∀ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), (∃ (i : dt.KIx), z.1 = Tag.arg i) → WMHasInp z) (hupinp : ∀ (z w : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMLe z w → WMHasInp z → WMHasInp w) {botE : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd} (hbotm : WMHasInp botE) (hleast : ∀ (z : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), WMHasInp z → WMLe botE z) (hbotarg : ∀ (i : dt.KIx), botE.1 ≠ Tag.arg i) (gtop gbot : dt.NexRegIx A R' (Option dt.KIx)) (htopF : ∀ (u : dt.RegIx), (regLaid h hord).le u gtop) (hbotF : ∀ (u : dt.RegIx), (regLaid h hord).le gbot u) {ιV : Type} [LinearOrder ιV] [Finite ιV] {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (htopV : ∀ (a : ιV), a ≤ aT) (mV : ιV → dt.NexRegIx A R' (Option dt.KIx) → Prop) (hmV0 : mV a₀ = fun (x : dt.NexRegIx A R' (Option dt.KIx)) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr (regLaid h hord).le (mV a) (mV a')) (hTestT : ∀ (u : dt.RegIx), dt.InnerFull (regLaid h hord).blk (mV aT) u) (hTestF : ∀ a < aT, ∃ (u : dt.RegIx), ¬dt.InnerFull (regLaid h hord).blk (mV a) u) (stL : TapeSt dt A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) (dt.NexRegIx A R' (Option dt.KIx))) (fsL : dt.CtlIx → A) (hstL : stL = dt.ixSpineStOfB (regLaid h hord) ⋯ ⋯ ⋯ mV (have __src := dt.nexEntrySt fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False; { mir := __src.mir, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := dt.guessTracks PR.zero PR.one σ s₀ top, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (fun (x : dt.CtlIx) => PR.zero) (regGatedSemP PR h hord mV) (Fin.last dt.nv)) (hfsL : fsL = dt.ixSpineFsOfB (regLaid h hord) ⋯ ⋯ ⋯ mV (have __src := dt.nexEntrySt fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False; { mir := __src.mir, tgt := __src.tgt, sav := __src.sav, val := __src.val, old := dt.guessTracks PR.zero PR.one σ s₀ top, new := __src.new, wk := __src.wk, bot := __src.bot, ltp := __src.ltp }) (fun (x : dt.CtlIx) => PR.zero) (regGatedSemP PR h hord mV) (Fin.last dt.nv)) (hmirL : stL.mir = ixMark (dt.regElt A R' (Option dt.KIx)) fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hbotL : stL.bot = fun (r : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd → Prop) => r = fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (hsavL : stL.sav = ixMark (dt.regElt A R' (Option dt.KIx)) fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) (htgtL : stL.tgt = ixMark (dt.regElt A R' (Option dt.KIx)) fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) {Use : dt.NexRegIx A R' (Option dt.KIx) → Prop} (hUse : ∀ (a : ιV) (u : dt.NexRegIx A R' (Option dt.KIx)), mV a u → Use u) (hmono : ∀ (u u' : dt.RegIx), WMLt (regLaid h hord).le u u' ↔ WMLt WMLe (dt.regElt A R' (Option dt.KIx) u) (dt.regElt A R' (Option dt.KIx) u')) (hup : ∀ (u : dt.NexRegIx A R' (Option dt.KIx)) (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), Use u → WMLt WMLe (dt.regElt A R' (Option dt.KIx) u) x → ∃ (u' : dt.NexRegIx A R' (Option dt.KIx)), Use u' ∧ dt.regElt A R' (Option dt.KIx) u' = x) (hKin : ∀ (a : ιV) (t : Tag R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx) (w : Fin dt.dd → A), ixAddr (dt.regElt A R' (Option dt.KIx)) (mV a) (t, w) → ∃ (jj : Fin dt.ki), t = argIn dt.ko jj) (hTop : ∀ (u : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => tagBlk u.1) (ixAddr (dt.regElt A R' (Option dt.KIx)) (mV aT)) u) {Below : (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) 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) → (stL.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 (dt.regElt A R' (Option dt.KIx)) (dt.ixStageTgt (regLaid h hord) ⋯ none ts (have __src := dt.ixRoundSt stL (mV a); { mir := __src.mir, tgt := __src.tgt, sav := ixMark (dt.regElt A R' (Option dt.KIx)) fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False, 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) (hout : dt.X.Map A ⊨ dt.d.out) {a b k j m : ℕ} (hk : 1 ≤ k) (hkj : k + 1 < j) (hm : 0 < m) (hcard : (k + j) * m ≤ Nat.card (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)) (ha : dt.ixEvalWidth A (dt.nexRegW A R' (Option dt.KIx)) (dt.nexRegWP A R' (Option dt.KIx)) (dt.nexRegWR A R' (Option dt.KIx)) (dt.nexRegWK A R' (Option dt.KIx)) ≤ a) (haa : a ≤ 2 ^ (k * m)) (hb : Nat.card ιV + 1 ≤ b) (hbb : b ≤ 2 ^ (k * m)) (hopenle : wideRank x - wideRank v₁ + (wideRank y - wideRank fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False) + (wideRank top - wideRank s₀ + (wideRank top - wideRank fun (x : Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd) => False)) + 7 + 1 ≤ 2 ^ ((k + 1) * m)) : WideRegAccept.Holds (Univ A R' (NexPh (Option dt.KIx) (EvalPh dt.nv dt.PMF)) dt.KIx dt.dd)

A program with the clocked rules accepts, at the file the channel gives it: the opening and the evaluation at that one file, joined. Nothing of the program is read but its rules at named sites, its channel and its constants, so the same statement serves the program a reduction emits and the padded one that buys the clock its room.