case a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ↑s₁ = ↑s₂
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ s₁ = s₂
apply Subtype.eq
case a.bisim
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ Stream'.IsBisimulation fun x y => ∃ s s', ↑s = x ∧ ↑s' = y ∧ R s s'

case a.a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
case a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ↑s₁ = ↑s₂
apply Stream'.eq_of_bisim fun x y => ∃ s s' : Computation α, s.1 = x ∧ s'.1 = y ∧ R s s'
case a.bisim
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∀ ⦃s₁ s₂ : Stream' (Option α)⦄,
    (∃ s s', ↑s = s₁ ∧ ↑s' = s₂ ∧ R s s') →
      Stream'.head s₁ = Stream'.head s₂ ∧ ∃ s s', ↑s = Stream'.tail s₁ ∧ ↑s' = Stream'.tail s₂ ∧ R s s'

case a.a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
case a.bisim
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ Stream'.IsBisimulation fun x y => ∃ s s', ↑s = x ∧ ↑s' = y ∧ R s s'

case a.a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
dsimp [Stream'.IsBisimulation]
case a.bisim
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
⊢ Stream'.head t₁ = Stream'.head t₂ ∧ ∃ s s', ↑s = Stream'.tail t₁ ∧ ↑s' = Stream'.tail t₂ ∧ R s s'

case a.a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
case a.bisim
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∀ ⦃s₁ s₂ : Stream' (Option α)⦄,
    (∃ s s', ↑s = s₁ ∧ ↑s' = s₂ ∧ R s s') →
      Stream'.head s₁ = Stream'.head s₂ ∧ ∃ s s', ↑s = Stream'.tail s₁ ∧ ↑s' = Stream'.tail s₂ ∧ R s s'

case a.a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
intro t₁ t₂ e
no goals
case a.a
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'
exact ⟨s₁, s₂, rfl, rfl, r⟩
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
⊢ head s = head s' ∧ R (tail s) (tail s')
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
⊢ Stream'.head ↑s = Stream'.head ↑s' ∧ ∃ s_1 s'_1, ↑s_1 = Stream'.tail ↑s ∧ ↑s'_1 = Stream'.tail ↑s' ∧ R s_1 s'_1
suffices head s = head s' ∧ R (tail s) (tail s') from
  And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
h : BisimO R (destruct s) (destruct s')
⊢ head s = head s' ∧ R (tail s) (tail s')
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
⊢ head s = head s' ∧ R (tail s) (tail s')
have h := bisim r
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
⊢ R s s' → BisimO R (destruct s) (destruct s') → head s = head s' ∧ R (tail s) (tail s')
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r : R s s'
h : BisimO R (destruct s) (destruct s')
⊢ head s = head s' ∧ R (tail s) (tail s')
revert r h
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (destruct (pure r')) (destruct (pure a'))
⊢ head (pure r') = head (pure a') ∧ R (tail (pure r')) (tail (pure a'))

α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') (think a')
h : BisimO R (destruct (pure r')) (destruct (think a'))
⊢ head (pure r') = head (think a') ∧ R (tail (pure r')) (tail (think a'))

α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R (think r') (pure a')
h : BisimO R (destruct (think r')) (destruct (pure a'))
⊢ head (think r') = head (pure a') ∧ R (tail (think r')) (tail (pure a'))

α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R (think r') (think a')
h : BisimO R (destruct (think r')) (destruct (think a'))
⊢ head (think r') = head (think a') ∧ R (tail (think r')) (tail (think a'))
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
⊢ R s s' → BisimO R (destruct s) (destruct s') → head s = head s' ∧ R (tail s) (tail s')
apply recOn s _ _ <;> intro r' <;> apply recOn s' _ _ <;> intro a' r h
case mk
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s' : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R { val := val✝, property := property✝ } s'
this : head { val := val✝, property := property✝ } = head s' ∧ R (tail { val := val✝, property := property✝ }) (tail s')
r : R (tail { val := val✝, property := property✝ }) (tail s')
⊢ ↑(tail { val := val✝, property := property✝ }) = Stream'.tail ↑{ val := val✝, property := property✝ }
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r✝ : R s s'
this : head s = head s' ∧ R (tail s) (tail s')
r : R (tail s) (tail s')
⊢ ↑(tail s) = Stream'.tail ↑s
cases s
no goals
case mk
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s' : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R { val := val✝, property := property✝ } s'
this : head { val := val✝, property := property✝ } = head s' ∧ R (tail { val := val✝, property := property✝ }) (tail s')
r : R (tail { val := val✝, property := property✝ }) (tail s')
⊢ ↑(tail { val := val✝, property := property✝ }) = Stream'.tail ↑{ val := val✝, property := property✝ }
rfl
case mk
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R s { val := val✝, property := property✝ }
this : head s = head { val := val✝, property := property✝ } ∧ R (tail s) (tail { val := val✝, property := property✝ })
r : R (tail s) (tail { val := val✝, property := property✝ })
⊢ ↑(tail { val := val✝, property := property✝ }) = Stream'.tail ↑{ val := val✝, property := property✝ }
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r✝ : R s s'
this : head s = head s' ∧ R (tail s) (tail s')
r : R (tail s) (tail s')
⊢ ↑(tail s') = Stream'.tail ↑s'
cases s'
no goals
case mk
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s : Computation α
val✝ : Stream' (Option α)
property✝ : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val✝ n = some a → val✝ (n + 1) = some a
r✝ : R s { val := val✝, property := property✝ }
this : head s = head { val := val✝, property := property✝ } ∧ R (tail s) (tail { val := val✝, property := property✝ })
r : R (tail s) (tail { val := val✝, property := property✝ })
⊢ ↑(tail { val := val✝, property := property✝ }) = Stream'.tail ↑{ val := val✝, property := property✝ }
rfl
case left
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ head (pure r') = head (pure a')

case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ R (tail (pure r')) (tail (pure a'))
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : BisimO R (destruct (pure r')) (destruct (pure a'))
⊢ head (pure r') = head (pure a') ∧ R (tail (pure r')) (tail (pure a'))
constructor <;> dsimp at h
case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ R (tail (pure r')) (tail (pure a'))
case left
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ head (pure r') = head (pure a')

case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ R (tail (pure r')) (tail (pure a'))
. rw [h]
no goals
case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ R (tail (pure r')) (tail (pure a'))
. rw [h] at r
  rw [tail_pure, tail_pure,h]
  assumption
no goals
case left
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ head (pure r') = head (pure a')
rw [h]
case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (tail (pure r')) (tail (pure a'))
case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
h : r' = a'
⊢ R (tail (pure r')) (tail (pure a'))
rw [h] at r
case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')
case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (tail (pure r')) (tail (pure a'))
rw [tail_pure, tail_pure,h]
no goals
case right
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure a') (pure a')
h : r' = a'
⊢ R (pure a') (pure a')
assumption
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') (think a')
h : BisimO R (Sum.inl r') (Sum.inr a')
⊢ head (pure r') = head (think a') ∧ R (tail (pure r')) (tail (think a'))
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') (think a')
h : BisimO R (destruct (pure r')) (destruct (think a'))
⊢ head (pure r') = head (think a') ∧ R (tail (pure r')) (tail (think a'))
rw [destruct_pure, destruct_think] at h
no goals
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') (think a')
h : BisimO R (Sum.inl r') (Sum.inr a')
⊢ head (pure r') = head (think a') ∧ R (tail (pure r')) (tail (think a'))
exact False.elim h
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R (think r') (pure a')
h : BisimO R (Sum.inr r') (Sum.inl a')
⊢ head (think r') = head (pure a') ∧ R (tail (think r')) (tail (pure a'))
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R (think r') (pure a')
h : BisimO R (destruct (think r')) (destruct (pure a'))
⊢ head (think r') = head (pure a') ∧ R (tail (think r')) (tail (pure a'))
rw [destruct_pure, destruct_think] at h
no goals
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R (think r') (pure a')
h : BisimO R (Sum.inr r') (Sum.inl a')
⊢ head (think r') = head (pure a') ∧ R (tail (think r')) (tail (pure a'))
exact False.elim h
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R (think r') (think a')
h : R r' a'
⊢ head (think r') = head (think a') ∧ R (tail (think r')) (tail (think a'))
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R (think r') (think a')
h : BisimO R (destruct (think r')) (destruct (think a'))
⊢ head (think r') = head (think a') ∧ R (tail (think r')) (tail (think a'))
simp at h
no goals
α : Type u
β : Type v
γ : Type w
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R (think r') (think a')
h : R r' a'
⊢ head (think r') = head (think a') ∧ R (tail (think r')) (tail (think a'))
simp [*]