theorem Std.Iterators.Types.Flatten.IsPlausibleStep.outerYield_flatMapM_pure {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ it₁' : Iter β} {it₂' : IterM m γ} {b : β} (h : it₁.IsPlausibleStep (IterStep.yield it₁' b)) (h' : MonadAttach.CanReturn (f b) it₂') :
(Iter.flatMapAfterM f it₁ none).IsPlausibleStep (IterStep.skip (Iter.flatMapAfterM f it₁' (some it₂')))
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.outerSkip_flatMapM_pure {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ it₁' : Iter β} (h : it₁.IsPlausibleStep (IterStep.skip it₁')) :
(Iter.flatMapAfterM f it₁ none).IsPlausibleStep (IterStep.skip (Iter.flatMapAfterM f it₁' none))
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.outerDone_flatMapM_pure {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : Iter β} (h : it₁.IsPlausibleStep IterStep.done) :
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.innerYield_flatMapM_pure {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : Iter β} {it₂ it₂' : IterM m γ} {b : γ} (h : it₂.IsPlausibleStep (IterStep.yield it₂' b)) :
(Iter.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.yield (Iter.flatMapAfterM f it₁ (some it₂')) b)
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.innerSkip_flatMapM_pure {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : Iter β} {it₂ it₂' : IterM m γ} (h : it₂.IsPlausibleStep (IterStep.skip it₂')) :
(Iter.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (Iter.flatMapAfterM f it₁ (some it₂')))
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.innerDone_flatMapM_pure {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : Iter β} {it₂ : IterM m γ} (h : it₂.IsPlausibleStep IterStep.done) :
(Iter.flatMapAfterM f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (Iter.flatMapAfterM f it₁ none))
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.outerYield_flatMap_pure {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ it₁' : Iter β} {b : β} (h : it₁.IsPlausibleStep (IterStep.yield it₁' b)) :
(Iter.flatMapAfter f it₁ none).IsPlausibleStep (IterStep.skip (Iter.flatMapAfter f it₁' (some (f b))))
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.outerSkip_flatMap_pure {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ it₁' : Iter β} (h : it₁.IsPlausibleStep (IterStep.skip it₁')) :
(Iter.flatMapAfter f it₁ none).IsPlausibleStep (IterStep.skip (Iter.flatMapAfter f it₁' none))
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.outerDone_flatMap_pure {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ : Iter β} (h : it₁.IsPlausibleStep IterStep.done) :
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.innerYield_flatMap_pure {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ : Iter β} {it₂ it₂' : Iter γ} {b : γ} (h : it₂.IsPlausibleStep (IterStep.yield it₂' b)) :
(Iter.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.yield (Iter.flatMapAfter f it₁ (some it₂')) b)
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.innerSkip_flatMap_pure {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ : Iter β} {it₂ it₂' : Iter γ} (h : it₂.IsPlausibleStep (IterStep.skip it₂')) :
(Iter.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (Iter.flatMapAfter f it₁ (some it₂')))
theorem Std.Iterators.Types.Flatten.IsPlausibleStep.innerDone_flatMap_pure {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ : Iter β} {it₂ : Iter γ} (h : it₂.IsPlausibleStep IterStep.done) :
(Iter.flatMapAfter f it₁ (some it₂)).IsPlausibleStep (IterStep.skip (Iter.flatMapAfter f it₁ none))
theorem Std.Iter.step_flatMapAfterM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : Iter β} {it₂ : Option (IterM m γ)} :
(flatMapAfterM f it₁ it₂).step = match hit : it₂ with
| none =>
match it₁.step with
| ⟨IterStep.yield it₁' b, h⟩ => do
let fx ← MonadAttach.attach (f b)
pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' (some fx.val)) ⋯))
| ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' it₂) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
| some it₂_1 => do
let __do_lift ← it₂_1.step
match __do_lift.inflate with
| ⟨IterStep.yield it₂' out, h⟩ =>
pure (Shrink.deflate (PlausibleIterStep.yield (flatMapAfterM f it₁ (some it₂')) out ⋯))
| ⟨IterStep.skip it₂', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁ (some it₂')) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁ none) ⋯))
theorem Std.Iter.step_flatMapM {α β α₂ γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ] {f : β → m (IterM m γ)} {it₁ : Iter β} :
(flatMapM f it₁).step = match it₁.step with
| ⟨IterStep.yield it₁' b, h⟩ => do
let fx ← MonadAttach.attach (f b)
pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' (some fx.val)) ⋯))
| ⟨IterStep.skip it₁', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (flatMapAfterM f it₁' none) ⋯))
| ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))
theorem Std.Iter.step_flatMapAfter {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ : Iter β} {it₂ : Option (Iter γ)} :
(flatMapAfter f it₁ it₂).step = match it₂ with
| none =>
match it₁.step with
| ⟨IterStep.yield it₁' b, h⟩ => PlausibleIterStep.skip (flatMapAfter f it₁' (some (f b))) ⋯
| ⟨IterStep.skip it₁', h⟩ => PlausibleIterStep.skip (flatMapAfter f it₁' none) ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯
| some it₂ =>
match it₂.step with
| ⟨IterStep.yield it₂' out, h⟩ => PlausibleIterStep.yield (flatMapAfter f it₁ (some it₂')) out ⋯
| ⟨IterStep.skip it₂', h⟩ => PlausibleIterStep.skip (flatMapAfter f it₁ (some it₂')) ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.skip (flatMapAfter f it₁ none) ⋯
theorem Std.Iter.step_flatMap {α β α₂ γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] {f : β → Iter γ} {it₁ : Iter β} :
(flatMap f it₁).step = match it₁.step with
| ⟨IterStep.yield it₁' b, h⟩ => PlausibleIterStep.skip (flatMapAfter f it₁' (some (f b))) ⋯
| ⟨IterStep.skip it₁', h⟩ => PlausibleIterStep.skip (flatMapAfter f it₁' none) ⋯
| ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯
theorem Std.Iter.toList_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ] [Iterators.Finite α Id] [Iterators.Finite α₂ m] {f : β → m (IterM m γ)} {it₁ : Iter β} {it₂ : Option (IterM m γ)} :
(flatMapAfterM f it₁ it₂).toList = match it₂ with
| none =>
List.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toList)
it₁).toList
| some it₂ => do
let __do_lift ← it₂.toList
let __do_lift_1 ←
List.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toList)
it₁).toList
pure (__do_lift ++ __do_lift_1)
theorem Std.Iter.toArray_flatMapAfterM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ] [Iterators.Finite α Id] [Iterators.Finite α₂ m] {f : β → m (IterM m γ)} {it₁ : Iter β} {it₂ : Option (IterM m γ)} :
(flatMapAfterM f it₁ it₂).toArray = match it₂ with
| none =>
Array.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toArray)
it₁).toArray
| some it₂ => do
let __do_lift ← it₂.toArray
let __do_lift_1 ←
Array.flatten <$> (mapM
(fun (b : β) => do
let __do_lift ← f b
__do_lift.toArray)
it₁).toArray
pure (__do_lift ++ __do_lift_1)
theorem Std.Iter.toList_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ] [Iterators.Finite α Id] [Iterators.Finite α₂ m] {f : β → m (IterM m γ)} {it₁ : Iter β} :
theorem Std.Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ] [Iterators.Finite α Id] [Iterators.Finite α₂ m] {f : β → m (IterM m γ)} {it₁ : Iter β} :
theorem Std.Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Iterators.Finite α Id] [Iterators.Finite α₂ Id] {f : β → Iter γ} {it₁ : Iter β} {it₂ : Option (Iter γ)} :
theorem Std.Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Iterators.Finite α Id] [Iterators.Finite α₂ Id] {f : β → Iter γ} {it₁ : Iter β} {it₂ : Option (Iter γ)} :
theorem Std.Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Iterators.Finite α Id] [Iterators.Finite α₂ Id] [Iterator α Id β] [Iterator α₂ Id γ] [Iterators.Finite α Id] [Iterators.Finite α₂ Id] {f : β → Iter γ} {it₁ : Iter β} :
theorem Std.Iter.toArray_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ] [Iterators.Finite α Id] [Iterators.Finite α₂ Id] [Iterator α Id β] [Iterator α₂ Id γ] [Iterators.Finite α Id] [Iterators.Finite α₂ Id] {f : β → Iter γ} {it₁ : Iter β} :