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