α : Type u
β : Type v
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : Terminates c
⊢ ∀ (n : ℕ) (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : Terminates c
⊢ Terminates (parallel S)
suffices
  ∀ (n) (l : List (Computation α)) (S c),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
  from
  let ⟨n, h⟩ := h
  this n [] S c (Or.inr h) T
α : Type u
β : Type v
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : Terminates c
n : ℕ
⊢ ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : Terminates c
⊢ ∀ (n : ℕ) (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
intro n
case zero
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = Seq.get? S Nat.zero
T : Terminates c
⊢ Terminates (corec parallel.aux1 (l, S))

case succ
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = Seq.get? S (Nat.succ n)
T : Terminates c
⊢ Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
S : WSeq (Computation α)
c : Computation α
h : c ∈ S
T : Terminates c
n : ℕ
⊢ ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
induction' n with n IH <;> intro l S c o T
case zero.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : c ∈ l
⊢ Terminates (corec parallel.aux1 (l, S))

case zero.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Terminates (corec parallel.aux1 (l, S))
case zero
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = Seq.get? S Nat.zero
T : Terminates c
⊢ Terminates (corec parallel.aux1 (l, S))
cases' o with a a
case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = ?m.67113

case zero.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = ?m.67113
⊢ Terminates (corec parallel.aux1 (l, S))

case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ corec parallel.aux1 (l, S) = ?m.67144

case zero.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C : corec parallel.aux1 (l, S) = ?m.67144
⊢ Terminates (corec parallel.aux1 (l, S))
case zero.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
⊢ Terminates (corec parallel.aux1 (l, S))
induction' h : parallel.aux2 l with a l' <;> have C : corec parallel.aux1 (l, S) = _
no goals
case zero.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : c ∈ l
⊢ Terminates (corec parallel.aux1 (l, S))
exact terminates_parallel.aux a T
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Option.map (fun a' => (a', Seq.tail S)) (some (some c)) = some (some c, ?m.64769)

α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Stream'.Seq (Option (Computation α))
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Option.map (fun a' => (a', Seq.tail S)) (Seq.get? S 0) = some (some c, ?m.64769)
rw [← a]
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ (some c, Seq.tail S) = (some c, ?m.64769)

α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Stream'.Seq (Option (Computation α))
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Option.map (fun a' => (a', Seq.tail S)) (some (some c)) = some (some c, ?m.64769)

α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Stream'.Seq (Option (Computation α))
simp
no goals
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ (some c, Seq.tail S) = (some c, ?m.64769)

α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
⊢ Stream'.Seq (Option (Computation α))
rfl
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = ?m.67113
apply destruct_eq_pure
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (match (l, S) with
      | (l, S) =>
        rmap
          (fun l' =>
            match Seq.destruct S with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))
          (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
rw [corec_eq, parallel.aux1]
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (match (l, S) with
      | (l, S) =>
        rmap
          (fun l' =>
            match Seq.destruct S with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))
          (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
dsimp only []
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
rw [h]
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Sum.inl a = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
simp only [rmap]
no goals
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Sum.inl a = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
rfl
case zero.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
case zero.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (corec parallel.aux1 (l, S))
rw [C]
case zero.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
case zero.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
skip
no goals
case zero.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
infer_instance
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ corec parallel.aux1 (l, S) = ?m.67144
apply destruct_eq_think
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
simp [parallel.aux1]
no goals
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
rw [h, H]
case zero.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))))
case zero.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates (corec parallel.aux1 (l, S))
rw [C]
case zero.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (corec parallel.aux1
      (match some (some c, Seq.tail S) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case zero.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))))
refine @Computation.think_terminates _ _ ?_
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ c ∈ c :: l'
case zero.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (corec parallel.aux1
      (match some (some c, Seq.tail S) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
apply terminates_parallel.aux _ T
no goals
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S Nat.zero
H : Seq.destruct S = some (some c, Seq.tail S)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match some (some c, Seq.tail S) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ c ∈ c :: l'
simp
case succ.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : c ∈ l
⊢ Terminates (corec parallel.aux1 (l, S))

case succ.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
⊢ Terminates (corec parallel.aux1 (l, S))
case succ
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
o : c ∈ l ∨ some (some c) = Seq.get? S (Nat.succ n)
T : Terminates c
⊢ Terminates (corec parallel.aux1 (l, S))
cases' o with a a
case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = ?m.73525

case succ.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = ?m.73525
⊢ Terminates (corec parallel.aux1 (l, S))

case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ corec parallel.aux1 (l, S) = ?m.73556

case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C : corec parallel.aux1 (l, S) = ?m.73556
⊢ Terminates (corec parallel.aux1 (l, S))
case succ.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
⊢ Terminates (corec parallel.aux1 (l, S))
induction' h : parallel.aux2 l with a l' <;> have C : corec parallel.aux1 (l, S) = _
no goals
case succ.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : c ∈ l
⊢ Terminates (corec parallel.aux1 (l, S))
exact terminates_parallel.aux a T
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = ?m.73525
apply destruct_eq_pure
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (match (l, S) with
      | (l, S) =>
        rmap
          (fun l' =>
            match Seq.destruct S with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))
          (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
rw [corec_eq, parallel.aux1]
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (match (l, S) with
      | (l, S) =>
        rmap
          (fun l' =>
            match Seq.destruct S with
            | none => (l', Seq.nil)
            | some (none, S') => (l', S')
            | some (some c, S') => (c :: l', S'))
          (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
dsimp only []
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
rw [h]
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Sum.inl a = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ rmap (corec parallel.aux1)
      (rmap
        (fun l' =>
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (Sum.inl a)) =
    Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
simp only [rmap]
no goals
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Sum.inl a = Sum.inl ?C.a

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α

case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ α
rfl
case succ.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
case succ.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (corec parallel.aux1 (l, S))
rw [C]
case succ.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
case succ.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
skip
no goals
case succ.inr.inl
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a✝ : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
C : corec parallel.aux1 (l, S) = pure a
⊢ Terminates (pure a)
infer_instance
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
case C
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ corec parallel.aux1 (l, S) = ?m.73556
apply destruct_eq_think
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
simp [parallel.aux1]
no goals
case C.a
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (match
      match parallel.aux2 l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (match Seq.destruct S with
          | none => (b, Seq.nil)
          | some (none, S') => (b, S')
          | some (some c, S') => (c :: b, S')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (corec parallel.aux1 b)) =
    Sum.inr ?C.s'

case C.s'
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Computation α
rw [h]
case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))))
case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates (corec parallel.aux1 (l, S))
rw [C]
case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))))
refine @Computation.think_terminates _ _ ?_
case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) := by
  intro
  apply IH _ _ _ (Or.inr _) T
  rw [a]
  cases' S with f al
  rfl
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))

case succ.inr.inr.some
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case succ.inr.inr
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
induction' e : Seq.get? S 0 with o
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
l'✝ : List (Computation α)
⊢ Terminates (corec parallel.aux1 (l'✝, Seq.tail S))
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
intro
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
l'✝ : List (Computation α)
⊢ some (some c) = Seq.get? (Seq.tail S) n
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
l'✝ : List (Computation α)
⊢ Terminates (corec parallel.aux1 (l'✝, Seq.tail S))
apply IH _ _ _ (Or.inr _) T
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
l'✝ : List (Computation α)
⊢ Seq.get? S (Nat.succ n) = Seq.get? (Seq.tail S) n
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
l'✝ : List (Computation α)
⊢ some (some c) = Seq.get? (Seq.tail S) n
rw [a]
case mk
α : Type u
β : Type v
S : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
c : Computation α
T : Terminates c
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
l'✝ : List (Computation α)
f : Stream' (Option (Option (Computation α)))
al : IsSeq f
a : some (some c) = Seq.get? { val := f, property := al } (Nat.succ n)
C :
  corec parallel.aux1 (l, { val := f, property := al }) =
    think
      (corec parallel.aux1
        (match Seq.destruct { val := f, property := al } with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Seq.get? { val := f, property := al } (Nat.succ n) = Seq.get? (Seq.tail { val := f, property := al }) n
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
l'✝ : List (Computation α)
⊢ Seq.get? S (Nat.succ n) = Seq.get? (Seq.tail S) n
cases' S with f al
no goals
case mk
α : Type u
β : Type v
S : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
c : Computation α
T : Terminates c
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
l'✝ : List (Computation α)
f : Stream' (Option (Option (Computation α)))
al : IsSeq f
a : some (some c) = Seq.get? { val := f, property := al } (Nat.succ n)
C :
  corec parallel.aux1 (l, { val := f, property := al }) =
    think
      (corec parallel.aux1
        (match Seq.destruct { val := f, property := al } with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Seq.get? { val := f, property := al } (Nat.succ n) = Seq.get? (Seq.tail { val := f, property := al }) n
rfl
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
have D : Seq.destruct S = none := by
  dsimp [Seq.destruct]
  rw [e]
  rfl
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
⊢ Terminates
    (corec parallel.aux1
      (match none with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
rw [D]
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
⊢ Terminates (corec parallel.aux1 (l', Seq.nil))
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
⊢ Terminates
    (corec parallel.aux1
      (match none with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
simp [parallel.aux1]
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT✝ : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
TT : Terminates (corec parallel.aux1 (l', Seq.tail S))
⊢ Terminates (corec parallel.aux1 (l', Seq.nil))
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
⊢ Terminates (corec parallel.aux1 (l', Seq.nil))
have TT := TT l'
no goals
case succ.inr.inr.none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT✝ : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
D : Seq.destruct S = none
TT : Terminates (corec parallel.aux1 (l', Seq.tail S))
⊢ Terminates (corec parallel.aux1 (l', Seq.nil))
rwa [Seq.destruct_eq_nil D, Seq.tail_nil] at TT
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
⊢ Option.map (fun a' => (a', Seq.tail S)) (Seq.get? S 0) = none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
⊢ Seq.destruct S = none
dsimp [Seq.destruct]
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
⊢ Option.map (fun a' => (a', Seq.tail S)) none = none
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
⊢ Option.map (fun a' => (a', Seq.tail S)) (Seq.get? S 0) = none
rw [e]
no goals
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
e : Seq.get? S 0 = none
⊢ Option.map (fun a' => (a', Seq.tail S)) none = none
rfl
case succ.inr.inr.some
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
D : Seq.destruct S = some (o, Seq.tail S)
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case succ.inr.inr.some
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
have D : Seq.destruct S = some (o, S.tail) := by
  dsimp [Seq.destruct]
  rw [e]
  rfl
case succ.inr.inr.some
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
D : Seq.destruct S = some (o, Seq.tail S)
⊢ Terminates
    (corec parallel.aux1
      (match some (o, Seq.tail S) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case succ.inr.inr.some
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
D : Seq.destruct S = some (o, Seq.tail S)
⊢ Terminates
    (corec parallel.aux1
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
rw [D]
no goals
case succ.inr.inr.some
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
D : Seq.destruct S = some (o, Seq.tail S)
⊢ Terminates
    (corec parallel.aux1
      (match some (o, Seq.tail S) with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
cases' o with c <;> simp [parallel.aux1, TT]
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
⊢ Option.map (fun a' => (a', Seq.tail S)) (Seq.get? S 0) = some (o, Seq.tail S)
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
⊢ Seq.destruct S = some (o, Seq.tail S)
dsimp [Seq.destruct]
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
⊢ Option.map (fun a' => (a', Seq.tail S)) (some o) = some (o, Seq.tail S)
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
⊢ Option.map (fun a' => (a', Seq.tail S)) (Seq.get? S 0) = some (o, Seq.tail S)
rw [e]
no goals
α : Type u
β : Type v
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝¹ : c✝ ∈ S✝
T✝ : Terminates c✝
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = Seq.get? S n → Terminates c → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : Terminates c
a : some (some c) = Seq.get? S (Nat.succ n)
x✝¹ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝¹
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    think
      (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
TT : ∀ (l' : List (Computation α)), Terminates (corec parallel.aux1 (l', Seq.tail S))
x✝ : Option (Option (Computation α))
e✝ : Seq.get? S 0 = x✝
o : Option (Computation α)
e : Seq.get? S 0 = some o
⊢ Option.map (fun a' => (a', Seq.tail S)) (some o) = some (o, Seq.tail S)
rfl