| Entry |
Value |
|
Name |
stream_36 |
|
Conclusion |
!s m n. snth s (m + n) = snth (sdrop s n) m |
|
Constructive Proof |
Yes |
|
Axiom |
N|A |
|
Classical Lemmas |
N|A |
|
Constructive Lemmas |
T!t. (!x. t) <=> t!t. (T <=> t) <=> t!s m n. snth s (m + n) = snth (sdrop s n) m!s n. sdrop s n = stream (\m. snth s (m + n))!s. stream (snth s) = sT <=> (\p. p) = (\p. p)(/\) = (\p q. (\f. f p q) = (\f. f T T))(==>) = (\p q. p /\ q <=> p)(!) = (\p. p = (\x. T)) |
|
Contained Package |
stream |
|
Comment |
Stream package from OpenTheory. |
