@[simp]

theorem Std.IterM.run_toList_mk' {α β : Type u} [Iterator α Id β] (a : α) : { internalState := a }.toList.run = { internalState := a }.toList

theorem Std.Iter.toArray_eq_toArray_toIterM {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toArray = it.toIterM.toArray.run

theorem Std.Iter.toList_eq_toList_toIterM {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toList = it.toIterM.toList.run

theorem Std.Iter.toListRev_eq_toListRev_toIterM {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toListRev = it.toIterM.toListRev.run

@[simp]

theorem Std.Iter.toArray_ensureTermination {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toArray = it.toArray

@[simp]

theorem Std.Iter.toList_ensureTermination {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toList = it.toList

@[simp]

theorem Std.Iter.toListRev_ensureTermination_eq_toListRev {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toListRev = it.toListRev

@[simp]

theorem Std.IterM.toArray_toIter {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : IterM Id β} : it.toIter.toArray = it.toArray.run

@[simp]

theorem Std.IterM.toList_toIter {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : IterM Id β} : it.toIter.toList = it.toList.run

@[simp]

theorem Std.IterM.toListRev_toIter {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : IterM Id β} : it.toIter.toListRev = it.toListRev.run

@[simp]

theorem Std.Iter.toList_toArray {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toArray.toList = it.toList

theorem Std.Iter.toList_toArray_ensureTermination {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toArray.toList = it.toList

@[simp]

theorem Std.Iter.toArray_toList {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toList.toArray = it.toArray

theorem Std.Iter.toArray_toList_ensureTermination {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toList.toArray = it.toArray

@[simp]

theorem Std.Iter.reverse_toListRev {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toListRev.reverse = it.toList

theorem Std.Iter.reverse_toListRev_ensureTermination {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toListRev.reverse = it.toList

theorem Std.Iter.toListRev_eq {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toListRev = it.toList.reverse

theorem Std.Iter.toListRev_ensureTermination {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toListRev = it.toList.reverse

theorem Std.Iter.toArray_eq_match_step {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toArray = match it.step.val with | IterStep.yield it' out => #[out] ++ it'.toArray | IterStep.skip it' => it'.toArray | IterStep.done => #[]

theorem Std.Iter.toArray_ensureTermination_eq_match_step {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toArray = match it.step.val with | IterStep.yield it' out => #[out] ++ it'.toArray | IterStep.skip it' => it'.toArray | IterStep.done => #[]

theorem Std.Iter.toList_eq_match_step {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toList = match it.step.val with | IterStep.yield it' out => out :: it'.toList | IterStep.skip it' => it'.toList | IterStep.done => []

theorem Std.Iter.toList_ensureTermination_eq_match_step {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toList = match it.step.val with | IterStep.yield it' out => out :: it'.toList | IterStep.skip it' => it'.toList | IterStep.done => []

theorem Std.Iter.toListRev_eq_match_step {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.toListRev = match it.step.val with | IterStep.yield it' out => it'.toListRev ++ [out] | IterStep.skip it' => it'.toListRev | IterStep.done => []

theorem Std.Iter.toListRev_ensureTermination_eq_match_step {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} : it.ensureTermination.toListRev = match it.step.val with | IterStep.yield it' out => it'.toListRev ++ [out] | IterStep.skip it' => it'.toListRev | IterStep.done => []

theorem Std.Iter.getElem?_toList_eq_atIdxSlow? {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} {k : Nat} : it.toList[k]? = atIdxSlow? k it

theorem Std.Iter.toList_eq_of_atIdxSlow?_eq {α₁ α₂ β : Type u_1} [Iterator α₁ Id β] [Iterators.Finite α₁ Id] [Iterator α₂ Id β] [Iterators.Finite α₂ Id] {it₁ : Iter β} {it₂ : Iter β} (h : ∀ (k : Nat), atIdxSlow? k it₁ = atIdxSlow? k it₂) : it₁.toList = it₂.toList

theorem Std.Iter.isPlausibleIndirectOutput_of_mem_toList {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} {b : β} : b ∈ it.toList → it.IsPlausibleIndirectOutput b

theorem Std.Iter.isPlausibleIndirectOutput_of_mem_toListRev {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} {b : β} : b ∈ it.toListRev → it.IsPlausibleIndirectOutput b

theorem Std.Iter.isPlausibleIndirectOutput_of_mem_toArray {α β : Type u_1} [Iterator α Id β] [Iterators.Finite α Id] {it : Iter β} {b : β} : b ∈ it.toArray → it.IsPlausibleIndirectOutput b