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

diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
index 1f32ee8e0..f305f90cb 100644
--- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
@@ -22,27 +22,44 @@ definition lsreds: pseq → relation term ≝ lstar … lsred.
 interpretation "labelled sequential computation"
    'SeqRedStar M s N = (lsreds s M N).
 
-notation "hvbox( M break ⇀* [ term 46 s ] break term 46 N )"
+notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )"
    non associative with precedence 45
    for @{ 'SeqRedStar $M $s $N }.
 
-lemma lsreds_step_rc: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
+lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
 /2 width=1/
 qed.
 
-lemma lsreds_inv_nil: ∀s,M1,M2. M1 ⇀*[s] M2 → ◊ = s → M1 = M2.
+lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2.
 /2 width=5 by lstar_inv_nil/
 qed-.
 
-lemma lsreds_inv_cons: ∀s,M1,M2. M1 ⇀*[s] M2 → ∀q,r. q::r = s →
-                       ∃∃M. M1 ⇀[q] M & M ⇀*[r] M2.
+lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s →
+                       ∃∃M. M1 ↦[q] M & M ↦*[r] M2.
 /2 width=3 by lstar_inv_cons/
 qed-.
 
-lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
+lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2.
 /2 width=1 by lstar_inv_step/
 qed-.
 
+lemma lsreds_inv_pos: ∀s,M1,M2. M1 ↦*[s] M2 → 0 < |s| →
+                      ∃∃p,r,M. p::r = s & M1 ↦[p] M & M ↦*[r] M2.
+/2 width=1 by lstar_inv_pos/
+qed-.
+
+lemma lsred_compatible_rc: ho_compatible_rc lsreds.
+/3 width=1/
+qed.
+
+lemma lsred_compatible_sn: ho_compatible_sn lsreds.
+/3 width=1/
+qed.
+
+lemma lsred_compatible_dx: ho_compatible_dx lsreds.
+/3 width=1/
+qed.
+
 lemma lsreds_lift: ∀s. liftable (lsreds s).
 /2 width=1/
 qed.
@@ -59,13 +76,12 @@ theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
 /3 width=7 by lstar_singlevalued, lsred_mono/
 qed-.
 
-theorem lsreds_trans: ∀s1,M1,M. M1 ⇀*[s1] M →
-                      ∀s2,M2. M ⇀*[s2] M2 → M1 ⇀*[s1@s2] M2.
-/2 width=3 by lstar_trans/
+theorem lsreds_trans: ltransitive … lsreds.
+/2 width=3 by lstar_ltransitive/
 qed-.
 
 (* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
+lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
 #s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
 #p #s #M1 #M #HM1 #_ #IHM2
 lapply (lsred_fwd_mult … HM1) -p #HM1