1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "paths/standard_precedence.ma".
17 (* ALTERNATIVE STANDARD ORDER ***********************************************)
19 (* Note: this is p < q *)
20 definition slt: relation path ≝ TC … sprec.
22 interpretation "standard 'less than' on paths"
25 lemma slt_step_rc: ∀p,q. p ≺ q → p < q.
29 lemma slt_nil: ∀o,p. ◊ < o::p.
33 lemma slt_skip: dx::◊ < ◊.
37 lemma slt_comp: ∀o,p,q. p < q → o::p < o::q.
38 #o #p #q #H elim H -q /3 width=1/ /3 width=3/
41 theorem slt_trans: transitive … slt.
45 lemma slt_refl: ∀p. p < p.
46 #p elim p -p /2 width=1/
47 @(slt_trans … (dx::◊)) //