theorem Vector.get_eq_getElem {α : Type u_1} {n : ℕ} (v : Vector α n) (i : Fin n) : v.get i = v[↑i]

theorem Vector.get_replicate {α : Type u_1} {n : ℕ} (a : α) (i : Fin n) : (replicate n a).get i = a

instance instNeZeroNatMaxVal_biasedBisect (s t : ℕ+) : NeZero (max ↑s ↑t)

structure ΦComputer (s t : ℕ+) : Type

• hst : s ≤ t
• buffer : Vector ℕ ↑t
• next_δ : ℕ
• next_pos : Fin ↑t
• eqΦ (i : Fin ↑t) : self.buffer.get (self.next_pos - Fin.ofNat (↑t) 1 - i) = Φ s t (↑self.next_δ - 1 - ↑↑i)

def ΦComputer.init (s t : ℕ+) (hst : s ≤ t) : ΦComputer s t

Equations

• ΦComputer.init s t hst = { hst := hst, buffer := Vector.replicate (↑t) 1, next_δ := 0, next_pos := ⟨0, ⋯⟩, eqΦ := ⋯ }

theorem Fin.coe_sub_one' {n a : ℕ+} : Fin.ofNat ↑n ↑a - 1 = Fin.ofNat (↑n) (↑a - 1)

theorem Fin.coe_neg_one' {n : ℕ+} : ↑(-1) = ↑n - 1

structure ΦOutput (s t : ℕ+) : Type

• δ : ℕ
• Φδ : ℕ
• Φs : ℕ
• Φt : ℕ
• Φeq : Φ s t ↑self.δ = self.Φδ
• Φseq : Φ s t (↑self.δ - ↑↑s) = self.Φs
• Φteq : Φ s t (↑self.δ - ↑↑t) = self.Φt

def ΦComputer.next {s t : ℕ+} (input : ΦComputer s t) : ΦComputer s t × ΦOutput s t

Equations

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

theorem ΦComputer.next_succδ {s t : ℕ+} (input : ΦComputer s t) : input.next.1.next.2.δ = input.next.2.δ + 1

theorem ΦComputer.next_init {s t : ℕ+} (hst : s ≤ t) : (init s t hst).next.2.δ = 0

inductive ΦComputer' (s t : ℕ+) : Type

• st {s t : ℕ+} : ΦComputer s t → ΦComputer' s t
• ts {s t : ℕ+} : ΦComputer t s → ΦComputer' s t

def ΦComputer'.init (s t : ℕ+) : ΦComputer' s t

Equations

• ΦComputer'.init s t = if hst : s ≤ t then ΦComputer'.st (ΦComputer.init s t hst) else ΦComputer'.ts (ΦComputer.init t s ⋯)

def ΦComputer'.next {s t : ℕ+} (input : ΦComputer' s t) : ΦComputer' s t × ΦOutput s t

Equations

• (ΦComputer'.st cst).next = (ΦComputer'.st cst.next.1, cst.next.2)
• (ΦComputer'.ts cts).next = (ΦComputer'.ts cts.next.1, { δ := cts.next.2.δ, Φδ := cts.next.2.Φδ, Φs := cts.next.2.Φt, Φt := cts.next.2.Φs, Φeq := ⋯, Φseq := ⋯, Φteq := ⋯ })

theorem ΦComputer'.next_succδ {s t : ℕ+} (input : ΦComputer' s t) : input.next.1.next.2.δ = input.next.2.δ + 1

theorem ΦComputer'.next_init (s t : ℕ+) : (init s t).next.2.δ = 0

structure ΦOutputK (s t : ℕ+) (k : ℕ) : Type

• Φcomp : ΦComputer' s t
• Φout : ΦOutput s t
• hk : self.Φout.Φδ = nₖ (↑↑s) (↑↑t) (k + 1)
• hδ : self.Φcomp.next.2.δ = self.Φout.δ + 1
• hδₖ : ↑self.Φout.δ = δₖ_int s t k

@[irreducible]

def ΦComputer'.next_after {s t : ℕ+} (input : ΦComputer' s t) (δ : ℤ) (Φδ k : ℕ) (hΦ : Φδ = Φ s t δ) (hnext : ↑input.next.2.δ = δ + 1) (hnₖ : Φδ = nₖ (↑↑s) (↑↑t) k) : ΦOutputK s t k

Equations

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

structure nwComputer (s t : ℕ+) : Type

• Φcomp : ΦComputer' s t
• next_k : ℕ
• prev_nₖ : ℕ
• prev_δ : ℤ
• δ_agree : ↑self.Φcomp.next.2.δ = self.prev_δ + 1
• nₖ_δ_agree : self.prev_nₖ = Φ s t self.prev_δ
• nₖ_eq : self.prev_nₖ = nₖ (↑↑s) (↑↑t) self.next_k

def nwComputer.init (s t : ℕ+) : nwComputer s t

Equations

• nwComputer.init s t = { Φcomp := ΦComputer'.init s t, next_k := 0, prev_nₖ := 1, prev_δ := -1, δ_agree := ⋯, nₖ_δ_agree := ⋯, nₖ_eq := ⋯ }

structure nwOutput (s t : ℕ+) : Type

• k : ℕ
• δₖ_val : ℕ
• nₖ₁_val : ℕ
• wₖ₁_val : ℕ
• δₖ_eq : ↑self.δₖ_val = δₖ_int s t self.k
• nₖ_eq : self.nₖ₁_val = nₖ (↑↑s) (↑↑t) (self.k + 1)
• wₖ_eq : self.wₖ₁_val = wₖ (↑↑s) (↑↑t) (self.k + 1)

def nwComputer.next {s t : ℕ+} (input : nwComputer s t) : nwComputer s t × nwOutput s t

Equations

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

theorem nwComputer.next_succ {s t : ℕ+} (input : nwComputer s t) : input.next.1.next.2.k = input.next.2.k + 1

theorem nwComputer.next_init (s t : ℕ+) : (init s t).next.2.k = 0

structure bbComputer (s t : ℕ+) : Type

• nwComp : nwComputer s t
• next_n : ℕ
• next_En : ℕ
• k : ℕ
• left_nₖ : ℕ
• right_nₖ : ℕ
• left_wₖ : ℕ
• right_wₖ : ℕ
• curr_δₖ : ℕ
• En_eq : ↑self.next_En = E ↑↑s ↑↑t ↑self.next_n
• next_k : self.nwComp.next.2.k = self.k + 1
• n_left : self.left_nₖ ≤ self.next_n
• n_right : self.next_n < self.right_nₖ
• left_nₖ_eq : self.left_nₖ = nₖ (↑↑s) (↑↑t) self.k
• right_nₖ_eq : self.right_nₖ = nₖ (↑↑s) (↑↑t) (self.k + 1)
• left_wₖ_eq : self.left_wₖ = wₖ (↑↑s) (↑↑t) self.k
• right_wₖ_eq : self.right_wₖ = wₖ (↑↑s) (↑↑t) (self.k + 1)
• δₖ_eq : ↑self.curr_δₖ = δₖ_int s t self.k

def bbComputer.init (s t : ℕ+) : bbComputer s t

Equations

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

structure bbOutput (s t : ℕ+) : Type

• n : ℕ
• En : ℕ
• wₘᵢₙn : ℤ
• wₘₐₓn : ℤ
• wₗᵢn : ℚ
• En_eq : ↑self.En = Eℤ ↑↑s ↑↑t ↑self.n
• wₘᵢₙn_eq : self.wₘᵢₙn = wₘᵢₙℤ ↑↑s ↑↑t ↑self.n
• wₘₐₓn_eq : self.wₘₐₓn = wₘₐₓℤ ↑↑s ↑↑t ↑self.n
• wₗᵢn_eq : ↑self.wₗᵢn = wₗᵢ ↑↑s ↑↑t ↑self.n

def instReprBbOutput.repr {s✝ t✝ : ℕ+} : bbOutput s✝ t✝ → ℕ → Std.Format

Equations

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

instance instReprBbOutput {s✝ t✝ : ℕ+} : Repr (bbOutput s✝ t✝)

Equations

• instReprBbOutput = { reprPrec := instReprBbOutput.repr }

def bbComputer.next {s t : ℕ+} (input : bbComputer s t) : bbComputer s t × bbOutput s t

Equations

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

theorem bbComputer.next_succ {s t : ℕ+} (input : bbComputer s t) : input.next.1.next.2.n = input.next.2.n + 1

theorem bbComputer.next_init (s t : ℕ+) : (init s t).next.2.n = 1

@[irreducible]

def calculateBbList' (s t : ℕ+) (n : ℕ) (prev : Array (bbOutput s t)) (comp : bbComputer s t) : Array (bbOutput s t)

Equations

• calculateBbList' s t n prev comp = if n = 0 then prev else have next := comp.next; calculateBbList' s t (n - 1) (prev ++ [next.2]) next.1

def calculateBbList (s t : ℕ+) (n : ℕ) : Array (bbOutput s t)

Equations

• calculateBbList s t n = calculateBbList' s t n (Array.emptyWithCapacity n) (bbComputer.init s t)