Generated control families: the runs, iterated

The run theorems of the layer take their control evolution as abstract families over the enumeration – fsOf a j, the pointer before the j-th read of round a – tied together by per-cover equations. An instantiation has to produce such a family, and its rounds are defined by iteration: the next round's entry is a function of the previous round's exit. This file builds the family once, for every instantiation:

• DescriptiveComplexity.Draw.iterOrd – a state iterated along a finite linear order, by recursion on DescriptiveComplexity.orank (the bottom is the base, each cover one step);
• DescriptiveComplexity.Draw.chainSt – the within-round read chain, each read's stored bit chosen classically;
• DescriptiveComplexity.Draw.elem_run_iter – the element loop's run at the generated family: the caller supplies only the name guards at the generated states, the exhaustion conditions, and the geometry.

Iteration along a finite linear order

noncomputable def DescriptiveComplexity.Draw.iterState {ι : Type} {Q' : Type u_1} [LinearOrder ι] (init : Q') (step : ι → Q' → Q') : ℕ → Q'

The iterated state at a rank: the base at 0, one step per rank – the element of that rank supplying the step's index.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.iterState init step 0 = init

noncomputable def DescriptiveComplexity.Draw.iterOrd {ι : Type} {Q' : Type u_1} [LinearOrder ι] (init : Q') (step : ι → Q' → Q') (a : ι) : Q'

A state iterated along the order: the base at the bottom, one step per cover.

Equations

• DescriptiveComplexity.Draw.iterOrd init step a = DescriptiveComplexity.Draw.iterState init step (DescriptiveComplexity.orank a)

theorem DescriptiveComplexity.Draw.iterOrd_bot {ι : Type} {Q' : Type u_1} [LinearOrder ι] {init : Q'} {step : ι → Q' → Q'} {a₀ : ι} (hbot : ∀ (b : ι), a₀ ≤ b) : iterOrd init step a₀ = init

At the bottom the iteration is the base.

theorem DescriptiveComplexity.Draw.iterOrd_covers {ι : Type} {Q' : Type u_1} [LinearOrder ι] [Finite ι] {init : Q'} {step : ι → Q' → Q'} {a a' : ι} (hlt : a < a') (hnb : ∀ (b : ι), ¬(a < b ∧ b < a')) : iterOrd init step a' = step a (iterOrd init step a)

Across a cover the iteration steps once, at the covered element.

theorem DescriptiveComplexity.Draw.iterOrd_invariant {ι : Type} {Q' : Type u_1} [LinearOrder ι] {init : Q'} {step : ι → Q' → Q'} {Inv : Q' → Prop} (hinit : Inv init) (hstep : ∀ (a : ι) (q : Q'), Inv q → Inv (step a q)) (a : ι) : Inv (iterOrd init step a)

An invariant of the step is an invariant of the iteration: what the base satisfies and every step preserves holds at every element. This is what a threaded tape family's field lemmas are proved by – the fields a round leaves alone are preserved by each step, hence along the whole loop.

The within-round read chain

noncomputable def DescriptiveComplexity.Draw.chainSt {Q' : Type} {nr : ℕ} (bit : Fin nr → Prop) (upd : Fin nr → Bool → Q' → Q') (base : Q') : ℕ → Q'

The read chain of one round: the j-th prefix of the reads applied to the round's entry state, each stored bit the read's.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.Draw.chainSt bit upd base 0 = base

@[simp]

theorem DescriptiveComplexity.Draw.chainSt_zero {Q' : Type} {nr : ℕ} {bit : Fin nr → Prop} {upd : Fin nr → Bool → Q' → Q'} {base : Q'} : chainSt bit upd base 0 = base

theorem DescriptiveComplexity.Draw.chainSt_succ_pos {Q' : Type} {nr : ℕ} {bit : Fin nr → Prop} {upd : Fin nr → Bool → Q' → Q'} {base : Q'} {j : ℕ} (h : j < nr) (hb : bit ⟨j, h⟩) : chainSt bit upd base (j + 1) = upd ⟨j, h⟩ true (chainSt bit upd base j)

A positive read's link.

theorem DescriptiveComplexity.Draw.chainSt_succ_neg {Q' : Type} {nr : ℕ} {bit : Fin nr → Prop} {upd : Fin nr → Bool → Q' → Q'} {base : Q'} {j : ℕ} (h : j < nr) (hb : ¬bit ⟨j, h⟩) : chainSt bit upd base (j + 1) = upd ⟨j, h⟩ false (chainSt bit upd base j)

A negative read's link.

The element loop's run, at the generated family

noncomputable def DescriptiveComplexity.Draw.elemIter {A R P Q W K : Type} {dd nr : ℕ} {I : Type} (setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl : (Q → A) → (W → A) → Q → A) {ι : Type} [LinearOrder ι] (rest : (Univ A R P K dd → Prop) → W → A) (v : Univ A R P K dd → Prop) (m : Fin nr → I → Prop) (xOf : ι → Fin nr → I) (f₀ : Q → A) (a : ι) : Q → A

The generated round-entry state: the loop's initEl at the bottom, each cover the previous round's reads folded and advanced.

Equations

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

noncomputable def DescriptiveComplexity.Draw.elemFam {A R P Q W K : Type} {dd nr : ℕ} {I : Type} (setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl : (Q → A) → (W → A) → Q → A) {ι : Type} [LinearOrder ι] (rest : (Univ A R P K dd → Prop) → W → A) (v : Univ A R P K dd → Prop) (m : Fin nr → I → Prop) (xOf : ι → Fin nr → I) (f₀ : Q → A) (a : ι) (j : Fin (nr + 1)) : Q → A

The generated within-round family: the read chain of round a applied to its entry state.

Equations

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

The background is read at the working cell alone. Both generated families mention rest only as rest v, so a background that moves elsewhere – at a register cell, say, where the four register slots live – generates the same control. This is what makes a loop blind to the two scratch registers of the state it is run at.

theorem DescriptiveComplexity.Draw.elemIter_congr_rest {A R P Q W K : Type} {dd nr : ℕ} {I : Type} {setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl : (Q → A) → (W → A) → Q → A} {ι : Type} [LinearOrder ι] {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {m : Fin nr → I → Prop} {rest' : (Univ A R P K dd → Prop) → W → A} (h : rest v = rest' v) (xOf : ι → Fin nr → I) (f₀ : Q → A) (a : ι) : elemIter setFlag initEl advEl rest v m xOf f₀ a = elemIter setFlag initEl advEl rest' v m xOf f₀ a

Two backgrounds agreeing at the working cell give one round-entry family.

theorem DescriptiveComplexity.Draw.elemFam_congr_rest {A R P Q W K : Type} {dd nr : ℕ} {I : Type} {setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl : (Q → A) → (W → A) → Q → A} {ι : Type} [LinearOrder ι] {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {m : Fin nr → I → Prop} {rest' : (Univ A R P K dd → Prop) → W → A} (h : rest v = rest' v) (xOf : ι → Fin nr → I) (f₀ : Q → A) (a : ι) (j : Fin (nr + 1)) : elemFam setFlag initEl advEl rest v m xOf f₀ a j = elemFam setFlag initEl advEl rest' v m xOf f₀ a j

Two backgrounds agreeing at the working cell give one within-round family.

theorem DescriptiveComplexity.Draw.elem_reachesIn_iter {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {nr : ℕ} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : ElemPh nr → P} {rdTrack : Fin nr → W} {MatchOf : Fin nr → (Q → A) → (W → A) → Prop} {setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl exitSt : (Q → A) → (W → A) → Q → A} {IsMaxEl : (Q → A) → Prop} {exitPh : P} {rEmb : (i : ElemSite nr) → ElemSh nr i → R} {ι : Type} [LinearOrder ι] [Finite ι] {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {m : Fin nr → I → Prop} (hrules : ∀ (i : ElemSite nr) (ρ : ElemSh nr i), PR.rules (rEmb i ρ) = elemRule PR.one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hm : ∀ (j : Fin nr) (r : Univ A R P K dd → Prop), rest r (rdTrack j) = bitVal PR.zero PR.one (bitAtOf RF.cell (m j) r)) (hnewk : ∀ (j : Fin nr), wk ≠ rdTrack j) (hnerg : ∀ (j : Fin nr), rg ≠ rdTrack j) {t₀ : W} {m₀ : I → Prop} (hm₀ : ∀ (r : Univ A R P K dd → Prop), rest r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r)) (hwkt₀ : wk ≠ t₀) (hrgt₀ : rg ≠ t₀) {a₀ aT : ι} (hbotI : ∀ (a : ι), a₀ ≤ a) (htopI : ∀ (a : ι), a ≤ aT) (xOf : ι → Fin nr → I) (f₀ : Q → A) (hname : ∀ (a : ι) (j : Fin nr), MatchOf j (elemFam setFlag initEl advEl rest v m xOf f₀ a j.castSucc) (PR.passTracksAt RF.cell (rdTrack j) rest (m j) (RF.cell (xOf a j)))) (huniq : ∀ (a : ι) (j : Fin nr) (r : Univ A R P K dd → Prop), MatchOf j (elemFam setFlag initEl advEl rest v m xOf f₀ a j.castSucc) (PR.passTracksAt RF.cell (rdTrack j) rest (m j) r) → r = RF.cell (xOf a j)) (hmaxT : IsMaxEl (elemFam setFlag initEl advEl rest v m xOf f₀ aT (Fin.last nr))) (hmaxF : ∀ a < aT, ¬IsMaxEl (elemFam setFlag initEl advEl rest v m xOf f₀ a (Fin.last nr))) (c : ℕ) (hcost : ∀ (a : ι) (j : Fin nr), 2 * (wideRank (RF.cell (xOf a j)) - wideRank v) + 2 ≤ c) : (wideData (Univ A R P K dd)).ReachesIn ((2 + (c + 2) * nr) * (Nat.card ι + 1) + 1) { state := Sum.inr (PR.stElt (emb ElemPh.e0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (exitSt (elemFam setFlag initEl advEl rest v m xOf f₀ aT (Fin.last nr)) (rest v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }

The element loop's run at the generated family, on a clock: only the name guards at the generated states, the exhaustion conditions and the geometry are owed; the family equations hold by construction.

theorem DescriptiveComplexity.Draw.elem_run_iter {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {nr : ℕ} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : ElemPh nr → P} {rdTrack : Fin nr → W} {MatchOf : Fin nr → (Q → A) → (W → A) → Prop} {setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl exitSt : (Q → A) → (W → A) → Q → A} {IsMaxEl : (Q → A) → Prop} {exitPh : P} {rEmb : (i : ElemSite nr) → ElemSh nr i → R} {ι : Type} [LinearOrder ι] [Finite ι] {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {m : Fin nr → I → Prop} (hrules : ∀ (i : ElemSite nr) (ρ : ElemSh nr i), PR.rules (rEmb i ρ) = elemRule PR.one wk rg emb rdTrack MatchOf setFlag initEl advEl exitSt IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hm : ∀ (j : Fin nr) (r : Univ A R P K dd → Prop), rest r (rdTrack j) = bitVal PR.zero PR.one (bitAtOf RF.cell (m j) r)) (hnewk : ∀ (j : Fin nr), wk ≠ rdTrack j) (hnerg : ∀ (j : Fin nr), rg ≠ rdTrack j) {t₀ : W} {m₀ : I → Prop} (hm₀ : ∀ (r : Univ A R P K dd → Prop), rest r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r)) (hwkt₀ : wk ≠ t₀) (hrgt₀ : rg ≠ t₀) {a₀ aT : ι} (hbotI : ∀ (a : ι), a₀ ≤ a) (htopI : ∀ (a : ι), a ≤ aT) (xOf : ι → Fin nr → I) (f₀ : Q → A) (hname : ∀ (a : ι) (j : Fin nr), MatchOf j (elemFam setFlag initEl advEl rest v m xOf f₀ a j.castSucc) (PR.passTracksAt RF.cell (rdTrack j) rest (m j) (RF.cell (xOf a j)))) (huniq : ∀ (a : ι) (j : Fin nr) (r : Univ A R P K dd → Prop), MatchOf j (elemFam setFlag initEl advEl rest v m xOf f₀ a j.castSucc) (PR.passTracksAt RF.cell (rdTrack j) rest (m j) r) → r = RF.cell (xOf a j)) (hmaxT : IsMaxEl (elemFam setFlag initEl advEl rest v m xOf f₀ aT (Fin.last nr))) (hmaxF : ∀ a < aT, ¬IsMaxEl (elemFam setFlag initEl advEl rest v m xOf f₀ a (Fin.last nr))) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (emb ElemPh.e0) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (exitSt (elemFam setFlag initEl advEl rest v m xOf f₀ aT (Fin.last nr)) (rest v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }

The element loop's run at the generated family, the budget forgotten.

The tag-branched machinery's run, at the generated families

noncomputable def DescriptiveComplexity.Draw.tagFam {A R P Q W K : Type} {dd m : ℕ} {I : Type} (setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A) (rest : (Univ A R P K dd → Prop) → W → A) (v : Univ A R P K dd → Prop) (mT : Fin m → I → Prop) (xT : Fin m → I) (f₀ : Q → A) (i : Fin (m + 1)) : Q → A

The generated witness chain: the i-th prefix of the witness reads applied to the entry control, each one-hot bit the read's.

Equations

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

theorem DescriptiveComplexity.Draw.tagFam_congr_rest {A R P Q W K : Type} {dd m : ℕ} {I : Type} {setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A} {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {mT : Fin m → I → Prop} {rest' : (Univ A R P K dd → Prop) → W → A} (h : rest v = rest' v) (xT : Fin m → I) (f₀ : Q → A) (i : Fin (m + 1)) : tagFam setTagFlag rest v mT xT f₀ i = tagFam setTagFlag rest' v mT xT f₀ i

The witness chain reads its background at the working cell alone.

theorem DescriptiveComplexity.Draw.tag_reachesIn_iter {A R P Q W K T : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {m : ℕ} {nrOf : T → ℕ} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : TagPh m T nrOf → P} {rdTrackT : Fin m → W} {MatchT : Fin m → (Q → A) → (W → A) → Prop} {setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A} {TagsAre : T → (Q → A) → Prop} {rdTrackE : (τ : T) → Fin (nrOf τ) → W} {MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop} {setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A} {IsMaxEl : T → (Q → A) → Prop} {exitPh : P} {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {mT : Fin m → I → Prop} {rEmb : (i : TagSite m T nrOf) → TagSh m T nrOf i → R} (hrules : ∀ (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i), PR.rules (rEmb i ρ) = tagRule PR.one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hmT : ∀ (i : Fin m) (r : Univ A R P K dd → Prop), rest r (rdTrackT i) = bitVal PR.zero PR.one (bitAtOf RF.cell (mT i) r)) (hnewkT : ∀ (i : Fin m), wk ≠ rdTrackT i) (hnergT : ∀ (i : Fin m), rg ≠ rdTrackT i) {t₀ : W} {m₀ : I → Prop} (hm₀ : ∀ (r : Univ A R P K dd → Prop), rest r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r)) (hwkt₀ : wk ≠ t₀) (hrgt₀ : rg ≠ t₀) (xT : Fin m → I) (f₀ : Q → A) (hnameT : ∀ (i : Fin m), MatchT i (tagFam setTagFlag rest v mT xT f₀ i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) (RF.cell (xT i)))) (huniqT : ∀ (i : Fin m) (r : Univ A R P K dd → Prop), MatchT i (tagFam setTagFlag rest v mT xT f₀ i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) r) → r = RF.cell (xT i)) {τ : T} (hτ : TagsAre τ (tagFam setTagFlag rest v mT xT f₀ (Fin.last m))) {mE : Fin (nrOf τ) → I → Prop} (hmE : ∀ (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop), rest r (rdTrackE τ j) = bitVal PR.zero PR.one (bitAtOf RF.cell (mE j) r)) (hnewkE : ∀ (j : Fin (nrOf τ)), wk ≠ rdTrackE τ j) (hnergE : ∀ (j : Fin (nrOf τ)), rg ≠ rdTrackE τ j) {ι : Type} [LinearOrder ι] [Finite ι] {a₀ aT : ι} (hbotI : ∀ (a : ι), a₀ ≤ a) (htopI : ∀ (a : ι), a ≤ aT) (xE : ι → Fin (nrOf τ) → I) (hnameE : ∀ (a : ι) (j : Fin (nrOf τ)), MatchE τ j (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) (RF.cell (xE a j)))) (huniqE : ∀ (a : ι) (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop), MatchE τ j (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) r) → r = RF.cell (xE a j)) (hmaxT : IsMaxEl τ (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) aT (Fin.last (nrOf τ)))) (hmaxF : ∀ a < aT, ¬IsMaxEl τ (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) a (Fin.last (nrOf τ)))) (c : ℕ) (hcostT : ∀ (i : Fin m), 2 * (wideRank (RF.cell (xT i)) - wideRank v) + 2 ≤ c) (hcostE : ∀ (a : ι) (j : Fin (nrOf τ)), 2 * (wideRank (RF.cell (xE a j)) - wideRank v) + 2 ≤ c) : (wideData (Univ A R P K dd)).ReachesIn ((c + 2) * m + 2 + ((2 + (c + 2) * nrOf τ) * (Nat.card ι + 1) + 1)) { state := Sum.inr (PR.stElt (tagFirstRd emb) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (exitSt τ (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) aT (Fin.last (nrOf τ))) (rest v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }

The tag-branched machinery's run at the generated families, on a clock: the witness chain and the branch's element loop are both generated, so only the name guards, the branch decode and the exhaustion conditions are owed, and the cost is the chain's reads plus the branch's whole loop.

theorem DescriptiveComplexity.Draw.tag_run_iter {A R P Q W K T : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {m : ℕ} {nrOf : T → ℕ} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : TagPh m T nrOf → P} {rdTrackT : Fin m → W} {MatchT : Fin m → (Q → A) → (W → A) → Prop} {setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A} {TagsAre : T → (Q → A) → Prop} {rdTrackE : (τ : T) → Fin (nrOf τ) → W} {MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop} {setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A} {initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A} {IsMaxEl : T → (Q → A) → Prop} {exitPh : P} {rest : (Univ A R P K dd → Prop) → W → A} {v : Univ A R P K dd → Prop} {mT : Fin m → I → Prop} {rEmb : (i : TagSite m T nrOf) → TagSh m T nrOf i → R} (hrules : ∀ (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i), PR.rules (rEmb i ρ) = tagRule PR.one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkS : ∀ (r : Univ A R P K dd → Prop), rest r wk = bitVal PR.zero PR.one (r = v)) (hrg : ∀ (r : Univ A R P K dd → Prop), rest r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hmT : ∀ (i : Fin m) (r : Univ A R P K dd → Prop), rest r (rdTrackT i) = bitVal PR.zero PR.one (bitAtOf RF.cell (mT i) r)) (hnewkT : ∀ (i : Fin m), wk ≠ rdTrackT i) (hnergT : ∀ (i : Fin m), rg ≠ rdTrackT i) {t₀ : W} {m₀ : I → Prop} (hm₀ : ∀ (r : Univ A R P K dd → Prop), rest r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r)) (hwkt₀ : wk ≠ t₀) (hrgt₀ : rg ≠ t₀) (xT : Fin m → I) (f₀ : Q → A) (hnameT : ∀ (i : Fin m), MatchT i (tagFam setTagFlag rest v mT xT f₀ i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) (RF.cell (xT i)))) (huniqT : ∀ (i : Fin m) (r : Univ A R P K dd → Prop), MatchT i (tagFam setTagFlag rest v mT xT f₀ i.castSucc) (PR.passTracksAt RF.cell (rdTrackT i) rest (mT i) r) → r = RF.cell (xT i)) {τ : T} (hτ : TagsAre τ (tagFam setTagFlag rest v mT xT f₀ (Fin.last m))) {mE : Fin (nrOf τ) → I → Prop} (hmE : ∀ (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop), rest r (rdTrackE τ j) = bitVal PR.zero PR.one (bitAtOf RF.cell (mE j) r)) (hnewkE : ∀ (j : Fin (nrOf τ)), wk ≠ rdTrackE τ j) (hnergE : ∀ (j : Fin (nrOf τ)), rg ≠ rdTrackE τ j) {ι : Type} [LinearOrder ι] [Finite ι] {a₀ aT : ι} (hbotI : ∀ (a : ι), a₀ ≤ a) (htopI : ∀ (a : ι), a ≤ aT) (xE : ι → Fin (nrOf τ) → I) (hnameE : ∀ (a : ι) (j : Fin (nrOf τ)), MatchE τ j (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) (RF.cell (xE a j)))) (huniqE : ∀ (a : ι) (j : Fin (nrOf τ)) (r : Univ A R P K dd → Prop), MatchE τ j (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) a j.castSucc) (PR.passTracksAt RF.cell (rdTrackE τ j) rest (mE j) r) → r = RF.cell (xE a j)) (hmaxT : IsMaxEl τ (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) aT (Fin.last (nrOf τ)))) (hmaxF : ∀ a < aT, ¬IsMaxEl τ (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) a (Fin.last (nrOf τ)))) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (tagFirstRd emb) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (exitSt τ (elemFam (setFlagE τ) (initEl τ) (advEl τ) rest v mE xE (tagFam setTagFlag rest v mT xT f₀ (Fin.last m)) aT (Fin.last (nrOf τ))) (rest v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ rest m₀) (PR.syElt PR.blank) }

The tag-branched machinery's run at the generated families, the budget forgotten.

The tuple loop's run, at the generated families

noncomputable def DescriptiveComplexity.Draw.tupleIterD {I ι : Type} [LinearOrder ι] (mSrc : I → Prop) (xS xD : ι → I) (mD₀ : I → Prop) (a : ι) : I → Prop

The generated destination track: empty of the loop's bits at the bottom, each cover the round's copy applied.

Equations

• DescriptiveComplexity.Draw.tupleIterD mSrc xS xD mD₀ a = DescriptiveComplexity.Draw.iterOrd mD₀ (fun (a' : ι) (m : I → Prop) (y : I) => y = xD a' ∧ mSrc (xS a') ∨ y ≠ xD a' ∧ m y) a

noncomputable def DescriptiveComplexity.Draw.tupleIter0 {A R P Q W K : Type} {dd : ℕ} {I : Type} (setBit : Bool → (Q → A) → (W → A) → Q → A) (initLv advLv : (Q → A) → (W → A) → Q → A) {ι : Type} [LinearOrder ι] (mSrc : I → Prop) (v : Univ A R P K dd → Prop) (restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A) (xS xD : ι → I) (mD₀ : I → Prop) (f₀ : Q → A) (a : ι) : Q → A

The generated pre-store control: the loop's initLv at the bottom, each cover the previous round folded and advanced, the round's symbol read from the destination-dependent background.

Equations

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

noncomputable def DescriptiveComplexity.Draw.tupleIter1 {A R P Q W K : Type} {dd : ℕ} {I : Type} (setBit : Bool → (Q → A) → (W → A) → Q → A) (initLv advLv : (Q → A) → (W → A) → Q → A) {ι : Type} [LinearOrder ι] (mSrc : I → Prop) (v : Univ A R P K dd → Prop) (restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A) (xS xD : ι → I) (mD₀ : I → Prop) (f₀ : Q → A) (a : ι) : Q → A

The generated post-store control: the round's bit stored.

Equations

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

theorem DescriptiveComplexity.Draw.tupleIter0_congr_restF {A R P Q W K : Type} {dd : ℕ} {I : Type} {setBit : Bool → (Q → A) → (W → A) → Q → A} {initLv advLv : (Q → A) → (W → A) → Q → A} {ι : Type} [LinearOrder ι] {mSrc : I → Prop} {v : Univ A R P K dd → Prop} {restF restF' : (I → Prop) → (Univ A R P K dd → Prop) → W → A} (h : ∀ (m' : I → Prop), restF m' v = restF' m' v) (xS xD : ι → I) (mD₀ : I → Prop) (f₀ : Q → A) (a : ι) : tupleIter0 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a = tupleIter0 setBit initLv advLv mSrc v restF' xS xD mD₀ f₀ a

The copy loop reads its background at the working cell alone – at every destination content, the cell being the same one.

theorem DescriptiveComplexity.Draw.tupleIter1_congr_restF {A R P Q W K : Type} {dd : ℕ} {I : Type} {setBit : Bool → (Q → A) → (W → A) → Q → A} {initLv advLv : (Q → A) → (W → A) → Q → A} {ι : Type} [LinearOrder ι] {mSrc : I → Prop} {v : Univ A R P K dd → Prop} {restF restF' : (I → Prop) → (Univ A R P K dd → Prop) → W → A} (h : ∀ (m' : I → Prop), restF m' v = restF' m' v) (xS xD : ι → I) (mD₀ : I → Prop) (f₀ : Q → A) (a : ι) : tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a = tupleIter1 setBit initLv advLv mSrc v restF' xS xD mD₀ f₀ a

The same, after the round's store.

theorem DescriptiveComplexity.Draw.tuple_reachesIn_iter {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : ChainPh 3 TuplePS → P} {tSrc tDst : W} {MatchS MatchD : (Q → A) → (W → A) → Prop} {bitFlag : (Q → A) → Prop} {setBit : Bool → (Q → A) → (W → A) → Q → A} {initLv advLv : (Q → A) → (W → A) → Q → A} {IsMaxLv : (Q → A) → Prop} {exitPh : P} {ι : Type} [LinearOrder ι] [Finite ι] {mSrc : I → Prop} {v : Univ A R P K dd → Prop} {restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A} {rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R} (hrules : ∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i), PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {a₀ aT : ι} (hbotI : ∀ (a : ι), a₀ ≤ a) (htopI : ∀ (a : ι), a ≤ aT) (xS xD : ι → I) (mD₀ : I → Prop) (f₀ : Q → A) (hwkS : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r wk = bitVal PR.zero PR.one (r = v)) (hrg : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hsrc : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r tSrc = bitVal PR.zero PR.one (bitAtOf RF.cell mSrc r)) (hdst : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r tDst = bitVal PR.zero PR.one (bitAtOf RF.cell m' r)) (hoff : ∀ (m₁ m₂ : I → Prop) (r : Univ A R P K dd → Prop) (s : W), s ≠ tDst → restF m₁ r s = restF m₂ r s) (hwkSrc : wk ≠ tSrc) (hwkDst : wk ≠ tDst) (hrgSrc : rg ≠ tSrc) (hrgDst : rg ≠ tDst) (hnameS : ∀ (a : ι), MatchS (tupleIter0 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a)) mSrc (RF.cell (xS a)))) (huniqS : ∀ (a : ι) (r : Univ A R P K dd → Prop), MatchS (tupleIter0 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a)) mSrc r) → r = RF.cell (xS a)) (hnameD : ∀ (a : ι), MatchD (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ a)) (tupleIterD mSrc xS xD mD₀ a) (RF.cell (xD a)))) (huniqD : ∀ (a : ι) (r : Univ A R P K dd → Prop), MatchD (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ a)) (tupleIterD mSrc xS xD mD₀ a) r) → r = RF.cell (xD a)) (hbitFlag : ∀ (a : ι), bitFlag (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) ↔ mSrc (xS a)) (hmaxT : IsMaxLv (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ aT)) (hmaxF : ∀ a < aT, ¬IsMaxLv (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a)) (w : ℕ) (hcost : ∀ (a : ι), 2 * (wideRank (RF.cell (xS a)) - wideRank v) + 2 ≤ w ∧ 2 * (wideRank (RF.cell (xD a)) - wideRank v) + 2 ≤ w) : (wideData (Univ A R P K dd)).ReachesIn ((2 * w + 8) * (Nat.card ι + 1) + 1) { state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, ⋯⟩)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a₀)) mSrc) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ aT)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ aT)) (tuplePost mSrc (tupleIterD mSrc xS xD mD₀) xS xD aT)) (PR.syElt PR.blank) }

The tuple loop's run at the generated families, on a clock: only the name guards, the copied-bit read-back and the exhaustion conditions are owed, and the cost is a round's width once per tuple of the enumeration.

theorem DescriptiveComplexity.Draw.tuple_run_iter {A R P Q W K : Type} {dd : ℕ} [Fintype Q] [Fintype W] [DecidableEq W] [LinearOrder A] [LinearOrder R] [LinearOrder P] [LinearOrder K] [FirstOrder.Language.wide.Structure (Univ A R P K dd)] [Finite A] [Finite R] [Finite P] [Finite K] {PR : Prog A R P Q W K dd} {I : Type} {ile : I → I → Prop} (RF : IxFile (Univ A R P K dd) I ile) {wk rg : W} {emb : ChainPh 3 TuplePS → P} {tSrc tDst : W} {MatchS MatchD : (Q → A) → (W → A) → Prop} {bitFlag : (Q → A) → Prop} {setBit : Bool → (Q → A) → (W → A) → Q → A} {initLv advLv : (Q → A) → (W → A) → Q → A} {IsMaxLv : (Q → A) → Prop} {exitPh : P} {ι : Type} [LinearOrder ι] [Finite ι] {mSrc : I → Prop} {v : Univ A R P K dd → Prop} {restF : (I → Prop) → (Univ A R P K dd → Prop) → W → A} {rEmb : (i : ChainSite 3 TupleSS) → ChainSh 3 TupleSS TupleSh i → R} (hrules : ∀ (i : ChainSite 3 TupleSS) (ρ : ChainSh 3 TupleSS TupleSh i), PR.rules (rEmb i ρ) = tupleRule PR.zero PR.one wk rg emb tSrc tDst MatchS MatchD bitFlag setBit initLv advLv IsMaxLv exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) (hix : IsLinOrd ile) {gbot : I} (hbot : ∀ (y : I), ile gbot y) {v' : Univ A R P K dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') {a₀ aT : ι} (hbotI : ∀ (a : ι), a₀ ≤ a) (htopI : ∀ (a : ι), a ≤ aT) (xS xD : ι → I) (mD₀ : I → Prop) (f₀ : Q → A) (hwkS : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r wk = bitVal PR.zero PR.one (r = v)) (hrg : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r rg = bitVal PR.zero PR.one (∃ (u : I), r = RF.cell u)) (hsrc : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r tSrc = bitVal PR.zero PR.one (bitAtOf RF.cell mSrc r)) (hdst : ∀ (m' : I → Prop) (r : Univ A R P K dd → Prop), restF m' r tDst = bitVal PR.zero PR.one (bitAtOf RF.cell m' r)) (hoff : ∀ (m₁ m₂ : I → Prop) (r : Univ A R P K dd → Prop) (s : W), s ≠ tDst → restF m₁ r s = restF m₂ r s) (hwkSrc : wk ≠ tSrc) (hwkDst : wk ≠ tDst) (hrgSrc : rg ≠ tSrc) (hrgDst : rg ≠ tDst) (hnameS : ∀ (a : ι), MatchS (tupleIter0 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a)) mSrc (RF.cell (xS a)))) (huniqS : ∀ (a : ι) (r : Univ A R P K dd → Prop), MatchS (tupleIter0 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a)) mSrc r) → r = RF.cell (xS a)) (hnameD : ∀ (a : ι), MatchD (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ a)) (tupleIterD mSrc xS xD mD₀ a) (RF.cell (xD a)))) (huniqD : ∀ (a : ι) (r : Univ A R P K dd → Prop), MatchD (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) (PR.passTracksAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ a)) (tupleIterD mSrc xS xD mD₀ a) r) → r = RF.cell (xD a)) (hbitFlag : ∀ (a : ι), bitFlag (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a) ↔ mSrc (xS a)) (hmaxT : IsMaxLv (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ aT)) (hmaxF : ∀ a < aT, ¬IsMaxLv (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ a)) : Relation.ReflTransGen (wideData (Univ A R P K dd)).Step { state := Sum.inr (PR.stElt (emb (ChainPh.chk ⟨0, ⋯⟩)) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell tSrc (restF (tupleIterD mSrc xS xD mD₀ a₀)) mSrc) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh (tupleIter1 setBit initLv advLv mSrc v restF xS xD mD₀ f₀ aT)), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell tDst (restF (tupleIterD mSrc xS xD mD₀ aT)) (tuplePost mSrc (tupleIterD mSrc xS xD mD₀) xS xD aT)) (PR.syElt PR.blank) }

The tuple loop's run at the generated families, the budget forgotten.

The destination track, in closed form

theorem DescriptiveComplexity.Draw.tupleIterD_of_mem {I ι : Type} [LinearOrder ι] [Finite ι] {mSrc : I → Prop} {xS xD : ι → I} {mD₀ : I → Prop} (Q : I → Prop) (hxD : ∀ (a : ι), Q (xD a)) (h₀ : ∀ (y : I), mD₀ y → Q y) (b : ι) {y : I} (hy : tupleIterD mSrc xS xD mD₀ b y) : Q y

What the copy loop can hold: every cell of the destination track is either one the loop wrote – a destination cell of some round – or one it started with. A property of cells closed under both is therefore closed under the whole loop; that is how the target of a random access is known to be an address of argument cells alone.

theorem DescriptiveComplexity.Draw.tupleIterD_iff {I ι : Type} [LinearOrder ι] [Finite ι] {mSrc : I → Prop} {xS xD : ι → I} (hinj : ∀ (u u' : ι), xD u = xD u' → u = u') {mD₀ : I → Prop} (b : ι) (y : I) : tupleIterD mSrc xS xD mD₀ b y ↔ (∃ u < b, y = xD u ∧ mSrc (xS u)) ∨ (∀ u < b, y ≠ xD u) ∧ mD₀ y

What the copy loop has written: a cell holds a bit exactly when some earlier round wrote it – that round's source bit – or it held one from the start and no round has touched it. The destination cells being distinct is what makes the disjunction honest: a cell is written at most once.