(* *)
(**************************************************************************)
-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):
- (â\87£*[n]â\87£t) = â\87£*{A}[↑n]t.
+ (â\87\82*[n]â\87\82t) = â\87\82*{A}[↑n]t.
// qed.