Name Conclusion Link
stream_1 sreplicate = siterate I link to proof
stream_2 smap I = I link to proof
stream_3 !s. stake s 0 = [] link to proof
stream_4 !s. stream (snth s) = s link to proof
stream_5 !s. sappend [] s = s link to proof
stream_6 !s. sdrop s 0 = s link to proof
stream_7 !f. snth (stream f) = f link to proof
stream_8 !s. shd s = snth s 0 link to proof
stream_9 !a. sreplicate a = scons a (sreplicate a) link to proof
stream_10 !s. stl s = sdrop s 1 link to proof
stream_11 !s. sdrop s 1 = stl s link to proof
stream_12 !a n. snth (sreplicate a) n = a link to proof
stream_13 !h t. shd (scons h t) = h link to proof
stream_14 !h t. stl (scons h t) = t link to proof
stream_15 !s n. LENGTH (stake s n) = n link to proof
stream_16 !s. snth s 1 = shd (stl s) link to proof
stream_17 !h t. snth (scons h t) 0 = h link to proof
stream_18 !f. siterate f = sunfold (\a. a,f a) link to proof
stream_19 !s. stake s 1 = [shd s] link to proof
stream_20 !s n. sdrop s n = funpow stl n s link to proof
stream_21 !s n. shd (sdrop s n) = snth s n link to proof
stream_22 !s1 s2. ssplit (sinterleave s1 s2) = s1,s2 link to proof
stream_23 !f b. shd (sunfold f b) = FST (f b) link to proof
stream_24 !s n. snth s (SUC n) = snth (stl s) n link to proof
stream_25 !s n. sdrop s (SUC n) = stl (sdrop s n) link to proof
stream_26 !s n. sdrop s (SUC n) = sdrop (stl s) n link to proof
stream_27 !f s. smap f s = stream (f o snth s) link to proof
stream_28 !f a. siterate f a = scons a (siterate f (f a)) link to proof
stream_29 !f g. smap f o smap g = smap (f o g) link to proof
stream_30 !f b. stl (sunfold f b) = sunfold f (SND (f b)) link to proof
stream_31 !s n. sdrop s n = stream (\m. snth s (m + n)) link to proof
stream_32 !h t n. snth (scons h t) (SUC n) = snth t n link to proof
stream_33 !s n. stake s (SUC n) = CONS (shd s) (stake (stl s) n) link to proof
stream_34 !h t s. sappend (CONS h t) s = scons h (sappend t s) link to proof
stream_35 !l1 l2 s. sappend (APPEND l1 l2) s = sappend l1 (sappend l2 s) link to proof
stream_36 !s m n. snth s (m + n) = snth (sdrop s n) m link to proof
stream_37 !s1 s2. (!n. snth s1 n = snth s2 n) <=> s1 = s2 link to proof
stream_38 !s1 s2. (!n. snth s1 n = snth s2 n) ==> s1 = s2 link to proof
stream_39 !f g s. smap (f o g) s = smap f (smap g s) link to proof
stream_40 !f b. sunfold f b = stream (\n. FST (f (funpow (SND o f) n b))) link to proof
stream_41 !s n. stake s (SUC n) = APPEND (stake s n) [snth s n] link to proof
stream_42 !s n i. i < n ==> nth (stake s n) i = snth s i link to proof
stream_43 !h t. scons h t = stream (\n. if n = 0 then h else snth t (n - 1)) link to proof
stream_44 !s m n. stake s (m + n) = APPEND (stake s m) (stake (sdrop s m) n) link to proof
stream_45 !s n. snth s n = (if n = 0 then shd s else snth (stl s) (n - 1)) link to proof
stream_46 !s n x. MEM x (stake s n) <=> (?i. i < n /\ x = snth s i) link to proof
stream_47 !s n. stake s n = (if n = 0 then [] else CONS (shd s) (stake (stl s) (n - 1))) link to proof
stream_48 !l s. sappend l s = stream (\n. if n < LENGTH l then nth l n else snth s (n - LENGTH l)) link to proof
stream_49 !f b. sunfold f b = (let a,b' = f b in scons a (sunfold f b')) link to proof
stream_50 !f b n k. snth (sunfold f b) (n + k) = snth (sunfold f (funpow (SND o f) n b)) k link to proof
stream_51 !l s n. snth (sappend l s) n = (if n < LENGTH l then nth l n else snth s (n - LENGTH l)) link to proof
stream_52 !s n. set_of_list (stake s n) = {x | ?i. i < n /\ x = snth s i} link to proof
stream_53 !s1 s2. sinterleave s1 s2 = stream (\n. if EVEN n then snth s1 (n DIV 2) else snth s2 (n DIV 2)) link to proof
stream_54 !s. ssplit s = stream (\n. snth s (2 * n)),stream (\n. snth s (2 * n + 1)) link to proof
stream_55 !p. (!m. ?n. m <= n /\ p n) ==> (?s. (!i j. snth s i <= snth s j <=> i <= j) /\ (!n. p n <=> (?i. snth s i = n))) link to proof
Back to ProofCloud main page