The blocks of an address are the valuation the fold runs on

The join between the two halves of the sweep. DescriptiveComplexity.Problems.Wide.Blocks reads an address over a block-major universe as a family of blocks and says how that family changes along one increment; DescriptiveComplexity.Problems.Wide.Fold says how a quantifier prefix folds along one step of the lexicographic enumeration of its valuations. They are the same step, and this file says so:

with the block index type taken to be Fin n – which a reduction may simply choose, one index per variable of its kernel – the family of blocks DescriptiveComplexity.wmBlk s is a valuation, the value order is DescriptiveComplexity.WMSetLe, and every hypothesis the fold's three step rules ask for is read off DescriptiveComplexity.wmIncr_lexRel_iff.

So DescriptiveComplexity.foldFrom_carry_of_wmIncr is the fold rule at the carry index, stated about an address increment and nothing else – the form a program's step obligation will be discharged in. The blocks after the carry are full before the step and empty after it, which is exactly the fold's “maximal” and “minimal” hypotheses (DescriptiveComplexity.wmSetLe_of_full, DescriptiveComplexity.wmSetLe_of_empty), and the successor hypothesis is DescriptiveComplexity.wmSetLt_iff_of_wmIncr read through DescriptiveComplexity.wmLt_wmSetLe_iff.

def DescriptiveComplexity.mkAddr {n : ℕ} {V : Type} (p : Fin n → V → Prop) : Fin n × V → Prop

The address a family of blocks is. A program's configurations sit at addresses it has to build from the blocks it means them to have, which is the inverse of DescriptiveComplexity.wmBlk.

Equations

• DescriptiveComplexity.mkAddr p q = p q.1 q.2

@[simp]

theorem DescriptiveComplexity.wmBlk_mkAddr {n : ℕ} {V : Type} (p : Fin n → V → Prop) : wmBlk (mkAddr p) = p

@[simp]

theorem DescriptiveComplexity.mkAddr_wmBlk {n : ℕ} {V : Type} (s : Fin n × V → Prop) : mkAddr (wmBlk s) = s

The fold rule of an address increment

theorem DescriptiveComplexity.foldFrom_carry_of_wmIncr {n : ℕ} {V : Type} [Finite V] {LeV : V → V → Prop} {s s' : Fin n × V → Prop} {τ : Fin n} {pol : ℕ → Bool} {P : (Fin n → V → Prop) → Prop} (hV : IsLinOrd LeV) (hfull : ∀ (σ : Fin n), WMLt (fun (x1 x2 : Fin n) => x1 ≤ x2) τ σ → ∀ (v : V), wmBlk s σ v) (hincr : WMIncr LeV (wmBlk s τ) (wmBlk s' τ)) (hbefore : ∀ (σ : Fin n), WMLt (fun (x1 x2 : Fin n) => x1 ≤ x2) σ τ → ∀ (v : V), wmBlk s' σ v ↔ wmBlk s σ v) : foldFrom pol P (WMSetLe LeV) (↑τ) (wmBlk s') ↔ if pol ↑τ = true then foldFrom pol P (WMSetLe LeV) (↑τ) (wmBlk s) ∨ foldFrom pol P (WMSetLe LeV) (↑τ + 1) (wmBlk s') else foldFrom pol P (WMSetLe LeV) (↑τ) (wmBlk s) ∧ foldFrom pol P (WMSetLe LeV) (↑τ + 1) (wmBlk s')

The fold rule at the carry index of an address increment. The accumulator at the carry index absorbs the subtree the sweep has just finished – every deeper block having been full – and takes in the accumulator one level down, which is the new leaf. This is the step obligation of a one-pass program, with the address layer and the fold joined.