α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 =>
    c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux
α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
⊢ destruct (join S) = Computation.bind (destruct S) destruct_join.aux
apply
  Computation.eq_of_bisim
    (fun c1 c2 =>
      c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux)
    _ (Or.inr ⟨S, rfl, rfl⟩)
α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux
⊢ Computation.BisimO
    (fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux)
    (Computation.destruct c1) (Computation.destruct c2)
α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 =>
    c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux
intro c1 c2 h
no goals
α : Type u
β : Type v
γ : Type w
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux
c : Computation (Option (α × WSeq α))
⊢ Computation.BisimO
    (fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux)
    (Computation.destruct c) (Computation.destruct c)
cases c.destruct <;> simp
case h3
α : Type u
β : Type v
γ : Type w
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux
S : WSeq (WSeq α)
⊢ (destruct (join S) =
      Computation.bind (destruct S) fun x =>
        match x with
        | none => Computation.pure none
        | some (s, S) => Computation.think (destruct (append s (join S)))) ∨
    ∃ S_1,
      destruct (join S) = destruct (join S_1) ∧
        (Computation.bind (destruct S) fun x =>
            match x with
            | none => Computation.pure none
            | some (s, S) => Computation.think (destruct (append s (join S)))) =
          Computation.bind (destruct S_1) fun x =>
            match x with
            | none => Computation.pure none
            | some (s, S) => Computation.think (destruct (append s (join S)))
α : Type u
β : Type v
γ : Type w
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux
S : WSeq (WSeq α)
⊢ Computation.BisimO
    (fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux)
    (Computation.destruct (destruct (join S))) (Computation.destruct (Computation.bind (destruct S) destruct_join.aux))
induction' S using WSeq.recOn with s S S <;> simp
no goals
case h3
α : Type u
β : Type v
γ : Type w
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = Computation.bind (destruct S) destruct_join.aux
S : WSeq (WSeq α)
⊢ (destruct (join S) =
      Computation.bind (destruct S) fun x =>
        match x with
        | none => Computation.pure none
        | some (s, S) => Computation.think (destruct (append s (join S)))) ∨
    ∃ S_1,
      destruct (join S) = destruct (join S_1) ∧
        (Computation.bind (destruct S) fun x =>
            match x with
            | none => Computation.pure none
            | some (s, S) => Computation.think (destruct (append s (join S)))) =
          Computation.bind (destruct S_1) fun x =>
            match x with
            | none => Computation.pure none
            | some (s, S) => Computation.think (destruct (append s (join S)))
refine' Or.inr ⟨S, rfl, rfl⟩