α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ IsBisimulation fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ join (cons (a, s) S) = cons a (append s (join S))
apply
  eq_of_bisim
    (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    _ (Or.inr ⟨a, s, S, rfl, rfl⟩)
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))) (destruct s1)
    (destruct s2)
α : Type u
β : Type v
γ : Type w
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ IsBisimulation fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
intro s1 s2 h
case h1
α : Type u
β : Type v
γ : Type w
a : α
s✝ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))) (destruct nil)
    (destruct nil)

case h2
α : Type u
β : Type v
γ : Type w
a : α
s✝ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s : Seq α
⊢ ∀ (x : α) (s : Seq α),
    BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
      (destruct (cons x s)) (destruct (cons x s))
α : Type u
β : Type v
γ : Type w
a : α
s✝ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))) (destruct s)
    (destruct s)
apply recOn s
no goals
case h1
α : Type u
β : Type v
γ : Type w
a : α
s✝ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))) (destruct nil)
    (destruct nil)
trivial
case h2
α : Type u
β : Type v
γ : Type w
a : α
s✝¹ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    (destruct (cons x s)) (destruct (cons x s))
case h2
α : Type u
β : Type v
γ : Type w
a : α
s✝ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s : Seq α
⊢ ∀ (x : α) (s : Seq α),
    BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
      (destruct (cons x s)) (destruct (cons x s))
intro x s
case h2
α : Type u
β : Type v
γ : Type w
a : α
s✝¹ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))) (some (x, s))
    (some (x, s))
case h2
α : Type u
β : Type v
γ : Type w
a : α
s✝¹ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    (destruct (cons x s)) (destruct (cons x s))
rw [destruct_cons]
no goals
case h2
α : Type u
β : Type v
γ : Type w
a : α
s✝¹ : Seq α
S : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
s✝ : Seq α
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))) (some (x, s))
    (some (x, s))
exact ⟨rfl, Or.inl rfl⟩
case h1
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    (destruct (join (cons (a, nil) S))) (destruct (cons a (append nil (join S))))

case h2
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ ∀ (x : α) (s : Seq α),
    BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
      (destruct (join (cons (a, cons x s) S))) (destruct (cons a (append (cons x s) (join S))))
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    (destruct (join (cons (a, s) S))) (destruct (cons a (append s (join S))))
apply recOn s
no goals
case h1
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    (destruct (join (cons (a, nil) S))) (destruct (cons a (append nil (join S))))
simp [join_cons_cons, join_cons_nil]
case h2
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝¹ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s✝ : Seq α
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    (destruct (join (cons (a, cons x s) S))) (destruct (cons a (append (cons x s) (join S))))
case h2
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s : Seq α
S : Seq (Seq1 α)
⊢ ∀ (x : α) (s : Seq α),
    BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
      (destruct (join (cons (a, cons x s) S))) (destruct (cons a (append (cons x s) (join S))))
intro x s
case h2
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝¹ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s✝ : Seq α
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ join (cons (x, s) S) = cons x (append s (join S)) ∨
    ∃ a s_1 S_1,
      join (cons (x, s) S) = join (cons (a, s_1) S_1) ∧ cons x (append s (join S)) = cons a (append s_1 (join S_1))
case h2
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝¹ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s✝ : Seq α
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ BisimO (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S)))
    (destruct (join (cons (a, cons x s) S))) (destruct (cons a (append (cons x s) (join S))))
simp [join_cons_cons, join_cons_nil]
no goals
case h2
α : Type u
β : Type v
γ : Type w
a✝ : α
s✝¹ : Seq α
S✝ : Seq (Seq1 α)
s1 s2 : Seq α
h : s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))
a : α
s✝ : Seq α
S : Seq (Seq1 α)
x : α
s : Seq α
⊢ join (cons (x, s) S) = cons x (append s (join S)) ∨
    ∃ a s_1 S_1,
      join (cons (x, s) S) = join (cons (a, s_1) S_1) ∧ cons x (append s (join S)) = cons a (append s_1 (join S_1))
refine' Or.inr ⟨x, s, S, rfl, rfl⟩