Theory itree

⊢ ∀itr f. ibind itr f = iflat (imap f itr)

⊢ ∀itr.
    iflat itr =
    itree_unfold
      (λx.
         case x of
           INL (ireturn (ireturn r0)) => Ret' r0
         | INL (ireturn Div) => Div'
         | INL (ireturn (Vis e f)) => Vis' e (λi. INR (f i))
         | INL Div => Div'
         | INL (Vis e f) => Vis' e (λi. INL (f i))
         | INR (ireturn r) => Ret' r
         | INR Div => Div'
         | INR (Vis e' f') => Vis' e' (λi. INR (f' i))) (INL itr)

⊢ ∀g itr.
    imap g itr =
    itree_unfold (λx. itree_CASE x (λr. Ret' (g r)) Div' (λe f. Vis' e f))
      itr

⊢ ∃rep. TYPE_DEFINITION itree_rep_ok rep

⊢ ∀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 Stuck 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 Stuck = 0

⊢ ∀f1 f2 f3.
    itree_nextMAP f1 f2 f3 =
    itree_next_ABS ∘ SUM_MAP f2 (SUM_MAP I (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 (K ∅) ∘ 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 v f0. itree_next_CASE (Ret' a0) f v f0 = f a0) ∧
  (∀f v f0. itree_next_CASE Div' f v f0 = v) ∧
  ∀a0 a1 f v f0. itree_next_CASE (Vis' a0 a1) f v f0 = f0 a0 a1

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

⊢ ∀x y. ireturn x = ireturn y ⇔ x = y

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

⊢ ∀a0 a1 a2.
    at_path a0 a1 a2 ⇔
    a0 = ireturn a2 ∧ a1 = [] ∨
    ∃f i ov p. a0 = Vis ov f ∧ a1 = (ov,i)::p ∧ at_path (f i) p a2

⊢ at_path itree p e ⇒ iset itree e

⊢ ∀at_path'.
    (∀e. at_path' (ireturn e) [] e) ∧
    (∀e f i ov p. at_path' (f i) p e ⇒ at_path' (Vis ov f) ((ov,i)::p) e) ⇒
    ∀a0 a1 a2. at_path a0 a1 a2 ⇒ at_path' a0 a1 a2

⊢ ∀e. at_path (ireturn e) [] e

⊢ (∀e. at_path (ireturn e) [] e) ∧
  ∀e f i ov p. at_path (f i) p e ⇒ at_path (Vis ov f) ((ov,i)::p) e

⊢ ∀at_path'.
    (∀e. at_path' (ireturn e) [] e) ∧
    (∀e f i ov p.
       at_path (f i) p e ∧ at_path' (f i) p e ⇒
       at_path' (Vis ov f) ((ov,i)::p) e) ⇒
    ∀a0 a1 a2. at_path a0 a1 a2 ⇒ at_path' a0 a1 a2

⊢ (at_path Div p e ⇔ F) ∧ (at_path (ireturn e) p a ⇔ p = [] ∧ a = e) ∧
  (at_path (Vis ov f) p e ⇔ ∃i l. p = (ov,i)::l ∧ at_path (f i) l e)

⊢ ∀e f i ov p. at_path (f i) p e ⇒ at_path (Vis ov f) ((ov,i)::p) e

⊢ DATATYPE (itree ireturn Div Vis)

⊢ DATATYPE (itree_el Event Return Stuck)

⊢ DATATYPE (itree_next Ret' Div' Vis')

⊢ ibind itr (λx. ibind (f x) g) = ibind (ibind itr f) g

⊢ ibind itr f = Div ⇔ itr = Div ∨ ∃x. itr = ireturn x ∧ f x = Div

⊢ ibind itr f = ireturn v ⇔ ∃v'. itr = ireturn v' ∧ f v' = ireturn v

⊢ ibind itr f = Vis rv g ⇔
  (∃h. itr = Vis rv h ∧ iflat ∘ imap f ∘ h = g) ∨
  ∃x. itr = ireturn x ∧ f x = Vis rv g

⊢ ibind (ireturn itr) f = f itr

⊢ ibind itr ireturn = itr

⊢ ∀P a0.
    ievery P a0 ⇔
    a0 = Div ∨ (∃e. a0 = ireturn e ∧ P e) ∨
    ∃f ov. a0 = Vis ov f ∧ ∀iv. ievery P (f iv)

⊢ ∀P ievery'.
    (∀a0.
       ievery' a0 ⇒
       a0 = Div ∨ (∃e. a0 = ireturn e ∧ P e) ∨
       ∃f ov. a0 = Vis ov f ∧ ∀iv. ievery' (f iv)) ⇒
    ∀a0. ievery' a0 ⇒ ievery P a0

⊢ ∀P. ievery P Div

⊢ ∀P e. P e ⇒ ievery P (ireturn e)

⊢ ∀P. ievery P Div ∧ (∀e. P e ⇒ ievery P (ireturn e)) ∧
      ∀f ov. (∀iv. ievery P (f iv)) ⇒ ievery P (Vis ov f)

⊢ ∀itr. ievery P itr ⇔ ∀rv. iset itr rv ⇒ P rv

⊢ (ievery P Div ⇔ T) ∧ (ievery P (ireturn e) ⇔ P e) ∧
  (ievery P (Vis ov f) ⇔ ∀iv. ievery P (f iv))

⊢ ∀P f ov. (∀iv. ievery P (f iv)) ⇒ ievery P (Vis ov f)

⊢ ∀P a0.
    iexists P a0 ⇔
    (∃e. a0 = ireturn e ∧ P e) ∨
    ∃f ov. a0 = Vis ov f ∧ ∃iv. iexists P (f iv)

⊢ ∀P iexists'.
    (∀e. P e ⇒ iexists' (ireturn e)) ∧
    (∀f ov. (∃iv. iexists' (f iv)) ⇒ iexists' (Vis ov f)) ⇒
    ∀a0. iexists P a0 ⇒ iexists' a0

⊢ ∀P e. P e ⇒ iexists P (ireturn e)

⊢ ∀P. (∀e. P e ⇒ iexists P (ireturn e)) ∧
      ∀f ov. (∃iv. iexists P (f iv)) ⇒ iexists P (Vis ov f)

⊢ iexists P itr ⇔ ∃x. iset itr x ∧ P x

⊢ ∀P iexists'.
    (∀e. P e ⇒ iexists' (ireturn e)) ∧
    (∀f ov. (∃iv. iexists P (f iv) ∧ iexists' (f iv)) ⇒ iexists' (Vis ov f)) ⇒
    ∀a0. iexists P a0 ⇒ iexists' a0

⊢ (iexists P Div ⇔ F) ∧ (iexists P (ireturn e) ⇔ P e) ∧
  (iexists P (Vis ov f) ⇔ ∃iv. iexists P (f iv))

⊢ ∀P f ov. (∃iv. iexists P (f iv)) ⇒ iexists P (Vis ov f)

⊢ ∀a0.
    ifinite a0 ⇔
    (∃e. a0 = ireturn e) ∨ a0 = Div ∨
    ∃f ov. a0 = Vis ov f ∧ ∀iv. ifinite (f iv)

⊢ ifinite Div

⊢ ∀ifinite'.
    (∀e. ifinite' (ireturn e)) ∧ ifinite' Div ∧
    (∀f ov. (∀iv. ifinite' (f iv)) ⇒ ifinite' (Vis ov f)) ⇒
    ∀a0. ifinite a0 ⇒ ifinite' a0

⊢ ∀e. ifinite (ireturn e)

⊢ (∀e. ifinite (ireturn e)) ∧ ifinite Div ∧
  ∀f ov. (∀iv. ifinite (f iv)) ⇒ ifinite (Vis ov f)

⊢ ∀ifinite'.
    (∀e. ifinite' (ireturn e)) ∧ ifinite' Div ∧
    (∀f ov. (∀iv. ifinite (f iv) ∧ ifinite' (f iv)) ⇒ ifinite' (Vis ov f)) ⇒
    ∀a0. ifinite a0 ⇒ ifinite' a0

⊢ ∀f ov. (∀iv. ifinite (f iv)) ⇒ ifinite (Vis ov f)

⊢ iflat Div = Div

⊢ iflat itr = Div ⇔ itr = Div ∨ itr = ireturn Div

⊢ (iflat itr = ireturn rv ⇔ itr = ireturn (ireturn rv)) ∧
  (ireturn rv = iflat itr ⇔ itr = ireturn (ireturn rv))

⊢ iflat itr = Vis ov f ⇔
  (∃g. itr = Vis ov g ∧ iflat ∘ g = f) ∨ itr = ireturn (Vis ov f)

⊢ iflat (ireturn r) = r

⊢ iflat (Vis ov f) = Vis ov (iflat ∘ f)

⊢ imap (f ∘ g) itr = imap f (imap g itr)

⊢ imap g Div = Div

⊢ (imap g itr = Div ⇔ itr = Div) ∧ (Div = imap g itr ⇔ itr = Div)

⊢ ireturn r = imap g itr ⇔ ∃x. itr = ireturn x ∧ g x = r

⊢ Vis rv f = imap g itr ⇔ ∃h. itr = Vis rv h ∧ imap g ∘ h = f

⊢ imap (λx. x) itr = itr

⊢ imap g (ireturn rv) = ireturn (g rv)

⊢ imap f (Vis ov g) = Vis ov (imap f ∘ g)

⊢ ∀a0 a1.
    iset a0 a1 ⇔ a0 = ireturn a1 ∨ ∃f i ov. a0 = Vis ov f ∧ iset (f i) a1

⊢ ∀itr e. iset (iflat itr) e ⇔ ∃t0. iset itr t0 ∧ iset t0 e

⊢ ∀itr e. iset (iflat itr) e ⇒ ∃t0. iset itr t0 ∧ iset t0 e

⊢ ∀itr t0 e. iset itr t0 ∧ iset t0 e ⇒ iset (iflat itr) e

⊢ iset itree e ⇔ ∃p. at_path itree p e

⊢ ∀iset'.
    (∀e. iset' (ireturn e) e) ∧
    (∀e f i ov. iset' (f i) e ⇒ iset' (Vis ov f) e) ⇒
    ∀a0 a1. iset a0 a1 ⇒ iset' a0 a1

⊢ iset (imap f itr) = IMAGE f (iset itr)

⊢ ∀itr x. iset (imap f itr) x ⇒ ∃y. x = f y ∧ iset itr y

⊢ ∀itr. iset itr y ⇒ iset (imap f itr) (f y)

⊢ ∀e. iset (ireturn e) e

⊢ (∀e. iset (ireturn e) e) ∧ ∀e f i ov. iset (f i) e ⇒ iset (Vis ov f) e

⊢ ∀iset'.
    (∀e. iset' (ireturn e) e) ∧
    (∀e f i ov. iset (f i) e ∧ iset' (f i) e ⇒ iset' (Vis ov f) e) ⇒
    ∀a0 a1. iset a0 a1 ⇒ iset' a0 a1

⊢ (iset (ireturn e) e' ⇔ e = e') ∧ (iset Div e ⇔ F) ∧
  (iset (Vis ov f) e ⇔ ∃i. iset (f i) e)

⊢ iset itr elem ⇒ ∃n. iset (itruncate n itr) elem

⊢ ∀e f i ov. iset (f i) e ⇒ iset (Vis ov f) e

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

⊢ itree_CASE (ireturn r) ret div vis = ret r ∧
  itree_CASE Div ret div vis = div ∧
  itree_CASE (Vis a g) ret div vis = vis a g

⊢ ∀M M' ret div vis ret' div' vis'.
    M = M' ∧ (∀x. M' = ireturn x ⇒ ret x = ret' x) ∧
    (M' = Div ⇒ div = div') ∧ (∀a g. M' = Vis a g ⇒ vis a g = vis' a g) ⇒
    itree_CASE M ret div vis = itree_CASE M' ret' div' vis'

⊢ ∀f. f (itree_CASE t ret div vis) ⇔
      (∃r. t = ireturn r ∧ f (ret r)) ∨ t = Div ∧ f div ∨
      ∃a g. t = Vis a g ∧ f (vis a g)

⊢ itree_CASE t ret div vis = v ⇔
  (∃r. t = ireturn r ∧ ret r = v) ∨ t = Div ∧ div = v ∨
  ∃a g. t = Vis a g ∧ vis a g = v

⊢ ∀t1 t2.
    t1 = t2 ⇔
    ∃R. R t1 t2 ∧ (∀x t. R (ireturn x) t ⇒ t = ireturn x) ∧
        (∀t. R Div t ⇒ t = Div) ∧
        ∀a f t. R (Vis a f) t ⇒ ∃b g. t = Vis a g ∧ ∀s. R (f s) (g s)

⊢ ∀t. (∃x. t = ireturn x) ∨ t = Div ∨ ∃a g. t = Vis a g

⊢ (∀x. ireturn x ≠ Div) ∧ (∀x g e. ireturn x ≠ Vis e g) ∧
  ∀g e. Div ≠ 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 Stuck = 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' = Stuck ⇒ 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 = Stuck ∧ v = v'

⊢ itree_el (ireturn r) [] = Return r ∧ itree_el Div [] = Stuck ∧
  itree_el (Vis e g) [] = Event e ∧
  itree_el (ireturn r) (a::ns) = Return ARB ∧
  itree_el Div (a::ns) = Return ARB ∧
  itree_el (Vis e g) (a::ns) = itree_el (g a) ns

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

⊢ ∀t1 t2. t1 = t2 ⇔ ∀path. itree_el t1 path = itree_el t2 path

⊢ ∀P. (∀e. P (Event e)) ∧ (∀r. P (Return r)) ∧ P Stuck ⇒ ∀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 = Stuck

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

⊢ (∀a0 a0'. Ret' a0 = Ret' 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) ∧ h Div' = f1 ∧
    ∀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 v f0.
    M = M' ∧ (∀a0. M' = Ret' a0 ⇒ f a0 = f' a0) ∧ (M' = Div' ⇒ v = v') ∧
    (∀a0 a1. M' = Vis' a0 a1 ⇒ f0 a0 a1 = f0' a0 a1) ⇒
    itree_next_CASE M f v f0 = itree_next_CASE M' f' v' f0'

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

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

⊢ ∀P. (∀r. P (Ret' r)) ∧ P Div' ∧ (∀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 (INR (ARB,K a3))) a3)) a3)

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

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

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

⊢ itree_unfold_err f (rel,err_f,err) seed =
  case f seed of
    Ret' r => ireturn r
  | Div' => Div
  | Vis' e g =>
    Vis e
      (λa.
         case a of
           INL x => ireturn (err_f e x)
         | INR y =>
           if rel e y then itree_unfold_err f (rel,err_f,err) (g y)
           else ireturn (err e))

⊢ (∀itr. itruncate 0 itr = Div) ∧
  (∀v2. itruncate (NUMERAL (BIT1 v2)) Div = Div) ∧
  (∀v2. itruncate (NUMERAL (BIT2 v2)) Div = Div) ∧
  (∀v3 rv. itruncate (NUMERAL (BIT1 v3)) (ireturn rv) = ireturn rv) ∧
  (∀v3 rv. itruncate (NUMERAL (BIT2 v3)) (ireturn rv) = ireturn rv) ∧
  (∀v4 ov f.
     itruncate (NUMERAL (BIT1 v4)) (Vis ov f) =
     Vis ov (λx. itruncate (NUMERAL (BIT1 v4) − 1) (f x))) ∧
  ∀v4 ov f.
    itruncate (NUMERAL (BIT2 v4)) (Vis ov f) =
    Vis ov (λx. itruncate (NUMERAL (BIT2 v4) − 1) (f x))

⊢ (∀itr. itruncate 0 itr = Div) ∧ (∀v2. itruncate (SUC v2) Div = Div) ∧
  (∀v3 rv. itruncate (SUC v3) (ireturn rv) = ireturn rv) ∧
  ∀v4 ov f.
    itruncate (SUC v4) (Vis ov f) =
    Vis ov (λx. itruncate (SUC v4 − 1) (f x))

⊢ ∀itr. itruncate n itr = itr ⇒ ifinite itr

⊢ ∀P. (∀itr. P 0 itr) ∧ (∀v2. P (SUC v2) Div) ∧
      (∀v3 rv. P (SUC v3) (ireturn rv)) ∧
      (∀v4 ov f. (∀x. P (SUC v4 − 1) (f x)) ⇒ P (SUC v4) (Vis ov f)) ⇒
      ∀v v1. P v v1

⊢ ∀n. itruncate n itr = ireturn r ⇔ itr = ireturn r ∧ n ≠ 0

⊢ ¬ievery P itr ⇔ iexists (λx. ¬P x) itr