more on lfpx_frees.ma ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_sor.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
index 839426b9acb8ede8d994f16e6a6dff43338631d6..f86e7f8092784bb8e8ddd8e07c07dc9134aba43e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -266,6 +266,19 @@ corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f.
 [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/
 qed-.
 
+(* Main properties **********************************************************)
+
+axiom monotonic_sle_sor: ∀f1,g1. f1 ⊆ g1 → ∀f2,g2. f2 ⊆ g2 →
+                         ∀f. f1 ⋓ f2 ≡ f → ∀g. g1 ⋓ g2 ≡ g → f ⊆ g.
+
+axiom sor_trans1: ∀f0,f3,f4. f0 ⋓ f3 ≡ f4 →
+                  ∀f1,f2. f1 ⋓ f2 ≡ f0 →
+                  ∀f. f2 ⋓ f3 ≡ f → f1 ⋓ f ≡ f4.
+
+axiom sor_trans2: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 →
+                  ∀f2, f3. f2 ⋓ f3 ≡ f0 →
+                  ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4.
+
 (* Properties with tail *****************************************************)
 
 lemma sor_tl: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ⫱f1 ⋓ ⫱f2 ≡ ⫱f.