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)

⊢ (∀a f f1 v. itree_el_CASE (Event a) f f1 v = f a) ∧
  (∀a f f1 v. itree_el_CASE (Return a) f f1 v = f1 a) ∧
  ∀f f1 v. itree_el_CASE Silence f f1 v = v

⊢ (∀f f1 a. itree_el_size f f1 (Event a) = 1 + f a) ∧
  (∀f f1 a. itree_el_size f f1 (Return a) = 1 + f1 a) ∧
  ∀f f1. itree_el_size f 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)

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

⊢ (∀f f1 f2 f3 a. itree_next_size f f1 f2 f3 (Ret' a) = 1 + f2 a) ∧
  (∀f f1 f2 f3 a. itree_next_size f f1 f2 f3 (Tau' a) = 1 + f3 a) ∧
  ∀f f1 f2 f3 a0 a1. itree_next_size f 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

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

⊢ ∀f0 f1 f2. ∃fn.
    (∀a. fn (Event a) = f0 a) ∧ (∀a. fn (Return a) = f1 a) ∧
    fn Silence = f2

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

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

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

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

⊢ ∀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

⊢ ∀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)

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

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

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

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

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

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

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

⊢ 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''