Entry |
Value |
Name |
stream_53 |
Conclusion |
!s1 s2.
sinterleave s1 s2 =
stream (\n. if EVEN n then snth s1 (n DIV 2) else snth s2 (n DIV 2)) |
Constructive Proof |
Yes |
Axiom |
N|A |
Classical Lemmas |
N|A |
Constructive Lemmas |
T!x. x = x!t. (!x. t) <=> t!f y. (\x. f x) y = f y!s1 s2.
sinterleave s1 s2 =
stream (\n. if EVEN n then snth s1 (n DIV 2) else snth s2 (n DIV 2))T <=> (\p. p) = (\p. p)(/\) = (\p q. (\f. f p q) = (\f. f T T))(==>) = (\p q. p /\ q <=> p)(!) = (\p. p = (\x. T))NUMERAL = (\n. n) |
Contained Package |
stream |
Comment |
Stream package from OpenTheory. |