Entry |
Value |
Name |
stream_51 |
Conclusion |
!l s n.
snth (sappend l s) n =
(if n < LENGTH l then nth l n else snth s (n - LENGTH l)) |
Constructive Proof |
Yes |
Axiom |
N|A |
Classical Lemmas |
N|A |
Constructive Lemmas |
T!t. (!x. t) <=> t!t. (T <=> t) <=> t!l s n.
snth (sappend l s) n =
(if n < LENGTH l then nth l n else snth s (n - LENGTH l))!l s.
sappend l s =
stream (\n. if n < LENGTH l then nth l n else snth s (n - LENGTH l))!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. |