update in ground

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / reduction / dfr_ifr.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index 2d3fdbdf596f7e405e1a29725db9c922314e6f56..29c44898d2d859a2dcdc1f72bd77cc101dc5c297 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -32,11 +32,11 @@ include "ground/relocation/tr_pap_pushs.ma".
 
 (* COMMENT
 axiom pippo (b) (q) (n):
-      ↑❘q❘ = (↑[q]𝐢)@❨n❩ →
-      ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩.
+      ↑❘q❘ = (↑[q]𝐢)＠⧣❨n❩ →
+      ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)＠⧣❨n+❘b❘❩.
 
 lemma unwind_rmap_tls_eq_id (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
+      ❘p❘ = ↑[p]𝐢＠⧣❨n❩ →
       (𝐢) ≗ ⇂*[n]↑[p]𝐢.
 #p @(list_ind_rcons … p) -p
 [ #n <depth_empty #H destruct
@@ -56,10 +56,10 @@ lemma unwind_rmap_tls_eq_id (p) (n):
 ]
 
 
-(*  (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢@❨n+❘b❘❩ *)
-(* [↑[p]𝐢@❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
+(*  (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢＠⧣❨n+❘b❘❩ *)
+(* [↑[p]𝐢＠⧣❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
 lemma unwind_rmap_tls_eq (f) (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
+      ❘p❘ = ↑[p]𝐢＠⧣❨n❩ →
       f ≗ ⇂*[n]↑[p]f.
 #f #p #n #Hp
 @(stream_eq_canc_dx … (stream_tls_eq_repl …))
@@ -124,9 +124,9 @@ lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ϵ 𝐓 →
 ]
 
 (*
-Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢@❨n❩
+Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢＠⧣❨n❩
 ---------------------------
-↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢@❨n+❘b❘❩❩] t
+↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢＠⧣❨n+❘b❘❩❩] t
 *)
 (*
 (↑[𝐮❨↑❘q❘❩]▼[⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢](t1⋔(p◖𝗦))⇔▼[𝐮❨↑❘q❘❩∘▼[p●𝗔◗b●𝗟◗q]𝐢](t1⋔(p◖𝗦))