theorem
Std.Iter.step_append
{α₁ α₂ β : Type w}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
{it₁ : Iter β}
{it₂ : Iter β}
:
(it₁.append it₂).step = match it₁.step with
| ⟨IterStep.yield it₁' out, h⟩ => PlausibleIterStep.yield (it₁'.append it₂) out ⋯
| ⟨IterStep.skip it₁', h⟩ => PlausibleIterStep.skip (it₁'.append it₂) ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.skip (Intermediate.appendSnd α₁ it₂) ⋯
theorem
Std.Iter.Intermediate.step_appendSnd
{α₁ α₂ β : Type w}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
{it₂ : Iter β}
:
(appendSnd α₁ it₂).step = match it₂.step with
| ⟨IterStep.yield it₂' out, h⟩ => PlausibleIterStep.yield (appendSnd α₁ it₂') out ⋯
| ⟨IterStep.skip it₂', h⟩ => PlausibleIterStep.skip (appendSnd α₁ it₂') ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯
@[simp]
theorem
Std.Iter.atIdxSlow?_appendSnd
{α₁ α₂ β : Type w}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Iterators.Productive α₁ Id]
[Iterators.Productive α₂ Id]
{it₂ : Iter β}
{n : Nat}
:
theorem
Std.Iter.atIdxSlow?_append_of_eq_some
{α₁ α₂ β : Type w}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Iterators.Productive α₁ Id]
[Iterators.Productive α₂ Id]
{it₁ : Iter β}
{it₂ : Iter β}
{n : Nat}
{b : β}
(h : atIdxSlow? n it₁ = some b)
:
theorem
Std.Iter.atIdxSlow?_append
{α₁ α₂ β : Type w}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Iterators.Finite α₁ Id]
[Iterators.Productive α₂ Id]
{it₁ : Iter β}
{it₂ : Iter β}
{n : Nat}
:
atIdxSlow? n (it₁.append it₂) = if n < it₁.toList.length then atIdxSlow? n it₁ else atIdxSlow? (n - it₁.toList.length) it₂
theorem
Std.Iter.atIdxSlow?_append_of_productive
{α₁ α₂ β : Type w}
[Iterator α₁ Id β]
[Iterator α₂ Id β]
[Iterators.Productive α₁ Id]
[Iterators.Productive α₂ Id]
{it₁ : Iter β}
{it₂ : Iter β}
{n k : Nat}
(hk : atIdxSlow? k it₁ = none)
(hmin : ∀ (j : Nat), j < k → (atIdxSlow? j it₁).isSome = true)
(hle : k ≤ n)
: