+++ /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/relocation/pstream_tls.ma".
-include "ground/relocation/pstream_istot.ma".
-include "ground/relocation/rtmap_after.ma".
-
-(* RELOCATION P-STREAM ******************************************************)
-
-corec definition compose: gr_map → gr_map → gr_map.
-#f2 * #p1 #f1 @(stream_cons … (f2@❨p1❩)) @(compose ? f1) -compose -f1
-@(⫰*[p1]f2)
-defined.
-
-interpretation "functional composition (nstream)"
- 'compose f2 f1 = (compose f2 f1).
-
-(* Basic properties on compose ***********************************************)
-
-lemma compose_rew: ∀f2,f1,p1. f2@❨p1❩⨮(⫰*[p1]f2)∘f1 = f2∘(p1⨮f1).
-#f2 #f1 #p1 <(stream_rew … (f2∘(p1⨮f1))) normalize //
-qed.
-
-lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
-#f2 * #p1 #f1 #f <compose_rew <compose_rew
-* -f /2 width=1 by eq_f2/
-qed.
-
-(* Basic inversion lemmas on compose ****************************************)
-
-lemma compose_inv_rew: ∀f2,f1,f,p1,p. f2∘(p1⨮f1) = p⨮f →
- f2@❨p1❩ = p ∧ (⫰*[p1]f2)∘f1 = f.
-#f2 #f1 #f #p1 #p <compose_rew
-#H destruct /2 width=1 by conj/
-qed-.
-
-lemma compose_inv_O2: ∀f2,f1,f,p2,p. (p2⨮f2)∘(⫯f1) = p⨮f →
- p2 = p ∧ f2∘f1 = f.
-#f2 #f1 #f #p2 #p <compose_rew
-#H destruct /2 width=1 by conj/
-qed-.
-
-lemma compose_inv_S2: ∀f2,f1,f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
- f2@❨p1❩+p2 = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
-#f2 #f1 #f #p2 #p1 #p <compose_rew
-#H destruct >nsucc_inj <stream_tls_swap
-/2 width=1 by conj/
-qed-.
-
-lemma compose_inv_S1: ∀f2,f1,f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
- ↑(f2@❨p1❩) = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
-#f2 #f1 #f #p1 #p <compose_rew
-#H destruct /2 width=1 by conj/
-qed-.
-
-(* Properties on after (specific) *********************************************)
-
-lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
- ∀p. p⨮f2 ⊚ ⫯f1 ≘ p⨮f.
-#f2 #f1 #f #Hf #p elim p -p
-/2 width=7 by gr_after_refl, gr_after_next/
-qed.
-
-lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
- ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
-#f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
-/2 width=7 by gr_after_next, gr_after_push/
-qed.
-
-lemma after_apply: ∀p1,f2,f1,f.
- (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
-#p1 elim p1 -p1
-[ * /2 width=1 by after_O2/
-| #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
- /3 width=1 by after_S2/
-]
-qed-.
-
-corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
-* #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
-[ cases p1 -p1
- [ #H cases (compose_inv_O2 … H) -H /3 width=7 by gr_after_refl, eq_f2/
- | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by gr_after_push/
- ]
-| #p2 >gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold
- /3 width=5 by gr_after_next/
-]
-qed-.
-
-theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
-/2 width=1 by after_total_aux/ qed.
-
-(* Inversion lemmas on after (specific) ***************************************)
-
-lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
- f2 ⊚ f1 ≘ f ∧ p2 = p.
-#f2 #g2 #f #p2 elim p2 -p2
-[ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ]
- #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
-| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
- #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
- #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
- #H destruct /2 width=1 by conj/
-]
-qed-.
-
-lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
- ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
-#f2 #g2 #f #p2 elim p2 -p2
-[ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ]
- #g #Hf #H elim (next_inv_seq_dx … H) -H
- #x #Hx #Hg destruct /2 width=3 by ex2_intro/
-| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
- #g #Hg #H elim (next_inv_seq_dx … H) -H
- #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
- #m #Hf #Hm destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma after_inv_const: ∀f2,f1,f,p1,p.
- p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
-#f2 #f1 #f #p1 #p elim p -p
-[ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ]
- #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
-| #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/
-]
-qed-.
-
-lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
-/2 width=4 by gr_after_mono/ qed-.
-
-(* Forward lemmas on after (specific) *****************************************)
-
-lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
-#f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
-/3 width=2 by at_inv_O1, sym_eq/
-qed-.
-
-lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
- (⫰*[↓p1]f2) ⊚ f1 ≘ f.
-#f #f1 #p1 elim p1 -p1
-[ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
-| #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
- #x #Hx #H destruct /2 width=3 by/
-]
-qed-.
-
-lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
- (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
-/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
-
-(* Properties on apply ******************************************************)
-
-lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
-/4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ 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/lib/stream_hdtl.ma".
-include "ground/relocation/pstream.ma".
-
-(* RELOCATION P-STREAM ******************************************************)
-
-(* Properties with stream_tl *************************************************)
-
-lemma tl_push: ∀f. f = ⫰⫯f.
-// qed.
-
-lemma tl_next: ∀f. ⫰f = ⫰↑f.
-* // 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/lib/stream_tls.ma".
-include "ground/arith/nat_pred_succ.ma".
-include "ground/relocation/pstream_tl.ma".
-
-(* RELOCATION P-STREAM ******************************************************)
-
-(* Properties with stream_tls ************************************************)
-
-lemma tls_next: ∀f. ∀p:pnat. ⫰*[p]f = ⫰*[p]↑f.
-#f #p >(npsucc_pred p) <stream_tls_swap <stream_tls_swap //
-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/lib/stream_tls.ma".
+include "ground/relocation/tr_pap.ma".
+
+(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************)
+
+corec definition tr_compose: tr_map → tr_map → tr_map.
+#f2 * #p1 #f1
+@(stream_cons … (f2@❨p1❩))
+@(tr_compose ? f1) -tr_compose -f1
+@(⇂*[p1]f2)
+defined.
+
+interpretation
+ "composition (total relocation maps)"
+ 'compose f2 f1 = (tr_compose f2 f1).
+
+(* Basic constructions ******************************************************)
+
+(*** compose_rew *)
+lemma tr_compose_unfold (f2) (f1):
+ ∀p1. f2@❨p1❩⨮(⇂*[p1]f2)∘f1 = f2∘(p1⨮f1).
+#f2 #f1 #p1 <(stream_unfold … (f2∘(p1⨮f1))) //
+qed.
+
+(* Basic inversions *********************************************************)
+
+(*** compose_inv_rew *)
+lemma tr_compose_inv_unfold (f2) (f1):
+ ∀f,p1,p. f2∘(p1⨮f1) = p⨮f →
+ ∧∧ f2@❨p1❩ = p & (⇂*[p1]f2)∘f1 = f.
+#f2 #f1 #f #p1 #p
+<tr_compose_unfold #H destruct
+/2 width=1 by conj/
+qed-.
+
+(*** compose_inv_S2 *)
+lemma tr_compose_inv_succ_dx (f2) (f1):
+ ∀f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
+ ∧∧ f2@❨p1❩+p2 = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+#f2 #f1 #f #p2 #p1 #p
+<tr_compose_unfold #H destruct
+>nsucc_inj <stream_tls_swap
+/2 width=1 by conj/
+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/relocation/pstream_tls.ma".
+include "ground/relocation/pstream_istot.ma".
+include "ground/relocation/rtmap_after.ma".
+
+(* Properties on after (specific) *********************************************)
+
+lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
+ ∀p. p⨮f2 ⊚ ⫯f1 ≘ p⨮f.
+#f2 #f1 #f #Hf #p elim p -p
+/2 width=7 by gr_after_refl, gr_after_next/
+qed.
+
+lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
+ ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
+#f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
+/2 width=7 by gr_after_next, gr_after_push/
+qed.
+
+lemma after_apply: ∀p1,f2,f1,f.
+ (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
+#p1 elim p1 -p1
+[ * /2 width=1 by after_O2/
+| #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
+ /3 width=1 by after_S2/
+]
+qed-.
+
+corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
+* #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
+[ cases p1 -p1
+ [ #H cases (compose_inv_O2 … H) -H /3 width=7 by gr_after_refl, eq_f2/
+ | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by gr_after_push/
+ ]
+| #p2 >gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold
+ /3 width=5 by gr_after_next/
+]
+qed-.
+
+theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
+/2 width=1 by after_total_aux/ qed.
+
+(* Inversion lemmas on after (specific) ***************************************)
+
+lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
+ f2 ⊚ f1 ≘ f ∧ p2 = p.
+#f2 #g2 #f #p2 elim p2 -p2
+[ #p #Hf #f1 #H2 elim (gr_after_inv_push_bi … Hf … H2) -g2 [|*: // ]
+ #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
+| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
+ #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
+ #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
+ #H destruct /2 width=1 by conj/
+]
+qed-.
+
+lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
+ ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
+#f2 #g2 #f #p2 elim p2 -p2
+[ #p #Hf #f1 #H2 elim (gr_after_inv_push_next … Hf … H2) -g2 [|*: // ]
+ #g #Hf #H elim (next_inv_seq_dx … H) -H
+ #x #Hx #Hg destruct /2 width=3 by ex2_intro/
+| #p2 #IH #p #Hf #f1 #H2 elim (gr_after_inv_next_sn … Hf) -Hf [|*: // ]
+ #g #Hg #H elim (next_inv_seq_dx … H) -H
+ #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
+ #m #Hf #Hm destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma after_inv_const: ∀f2,f1,f,p1,p.
+ p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
+#f2 #f1 #f #p1 #p elim p -p
+[ #H elim (gr_after_inv_push_sn_push … H) -H [|*: // ]
+ #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
+| #p #IH #H lapply (gr_after_inv_next_sn_next … H ????) -H /2 width=5 by/
+]
+qed-.
+
+lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
+/2 width=4 by gr_after_mono/ qed-.
+
+(* Forward lemmas on after (specific) *****************************************)
+
+lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
+#f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
+/3 width=2 by at_inv_O1, sym_eq/
+qed-.
+
+lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
+ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
+#f #f1 #p1 elim p1 -p1
+[ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
+| #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
+ #x #Hx #H destruct /2 width=3 by/
+]
+qed-.
+
+lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
+ (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
+/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
+
+(* Properties on apply ******************************************************)
+
+lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
+/4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ 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/relocation/tr_pn_tls.ma".
+include "ground/relocation/tr_pap_pn.ma".
+include "ground/relocation/tr_compose.ma".
+
+(* COMPOSITION FOR PARTIAL RELOCATION MAPS **********************************)
+
+(* Constructions with tr_push anf tr_next ***********************************)
+
+(*** compose_next *)
+lemma tr_compose_next_sn (f2) (f1):
+ ∀f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
+#f2 * #p1 #f1 #f
+<tr_compose_unfold <tr_compose_unfold * -f
+<tr_pap_next
+/3 width=1 by compose_repl_fwd_dx/
+qed.
+
+(* Inversions with tr_push anf tr_next **************************************)
+
+(*** compose_inv_O2 *)
+lemma tr_compose_inv_push_dx (f2) (f1):
+ ∀f,p2,p. (p2⨮f2)∘(⫯f1) = p⨮f →
+ ∧∧ p2 = p & f2∘f1 = f.
+#f2 #f1 #f #p2 #p
+<tr_compose_unfold #H destruct
+/2 width=1 by conj/
+qed-.
+
+(*** compose_inv_S1 *)
+lemma tr_compose_inv_next_sn (f2) (f1):
+ ∀f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
+ ∧∧ ↑(f2@❨p1❩) = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+#f2 #f1 #f #p1 #p
+<tr_compose_unfold #H destruct
+/2 width=1 by conj/
+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/lib/stream_hdtl.ma".
+include "ground/relocation/tr_pn.ma".
+
+(* PUSH AND NEXT FOR TOTAL RELOCATION MAPS **********************************)
+
+(* Constructions with stream_tl *********************************************)
+
+(*** tl_push *)
+lemma tr_tl_push (f):
+ f = ⇂⫯f.
+// qed.
+
+(*** tl_next *)
+lemma tr_tl_next (f):
+ ⇂f = ⇂↑f.
+* // 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/lib/stream_tls.ma".
+include "ground/arith/nat_pred_succ.ma".
+include "ground/relocation/tr_pn_hdtl.ma".
+
+(* PUSH AND NEXT FOR TOTAL RELOCATION MAPS **********************************)
+
+(* Constructions with stream_tls ********************************************)
+
+(*** tls_next *)
+lemma tr_tls_next (f):
+ ∀p:pnat. ⇂*[p]f = ⇂*[p]↑f.
+#f #p
+>(npsucc_pred p) <stream_tls_swap <stream_tls_swap //
+qed.
}
]
[ { "total relocation" * } {
+ [ "tr_compose ( ?∘? )" "tr_compose_pn" * ]
[ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
- [ "tr_pn ( ⫯? ) ( ↑? )" * ]
+ [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
[ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
}
]
projects / helm.git / commitdiff