case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)

case r
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ ∃ s_1,
    destruct (map f s) = destruct (map f s_1) ∧
      Computation.map (Option.map (Prod.map f (map f))) (destruct s) =
        Computation.map (Option.map (Prod.map f (map f))) (destruct s_1)
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ destruct (map f s) = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
apply
  Computation.eq_of_bisim fun c1 c2 =>
    ∃ s,
      c1 = destruct (map f s) ∧
        c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s))
    (Computation.destruct c1) (Computation.destruct c2)
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 =>
    ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
intro c1 c2 h
case bisim.intro
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s))
    (Computation.destruct c1) (Computation.destruct c2)
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s))
    (Computation.destruct c1) (Computation.destruct c2)
cases' h with s h
case bisim.intro
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s))
    (Computation.destruct (destruct (map f s)))
    (Computation.destruct (Computation.map (Option.map (Prod.map f (map f))) (destruct s)))
case bisim.intro
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s))
    (Computation.destruct c1) (Computation.destruct c2)
rw [h.left, h.right]
case bisim.intro.h3
α : Type u
β : Type v
γ : Type w
f : α → β
s✝¹ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s✝ : WSeq α
h✝ : c1 = destruct (map f s✝) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s✝)
s : WSeq α
h : c1 = destruct (map f (think s)) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct (think s))
⊢ ∃ s_1,
    destruct (map f s) = destruct (map f s_1) ∧
      Computation.map (Option.map (Prod.map f (map f))) (destruct s) =
        Computation.map (Option.map (Prod.map f (map f))) (destruct s_1)
case bisim.intro
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
⊢ Computation.BisimO
    (fun c1 c2 => ∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s))
    (Computation.destruct (destruct (map f s)))
    (Computation.destruct (Computation.map (Option.map (Prod.map f (map f))) (destruct s)))
induction' s using WSeq.recOn with a s s <;> simp
no goals
case bisim.intro.h3
α : Type u
β : Type v
γ : Type w
f : α → β
s✝¹ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s✝ : WSeq α
h✝ : c1 = destruct (map f s✝) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s✝)
s : WSeq α
h : c1 = destruct (map f (think s)) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct (think s))
⊢ ∃ s_1,
    destruct (map f s) = destruct (map f s_1) ∧
      Computation.map (Option.map (Prod.map f (map f))) (destruct s) =
        Computation.map (Option.map (Prod.map f (map f))) (destruct s_1)
exact ⟨s, rfl, rfl⟩
no goals
case r
α : Type u
β : Type v
γ : Type w
f : α → β
s : WSeq α
⊢ ∃ s_1,
    destruct (map f s) = destruct (map f s_1) ∧
      Computation.map (Option.map (Prod.map f (map f))) (destruct s) =
        Computation.map (Option.map (Prod.map f (map f))) (destruct s_1)
exact ⟨s, rfl, rfl⟩