X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Flabelled_hap_reduction.ma;h=6d08b8c5c095c8a77097247c265ccda53e011769;hb=5ca47b58902b9f2583ad1354b860c04ea62df46c;hp=e1f279f67eaa65e285286429534bc2123a492fcb;hpb=23e75ebc00553e178e090ca1373ac075ee650a60;p=helm.git

diff --git a/matita/matita/contribs/lambda/labelled_hap_reduction.ma b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
index e1f279f67..6d08b8c5c 100644
--- a/matita/matita/contribs/lambda/labelled_hap_reduction.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "pointer_order.ma".
 include "labelled_sequential_reduction.ma".
 
 (* KASHIMA'S "HAP" COMPUTATION (LABELLED SINGLE STEP) ***********************)
@@ -21,27 +20,27 @@ include "labelled_sequential_reduction.ma".
          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
 *)
 inductive lhap1: ptr → relation term ≝
-| hap1_beta: ∀B,A. lhap1 (◊) (@B.𝛌.A) ([⬐B]A)
+| hap1_beta: ∀B,A. lhap1 (◊) (@B.𝛌.A) ([↙B]A)
 | hap1_appl: ∀p,B,A1,A2. lhap1 p A1 A2 → lhap1 (dx::p) (@B.A1) (@B.A2)
 .
 
 interpretation "labelled 'hap' reduction"
    'HAp M p N = (lhap1 p M N).
 
-notation "hvbox( M break ⓗ⇀ [ term 46 p ] break term 46 N )"
+notation "hvbox( M break ⓗ↦ [ term 46 p ] break term 46 N )"
    non associative with precedence 45
    for @{ 'HAp $M $p $N }.
 
-lemma lhap1_inv_nil: ∀p,M,N. M ⓗ⇀[p] N → ◊ = p →
-                     ∃∃B,A. @B.𝛌.A = M & [⬐B]A = N.
+lemma lhap1_inv_nil: ∀p,M,N. M ⓗ↦[p] N → ◊ = p →
+                     ∃∃B,A. @B.𝛌.A = M & [↙B]A = N.
 #p #M #N * -p -M -N
 [ #B #A #_ /2 width=4/
 | #p #B #A1 #A2 #_ #H destruct
 ]
 qed-.
 
-lemma lhap1_inv_cons: ∀p,M,N. M ⓗ⇀[p] N → ∀c,q. c::q = p →
-                      ∃∃B,A1,A2. dx = c & A1 ⓗ⇀[q] A2 & @B.A1 = M & @B.A2 = N.
+lemma lhap1_inv_cons: ∀p,M,N. M ⓗ↦[p] N → ∀c,q. c::q = p →
+                      ∃∃B,A1,A2. dx = c & A1 ⓗ↦[q] A2 & @B.A1 = M & @B.A2 = N.
 #p #M #N * -p -M -N
 [ #B #A #c #q #H destruct
 | #p #B #A1 #A2 #HA12 #c #q #H destruct /2 width=6/
@@ -70,7 +69,7 @@ lemma lhap1_dsubst: ∀p. dsubstable_dx (lhap1 p).
 #D2 #A #d >dsubst_dsubst_ge //
 qed.
 
-lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N.
+lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ↦[p] N → M ⓗ↦[p] N.
 #p #H @(in_head_ind … H) -p
 [ #M #N #H elim (lsred_inv_nil … H ?) -H //
 | #p #_ #IHp #M #N #H
@@ -78,11 +77,11 @@ lemma head_lsred_lhap1: ∀p. in_head p → ∀M,N. M ⇀[p] N → M ⓗ⇀[p] N
 ]
 qed.
 
-lemma lhap1_inv_head: ∀p,M,N. M ⓗ⇀[p] N → in_head p.
+lemma lhap1_inv_head: ∀p,M,N. M ⓗ↦[p] N → in_head p.
 #p #M #N #H elim H -p -M -N // /2 width=1/
 qed-.
 
-lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ⇀[p] N → M ⇀[p] N.
+lemma lhap1_inv_lsred: ∀p,M,N. M ⓗ↦[p] N → M ↦[p] N.
 #p #M #N #H elim H -p -M -N // /2 width=1/
 qed-.