α : Type u
β : Type v
γ : Type w
f : α → β
s t : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
α : Type u
β : Type v
γ : Type w
f : α → β
s t : Seq α
⊢ map f (append s t) = append (map f s) (map f t)
apply
  eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _
    ⟨s, t, rfl, rfl⟩
α : Type u
β : Type v
γ : Type w
f : α → β
s t : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
⊢ BisimO (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) (destruct s1) (destruct s2)
α : Type u
β : Type v
γ : Type w
f : α → β
s t : Seq α
⊢ IsBisimulation fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
intro s1 s2 h
case h1
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t : Seq α
⊢ match destruct (map f t), destruct (map f t) with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t, s = map f (append s_1 t) ∧ s' = append (map f s_1) (map f t)
  | x, x_1 => False

case h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t : Seq α
⊢ α →
    ∀ (s : Seq α),
      ∃ s_1 t_1,
        map f (append s t) = map f (append s_1 t_1) ∧ append (map f s) (map f t) = append (map f s_1) (map f t_1)
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t : Seq α
⊢ BisimO (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) (destruct (map f (append s t)))
    (destruct (append (map f s) (map f t)))
apply recOn s <;> simp
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t : Seq α
⊢ α → ∀ (s : Seq α), ∃ s_1 t, map f s = map f (append s_1 t) ∧ map f s = append (map f s_1) (map f t)
case h1
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t : Seq α
⊢ match destruct (map f t), destruct (map f t) with
  | none, none => True
  | some (a, s), some (a', s') => a = a' ∧ ∃ s_1 t, s = map f (append s_1 t) ∧ s' = append (map f s_1) (map f t)
  | x, x_1 => False
apply recOn t <;> simp
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝¹ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ ∃ s t_1, map f t = map f (append s t_1) ∧ map f t = append (map f s) (map f t_1)
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t : Seq α
⊢ α → ∀ (s : Seq α), ∃ s_1 t, map f s = map f (append s_1 t) ∧ map f s = append (map f s_1) (map f t)
intro _ t
no goals
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝¹ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t✝ : Seq α
x✝ : α
t : Seq α
⊢ ∃ s t_1, map f t = map f (append s t_1) ∧ map f t = append (map f s) (map f t_1)
refine' ⟨nil, t, _, _⟩ <;> simp
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝¹ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s✝ t : Seq α
x✝ : α
s : Seq α
⊢ ∃ s_1 t_1, map f (append s t) = map f (append s_1 t_1) ∧ append (map f s) (map f t) = append (map f s_1) (map f t_1)
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s t : Seq α
⊢ α →
    ∀ (s : Seq α),
      ∃ s_1 t_1,
        map f (append s t) = map f (append s_1 t_1) ∧ append (map f s) (map f t) = append (map f s_1) (map f t_1)
intro _ s
no goals
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
s✝¹ t✝ : Seq α
s1 s2 : Seq β
h : ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)
s✝ t : Seq α
x✝ : α
s : Seq α
⊢ ∃ s_1 t_1, map f (append s t) = map f (append s_1 t_1) ∧ append (map f s) (map f t) = append (map f s_1) (map f t_1)
refine' ⟨s, t, rfl, rfl⟩