Theory stream

⊢ ∀f s1 s2. liftBin f s1 s2 = (λi. f (s1 i) (s2 i))

⊢ (∀a s. scons a s 0 = a) ∧ ∀a s n. scons a s (SUC n) = s n

⊢ ∀x. sconst x = (λi. x)

⊢ ∀n s. sdrop n s = FUNPOW stl n s

⊢ ∀s t. seventuallyeq s t ⇔ ∃i. sdrop i s = sdrop i t

⊢ ∀P s. sexists P s ⇔ ∃i. P (s i)

⊢ ∀f x. siterate f x = (λn. FUNPOW f n x)

⊢ ∀f s. smap f s = sunfold (f ∘ (λs. s 0)) stl s

⊢ ∀R s1 s2. srel R s1 s2 ⇔ ∀i. R (s1 i) (s2 i)

⊢ ∀s. sset s = {a | ∃i. s i = a}

⊢ ∀s. stl s = (λn. s (n + 1))

⊢ ∀hd tl sd. sunfold hd tl sd = (λn. hd (siterate tl sd n))

⊢ ∀s. sunzip s = (smap FST s,smap SND s)

⊢ szip = liftBin $,

⊢ countable (sset s)

⊢ (∀x y. f x y = f y x) ⇒ liftBin f s1 s2 = liftBin f s2 s1

⊢ s1 = s2 ⇔
  ∃R. R s1 s2 ∧
      ∀t1 t2.
        R t1 t2 ⇒ t1 0 = t2 0 ∧ (R (stl t1) (stl t2) ∨ stl t1 = stl t2)

⊢ scons a s = scons b t ⇔ a = b ∧ s = t

⊢ scons a s = (λn. case n of 0 => a | SUC m => s m)

⊢ (∀a s. scons a s 0 = a) ∧
  (∀a s n. scons a s (NUMERAL (BIT1 n)) = s (NUMERAL (BIT1 n) − 1)) ∧
  ∀a s n. scons a s (NUMERAL (BIT2 n)) = s (NUMERAL (BIT1 n))

⊢ scons (s 0) (stl s) = s

⊢ sconst x = scons x (sconst x)

⊢ ∀m n s t. sdrop m s = sdrop m t ∧ m ≤ n ⇒ sdrop n s = sdrop n t

⊢ sdrop 0 s = s ∧ sdrop (SUC n) s = stl (sdrop n s) ∧
  sdrop (NUMERAL (BIT2 n)) s = stl (sdrop (NUMERAL (BIT1 n)) s) ∧
  sdrop (NUMERAL (BIT1 n)) s = stl (sdrop (NUMERAL (BIT1 n) − 1) s)

⊢ seventuallyeq s s

⊢ seventuallyeq s t ⇔ seventuallyeq t s

⊢ seventuallyeq s t ∧ seventuallyeq t u ⇒ seventuallyeq s u

⊢ ∀P. (∀s. P s s) ∧
      (∀h1 h2 s t. P s t ∧ seventuallyeq s t ⇒ P (scons h1 s) (scons h2 t)) ⇒
      ∀s t. seventuallyeq s t ⇒ P s t

⊢ ∀P. (∀h t. P h ⇒ Q (scons h t)) ∧
      (∀h t. Q t ∧ sexists P t ⇒ Q (scons h t)) ⇒
      ∀s. sexists P s ⇒ Q s

⊢ sexists P (scons h t) ⇔ P h ∨ sexists P t

⊢ scons a s 0 = a

⊢ liftBin f s1 s2 0 = f (s1 0) (s2 0)

⊢ siterate f sd 0 = sd

⊢ siterate f sd = scons sd (siterate f (f sd))

⊢ smap f s = f ∘ s

⊢ s1 = s2 ∧ (∀x. x ∈ sset s2 ⇒ f x = g x) ⇒ smap f s1 = smap g s2

⊢ smap (λx. x) s = s

⊢ smap f (smap g s) = smap (f ∘ g) s

⊢ smap f (scons a s) = scons (f a) (smap f s)

⊢ srel R s1 s2 ⇔
  ∃sps.
    (∀a b. (a,b) ∈ sset sps ⇒ R a b) ∧ smap FST sps = s1 ∧
    smap SND sps = s2

⊢ sset (smap f s) = IMAGE f (sset s)

⊢ stl (scons a s) = s

⊢ stl (liftBin f s1 s2) = liftBin f (stl s1) (stl s2)

⊢ stl (sdrop i s) = sdrop i (stl s)

⊢ stl (siterate f sd) = siterate f (f sd)

⊢ ∀s. ∃h t. s = scons h t

⊢ sunfold hd tl sd0 =
  (let a = hd sd0; sd = tl sd0 in scons a (sunfold hd tl sd))

⊢ szip s1 s2 = (λi. (s1 i,s2 i))

⊢ szip (scons a s1) s2 = scons (a,s2 0) (szip s1 (stl s2)) ∧
  szip s1 (scons b s2) = scons (s1 0,b) (szip (stl s1) s2)

⊢ UNCURRY szip (sunzip s) = s ∧ sunzip (szip s1 s2) = (s1,s2)