Additivity of finite recursive block maps #
Splitting only reindexes coordinates. Induction therefore transfers the supplied fixed-seed addition laws through precisely the executed levels.
theorem
Algebraic.Cutwidth.Extractor.Internal.recursiveBlockMap_add
{X : Type v}
{Earlier : Type u}
{Fresh : ℕ → Type u}
{α : ℕ → Type w}
[Add X]
[(i : ℕ) → Add (α i)]
{t : ℕ}
(initial : X → Earlier → Fin t → α 0)
(C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1))
(n : ℕ)
(initial_add : ∀ (x x' : X) (y : Earlier), initial (x + x') y = initial x y + initial x' y)
(C_add : ∀ i < n, ∀ (a b : α i) (y : Fresh i), C i (a + b) y = C i a y + C i b y)
(x x' : X)
(seeds : RecursiveSeeds Earlier Fresh n)
:
recursiveBlockMap initial C n (x + x') seeds = recursiveBlockMap initial C n x seeds + recursiveBlockMap initial C n x' seeds
theorem
Algebraic.Cutwidth.Extractor.Internal.recursiveBlockExtractor_add
{X : Type v}
{Earlier : Type u}
{Fresh : ℕ → Type u}
{α : ℕ → Type w}
{Last : Type z}
{Ω : Type r}
[Add X]
[(i : ℕ) → Add (α i)]
[Add Ω]
(initial : X → Earlier → α 0)
(C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1))
(n : ℕ)
(E : α n → Last → Ω)
(initial_add : ∀ (x x' : X) (y : Earlier), initial (x + x') y = initial x y + initial x' y)
(C_add : ∀ i < n, ∀ (a b : α i) (y : Fresh i), C i (a + b) y = C i a y + C i b y)
(E_add : ∀ (a b : α n) (y : Last), E (a + b) y = E a y + E b y)
(x x' : X)
(seeds : RecursiveSeeds Earlier Fresh n × Last)
:
recursiveBlockExtractor initial C n E (x + x') seeds = recursiveBlockExtractor initial C n E x seeds + recursiveBlockExtractor initial C n E x' seeds