--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/drops_2.ma".
+include "ground_2/lib/streams_hdtl.ma".
+
+(* STREAMS ******************************************************************)
+
+let rec tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
+cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
+qed.
+
+interpretation "recursive tail (strams)" 'Drops n f = (tls ? n f).
+
+(* basic properties *********************************************************)
+
+lemma tls_rew_O (A) (t): t = tls A 0 t.
+// qed.
+
+lemma tls_rew_S (A) (n) (t): ↓↓*[n]t = tls A (⫯n) t.
+// qed.
+
+lemma tls_S1 (A) (n) (t): ↓*[n]↓t = tls A (⫯n) t.
+#A #n elim n -n //
+qed.
+
+lemma tls_eq_repl (A) (n): eq_stream_repl A (λt1,t2. ↓*[n] t1 ≐ ↓*[n] t2).
+#A #n elim n -n //
+#n #IH * #n1 #t1 * #n2 #t2 #H elim (eq_stream_inv_seq … H) /2 width=7 by/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_sand.ma".
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/rintersection_3.ma".
+include "ground_2/relocation/rtmap_sle.ma".
+
+coinductive sand: relation3 rtmap rtmap rtmap ≝
+| sand_pp: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → sand g1 g2 g
+| sand_np: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ⫯f1 = g1 → ↑f2 = g2 → ↑f = g → sand g1 g2 g
+| sand_pn: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → sand g1 g2 g
+| sand_nn: ∀f1,f2,f,g1,g2,g. sand f1 f2 f → ⫯f1 = g1 → ⫯f2 = g2 → ⫯f = g → sand g1 g2 g
+.
+
+interpretation "intersection (rtmap)"
+ 'RIntersection f1 f2 f = (sand f1 f2 f).
+
+(* Basic properties *********************************************************)
+
+let corec sand_refl: ∀f. f ⋒ f ≡ f ≝ ?.
+#f cases (pn_split f) * #g #H
+[ @(sand_pp … H H H) | @(sand_nn … H H H) ] -H //
+qed.
+
+let corec sand_sym: ∀f1,f2,f. f1 ⋒ f2 ≡ f → f2 ⋒ f1 ≡ f ≝ ?.
+#f1 #f2 #f * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
+[ @sand_pp | @sand_pn | @sand_np | @sand_nn ]
+[4,11,18,25: @sand_sym // |1,2,3,8,9,10,15,16,17,22,23,24: skip |*: // ]
+qed-.
[ { "multiple relocation" * } {
[ { "" * } {
[ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
- [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_sand" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
+ [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "nstream_sand" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
(*
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]