(* *)
(**************************************************************************)
-include "ground/notation/functions/downspoonstar_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)"
- 'DownSpoonStar 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 = â«°*{A}[𝟎]t.
+ t = â\87\82*{A}[𝟎]t.
// qed.
lemma stream_tls_tl (A) (n) (t):
- (â«°â«°*[n]t) = â«°*{A}[n]â«°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):
- (â«°â«°*[n]t) = â«°*{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.