α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S))
have lem1 :
  ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) := by
  intro l S e
  cases' e with a e
  have : corec parallel.aux1 (l, S) = return a := by
    apply destruct_eq_pure
    simp [parallel.aux1]
    rw [e]
  rw [this]
  exact ret_terminates a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
T : Terminates c
⊢ Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)} {c : Computation α},
    c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S))
intro l S c m T
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, c ∈ l → Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
T : Terminates c
⊢ Terminates (corec parallel.aux1 (l, S))
revert l S
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
⊢ ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → Terminates (corec parallel.aux1 (l, S))

α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
⊢ ∀ (s : Computation α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, think s ∈ l → Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, c ∈ l → Terminates (corec parallel.aux1 (l, S))
apply @terminatesRecOn _ _ c T _ _
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
e : ∃ a, parallel.aux2 l = Sum.inl a
⊢ Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
⊢ ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
intro l S e
case intro
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
e : ∃ a, parallel.aux2 l = Sum.inl a
⊢ Terminates (corec parallel.aux1 (l, S))
cases' e with a e
case intro
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ Terminates (corec parallel.aux1 (l, S))
case intro
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ Terminates (corec parallel.aux1 (l, S))
have : corec parallel.aux1 (l, S) = return a := by
  apply destruct_eq_pure
  simp [parallel.aux1]
  rw [e]
case intro
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ Terminates (Pure.pure a)
case intro
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ Terminates (corec parallel.aux1 (l, S))
rw [this]
no goals
case intro
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
this : corec parallel.aux1 (l, S) = Pure.pure a
⊢ Terminates (Pure.pure a)
exact ret_terminates a
case a
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inl a
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ corec parallel.aux1 (l, S) = Pure.pure a
apply destruct_eq_pure
case a
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (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
          (fun x =>
            match parallel.aux2 x.fst with
            | Sum.inl a => Sum.inl a
            | Sum.inr b =>
              Sum.inr
                (match Seq.destruct x.snd with
                | none => (b, Seq.nil)
                | some (none, S') => (b, S')
                | some (some c, S') => (c :: b, S')))
          b)) =
    Sum.inl a
case a
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ destruct (corec parallel.aux1 (l, S)) = Sum.inl a
simp [parallel.aux1]
no goals
case a
α : Type u
β : Type v
l : List (Computation α)
S : WSeq (Computation α)
a : α
e : parallel.aux2 l = Sum.inl a
⊢ (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
          (fun x =>
            match parallel.aux2 x.fst with
            | Sum.inl a => Sum.inl a
            | Sum.inr b =>
              Sum.inr
                (match Seq.destruct x.snd with
                | none => (b, Seq.nil)
                | some (none, S') => (b, S')
                | some (some c, S') => (c :: b, S')))
          b)) =
    Sum.inl a
rw [e]
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
⊢ ∀ (a : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → Terminates (corec parallel.aux1 (l, S))
intro a l S m
case a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 l = Sum.inl a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ Terminates (corec parallel.aux1 (l, S))
apply lem1
case a.cons
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a = c ∨ pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
case a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
a : α
l : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 l = Sum.inl a
induction' l with c l IH <;> simp at m
case a.cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a

case a.cons.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
case a.cons
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a = c ∨ pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
cases' m with e m
case a.cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a_1, parallel.aux2 (pure a :: l) = Sum.inl a_1
case a.cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
rw [← e]
case a.cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a_1,
    (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => Sum.inl a) =
      Sum.inl a_1
case a.cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a_1, parallel.aux2 (pure a :: l) = Sum.inl a_1
simp [parallel.aux2]
case a.cons.inl.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
a' : α
⊢ ∃ a_1,
    (match Sum.inl a' with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => Sum.inl a) =
      Sum.inl a_1

case a.cons.inl.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
ls : List (Computation α)
⊢ ∃ a_1,
    (match Sum.inr ls with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => Sum.inl a) =
      Sum.inl a_1
case a.cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
⊢ ∃ a_1,
    (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => Sum.inl a) =
      Sum.inl a_1
cases' List.foldr (fun c o =>
  match o with
  | Sum.inl a => Sum.inl a
  | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c)) (Sum.inr List.nil) l with a' ls
no goals
case a.cons.inl.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
a' : α
⊢ ∃ a_1,
    (match Sum.inl a' with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => Sum.inl a) =
      Sum.inl a_1

case a.cons.inl.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
ls : List (Computation α)
⊢ ∃ a_1,
    (match Sum.inr ls with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls => Sum.inl a) =
      Sum.inl a_1
exacts [⟨a', rfl⟩, ⟨a, rfl⟩]
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e : parallel.aux2 l = Sum.inl a'
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
case a.cons.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
cases' IH m with a' e
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e : parallel.aux2 l = Sum.inl a'
⊢ ∃ a,
    (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct c with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e : parallel.aux2 l = Sum.inl a'
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a
simp [parallel.aux2]
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match destruct c with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ ∃ a,
    (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct c with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e : parallel.aux2 l = Sum.inl a'
⊢ ∃ a,
    (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct c with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a
simp [parallel.aux2] at e
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match destruct c with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ ∃ a,
    (match Sum.inl a' with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct c with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match destruct c with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ ∃ a,
    (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct c with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a
rw [e]
no goals
case a.cons.inr.intro
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
a : α
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : pure a ∈ l✝
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ l
a' : α
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match destruct c with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a'
⊢ ∃ a,
    (match Sum.inl a' with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct c with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inl a
exact ⟨a', rfl⟩
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
⊢ Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
⊢ ∀ (s : Computation α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, think s ∈ l → Terminates (corec parallel.aux1 (l, S))
intro s IH l S m
case inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Terminates (corec parallel.aux1 (l, S))

case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Terminates (corec parallel.aux1 (l, S))
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
⊢ Terminates (corec parallel.aux1 (l, S))
induction' h : parallel.aux2 l with a l'
case cons
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
m : think s = c ∨ think s ∈ l
⊢ s ∈ l'
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
⊢ ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
induction' l with c l IH' <;> intro l' e' <;> simp at m
case cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match destruct c with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : think s = c
⊢ s ∈ l'

case cons.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match destruct c with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
m : think s ∈ l
⊢ s ∈ l'
case cons
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' : parallel.aux2 (c :: l) = Sum.inr l'
m : think s = c ∨ think s ∈ l
⊢ s ∈ l'
cases' m with e m <;> simp [parallel.aux2] at e'
case cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match destruct c with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct (think s) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : think s = c
⊢ s ∈ l'
case cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match destruct c with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : think s = c
⊢ s ∈ l'
rw [← e] at e'
case cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : think s = c
⊢ (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct (think s) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inr l' →
    s ∈ l'
case cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match destruct c with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct (think s) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e : think s = c
⊢ s ∈ l'
revert e'
case cons.inl.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : think s = c
ls : List (Computation α)
e' : tail (think s) :: ls = l'
⊢ s ∈ l'
case cons.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : think s = c
⊢ (match
        List.foldr
          (fun c o =>
            match o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match destruct c with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match destruct (think s) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inr l' →
    s ∈ l'
cases' List.foldr (fun c o =>
    match o with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
  (Sum.inr []) l with a' ls <;> intro e' <;> [injection e'; injection e' with e']
case cons.inl.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : think s = c
ls : List (Computation α)
e' : tail (think s) :: ls = l'
⊢ s ∈ tail (think s) :: ls
case cons.inl.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : think s = c
ls : List (Computation α)
e' : tail (think s) :: ls = l'
⊢ s ∈ l'
rw [← e']
no goals
case cons.inl.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : think s = c
ls : List (Computation α)
e' : tail (think s) :: ls = l'
⊢ s ∈ tail (think s) :: ls
simp
case cons.inr.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
a' : α
e' :
  (match Sum.inl a' with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inl a'
⊢ s ∈ l'

case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
⊢ s ∈ l'
case cons.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e' :
  (match
      List.foldr
        (fun c o =>
          match o with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match destruct c with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls))
        (Sum.inr []) l with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
m : think s ∈ l
⊢ s ∈ l'
induction' e : List.foldr (fun c o =>
    match o with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
  (Sum.inr List.nil) l with a' ls <;> erw [e] at e'
case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ s ∈ l'
case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
⊢ s ∈ l'
have := IH' m _ e
case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e' :
  (match destruct c with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ s ∈ l'
case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e' :
  (match Sum.inr ls with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ s ∈ l'
simp [parallel.aux2] at e'
case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ (match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inr l' →
    s ∈ l'
case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e' :
  (match destruct c with
    | Sum.inl a => Sum.inl a
    | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ s ∈ l'
revert e'
case cons.inr.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
val✝ : Computation α
h' : val✝ :: ls = l'
⊢ s ∈ l'
case cons.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
⊢ (match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
      Sum.inr l' →
    s ∈ l'
cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
case cons.inr.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
val✝ : Computation α
h' : val✝ :: ls = l'
⊢ s ∈ val✝ :: ls
case cons.inr.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
val✝ : Computation α
h' : val✝ :: ls = l'
⊢ s ∈ l'
rw [← h']
no goals
case cons.inr.inr.inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
ls : List (Computation α)
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inr ls
this : s ∈ ls
val✝ : Computation α
h' : val✝ :: ls = l'
⊢ s ∈ val✝ :: ls
simp [this]
no goals
case cons.inr.inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c✝ : Computation α
T : Terminates c✝
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l✝ : List (Computation α)
S : WSeq (Computation α)
m✝ : think s ∈ l✝
c : Computation α
l : List (Computation α)
IH' : think s ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
m : think s ∈ l
x✝ : α ⊕ List (Computation α)
e✝ :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    x✝
a' : α
e' :
  (match Sum.inl a' with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match destruct c with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls)) =
    Sum.inr l'
e :
  List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
      (Sum.inr []) l =
    Sum.inl a'
⊢ s ∈ l'
contradiction
no goals
case inl
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
a : α
h : parallel.aux2 l = Sum.inl a
⊢ Terminates (corec parallel.aux1 (l, S))
exact lem1 _ _ ⟨a, h⟩
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (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))
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ Terminates (corec parallel.aux1 (l, S))
have H2 : corec parallel.aux1 (l, S) = think _ := by
  apply destruct_eq_think
  simp [parallel.aux1]
  rw [h]
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))))
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (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 [H2]
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (corec
      (fun x =>
        match parallel.aux2 x.fst with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (match Seq.destruct x.snd with
            | none => (b, Seq.nil)
            | some (none, S') => (b, S')
            | some (some c, S') => (c :: b, S')))
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (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 inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
this : s ∈ l'
⊢ Terminates
    (corec
      (fun x =>
        match parallel.aux2 x.fst with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (match Seq.destruct x.snd with
            | none => (b, Seq.nil)
            | some (none, S') => (b, S')
            | some (some c, S') => (c :: b, S')))
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
⊢ Terminates
    (corec
      (fun x =>
        match parallel.aux2 x.fst with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (match Seq.destruct x.snd with
            | none => (b, Seq.nil)
            | some (none, S') => (b, S')
            | some (some c, S') => (c :: b, S')))
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
have := H1 _ h
no goals
case inr
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    think
      (corec
        (fun x =>
          match parallel.aux2 x.fst with
          | Sum.inl a => Sum.inl a
          | Sum.inr b =>
            Sum.inr
              (match Seq.destruct x.snd with
              | none => (b, Seq.nil)
              | some (none, S') => (b, S')
              | some (some c, S') => (c :: b, S')))
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S')))
this : s ∈ l'
⊢ Terminates
    (corec
      (fun x =>
        match parallel.aux2 x.fst with
        | Sum.inl a => Sum.inl a
        | Sum.inr b =>
          Sum.inr
            (match Seq.destruct x.snd with
            | none => (b, Seq.nil)
            | some (none, S') => (b, S')
            | some (some c, S') => (c :: b, S')))
      (match Seq.destruct S with
      | none => (l', Seq.nil)
      | some (none, S') => (l', S')
      | some (some c, S') => (c :: l', S')))
rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> simp [parallel.aux1] <;> apply IH <;>
  simp [this]
case a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
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 ?m.51261
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
x✝ : α ⊕ List (Computation α)
h✝ : parallel.aux2 l = x✝
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ corec parallel.aux1 (l, S) = think ?m.51261
apply destruct_eq_think
case a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
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
          (fun x =>
            match parallel.aux2 x.fst with
            | Sum.inl a => Sum.inl a
            | Sum.inr b =>
              Sum.inr
                (match Seq.destruct x.snd with
                | none => (b, Seq.nil)
                | some (none, S') => (b, S')
                | some (some c, S') => (c :: b, S')))
          b)) =
    Sum.inr ?m.51261
case a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
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 ?m.51261
simp [parallel.aux1]
no goals
case a
α : Type u
β : Type v
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S))
c : Computation α
T : Terminates c
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → Terminates (corec parallel.aux1 (l, S))
l : List (Computation α)
S : WSeq (Computation α)
m : think s ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
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
          (fun x =>
            match parallel.aux2 x.fst with
            | Sum.inl a => Sum.inl a
            | Sum.inr b =>
              Sum.inr
                (match Seq.destruct x.snd with
                | none => (b, Seq.nil)
                | some (none, S') => (b, S')
                | some (some c, S') => (c :: b, S')))
          b)) =
    Sum.inr ?m.51261
rw [h]