case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 => ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))

case r
α : Type u
β : Type v
γ : Type w
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f (join S) = append s (map f (join S_1)) ∧ join (map (map f) S) = append s (join (map (map f) S_1))
α : Type u
β : Type v
γ : Type w
f : α → β
S : WSeq (WSeq α)
⊢ map f (join S) = join (map (map f) S)
apply
  Seq.eq_of_bisim fun s1 s2 =>
    ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
S : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
⊢ Seq.BisimO (fun s1 s2 => ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S)))
    (Seq.destruct s1) (Seq.destruct s2)
case bisim
α : Type u
β : Type v
γ : Type w
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 => ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
intro s1 s2 h
case h1
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
⊢ match Seq.destruct (map f (join S)), Seq.destruct (join (map (map f) S)) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (map f (join S)) ∧ s' = append s_1 (join (map (map f) S))
  | x, x_1 => False

case h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
a : β
s : WSeq β
⊢ ∃ s_1 S_1,
    append s (map f (join S)) = append s_1 (map f (join S_1)) ∧
      append s (join (map (map f) S)) = append s_1 (join (map (map f) S_1))

case h3
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
s : WSeq β
⊢ ∃ s_1 S_1,
    append s (map f (join S)) = append s_1 (map f (join S_1)) ∧
      append s (join (map (map f) S)) = append s_1 (join (map (map f) S_1))
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
s : WSeq β
S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 => ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S)))
    (Seq.destruct (append s (map f (join S)))) (Seq.destruct (append s (join (map (map f) S))))
induction' s using WSeq.recOn with a s s <;> simp
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1,
    append (map f s) (map f (join S)) = append s_1 (map f (join S_1)) ∧
      append (map f s) (join (map (map f) S)) = append s_1 (join (map (map f) S_1))

case h1.h3
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f (join S) = append s (map f (join S_1)) ∧ join (map (map f) S) = append s (join (map (map f) S_1))
case h1
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
⊢ match Seq.destruct (map f (join S)), Seq.destruct (join (map (map f) S)) with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧ ∃ s_1 S, s = append s_1 (map f (join S)) ∧ s' = append s_1 (join (map (map f) S))
  | x, x_1 => False
induction' S using WSeq.recOn with s S S <;> simp
no goals
case h1.h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
s : WSeq α
S : WSeq (WSeq α)
⊢ ∃ s_1 S_1,
    append (map f s) (map f (join S)) = append s_1 (map f (join S_1)) ∧
      append (map f s) (join (map (map f) S)) = append s_1 (join (map (map f) S_1))
exact ⟨map f s, S, rfl, rfl⟩
no goals
case h1.h3
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f (join S) = append s (map f (join S_1)) ∧ join (map (map f) S) = append s (join (map (map f) S_1))
refine' ⟨nil, S, _, _⟩ <;> simp
no goals
case h2
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
a : β
s : WSeq β
⊢ ∃ s_1 S_1,
    append s (map f (join S)) = append s_1 (map f (join S_1)) ∧
      append s (join (map (map f) S)) = append s_1 (join (map (map f) S_1))
exact ⟨_, _, rfl, rfl⟩
no goals
case h3
α : Type u
β : Type v
γ : Type w
f : α → β
S✝ : WSeq (WSeq α)
s1 s2 : Seq (Option β)
h : ∃ s S, s1 = append s (map f (join S)) ∧ s2 = append s (join (map (map f) S))
S : WSeq (WSeq α)
s : WSeq β
⊢ ∃ s_1 S_1,
    append s (map f (join S)) = append s_1 (map f (join S_1)) ∧
      append s (join (map (map f) S)) = append s_1 (join (map (map f) S_1))
exact ⟨_, _, rfl, rfl⟩
no goals
case r
α : Type u
β : Type v
γ : Type w
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f (join S) = append s (map f (join S_1)) ∧ join (map (map f) S) = append s (join (map (map f) S_1))
refine' ⟨nil, S, _, _⟩ <;> simp