case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g

case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ (bind (bind s f) g = bind s fun x => bind (f x) g) ∨
    ∃ s_1, bind (bind s f) g = bind (bind s_1 f) g ∧ (bind s fun x => bind (f x) g) = bind s_1 fun x => bind (f x) g
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ bind (bind s f) g = bind s fun x => bind (f x) g
apply
  eq_of_bisim fun c₁ c₂ =>
    c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x : α => bind (f x) g
case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g) (destruct c₁)
    (destruct c₂)
case bisim
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
intro c₁ c₂ h
no goals
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂✝ : Computation γ
h : c₁ = c₂✝ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂✝ = bind s fun x => bind (f x) g
c₂ : Computation γ
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g) (destruct c₂)
    (destruct c₂)
cases' destruct c₂ with b cb <;> simp
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ : Computation α
s : α
⊢ match destruct (bind (f s) g), destruct (bind (f s) g) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = bind (bind s_1 f) g ∧ s' = bind s_1 fun x => bind (f x) g
  | x, x_1 => False

case h2
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ s : Computation α
⊢ (bind (bind s f) g = bind s fun x => bind (f x) g) ∨
    ∃ s_1, bind (bind s f) g = bind (bind s_1 f) g ∧ (bind s fun x => bind (f x) g) = bind s_1 fun x => bind (f x) g
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g)
    (destruct (bind (bind s f) g)) (destruct (bind s fun x => bind (f x) g))
apply recOn s <;> intro s <;> simp
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ : Computation α
s : α
fs : Computation β
⊢ match destruct (bind fs g), destruct (bind fs g) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = bind (bind s_1 f) g ∧ s' = bind s_1 fun x => bind (f x) g
  | x, x_1 => False
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ : Computation α
s : α
⊢ match destruct (bind (f s) g), destruct (bind (f s) g) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = bind (bind s_1 f) g ∧ s' = bind s_1 fun x => bind (f x) g
  | x, x_1 => False
generalize f s = fs
case h1.h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ : Computation α
s : α
fs : Computation β
t : β
⊢ match destruct (g t), destruct (g t) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = bind (bind s_1 f) g ∧ s' = bind s_1 fun x => bind (f x) g
  | x, x_1 => False
case h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ : Computation α
s : α
fs : Computation β
⊢ match destruct (bind fs g), destruct (bind fs g) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = bind (bind s_1 f) g ∧ s' = bind s_1 fun x => bind (f x) g
  | x, x_1 => False
apply recOn fs <;> intro t <;> simp
no goals
case h1.h1
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ : Computation α
s : α
fs : Computation β
t : β
⊢ match destruct (g t), destruct (g t) with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ s_1, s = bind (bind s_1 f) g ∧ s' = bind s_1 fun x => bind (f x) g
  | x, x_1 => False
cases' destruct (g t) with b cb <;> simp
no goals
case h2
α : Type u
β : Type v
γ : Type w
s✝¹ : Computation α
f : α → Computation β
g : β → Computation γ
c₁ c₂ : Computation γ
h : c₁ = c₂ ∨ ∃ s, c₁ = bind (bind s f) g ∧ c₂ = bind s fun x => bind (f x) g
s✝ s : Computation α
⊢ (bind (bind s f) g = bind s fun x => bind (f x) g) ∨
    ∃ s_1, bind (bind s f) g = bind (bind s_1 f) g ∧ (bind s fun x => bind (f x) g) = bind s_1 fun x => bind (f x) g
exact Or.inr ⟨s, rfl, rfl⟩
no goals
case r
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
g : β → Computation γ
⊢ (bind (bind s f) g = bind s fun x => bind (f x) g) ∨
    ∃ s_1, bind (bind s f) g = bind (bind s_1 f) g ∧ (bind s fun x => bind (f x) g) = bind s_1 fun x => bind (f x) g
exact Or.inr ⟨s, rfl, rfl⟩