(* *)
(**************************************************************************)
-include "ground/notation/functions/downdashedarrowstar_3.ma".
+include "ground/notation/functions/downharpoonrightstar_3.ma".
include "ground/lib/stream_hdtl.ma".
include "ground/arith/nat_succ_iter.ma".
interpretation
"iterated tail (strams)"
- 'DownDashedArrowStar A n f = (stream_tls A n f).
+ 'DownHarpoonRightStar A n f = (stream_tls A n f).
(* Basic constructions ******************************************************)
lemma stream_tls_zero (A) (t):
- t = â\87£*{A}[𝟎]t.
+ t = â\87\82*{A}[𝟎]t.
// qed.
lemma stream_tls_tl (A) (n) (t):
- (â\87£â\87£*[n]t) = â\87£*{A}[n]â\87£t.
+ (â\87\82â\87\82*[n]t) = â\87\82*{A}[n]â\87\82t.
#A #n #t
@(niter_appl … (stream_tl …))
qed.
lemma stream_tls_succ (A) (n) (t):
- (â\87£â\87£*[n]t) = â\87£*{A}[↑n]t.
+ (â\87\82â\87\82*[n]t) = â\87\82*{A}[↑n]t.
#A #n #t
@(niter_succ … (stream_tl …))
qed.
lemma stream_tls_swap (A) (n) (t):
- (⇣*[n]⇣t) = ⇣*{A}[↑n]t.
+ (⇂*[n]⇂t) = ⇂*{A}[↑n]t.
+// qed.
+
+(* Advanced constructions ***************************************************)
+
+lemma stream_tls_unit (A) (t):
+ ⇂t = ⇂*{A}[𝟏]t.
+// qed.
+
+lemma stream_tls_succ_lcons (A) (n) (a) (t):
+ ⇂*[n]t = ⇂*{A}[↑n](a⨮t).
// qed.