]
qed-.
+lemma le_elim: ∀R:relation nat.
+ (∀n2. R O (n2)) →
+ (∀n1,n2. R n1 n2 → R (⫯n1) (⫯n2)) →
+ ∀n1,n2. n1 ≤ n2 → R n1 n2.
+#R #IH1 #IH2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2
+/4 width=1 by monotonic_pred/ -IH1 -IH2
+#n1 #H elim (lt_le_false … H) -H //
+qed-.
+
(* Iterators ****************************************************************)
(* Note: see also: lib/arithemetics/bigops.ma *)
interpretation "cons (nstream)" 'Cons b t = (seq ? b t).
coinductive eq_stream (A): relation (stream A) ≝
-| eq_sec: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1@t1) (b2@t2)
+| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1@t1) (b2@t2)
.
interpretation "extensional equivalence (nstream)"
'ExtEq A t1 t2 = (eq_stream A t1 t2).
-definition eq_stream_repl_back (A) (R:predicate …) (t1,t2) ≝
- t1 ≐⦋A⦌ t2 → R t1 → R t2.
+definition eq_stream_repl_back (A) (R:predicate …) ≝
+ ∀t1,t2. t1 ≐⦋A⦌ t2 → R t1 → R t2.
-definition eq_stream_repl_fwd (A) (R:predicate …) (t1,t2) ≝
- t2 ≐⦋A⦌ t1 → R t1 → R t2.
+definition eq_stream_repl_fwd (A) (R:predicate …) ≝
+ ∀t1,t2. t2 ≐⦋A⦌ t1 → R t1 → R t2.
(* Basic inversion lemmas ***************************************************)
qed.
let corec eq_stream_refl: ∀A. reflexive … (eq_stream A) ≝ ?.
-#A * #b #t @eq_sec //
+#A * #b #t @eq_seq //
qed.
let corec eq_stream_sym: ∀A. symmetric … (eq_stream A) ≝ ?.
#A #t1 #t2 * -t1 -t2
-#t1 #t2 #b1 #b2 #Hb #Ht @eq_sec /2 width=1 by/
+#t1 #t2 #b1 #b2 #Hb #Ht @eq_seq /2 width=1 by/
qed-.
-lemma eq_stream_repl_sym: ∀A,R,t1,t2. eq_stream_repl_back A R t1 t2 → eq_stream_repl_fwd A R t1 t2.
-/3 width=1 by eq_stream_sym/ qed-.
+lemma eq_stream_repl_sym: ∀A,R. eq_stream_repl_back A R → eq_stream_repl_fwd A R.
+/3 width=3 by eq_stream_sym/ qed-.
(* Main properties **********************************************************)
let corec eq_stream_trans: ∀A. Transitive … (eq_stream A) ≝ ?.
#A #t1 #t * -t1 -t
#t1 #t #b1 #b #Hb1 #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H
-#Hb2 #Ht2 @eq_sec /2 width=3 by/
+#Hb2 #Ht2 @eq_seq /2 width=3 by/
qed-.
theorem eq_stream_canc_sn: ∀A,t,t1,t2. t ≐ t1 → t ≐ t2 → t1 ≐⦋A⦌ t2.
-/3 width=4 by eq_stream_trans, eq_stream_repl_sym/ qed-.
+/3 width=3 by eq_stream_trans, eq_stream_sym/ qed-.
theorem eq_stream_canc_dx: ∀A,t,t1,t2. t1 ≐ t → t2 ≐ t → t1 ≐⦋A⦌ t2.
-/3 width=4 by eq_stream_trans, eq_stream_repl_sym/ qed-.
+/3 width=3 by eq_stream_trans, eq_stream_sym/ 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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐈𝐝 )"
+ non associative with precedence 90
+ for @{ 'Identity }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ↑ term 46 T )"
+ non associative with precedence 46
+ for @{ 'Lift $T }.
* #a1 #t1 * #a2 #t2 * #c #x #Hx * #d #y #Hy
cases (after_inv_apply … Hx) -Hx #Hc #Hx
cases (after_inv_apply … Hy) -Hy #Hd #Hy
-/3 width=4 by eq_sec/
+/3 width=4 by eq_seq/
qed-.
let corec after_inj: ∀t1,x,t. t1 ⊚ x ≡ t → ∀y. t1 ⊚ y ≡ t → x ≐ y ≝ ?.
* #a1 #t1 * #c #x * #a #t #Hx * #d #y #Hy
cases (after_inv_apply … Hx) -Hx #Hc #Hx
cases (after_inv_apply … Hy) -Hy #Hd
-cases (apply_inj_aux … Hc Hd) #Hy -a -d /3 width=4 by eq_sec/
+cases (apply_inj_aux … Hc Hd) //
+#Hy -a -d /3 width=4 by eq_seq/
qed-.
(* Main inversion lemmas on after *******************************************)
lemma at_total: ∀i,t. @⦃i, t⦄ ≡ t@❴i❵.
#i elim i -i
[ * // | #i #IH * /3 width=1 by at_S1/ ]
-qed.
+qed.
(* Advanced forward lemmas on at ********************************************)
#j2 #Hj #H destruct /4 width=2 by conj, at_increasing, le_S_S/
qed-.
+lemma at_fwd_id: ∀t,b,i. @⦃i, b@t⦄ ≡ i → b = 0.
+#t #b *
+[ #H <(at_inv_O1 … H) -t -b //
+| #i #H elim (at_inv_S1 … H) -H
+ #j #H #H0 destruct lapply (at_increasing … H) -H
+ #H lapply (eq_minus_O … H) -H //
+]
+qed.
+
(* Main properties on at ****************************************************)
+lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀t. @⦃i2, t⦄ ≡ i2 → @⦃i1, t⦄ ≡ i1.
+#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
+* #b #t #H lapply (at_fwd_id … H)
+#H0 destruct /4 width=1 by at_S1, at_inv_SOS/
+qed-.
+
let corec at_ext: ∀t1,t2. (∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i1 = i2) → t1 ≐ t2 ≝ ?.
* #b1 #t1 * #b2 #t2 #Hi lapply (Hi 0 b1 b2 ? ?) //
-#H lapply (at_ext t1 t2 ?) /2 width=1 by eq_sec/ -at_ext
+#H lapply (at_ext t1 t2 ?) /2 width=1 by eq_seq/ -at_ext
#j #j1 #j2 #H1 #H2 @(injective_plus_r … b2) /4 width=5 by at_S1, injective_S/ (**) (* full auto fails *)
qed-.
-theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀t,j1,j2. @⦃i1, t⦄ ≡ j1 → @⦃i2, t⦄ ≡ j2 → j1 < j2.
+theorem at_monotonic: ∀i1,i2. i1 < i2 → ∀t1,t2. t1 ≐ t2 → ∀j1,j2. @⦃i1, t1⦄ ≡ j1 → @⦃i2, t2⦄ ≡ j2 → j1 < j2.
#i1 #i2 #H @(lt_elim … H) -i1 -i2
-[ #i2 *#b #t #j1 #j2 #H1 #H2 >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 //
-| #i1 #i2 #IH * #b #t #j1 #j2 #H1 #H2 elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2
- #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=3 by lt_S_S, monotonic_lt_plus_r/
+[ #i2 * #b1 #t1 * #b2 #t2 #H elim (eq_stream_inv_seq ????? H) -H
+ #H #Ht #j1 #j2 #H1 #H2 destruct
+ >(at_inv_O1 … H1) elim (at_inv_S1 … H2) -H2 -j1 //
+| #i1 #i2 #IH * #b1 #t1 * #b2 #t2 #H elim (eq_stream_inv_seq ????? H) -H
+ #H #Ht #j1 #j2 #H1 #H2 destruct
+ elim (at_inv_S1 … H2) elim (at_inv_S1 … H1) -H1 -H2
+ #x1 #Hx1 #H1 #x2 #Hx2 #H2 destruct /4 width=5 by lt_S_S, monotonic_lt_plus_r/
]
qed-.
-theorem at_inv_monotonic: ∀t,i1,j1. @⦃i1, t⦄ ≡ j1 → ∀i2,j2. @⦃i2, t⦄ ≡ j2 → j2 < j1 → i2 < i1.
-#t #i1 #j1 #H elim H -t -i1 -j1
-[ #t #i2 #j2 #_ #H elim (lt_le_false … H) //
-| #t #i1 #j1 #_ #IH #i2 #j2 #H #Hj elim (at_inv_xOx … H) -H *
+theorem at_inv_monotonic: ∀t1,i1,j1. @⦃i1, t1⦄ ≡ j1 → ∀t2,i2,j2. @⦃i2, t2⦄ ≡ j2 → t1 ≐ t2 → j2 < j1 → i2 < i1.
+#t1 #i1 #j1 #H elim H -t1 -i1 -j1
+[ #t1 #t2 #i2 #j2 #_ #_ #H elim (lt_le_false … H) //
+| #t1 #i1 #j1 #_ #IH * #b2 #t2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
+ #H0 #Ht destruct elim (at_inv_xOx … H) -H *
[ #H1 #H2 destruct //
- | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=3 by lt_S_S_to_lt, lt_S_S/
+ | #x2 #y2 #Hxy #H1 #H2 destruct /4 width=5 by lt_S_S_to_lt, lt_S_S/
]
-| #t #b1 #i1 #j1 #_ #IH #i2 #j2 #H #Hj elim (at_inv_xSx … H) -H
- #y2 #Hy #H destruct /3 width=3 by lt_S_S_to_lt/
+| #t1 #b1 #i1 #j1 #_ #IH * #b2 #t2 #i2 #j2 #H #Ht #Hj elim (eq_stream_inv_seq ????? Ht) -Ht
+ #H0 #Ht destruct elim (at_inv_xSx … H) -H
+ #y2 #Hy #H destruct /3 width=5 by eq_seq, lt_S_S_to_lt/
]
qed-.
-theorem at_mono: ∀t,i,i1. @⦃i, t⦄ ≡ i1 → ∀i2. @⦃i, t⦄ ≡ i2 → i2 = i1.
-#t #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /2 width=6 by at_inv_monotonic/
+theorem at_mono: ∀t1,t2. t1 ≐ t2 → ∀i,i1. @⦃i, t1⦄ ≡ i1 → ∀i2. @⦃i, t2⦄ ≡ i2 → i2 = i1.
+#t1 #t2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+#Hi elim (lt_le_false i i) /3 width=8 by at_inv_monotonic, eq_stream_sym/
qed-.
-theorem at_inj: ∀t,i1,i. @⦃i1, t⦄ ≡ i → ∀i2. @⦃i2, t⦄ ≡ i → i1 = i2.
-#t #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /2 width=6 by at_monotonic/
+theorem at_inj: ∀t1,t2. t1 ≐ t2 → ∀i1,i. @⦃i1, t1⦄ ≡ i → ∀i2. @⦃i2, t2⦄ ≡ i → i1 = i2.
+#t1 #t2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+#Hi elim (lt_le_false i i) /3 width=8 by at_monotonic, eq_stream_sym/
qed-.
lemma at_inv_total: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → i2 = t@❴i1❵.
-/2 width=4 by at_mono/ qed-.
+/2 width=6 by at_mono/ qed-.
+
+lemma at_repl_back: ∀i1,i2. eq_stream_repl_back ? (λt. @⦃i1, t⦄ ≡ i2).
+#i1 #i2 #t1 #t2 #Ht #H1 lapply (at_total i1 t2)
+#H2 <(at_mono … Ht … H1 … H2) -t1 -i2 //
+qed-.
+
+lemma at_repl_fwd: ∀i1,i2. eq_stream_repl_fwd ? (λt. @⦃i1, t⦄ ≡ i2).
+#i1 #i2 @eq_stream_repl_sym /2 width=3 by at_repl_back/
+qed-.
(* Advanced properties on at ************************************************)
#t #i1 #i2 lapply (at_total i1 t)
#Ht elim (eq_nat_dec i2 (t@❴i1❵))
[ #H destruct /2 width=1 by or_introl/
-| /4 width=4 by at_mono, or_intror/
+| /4 width=6 by at_mono, or_intror/
]
qed-.
(* Advanced properties on apply *********************************************)
-fact apply_inj_aux: ∀t,i,i1,i2. i = t@❴i1❵ → i = t@❴i2❵ → i1 = i2.
-/2 width=4 by at_inj/ qed-.
+fact apply_inj_aux: ∀t1,t2. t1 ≐ t2 → ∀i,i1,i2. i = t1@❴i1❵ → i = t2@❴i2❵ → i1 = i2.
+/2 width=6 by at_inj/ 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/notation/functions/identity_0.ma".
+include "ground_2/notation/relations/isidentity_1.ma".
+include "ground_2/relocation/nstream_lift.ma".
+include "ground_2/relocation/nstream_after.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+let corec id: nstream ≝ ↑id.
+
+interpretation "identity (nstream)"
+ 'Identity = (id).
+
+definition isid: predicate nstream ≝ λt. t ≐ 𝐈𝐝.
+
+interpretation "test for identity (trace)"
+ 'IsIdentity t = (isid t).
+
+(* Basic properties on id ***************************************************)
+
+lemma id_unfold: 𝐈𝐝 = ↑𝐈𝐝.
+>(stream_expand … (𝐈𝐝)) in ⊢ (??%?); normalize //
+qed.
+
+(* Basic properties on isid *************************************************)
+
+lemma isid_id: 𝐈⦃𝐈𝐝⦄.
+// qed.
+
+lemma isid_push: ∀t. 𝐈⦃t⦄ → 𝐈⦃↑t⦄.
+#t #H normalize >id_unfold /2 width=1 by eq_seq/
+qed.
+
+(* Basic inversion lemmas on isid *******************************************)
+
+lemma isid_inv_seq: ∀t,a. 𝐈⦃a@t⦄ → 𝐈⦃t⦄ ∧ a = 0.
+#t #a normalize >id_unfold in ⊢ (???%→?);
+#H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/
+qed-.
+
+lemma isid_inv_push: ∀t. 𝐈⦃↑t⦄ → 𝐈⦃t⦄.
+* #a #t #H elim (isid_inv_seq … H) -H //
+qed-.
+
+lemma isid_inv_next: ∀t. 𝐈⦃⫯t⦄ → ⊥.
+* #a #t #H elim (isid_inv_seq … H) -H
+#_ #H destruct
+qed-.
+
+(* inversion lemmas on at ***************************************************)
+
+let corec id_inv_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → t ≐ 𝐈𝐝 ≝ ?.
+* #a #t #Ht lapply (Ht 0)
+#H lapply (at_inv_O1 … H) -H
+#H0 >id_unfold @eq_seq
+[ cases H0 -a //
+| @id_inv_at -id_inv_at
+ #i lapply (Ht (⫯i)) -Ht cases H0 -a
+ #H elim (at_inv_SOx … H) -H //
+]
+qed-.
+
+lemma isid_inv_at: ∀i,t. 𝐈⦃t⦄ → @⦃i, t⦄ ≡ i.
+#i elim i -i
+[ * #a #t #H elim (isid_inv_seq … H) -H //
+| #i #IH * #a #t #H elim (isid_inv_seq … H) -H
+ /3 width=1 by at_S1/
+]
+qed-.
+
+lemma isid_inv_at_mono: ∀t,i1,i2. 𝐈⦃t⦄ → @⦃i1, t⦄ ≡ i2 → i1 = i2.
+/3 width=6 by isid_inv_at, at_mono/ qed-.
+
+(* Properties on at *********************************************************)
+
+lemma id_at: ∀i. @⦃i, 𝐈𝐝⦄ ≡ i.
+/2 width=1 by isid_inv_at/ qed.
+
+lemma isid_at: ∀t. (∀i. @⦃i, t⦄ ≡ i) → 𝐈⦃t⦄.
+/2 width=1 by id_inv_at/ qed.
+
+lemma isid_at_total: ∀t. (∀i1,i2. @⦃i1, t⦄ ≡ i2 → i1 = i2) → 𝐈⦃t⦄.
+#t #Ht @isid_at
+#i lapply (at_total i t)
+#H >(Ht … H) in ⊢ (???%); -Ht //
+qed.
+
+(* Properties on after ******************************************************)
+
+lemma after_isid_dx: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t2 ≐ t → 𝐈⦃t1⦄.
+#t2 #t1 #t #Ht #H2 @isid_at_total
+#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Ht) -t1
+/3 width=6 by at_inj, eq_stream_sym/
+qed.
+
+lemma after_isid_sn: ∀t2,t1,t. t2 ⊚ t1 ≡ t → t1 ≐ t → 𝐈⦃t2⦄.
+#t2 #t1 #t #Ht #H1 @isid_at_total
+#i2 #i #Hi2 lapply (at_total i2 t1)
+#H0 lapply (at_increasing … H0)
+#Ht1 lapply (after_fwd_at2 … (t1@❴i2❵) … H0 … Ht)
+/3 width=7 by at_repl_back, at_mono, at_id_le/
+qed.
+
+(* Inversion lemmas on after ************************************************)
+
+let corec isid_after_sn: ∀t1,t2. 𝐈⦃t1⦄ → t1 ⊚ t2 ≡ t2 ≝ ?.
+* #a1 #t1 * * [ | #a2 ] #t2 #H cases (isid_inv_seq … H) -H
+#Ht1 #H1
+[ @(after_zero … H1) -H1 /2 width=1 by/
+| @(after_skip … H1) -H1 /2 width=5 by/
+]
+qed-.
+
+let corec isid_after_dx: ∀t2,t1. 𝐈⦃t2⦄ → t1 ⊚ t2 ≡ t1 ≝ ?.
+* #a2 #t2 * *
+[ #t1 #H cases (isid_inv_seq … H) -H
+ #Ht2 #H2 @(after_zero … H2) -H2 /2 width=1 by/
+| #a1 #t1 #H @(after_drop … a1 a1) /2 width=5 by/
+]
+qed-.
+
+lemma after_isid_inv_sn: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t1⦄ → t2 ≐ t.
+/3 width=4 by isid_after_sn, after_mono/
+qed-.
+
+lemma after_isid_inv_dx: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t2⦄ → t1 ≐ t.
+/3 width=4 by isid_after_dx, after_mono/
+qed-.
+(*
+lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
+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/notation/functions/lift_1.ma".
+include "ground_2/relocation/nstream_at.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+definition push: nstream → nstream ≝ λt. 0@t.
+
+interpretation "push (nstream)" 'Lift t = (push t).
+
+definition next: nstream → nstream.
+* #a #t @(⫯a@t)
+qed.
+
+interpretation "next (nstream)" 'Successor t = (next t).
+
+(* Basic properties on push *************************************************)
+
+lemma push_at_O: ∀t. @⦃0, ↑t⦄ ≡ 0.
+// qed.
+
+lemma push_at_S: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃⫯i1, ↑t⦄ ≡ ⫯i2.
+/2 width=1 by at_S1/ qed.
+
+(* Basic inversion lemmas on push *******************************************)
+
+lemma push_inv_at_S: ∀t,i1,i2. @⦃⫯i1, ↑t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2.
+/2 width=1 by at_inv_SOS/ qed-.
+
+lemma injective_push: injective ? ? push.
+#t1 #t2 normalize #H destruct //
+qed-.
+
+(* Basic properties on next *************************************************)
+
+lemma next_at: ∀t,i1,i2. @⦃i1, t⦄ ≡ i2 → @⦃i1, ⫯t⦄ ≡ ⫯i2.
+* /2 width=1 by at_lift/
+qed.
+
+(* Basic inversion lemmas on next *******************************************)
+
+lemma next_inv_at: ∀t,i1,i2. @⦃i1, ⫯t⦄ ≡ ⫯i2 → @⦃i1, t⦄ ≡ i2.
+* /2 width=1 by at_inv_xSS/
+qed-.
+
+lemma injective_next: injective ? ? next.
+* #a1 #t1 * #a2 #t2 normalize #H destruct //
+qed-.
class "green"
[ { "multiple relocation" * } {
[ { "" * } {
- [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ]
+ [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" "nstream_id ( 𝐈𝐝 ) ( 𝐈⦃?⦄ )" * ]
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
[ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
projects / helm.git / commitdiff