Theory itreeTau

⊢ ∃rep. TYPE_DEFINITION itree_rep_ok rep

⊢ ∀t k.
    itree_bind t k =
    itree_unfold
      (λx.
         case x of
           INL (Ret r) =>
             (case k r of
                Ret s => Ret' s
              | Tau t => Tau' (INR t)
              | Vis e g => Vis' e (INR ∘ g))
         | INL (Tau t) => Tau' (INL t)
         | INL (Vis e g) => Vis' e (INL ∘ g)
         | INR (Ret r') => Ret' r'
         | INR (Tau t') => Tau' (INR t')
         | INR (Vis e' g') => Vis' e' (INR ∘ g')) (INL t)

⊢ ∀f1 f2.
    itree_elMAP f1 f2 =
    itree_el_ABS ∘ SUM_MAP f1 (SUM_MAP f2 I) ∘ itree_el_REP

⊢ itree_elREL =
  (λR1 R2 x y.
     ∃z. (∀p. p ∈ itree_elSET1 z ⇒ R1 (FST p) (SND p)) ∧
         (∀p. p ∈ itree_elSET2 z ⇒ R2 (FST p) (SND p)) ∧
         itree_elMAP FST FST z = x ∧ itree_elMAP SND SND z = y)

⊢ itree_elSET1 =
  S ($UNION ∘ BIMG $= ∘ setL)
    (BIMG (S ($UNION ∘ BIMG (K ∅) ∘ setL) (BIMG (K ∅) ∘ setR)) ∘ setR) ∘
  itree_el_REP

⊢ itree_elSET2 =
  S ($UNION ∘ BIMG (K ∅) ∘ setL)
    (BIMG (S ($UNION ∘ BIMG $= ∘ setL) (BIMG (K ∅) ∘ setR)) ∘ setR) ∘
  itree_el_REP

⊢ (∀a. itree_el_ABS (itree_el_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ itree_el_REP (itree_el_ABS r) = r

⊢ itree_el_CONS = itree_el_ABS

⊢ (∀a0 f f0 v. itree_el_CASE (Event a0) f f0 v = f a0) ∧
  (∀a0 f f0 v. itree_el_CASE (Return a0) f f0 v = f0 a0) ∧
  ∀f f0 v. itree_el_CASE Silence f f0 v = v

⊢ ∀f0 f1.
    (∀a0. itree_el_size f0 f1 (Event a0) = 1 + f0 a0) ∧
    (∀a0. itree_el_size f0 f1 (Return a0) = 1 + f1 a0) ∧
    itree_el_size f0 f1 Silence = 0

⊢ ∀body seed.
    itree_iter body seed =
    itree_unfold
      (λx.
         case x of
           Ret (INL seed') => Tau' (body seed')
         | Ret (INR v) => Ret' v
         | Tau u => Tau' u
         | Vis e g => Vis' e g) (body seed)

⊢ ∀body seed.
    itree_loop body seed =
    itree_iter
      (λx.
         itree_bind (body x)
           (λcb.
              case cb of INL c => Ret (INL (INL c)) | INR b => Ret (INR b)))
      (INR seed)

⊢ ∀f1 f2 f3.
    itree_nextMAP f1 f2 f3 =
    itree_next_ABS ∘ SUM_MAP f2 (SUM_MAP f3 (f1 ## $o f3)) ∘ itree_next_REP

⊢ itree_nextREL =
  (λR1 R2 R3 x y.
     ∃z. (∀p. p ∈ itree_nextSET1 z ⇒ R1 (FST p) (SND p)) ∧
         (∀p. p ∈ itree_nextSET2 z ⇒ R2 (FST p) (SND p)) ∧
         (∀p. p ∈ itree_nextSET3 z ⇒ R3 (FST p) (SND p)) ∧
         itree_nextMAP FST FST FST z = x ∧ itree_nextMAP SND SND SND z = y)

⊢ itree_nextSET1 =
  S ($UNION ∘ BIMG (K ∅) ∘ setL)
    (BIMG
       (S ($UNION ∘ BIMG (K ∅) ∘ setL)
          (BIMG
             (S ($UNION ∘ BIMG $= ∘ setFST)
                (BIMG (BIMG (K ∅) ∘ flip IMAGE 𝕌(:α)) ∘ setSND)) ∘ setR)) ∘
     setR) ∘ itree_next_REP

⊢ itree_nextSET2 =
  S ($UNION ∘ BIMG $= ∘ setL)
    (BIMG
       (S ($UNION ∘ BIMG (K ∅) ∘ setL)
          (BIMG
             (S ($UNION ∘ BIMG (K ∅) ∘ setFST)
                (BIMG (BIMG (K ∅) ∘ flip IMAGE 𝕌(:α)) ∘ setSND)) ∘ setR)) ∘
     setR) ∘ itree_next_REP

⊢ itree_nextSET3 =
  S ($UNION ∘ BIMG (K ∅) ∘ setL)
    (BIMG
       (S ($UNION ∘ BIMG $= ∘ setL)
          (BIMG
             (S ($UNION ∘ BIMG (K ∅) ∘ setFST)
                (BIMG (BIMG $= ∘ flip IMAGE 𝕌(:α)) ∘ setSND)) ∘ setR)) ∘
     setR) ∘ itree_next_REP

⊢ (∀a. itree_next_ABS (itree_next_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ itree_next_REP (itree_next_ABS r) = r

⊢ itree_next_CONS = itree_next_ABS

⊢ (∀a0 f f0 f1. itree_next_CASE (Ret' a0) f f0 f1 = f a0) ∧
  (∀a0 f f0 f1. itree_next_CASE (Tau' a0) f f0 f1 = f0 a0) ∧
  ∀a0 a1 f f0 f1. itree_next_CASE (Vis' a0 a1) f f0 f1 = f1 a0 a1

⊢ ∀f0 f1 f2 f3.
    (∀a0. itree_next_size f0 f1 f2 f3 (Ret' a0) = 1 + f2 a0) ∧
    (∀a0. itree_next_size f0 f1 f2 f3 (Tau' a0) = 1 + f3 a0) ∧
    ∀a0 a1. itree_next_size f0 f1 f2 f3 (Vis' a0 a1) = 1 + f1 a0

⊢ untau =
  itree_unfold
    (λt.
       case some t'. strip_tau t t' of
         NONE => Div'
       | SOME (Ret v) => Ret' v
       | SOME (Tau t') => Div'
       | SOME (Vis e k) => Vis' e k)

⊢ ∀R. upto_taus_func R = R ∪ rel_to_reln (after_taus (reln_to_rel R))

⊢ ∀R. wbisim_functional R =
      {(t,t') | ∃r. strip_tau t (Ret r) ∧ strip_tau t' (Ret r)} ∪
      {(t,t') |
       ∃e k k'.
         strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
         ∀r. (k r,k' r) ∈ R} ∪ {(Tau t,Tau t') | (t,t') ∈ R}

⊢ FUNPOW Tau n (Ret x) = spin ⇒ F

⊢ FUNPOW Tau n (Ret x) = FUNPOW Tau m (Ret y) ⇒ n = m ∧ x = y

⊢ t = FUNPOW Tau (SUC n) t ⇔ t = spin

⊢ FUNPOW Tau n (Vis a g) = FUNPOW Tau m (Vis e k) ⇒ n = m ∧ a = e ∧ g = k

⊢ (∀r. ∃n r'. abs r = FUNPOW Tau (SUC n) (abs r')) ⇔ ∀r. abs r = spin

⊢ itree_bind (FUNPOW Tau n t) g = FUNPOW Tau n (itree_bind t g)

⊢ t = FUNPOW Tau n t' ⇒ itree_wbisim t t'

⊢ Ret x ≠ FUNPOW Tau n (Vis a g) ∧ Vis a g ≠ FUNPOW Tau n (Ret x)

⊢ FUNPOW Tau n' (Ret x) ≠ FUNPOW Tau n (Vis a g)

⊢ itree_wbisim (FUNPOW Tau n x) x

⊢ itree_wbisim x y ⇒ itree_wbisim (FUNPOW Tau n x) (FUNPOW Tau n' y)

⊢ FUNPOW Tau n (Vis e k) = spin ⇒ F

⊢ ∀x y. Ret x = Ret y ⇔ x = y

⊢ ∀x y. Tau x = Tau y ⇔ x = y

⊢ INJ Tau 𝕌(:(α, β, γ) itree) 𝕌(:(α, β, γ) itree)

⊢ ∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g

⊢ after_taus R x y ⇒ after_taus R (FUNPOW Tau n x) y

⊢ after_taus R x y ⇒ after_taus R x (FUNPOW Tau n y)

⊢ ∀R a0 a1.
    after_taus R a0 a1 ⇔
    R a0 a1 ∨ (∃x. a0 = Tau x ∧ after_taus R x a1) ∨
    ∃y. a1 = Tau y ∧ after_taus R a0 y

⊢ ∀R after_taus'.
    (∀x y. R x y ⇒ after_taus' x y) ∧
    (∀x y. after_taus' x y ⇒ after_taus' (Tau x) y) ∧
    (∀x y. after_taus' x y ⇒ after_taus' x (Tau y)) ⇒
    ∀a0 a1. after_taus R a0 a1 ⇒ after_taus' a0 a1

⊢ after_taus $= t t' ⇒ t' = spin ⇒ t = spin

⊢ after_taus $= t t' ⇔
  (∃t''. strip_tau t t'' ∧ strip_tau t' t'') ∨ t = spin ∧ t' = spin

⊢ after_taus itree_wbisim t t' ⇔ itree_wbisim t t'

⊢ after_taus itree_wbisim t t' ⇒ t' = spin ⇒ t = spin

⊢ ∀R x y. R x y ⇒ after_taus R x y

⊢ ∀R. (∀x y. R x y ⇒ after_taus R x y) ∧
      (∀x y. after_taus R x y ⇒ after_taus R (Tau x) y) ∧
      ∀x y. after_taus R x y ⇒ after_taus R x (Tau y)

⊢ ∀R after_taus'.
    (∀x y. R x y ⇒ after_taus' x y) ∧
    (∀x y. after_taus R x y ∧ after_taus' x y ⇒ after_taus' (Tau x) y) ∧
    (∀x y. after_taus R x y ∧ after_taus' x y ⇒ after_taus' x (Tau y)) ⇒
    ∀a0 a1. after_taus R a0 a1 ⇒ after_taus' a0 a1

⊢ ∀R x y. after_taus R x y ⇒ after_taus R (Tau x) y

⊢ ∀R x y. after_taus R x y ⇒ after_taus R x (Tau y)

⊢ (∀r. strong_bisim_upfrom_abs (abs,abs') (abs r) (abs' r)) ⇔ abs = abs'

⊢ (∀r. strong_bisim_upfrom_abs (abs,abs') (abs r) (abs' r)) ∧
  strong_bisim_upfrom_abs (abs,abs') t t' ⇒
  t = t'

⊢ (∀r. weak_bisim_upfrom_abs (abs,abs') (abs r) (abs' r)) ⇔
  ∀r. itree_wbisim (abs r) (abs' r)

⊢ (∀r. weak_bisim_upfrom_abs (abs,abs') (abs r) (abs' r)) ∧
  weak_bisim_upfrom_abs (abs,abs') t t' ⇒
  itree_wbisim t t'

⊢ DATATYPE (itree Ret Tau Vis)

⊢ DATATYPE (itree_el Event Return Silence)

⊢ DATATYPE (itree_next Ret' Tau' Vis')

⊢ (∀x y. Ret x = Ret y ⇔ x = y) ∧ (∀x y. Tau x = Tau y ⇔ x = y) ∧
  ∀x f y g. Vis x f = Vis y g ⇔ x = y ∧ f = g

⊢ itree_CASE (Ret r) ret tau vis = ret r ∧
  itree_CASE (Tau t) ret tau vis = tau t ∧
  itree_CASE (Vis a g) ret tau vis = vis a g

⊢ ∀M M' ret tau vis ret' tau' vis'.
    M = M' ∧ (∀x. M' = Ret x ⇒ ret x = ret' x) ∧
    (∀t. M' = Tau t ⇒ tau t = tau' t) ∧
    (∀a g. M' = Vis a g ⇒ vis a g = vis' a g) ⇒
    itree_CASE M ret tau vis = itree_CASE M' ret' tau' vis'

⊢ ∀f. f (itree_CASE t ret tau vis) ⇔
      (∃r. t = Ret r ∧ f (ret r)) ∨ (∃u. t = Tau u ∧ f (tau u)) ∨
      ∃a g. t = Vis a g ∧ f (vis a g)

⊢ itree_CASE t ret tau vis = v ⇔
  (∃r. t = Ret r ∧ ret r = v) ∨ (∃u. t = Tau u ∧ tau u = v) ∨
  ∃a g. t = Vis a g ∧ vis a g = v

⊢ itree_bind (itree_bind t k) k' = itree_bind t (λx. itree_bind (k x) k')

⊢ ∀t k1 k2.
    (∀r. itree_wbisim (k1 r) (k2 r)) ⇒
    itree_wbisim (itree_bind t k1) (itree_bind t k2)

⊢ ∀a b k. itree_wbisim a b ⇒ itree_wbisim (itree_bind a k) (itree_bind b k)

⊢ ∀a b k1 k2.
    itree_wbisim a b ∧ (∀r. itree_wbisim (k1 r) (k2 r)) ⇒
    itree_wbisim (itree_bind a k1) (itree_bind b k2)

⊢ itree_bind t k = Ret r ⇒ ∃r'. t = Ret r' ∧ k r' = Ret r

⊢ itree_bind t Ret = t

⊢ ∀u u' k. strip_tau u u' ⇒ itree_wbisim (itree_bind u k) (itree_bind u' k)

⊢ itree_bind (Ret r) k = k r ∧
  itree_bind (Tau t) k = Tau (itree_bind t k) ∧
  itree_bind (Vis e k') k = Vis e (λx. itree_bind (k' x) k)

⊢ ∀u k k' e.
    strip_tau u (Vis e k') ⇒
    strip_tau (itree_bind u k) (Vis e (λx. itree_bind (k' x) k))

⊢ ∀t1 t2.
    t1 = t2 ⇔
    ∃R. R t1 t2 ∧ (∀x t. R (Ret x) t ⇒ t = Ret x) ∧
        (∀u t. R (Tau u) t ⇒ ∃v. t = Tau v ∧ R u v) ∧
        ∀a f t. R (Vis a f) t ⇒ ∃g. t = Vis a g ∧ ∀s. R (f s) (g s)

⊢ ∀t. (∃x. t = Ret x) ∨ (∃u. t = Tau u) ∨ ∃a g. t = Vis a g

⊢ ∀R. rel_to_reln R ⊆
      rel_to_reln itree_wbisim ∪
      wbisim_functional
        (upto_taus_func (rel_to_reln R) ∪ rel_to_reln itree_wbisim) ⇒
      rel_to_reln R ⊆ rel_to_reln itree_wbisim

⊢ Ret x ≠ Tau t ∧ Ret x ≠ Vis e g ∧ Tau t ≠ Vis e g

⊢ (∀a0 a0'. Event a0 = Event a0' ⇔ a0 = a0') ∧
  ∀a0 a0'. Return a0 = Return a0' ⇔ a0 = a0'

⊢ ∀f0 f1 f2. ∃h.
    (∀a0. h (Event a0) = f0 a0) ∧ (∀a0. h (Return a0) = f1 a0) ∧
    h Silence = f2

⊢ ∀f1 f2 g1 g2 x.
    (∀a. a ∈ itree_elSET1 x ⇒ f1 a = g1 a) ∧
    (∀a. a ∈ itree_elSET2 x ⇒ f2 a = g2 a) ⇒
    itree_elMAP f1 f2 x = itree_elMAP g1 g2 x

⊢ itree_elMAP I I = I

⊢ ∀f1 f2 x. itree_elSET1 (itree_elMAP f1 f2 x) = IMAGE f1 (itree_elSET1 x)

⊢ ∀f1 f2 x. itree_elSET2 (itree_elMAP f1 f2 x) = IMAGE f2 (itree_elSET2 x)

⊢ itree_elMAP g1 g2 ∘ itree_elMAP f1 f2 = itree_elMAP (g1 ∘ f1) (g2 ∘ f2)

⊢ ∀x. cardleq (itree_elSET1 x) 𝕌(:num)

⊢ ∀x. cardleq (itree_elSET2 x) 𝕌(:num)

⊢ ∀M M' f f0 v.
    M = M' ∧ (∀a0. M' = Event a0 ⇒ f a0 = f' a0) ∧
    (∀a0. M' = Return a0 ⇒ f0 a0 = f0' a0) ∧ (M' = Silence ⇒ v = v') ⇒
    itree_el_CASE M f f0 v = itree_el_CASE M' f' f0' v'

⊢ itree_el_CASE x f f0 v = v' ⇔
  (∃e. x = Event e ∧ f e = v') ∨ (∃r. x = Return r ∧ f0 r = v') ∨
  x = Silence ∧ v = v'

⊢ (∀a0' a0. Event a0 ≠ Return a0') ∧ (∀a0. Event a0 ≠ Silence) ∧
  ∀a0. Return a0 ≠ Silence

⊢ ∀P. (∀e. P (Event e)) ∧ (∀r. P (Return r)) ∧ P Silence ⇒ ∀i. P i

⊢ ∀a1. a1 ∈ itree_elSET1 ((λa1. itree_el_ABS ((λa1. INL a1) a1)) a1)

⊢ ∀a2. a2 ∈ itree_elSET2 ((λa2. itree_el_ABS ((λa2. INR (INL a2)) a2)) a2)

⊢ ∀ii. (∃e. ii = Event e) ∨ (∃r. ii = Return r) ∨ ii = Silence

⊢ itree_el (Ret r) [] = Return r ∧ itree_el (Tau t) [] = Silence ∧
  itree_el (Vis e g) [] = Event e ∧ itree_el (Ret r) (NONE::ns) = Silence ∧
  itree_el (Tau t) (NONE::ns) = itree_el t ns ∧
  itree_el (Vis e g) (NONE::ns) = Silence ∧
  itree_el (Ret r) (SOME a::ns) = Silence ∧
  itree_el (Tau t) (SOME a::ns) = Silence ∧
  itree_el (Vis e g) (SOME a::ns) = itree_el (g a) ns

⊢ ∀a1 a2.
    itree_elSET1
      ((λa1 a2. itree_el_ABS ((λa1 a2. K INR ARB (K INR ARB ARB)) a1 a2))
         a1 a2) ⊆ ∅ ∧
    itree_elSET2
      ((λa1 a2. itree_el_ABS ((λa1 a2. K INR ARB (K INR ARB ARB)) a1 a2))
         a1 a2) ⊆ ∅

⊢ ∀body body' seed seed'.
    itree_wbisim seed seed' ∧
    (∀seed seed'. itree_wbisim (body seed) (body' seed')) ⇒
    itree_wbisim (itree_iter body seed) (itree_iter body' seed')

⊢ ∀t k1 k2.
    (∀r. itree_wbisim (k1 r) (k2 r)) ⇒
    itree_wbisim (itree_iter k1 t) (itree_iter k2 t)

⊢ ∀body seed seed'.
    itree_wbisim seed seed' ∧ itree_wbisim (body seed) (body seed') ⇒
    itree_wbisim (itree_iter body seed) (itree_iter body seed')

⊢ itree_iter body seed =
  itree_bind (body seed)
    (λx. case x of INL a => Tau (itree_iter body a) | INR b => Ret b)

⊢ (∀a0 a0'. Ret' a0 = Ret' a0' ⇔ a0 = a0') ∧
  (∀a0 a0'. Tau' a0 = Tau' a0' ⇔ a0 = a0') ∧
  ∀a0 a1 a0' a1'. Vis' a0 a1 = Vis' a0' a1' ⇔ a0 = a0' ∧ a1 = a1'

⊢ ∀f0 f1 f2. ∃h.
    (∀a0. h (Ret' a0) = f0 a0) ∧ (∀a0. h (Tau' a0) = f1 a0) ∧
    ∀a0 a1. h (Vis' a0 a1) = f2 a0 a1

⊢ ∀f1 f2 f3 g1 g2 g3 x.
    (∀a. a ∈ itree_nextSET1 x ⇒ f1 a = g1 a) ∧
    (∀a. a ∈ itree_nextSET2 x ⇒ f2 a = g2 a) ∧
    (∀a. a ∈ itree_nextSET3 x ⇒ f3 a = g3 a) ⇒
    itree_nextMAP f1 f2 f3 x = itree_nextMAP g1 g2 g3 x

⊢ itree_nextMAP I I I = I

⊢ ∀f1 f2 f3 x.
    itree_nextSET1 (itree_nextMAP f1 f2 f3 x) = IMAGE f1 (itree_nextSET1 x)

⊢ ∀f1 f2 f3 x.
    itree_nextSET2 (itree_nextMAP f1 f2 f3 x) = IMAGE f2 (itree_nextSET2 x)

⊢ ∀f1 f2 f3 x.
    itree_nextSET3 (itree_nextMAP f1 f2 f3 x) = IMAGE f3 (itree_nextSET3 x)

⊢ itree_nextMAP g1 g2 g3 ∘ itree_nextMAP f1 f2 f3 =
  itree_nextMAP (g1 ∘ f1) (g2 ∘ f2) (g3 ∘ f3)

⊢ ∀x. cardleq (itree_nextSET1 x) 𝕌(:num + 'b1)

⊢ ∀x. cardleq (itree_nextSET2 x) 𝕌(:num + 'b1)

⊢ ∀x. cardleq (itree_nextSET3 x) 𝕌(:num + 'b1)

⊢ ∀M M' f f0 f1.
    M = M' ∧ (∀a0. M' = Ret' a0 ⇒ f a0 = f' a0) ∧
    (∀a0. M' = Tau' a0 ⇒ f0 a0 = f0' a0) ∧
    (∀a0 a1. M' = Vis' a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ⇒
    itree_next_CASE M f f0 f1 = itree_next_CASE M' f' f0' f1'

⊢ itree_next_CASE x f f0 f1 = v ⇔
  (∃r. x = Ret' r ∧ f r = v) ∨ (∃s. x = Tau' s ∧ f0 s = v) ∨
  ∃e f'. x = Vis' e f' ∧ f1 e f' = v

⊢ (∀a0' a0. Ret' a0 ≠ Tau' a0') ∧ (∀a1 a0' a0. Ret' a0 ≠ Vis' a0' a1) ∧
  ∀a1 a0' a0. Tau' a0 ≠ Vis' a0' a1

⊢ ∀P. (∀r. P (Ret' r)) ∧ (∀s. P (Tau' s)) ∧ (∀e f. P (Vis' e f)) ⇒ ∀i. P i

⊢ ∀a1.
    a1 ∈
    itree_nextSET1
      ((λa1. itree_next_ABS ((λa1. INR (INR (flip $, ARB a1))) a1)) a1)

⊢ ∀a2. a2 ∈ itree_nextSET2 ((λa2. itree_next_ABS ((λa2. INL a2) a2)) a2)

⊢ ∀a3.
    a3 ∈ itree_nextSET3 ((λa3. itree_next_ABS ((λa3. INR (INL a3)) a3)) a3)

⊢ ∀ii. (∃r. ii = Ret' r) ∨ (∃s. ii = Tau' s) ∨ ∃e f. ii = Vis' e f

⊢ ∀a1 a2 a3.
    itree_nextSET1
      ((λa1 a2 a3. itree_next_ABS ((λa1 a2 a3. (K ∘ INL) a2 ARB) a1 a2 a3))
         a1 a2 a3) ⊆ ∅ ∧
    itree_nextSET2
      ((λa1 a2 a3. itree_next_ABS ((λa1 a2 a3. (K ∘ INL) a2 ARB) a1 a2 a3))
         a1 a2 a3) ⊆ {a2} ∧
    itree_nextSET3
      ((λa1 a2 a3. itree_next_ABS ((λa1 a2 a3. (K ∘ INL) a2 ARB) a1 a2 a3))
         a1 a2 a3) ⊆ ∅

⊢ ∀a1 a2 a3.
    itree_nextSET1
      ((λa1 a2 a3.
          itree_next_ABS
            ((λa1 a2 a3. K INR ARB ((K ∘ INL) a3 ARB)) a1 a2 a3)) a1 a2 a3) ⊆
    ∅ ∧
    itree_nextSET2
      ((λa1 a2 a3.
          itree_next_ABS
            ((λa1 a2 a3. K INR ARB ((K ∘ INL) a3 ARB)) a1 a2 a3)) a1 a2 a3) ⊆
    ∅ ∧
    itree_nextSET3
      ((λa1 a2 a3.
          itree_next_ABS
            ((λa1 a2 a3. K INR ARB ((K ∘ INL) a3 ARB)) a1 a2 a3)) a1 a2 a3) ⊆
    {a3}

⊢ strong_bisim_upfrom_abs (abs,abs') t t

⊢ ∀t1 t2.
    t1 = t2 ⇔
    ∃R. R t1 t2 ∧ (∀x t. R (Ret x) t ⇒ t = Ret x) ∧
        (∀u t. R (Tau u) t ⇒ ∃v. t = Tau v ∧ (R u v ∨ u = v)) ∧
        ∀a f t.
          R (Vis a f) t ⇒ ∃g. t = Vis a g ∧ ∀s. R (f s) (g s) ∨ f s = g s

⊢ itree_unfold f seed =
  case f seed of
    Ret' r => Ret r
  | Tau' s => Tau (itree_unfold f s)
  | Vis' e g => Vis e (itree_unfold f ∘ g)

⊢ itree_wbisim t (Ret x) ⇒ ∃n. t = FUNPOW Tau n (Ret x)

⊢ itree_wbisim t (Vis a g) ⇒
  ∃n k. t = FUNPOW Tau n (Vis a k) ∧ ∀r. itree_wbisim (k r) (g r)

⊢ ∀a0 a1.
    itree_wbisim a0 a1 ⇔
    (∃t t'. a0 = Tau t ∧ a1 = Tau t' ∧ itree_wbisim t t') ∨
    (∃e k k'.
       strip_tau a0 (Vis e k) ∧ strip_tau a1 (Vis e k') ∧
       ∀r. itree_wbisim (k r) (k' r)) ∨
    ∃r. strip_tau a0 (Ret r) ∧ strip_tau a1 (Ret r)

⊢ ∀itree_wbisim'.
    (∀a0 a1.
       itree_wbisim' a0 a1 ⇒
       (∃t t'. a0 = Tau t ∧ a1 = Tau t' ∧ itree_wbisim' t t') ∨
       (∃e k k'.
          strip_tau a0 (Vis e k) ∧ strip_tau a1 (Vis e k') ∧
          ∀r. itree_wbisim' (k r) (k' r)) ∨
       ∃r. strip_tau a0 (Ret r) ∧ strip_tau a1 (Ret r)) ⇒
    ∀a0 a1. itree_wbisim' a0 a1 ⇒ itree_wbisim a0 a1

⊢ ∀R. (∀t t'.
         R t t' ⇒
         (∃t2 t3. t = Tau t2 ∧ t' = Tau t3 ∧ (R t2 t3 ∨ itree_wbisim t2 t3)) ∨
         (∃e k k'.
            strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
            ∀r. R (k r) (k' r) ∨ itree_wbisim (k r) (k' r)) ∨
         (∃r. strip_tau t (Ret r) ∧ strip_tau t' (Ret r)) ∨
         itree_wbisim t t') ⇒
      ∀t t'. R t t' ⇒ itree_wbisim t t'

⊢ ∀R. rel_to_reln R ⊆
      rel_to_reln itree_wbisim ∪
      wbisim_functional (set_companion wbisim_functional (rel_to_reln R)) ⇒
      rel_to_reln R ⊆ rel_to_reln itree_wbisim

⊢ itree_wbisim t t

⊢ (∀t t'. itree_wbisim t t' ⇒ itree_wbisim (Tau t) (Tau t')) ∧
  (∀e k k' t t'.
     strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
     (∀r. itree_wbisim (k r) (k' r)) ⇒
     itree_wbisim t t') ∧
  ∀r t t'. strip_tau t (Ret r) ∧ strip_tau t' (Ret r) ⇒ itree_wbisim t t'

⊢ ∀t t' t''. itree_wbisim t t' ∧ strip_tau t t'' ⇒ itree_wbisim t'' t'

⊢ ∀t t' v. itree_wbisim t t' ∧ strip_tau t (Ret v) ⇒ strip_tau t' (Ret v)

⊢ ∀t t' e k.
    itree_wbisim t t' ∧ strip_tau t (Vis e k) ⇒
    ∃k'. strip_tau t' (Vis e k') ∧ ∀r. itree_wbisim (k r) (k' r)

⊢ itree_wbisim t t' ⇔
  t = spin ∧ t' = spin ∨ (∃r. strip_tau t (Ret r) ∧ strip_tau t' (Ret r)) ∨
  ∃e k k'.
    strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
    ∀l. itree_wbisim (k l) (k' l)

⊢ ∀t t' t''. itree_wbisim t t' ∧ strip_tau t' t'' ⇒ itree_wbisim t t''

⊢ ∀R. (∀t t'.
         R t t' ⇒
         (∃t2 t3. t = Tau t2 ∧ t' = Tau t3 ∧ (R t2 t3 ∨ itree_wbisim t2 t3)) ∨
         (∃e k k'.
            strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
            ∀r. R (k r) (k' r) ∨ itree_wbisim (k r) (k' r)) ∨
         ∃r. strip_tau t (Ret r) ∧ strip_tau t' (Ret r)) ⇒
      ∀t t'. R t t' ⇒ itree_wbisim t t'

⊢ ∀t t'. itree_wbisim t t' ⇒ itree_wbisim t' t

⊢ ∀t t'. itree_wbisim (Tau t) t' ⇒ itree_wbisim t t'

⊢ itree_wbisim (Tau t) t

⊢ (itree_wbisim (Tau t1) t2 ⇔ itree_wbisim t1 t2) ∧
  (itree_wbisim t1 (Tau t2) ⇔ itree_wbisim t1 t2)

⊢ ∀t t' t''. itree_wbisim t t' ∧ itree_wbisim t' t'' ⇒ itree_wbisim t t''

⊢ ∀e k1 k2.
    (∀r. itree_wbisim (k1 r) (k2 r)) ⇒ itree_wbisim (Vis e k1) (Vis e k2)

⊢ itree_wbisim (Vis a g) (Vis a' g') ⇔
  a = a' ∧ ∀r. itree_wbisim (g r) (g' r)

⊢ itree_wbisim t t' ⇒ weak_bisim_upfrom_abs (abs,abs') t t'

⊢ itree_wbisim t' t'' ⇒ weak_bisim_upfrom_abs (abs,abs) t' t''

⊢ spin = Tau spin

⊢ ∀n. spin = FUNPOW Tau n spin

⊢ itree_bind spin k = spin

⊢ ∀t. strip_tau spin t ⇒ F

⊢ ∀t1 t2. strip_tau t1 t2 ⇒ ∃n. t1 = FUNPOW Tau n t2

⊢ (∀u. t ≠ Tau u) ⇒ strip_tau (FUNPOW Tau n t) t

⊢ ∀t t' n. strip_tau t t' ⇒ strip_tau (FUNPOW Tau n t) t'

⊢ ∀a0 a1.
    strip_tau a0 a1 ⇔
    (∃t. a0 = Tau t ∧ strip_tau t a1) ∨
    (∃e k. a0 = Vis e k ∧ a1 = Vis e k) ∨ ∃v. a0 = Ret v ∧ a1 = Ret v

⊢ ∀strip_tau'.
    (∀t t'. strip_tau' t t' ⇒ strip_tau' (Tau t) t') ∧
    (∀e k. strip_tau' (Vis e k) (Vis e k)) ∧
    (∀v. strip_tau' (Ret v) (Ret v)) ⇒
    ∀a0 a1. strip_tau a0 a1 ⇒ strip_tau' a0 a1

⊢ ∀t t' t''. strip_tau t t' ∧ strip_tau t t'' ⇒ t' = t''

⊢ (∀t t'. strip_tau t t' ⇒ strip_tau (Tau t) t') ∧
  (∀e k. strip_tau (Vis e k) (Vis e k)) ∧ ∀v. strip_tau (Ret v) (Ret v)

⊢ (strip_tau t' (Tau t) ⇔ F) ∧ (strip_tau (Ret v) (Vis e k) ⇔ F) ∧
  (strip_tau (Vis e k) (Ret v) ⇔ F) ∧
  (strip_tau (Tau t) t' ⇔ strip_tau t t')

⊢ strip_tau (Ret v) (Ret v') ⇔ v = v'

⊢ strip_tau (Vis e k) (Vis e' k') ⇔ e = e' ∧ k = k'

⊢ (∀t'. ¬strip_tau t t') ⇒ t = spin

⊢ ∀strip_tau'.
    (∀t t'. strip_tau t t' ∧ strip_tau' t t' ⇒ strip_tau' (Tau t) t') ∧
    (∀e k. strip_tau' (Vis e k) (Vis e k)) ∧
    (∀v. strip_tau' (Ret v) (Ret v)) ⇒
    ∀a0 a1. strip_tau a0 a1 ⇒ strip_tau' a0 a1

⊢ ∀e k k'.
    strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
    (∀r. itree_wbisim (k r) (k' r)) ⇒
    itree_wbisim t t'

⊢ strong_bisim_upfrom_abs (abs,abs') t t' ⇒
  strong_bisim_upfrom_abs (abs,abs') (FUNPOW Tau n t) (FUNPOW Tau n t')

⊢ strong_bisim_upfrom_abs (abs,abs') (FUNPOW Tau (SUC n) (abs r))
    (FUNPOW Tau (SUC n) (abs' r))

⊢ ∀a0 a1 a2.
    strong_bisim_upfrom_abs a0 a1 a2 ⇔
    (∃abs abs' x. a0 = (abs,abs') ∧ a1 = Ret x ∧ a2 = Ret x) ∨
    (∃abs abs' e k k'.
       a0 = (abs,abs') ∧ a1 = Vis e k ∧ a2 = Vis e k' ∧
       ∀l. strong_bisim_upfrom_abs (abs,abs') (k l) (k' l) ∨
           ∃r. k l = abs r ∧ k' l = abs' r) ∨
    (∃abs abs' t t'.
       a0 = (abs,abs') ∧ a1 = Tau t ∧ a2 = Tau t' ∧
       ∃r. t = abs r ∧ t' = abs' r) ∨
    ∃abs abs' t t'.
      a0 = (abs,abs') ∧ a1 = Tau t ∧ a2 = Tau t' ∧
      strong_bisim_upfrom_abs (abs,abs') t t'

⊢ ∀strong_bisim_upfrom_abs'.
    (∀a0 a1 a2.
       strong_bisim_upfrom_abs' a0 a1 a2 ⇒
       (∃abs abs' x. a0 = (abs,abs') ∧ a1 = Ret x ∧ a2 = Ret x) ∨
       (∃abs abs' e k k'.
          a0 = (abs,abs') ∧ a1 = Vis e k ∧ a2 = Vis e k' ∧
          ∀l. strong_bisim_upfrom_abs' (abs,abs') (k l) (k' l) ∨
              ∃r. k l = abs r ∧ k' l = abs' r) ∨
       (∃abs abs' t t'.
          a0 = (abs,abs') ∧ a1 = Tau t ∧ a2 = Tau t' ∧
          ∃r. t = abs r ∧ t' = abs' r) ∨
       ∃abs abs' t t'.
         a0 = (abs,abs') ∧ a1 = Tau t ∧ a2 = Tau t' ∧
         strong_bisim_upfrom_abs' (abs,abs') t t') ⇒
    ∀a0 a1 a2.
      strong_bisim_upfrom_abs' a0 a1 a2 ⇒ strong_bisim_upfrom_abs a0 a1 a2

⊢ (∀abs abs' x. strong_bisim_upfrom_abs (abs,abs') (Ret x) (Ret x)) ∧
  (∀abs abs' e k k'.
     (∀l. strong_bisim_upfrom_abs (abs,abs') (k l) (k' l) ∨
          ∃r. k l = abs r ∧ k' l = abs' r) ⇒
     strong_bisim_upfrom_abs (abs,abs') (Vis e k) (Vis e k')) ∧
  (∀abs abs' t t'.
     (∃r. t = abs r ∧ t' = abs' r) ⇒
     strong_bisim_upfrom_abs (abs,abs') (Tau t) (Tau t')) ∧
  ∀abs abs' t t'.
    strong_bisim_upfrom_abs (abs,abs') t t' ⇒
    strong_bisim_upfrom_abs (abs,abs') (Tau t) (Tau t')

⊢ ∀abs t t'. strong_bisim_upfrom_abs (abs,abs) t t' ⇔ t = t'

⊢ (∀r. strong_bisim_upfrom_abs (abs,abs') (k r) (k' r)) ⇒
  strong_bisim_upfrom_abs (abs,abs') (itree_bind t k) (itree_bind t k')

⊢ ∀t t'. untau t = untau t' ⇒ itree_wbisim t t'

⊢ untau spin = Div

⊢ set_compatible wbisim_functional upto_taus_func

⊢ (itree_wbisim t (FUNPOW Tau n ht) ⇔ itree_wbisim t ht) ∧
  (itree_wbisim (FUNPOW Tau n ht) t ⇔ itree_wbisim ht t)

⊢ ∀t t'. itree_wbisim t t' ⇒ untau t = untau t'

⊢ X ⊆ Y ⇒ wbisim_functional X ⊆ wbisim_functional Y

⊢ gfp wbisim_functional = rel_to_reln itree_wbisim

⊢ monotone wbisim_functional

⊢ itree_wbisim t spin ⇔ t = spin

⊢ ∀a0 a1 a2.
    weak_bisim_upfrom_abs a0 a1 a2 ⇔
    (∃abs abs' x.
       a0 = (abs,abs') ∧ strip_tau a1 (Ret x) ∧ strip_tau a2 (Ret x)) ∨
    (∃abs abs' e k k' n n' r.
       a0 = (abs,abs') ∧ strip_tau a1 (Vis e k) ∧ strip_tau a2 (Vis e k') ∧
       ∀l. weak_bisim_upfrom_abs (abs,abs') (k l) (k' l) ∨
           k l = FUNPOW Tau n (abs r) ∧ k' l = FUNPOW Tau n' (abs' r)) ∨
    (∃abs abs' n n' r.
       a0 = (abs,abs') ∧ a1 = FUNPOW Tau (SUC n) (abs r) ∧
       a2 = FUNPOW Tau (SUC n') (abs' r)) ∨
    ∃abs abs' n n' t t'.
      a0 = (abs,abs') ∧ a1 = FUNPOW Tau (SUC n) t ∧
      a2 = FUNPOW Tau (SUC n') t' ∧ weak_bisim_upfrom_abs (abs,abs') t t'

⊢ ∀weak_bisim_upfrom_abs'.
    (∀a0 a1 a2.
       weak_bisim_upfrom_abs' a0 a1 a2 ⇒
       (∃abs abs' x.
          a0 = (abs,abs') ∧ strip_tau a1 (Ret x) ∧ strip_tau a2 (Ret x)) ∨
       (∃abs abs' e k k' n n' r.
          a0 = (abs,abs') ∧ strip_tau a1 (Vis e k) ∧
          strip_tau a2 (Vis e k') ∧
          ∀l. weak_bisim_upfrom_abs' (abs,abs') (k l) (k' l) ∨
              k l = FUNPOW Tau n (abs r) ∧ k' l = FUNPOW Tau n' (abs' r)) ∨
       (∃abs abs' n n' r.
          a0 = (abs,abs') ∧ a1 = FUNPOW Tau (SUC n) (abs r) ∧
          a2 = FUNPOW Tau (SUC n') (abs' r)) ∨
       ∃abs abs' n n' t t'.
         a0 = (abs,abs') ∧ a1 = FUNPOW Tau (SUC n) t ∧
         a2 = FUNPOW Tau (SUC n') t' ∧
         weak_bisim_upfrom_abs' (abs,abs') t t') ⇒
    ∀a0 a1 a2.
      weak_bisim_upfrom_abs' a0 a1 a2 ⇒ weak_bisim_upfrom_abs a0 a1 a2

⊢ (∀abs abs' t t' x.
     strip_tau t (Ret x) ∧ strip_tau t' (Ret x) ⇒
     weak_bisim_upfrom_abs (abs,abs') t t') ∧
  (∀abs abs' e k k' n n' r t t'.
     strip_tau t (Vis e k) ∧ strip_tau t' (Vis e k') ∧
     (∀l. weak_bisim_upfrom_abs (abs,abs') (k l) (k' l) ∨
          k l = FUNPOW Tau n (abs r) ∧ k' l = FUNPOW Tau n' (abs' r)) ⇒
     weak_bisim_upfrom_abs (abs,abs') t t') ∧
  (∀abs abs' n n' r.
     weak_bisim_upfrom_abs (abs,abs') (FUNPOW Tau (SUC n) (abs r))
       (FUNPOW Tau (SUC n') (abs' r))) ∧
  ∀abs abs' n n' t t'.
    weak_bisim_upfrom_abs (abs,abs') t t' ⇒
    weak_bisim_upfrom_abs (abs,abs') (FUNPOW Tau (SUC n) t)
      (FUNPOW Tau (SUC n') t')

⊢ weak_bisim_upfrom_abs (abs,abs') spin spin

⊢ weak_bisim_upfrom_abs (abs,abs') t'' t'³' ⇒
  weak_bisim_upfrom_abs (abs,abs') (Tau t'') t'³'

⊢ weak_bisim_upfrom_abs (abs,abs') t'' t'³' ⇒
  weak_bisim_upfrom_abs (abs,abs') t'' (Tau t'³')

⊢ itree_wbisim t t' ∧ (∀r. weak_bisim_upfrom_abs (abs,abs') (k r) (k' r)) ⇒
  weak_bisim_upfrom_abs (abs,abs') (itree_bind t k) (itree_bind t' k')

⊢ weak_bisim_upfrom_abs (abs,abs') t'' t'³' ⇒
  weak_bisim_upfrom_abs (abs,abs') (FUNPOW Tau n t'') (FUNPOW Tau n' t'³')

⊢ weak_bisim_upfrom_abs (abs,abs) t' t'' ⇔ itree_wbisim t' t''