X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Fstandard_order.ma;h=9bf484143fdf517dc5a8c30da85d2c0dd78a4bf6;hb=e47584d3cc500acd8ffb533810daabd3b2ff8300;hp=563cdce3488a49074b89742c81291f796655f8ee;hpb=5c792a695677f2857e1984ababc9998d42fc8033;p=helm.git

diff --git a/matita/matita/contribs/lambda/paths/standard_order.ma b/matita/matita/contribs/lambda/paths/standard_order.ma
index 563cdce34..9bf484143 100644
--- a/matita/matita/contribs/lambda/paths/standard_order.ma
+++ b/matita/matita/contribs/lambda/paths/standard_order.ma
@@ -12,73 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "paths/path.ma".
+include "paths/standard_precedence.ma".
 
 (* STANDARD ORDER ************************************************************)
 
-(* Note: standard precedence relation on paths: p ≺ q
-         to serve as base for the order relations: p < q and p ≤ q *)
-inductive sprec: relation path ≝
-| sprec_nil : ∀c,q.   sprec (◊) (c::q)
-| sprec_rc  : ∀p,q.   sprec (dx::p) (rc::q)
-| sprec_sn  : ∀p,q.   sprec (rc::p) (sn::q)
-| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q)
-| sprec_skip:         sprec (dx::◊) ◊
-.
-
-interpretation "standard 'precedes' on paths"
-   'prec p q = (sprec p q).
-
-lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
-                    ∃∃q0. p0 ≺ q0 & sn::q0 = q.
-#p #q * -p -q
-[ #c #q #p0 #H destruct
-| #p #q #p0 #H destruct
-| #p #q #p0 #H destruct
-| #c #p #q #Hpq #p0 #H destruct /2 width=3/
-| #p0 #H destruct
-]
-qed-.
-
-lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
-#p #q #H elim H -p -q // /2 width=1/
-[ #p #q * #H destruct
-| #p #q * #H destruct
-| #c #p #q #_ #IHpq * #H destruct /3 width=1/
-]
-qed-.
-
-(* Note: this is p < q *)
-definition slt: relation path ≝ TC … sprec.
-
-interpretation "standard 'less than' on paths"
-   'lt p q = (slt p q).
-
-lemma slt_step_rc: ∀p,q. p ≺ q → p < q.
-/2 width=1/
-qed.
-
-lemma slt_nil: ∀c,p. ◊ < c::p.
-/2 width=1/
-qed.
-
-lemma slt_skip: dx::◊ < ◊.
-/2 width=1/
-qed.
-
-lemma slt_comp: ∀c,p,q. p < q → c::p < c::q.
-#c #p #q #H elim H -q /3 width=1/ /3 width=3/
-qed.
-
-theorem slt_trans: transitive … slt.
-/2 width=3/
-qed-.
-
-lemma slt_refl: ∀p. p < p.
-#p elim p -p /2 width=1/
-@(slt_trans … (dx::◊)) //
-qed.
-
 (* Note: this is p ≤ q *)
 definition sle: relation path ≝ star … sprec.
 
@@ -109,7 +46,7 @@ lemma sle_nil: ∀p. ◊ ≤ p.
 * // /2 width=1/
 qed.
 
-lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀c. (c::p1) ≤ (c::p2).
+lemma sle_comp: ∀p1,p2. p1 ≤ p2 → ∀o. (o::p1) ≤ (o::p2).
 #p1 #p2 #H elim H -p2 // /3 width=3/
 qed.
 
@@ -130,8 +67,8 @@ qed.
 lemma sle_dichotomy: ∀p1,p2:path. p1 ≤ p2 ∨ p2 ≤ p1.
 #p1 elim p1 -p1
 [ * /2 width=1/
-| #c1 #p1 #IHp1 * /2 width=1/
-  * #p2 cases c1 -c1 /2 width=1/
+| #o1 #p1 #IHp1 * /2 width=1/
+  * #p2 cases o1 -o1 /2 width=1/
   elim (IHp1 p2) -IHp1 /3 width=1/
 ]
 qed-.