From 86d7622f88247d83b2c366a722d2994a4af91929 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 21 Oct 2017 18:25:40 +0000
Subject: [PATCH] - one conjecture closed on lsubf - some renaming in rtmap_sor

---
 .../lambdadelta/basic_2/static/frees_fqup.ma  |  4 +-
 .../lambdadelta/basic_2/static/lsubf.ma       | 34 ++++++++++
 .../lambdadelta/basic_2/static/lsubf_frees.ma |  4 --
 .../lambdadelta/basic_2/static/lsubf_lsubf.ma |  7 +-
 .../ground_2/relocation/rtmap_coafter.ma      |  2 +-
 .../ground_2/relocation/rtmap_sor.ma          | 66 ++++++++++++++-----
 6 files changed, 90 insertions(+), 27 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index 8c89346f0..9bbc83a89 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -67,7 +67,7 @@ elim (pn_split f2) * #g2 #H destruct
   lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
   lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
   lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
-  lapply (sor_sym … Hz) -Hz #Hz
+  lapply (sor_comm … Hz) -Hz #Hz
   lapply (sor_mono … f Hz ?) // -Hz #H
   lapply (sor_inv_sle_sn … Hf) -Hf #Hf
   lapply (frees_eq_repl_back … Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
@@ -96,6 +96,6 @@ elim (pn_split f0) * #g0 #H destruct
   lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
   lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
   @(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
-  /2 width=3 by sor_trans2_idem/
+  /2 width=3 by sor_comm_23_idem/
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
index 72e63576e..b6d5abd56 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lrsubeqf_4.ma".
+include "ground_2/relocation/nstream_sor.ma".
 include "basic_2/static/frees.ma".
 
 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
@@ -311,3 +312,36 @@ elim (pn_split f2) * #g2 #H2 destruct
 @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
 qed-.
 
+lemma lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                        ∀f2l,f2r. f2l⋓f2r ≡ f2 →
+                        ∃∃f1l,f1r. ⦃L1, f1l⦄ ⫃𝐅* ⦃L2, f2l⦄ & ⦃L1, f1r⦄ ⫃𝐅* ⦃L2, f2r⦄ & f1l⋓f1r ≡ f1.
+#f1 #f2 #L1 #L2 #H elim H -f1 -f2 -L1 -L2
+[ /3 width=7 by sor_eq_repl_fwd3, ex3_2_intro/
+| #g1 #g2 #I1 #I2 #L1 #L2 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxp … H) -H [|*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, sor_pp, ex3_2_intro/
+| #g1 #g2 #I #L1 #L2 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 /3 width=11 by lsubf_push, lsubf_bind, sor_np, sor_pn, sor_nn, ex3_2_intro/
+| #g #g0 #g1 #g2 #L1 #L2 #W #V #Hg #Hg1 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
+  [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_beta, sor_np, ex3_2_intro/
+  | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_beta, sor_pn, ex3_2_intro/
+  | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
+    /3 width=11 by lsubf_beta, sor_nn, ex3_2_intro/
+  ]
+| #g #g0 #g1 #g2 #I1 #I2 #L1 #L2 #V #Hg #Hg1 #_ #IH #f2l #f2r #H
+  elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g2l #g2r #Hg2 #Hl #Hr destruct
+  elim (IH … Hg2) -g2 #g1l #g1r #Hl #Hr #Hg0
+  [ lapply (sor_comm_23 … Hg0 Hg1 ?) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_unit, sor_np, ex3_2_intro/
+  | lapply (sor_assoc_dx … Hg1 … Hg0 ??) -g0 [3: |*: // ] #Hg1
+    /3 width=11 by lsubf_push, lsubf_unit, sor_pn, ex3_2_intro/
+  | lapply (sor_distr_dx … Hg0 … Hg1) -g0 [5: |*: // ] #Hg1
+    /3 width=11 by lsubf_unit, sor_nn, ex3_2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
index 700bb0bb0..09d8339d1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
@@ -14,10 +14,6 @@
 
 include "basic_2/static/lsubf.ma".
 
-axiom lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                        ∀x2,y2. x2⋓y2 ≡ f2 →
-                        ∃∃x1,y1. ⦃L1, x1⦄ ⫃𝐅* ⦃L2, x2⦄ & ⦃L1, y1⦄ ⫃𝐅* ⦃L2, y2⦄ & x1⋓y1 ≡ f1.
-
 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
 
 (* Properties with context-sensitive free variables *************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubf.ma
index 6813b2a90..ff05e0107 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubf.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/relocation/nstream_sor.ma".
 include "basic_2/static/frees_frees.ma".
 include "basic_2/static/lsubf.ma".
 
@@ -47,7 +46,7 @@ theorem lsubf_sor: ∀K,L,g1,f1. ⦃K, g1⦄ ⫃𝐅* ⦃L, f1⦄ →
       ]
     ]
     elim (sor_inv_pnx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
-    /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_trans2/
+    /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_assoc_sn/
   | elim (sor_inv_npx … Hg) -Hg [|*: // ] #y #Hy #H destruct
     elim (lsubf_inv_push1 … H2) -H2 #x2 #Z2 #Y2 #H2 #H #H0 destruct
     generalize in match H1; -H1 cases J -J #J [| #V ] #H1
@@ -59,7 +58,7 @@ theorem lsubf_sor: ∀K,L,g1,f1. ⦃K, g1⦄ ⫃𝐅* ⦃L, f1⦄ →
       ]
     ]
     elim (sor_inv_npx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
-    /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_trans1_sym/
+    /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_comm_23/
   | elim (sor_inv_nnx … Hg) -Hg [|*: // ] #y #Hy #H destruct
     generalize in match H2; generalize in match H1; -H1 -H2 cases J -J #J [| #V ] #H1 #H2
     [ elim (lsubf_inv_unit1 … H1) -H1 #x1 #Y1 #H1 #H #H0 destruct
@@ -78,7 +77,7 @@ theorem lsubf_sor: ∀K,L,g1,f1. ⦃K, g1⦄ ⫃𝐅* ⦃L, f1⦄ →
       ]
     ]
     elim (sor_inv_nnx … Hf) -Hf [1,6,11,16:|*: // ] #x #Hx #H destruct
-    /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_distr_dx/
+    /3 width=12 by lsubf_unit, lsubf_beta, lsubf_bind, sor_coll_dx/
   ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
index 44f491de5..2d1d860f9 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
@@ -694,7 +694,7 @@ lemma coafter_sor: ∀f. 𝐅⦃f⦄ → ∀f2. 𝐓⦃f2⦄ → ∀f1. f2 ~⊚
 [ #f #Hf #f2 #Hf2 #f1 #Hf #f1a #f1b #Hf1
   lapply (coafter_fwd_isid2 … Hf ??) -Hf // #H2f1
   elim (sor_inv_isid3 … Hf1) -Hf1 //
-  /3 width=5 by coafter_isid_dx, sor_refl, ex3_2_intro/
+  /3 width=5 by coafter_isid_dx, sor_idem, ex3_2_intro/
 | #f #_ #IH #f2 #Hf2 #f1 #H1 #f1a #f1b #H2
   elim (coafter_inv_xxp … H1) -H1 [1,3: * |*: // ]
   [ #g2 #g1 #Hf #Hgf2 #Hgf1
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 49d01728c..7c5dc5435 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -255,12 +255,12 @@ lemma sor_eq_repl_fwd3: ∀f1,f2. eq_repl_fwd … (λf. f1 ⋓ f2 ≡ f).
 #f1 #f2 @eq_repl_sym /2 width=3 by sor_eq_repl_back3/
 qed-.
 
-corec lemma sor_refl: ∀f. f ⋓ f ≡ f.
+corec lemma sor_idem: ∀f. f ⋓ f ≡ f.
 #f cases (pn_split f) * #g #H
 [ @(sor_pp … H H H) | @(sor_nn … H H H) ] -H //
 qed.
 
-corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f.
+corec lemma sor_comm: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f.
 #f1 #f2 #f * -f1 -f2 -f
 #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
 [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/
@@ -286,6 +286,13 @@ lemma sor_xxn_tl: ∀g1,g2,g. g1 ⋓ g2 ≡ g → ∀f. ⫯f = g →
 /3 width=5 by ex3_2_intro, or_introl, or_intror/
 qed-.
 
+lemma sor_xnx_tl: ∀g1,g2,g. g1 ⋓ g2 ≡ g → ∀f2. ⫯f2 = g2 →
+                  ∃∃f1,f. f1 ⋓ f2 ≡ f & ⫱g1 = f1 & ⫯f = g.
+#g1 elim (pn_split g1) * #f1 #H1 #g2 #g #H #f2 #H2
+[ elim (sor_inv_pnx … H … H1 H2) | elim (sor_inv_nnx … H … H1 H2) ] -g2 #f #Hf #H0
+/3 width=5 by ex3_2_intro/
+qed-.
+
 (* Properties with iterated tail ********************************************)
 
 lemma sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
@@ -386,7 +393,7 @@ qed-.
 
 lemma sor_fwd_fcla_dx_ex: ∀f,n. 𝐂⦃f⦄ ≡ n → ∀f1,f2. f1 ⋓ f2 ≡ f →
                           ∃∃n2.  𝐂⦃f2⦄ ≡ n2 & n2 ≤ n.
-/3 width=4 by sor_fwd_fcla_sn_ex, sor_sym/ qed-.
+/3 width=4 by sor_fwd_fcla_sn_ex, sor_comm/ qed-.
 
 (* Properties with test for finite colength *********************************)
 
@@ -454,20 +461,20 @@ qed.
 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_assoc_dx: ∀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.
+axiom sor_assoc_sn: ∀f1,f0,f4. f1 ⋓ f0 ≡ f4 →
+                    ∀f2, f3. f2 ⋓ f3 ≡ f0 →
+                    ∀f. f1 ⋓ f2 ≡ f → f ⋓ f3 ≡ f4.
 
-lemma sor_trans1_sym: ∀f0,f1,f2,f3,f4,f.
-                      f0⋓f4 ≡ f1 → f1⋓f2 ≡ f → f0⋓f2 ≡ f3 → f3⋓f4 ≡ f.
-/4 width=6 by sor_sym, sor_trans1/ qed-.
+lemma sor_comm_23: ∀f0,f1,f2,f3,f4,f.
+                   f0⋓f4 ≡ f1 → f1⋓f2 ≡ f → f0⋓f2 ≡ f3 → f3⋓f4 ≡ f.
+/4 width=6 by sor_comm, sor_assoc_dx/ qed-.
 
-corec theorem sor_trans2_idem: ∀f0,f1,f2. f0 ⋓ f1 ≡ f2 →
-                               ∀f. f1 ⋓ f2 ≡ f → f1 ⋓ f0 ≡ f.
+corec theorem sor_comm_23_idem: ∀f0,f1,f2. f0 ⋓ f1 ≡ f2 →
+                                ∀f. f1 ⋓ f2 ≡ f → f1 ⋓ f0 ≡ f.
 #f0 #f1 #f2 * -f0 -f1 -f2
 #f0 #f1 #f2 #g0 #g1 #g2 #Hf2 #H0 #H1 #H2 #g #Hg
 [ cases (sor_inv_ppx … Hg … H1 H2)
@@ -478,8 +485,8 @@ corec theorem sor_trans2_idem: ∀f0,f1,f2. f0 ⋓ f1 ≡ f2 →
 /3 width=7 by sor_nn, sor_np, sor_pn, sor_pp/
 qed-.
 
-corec theorem sor_distr_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g1,g2,g. g1 ⋓ g2 ≡ g →
-                            ∀g0. g1 ⋓ g0 ≡ f1 → g2 ⋓ g0 ≡ f2 → g ⋓ g0 ≡ f.
+corec theorem sor_coll_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g1,g2,g. g1 ⋓ g2 ≡ g →
+                           ∀g0. g1 ⋓ g0 ≡ f1 → g2 ⋓ g0 ≡ f2 → g ⋓ g0 ≡ f.
 #f1 #f2 #f cases (pn_split f) * #x #Hx #Hf #g1 #g2 #g #Hg #g0 #Hf1 #Hf2
 [ cases (sor_inv_xxp … Hf … Hx) -Hf #x1 #x2 #Hf #Hx1 #Hx2
   cases (sor_inv_xxp … Hf1 … Hx1) -f1 #y1 #y0 #Hf1 #Hy1 #Hy0
@@ -508,3 +515,30 @@ corec theorem sor_distr_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g1,g2,g. g1 ⋓ g
 ]
 qed-.
 
+corec theorem sor_distr_dx: ∀g0,g1,g2,g. g1 ⋓ g2 ≡ g →
+                            ∀f1,f2,f. g1 ⋓ g0 ≡ f1 → g2 ⋓ g0 ≡ f2 → g ⋓ g0 ≡ f →
+                            f1 ⋓ f2 ≡ f.
+#g0 cases (pn_split g0) * #y0 #H0 #g1 #g2 #g
+[ * -g1 -g2 -g #y1 #y2 #y #g1 #g2 #g #Hy #Hy1 #Hy2 #Hy #f1 #f2 #f #Hf1 #Hf2 #Hf
+  [ cases (sor_inv_ppx … Hf1 … Hy1 H0) -g1
+    cases (sor_inv_ppx … Hf2 … Hy2 H0) -g2
+    cases (sor_inv_ppx … Hf … Hy H0) -g
+  | cases (sor_inv_npx … Hf1 … Hy1 H0) -g1
+    cases (sor_inv_ppx … Hf2 … Hy2 H0) -g2
+    cases (sor_inv_npx … Hf … Hy H0) -g
+  | cases (sor_inv_ppx … Hf1 … Hy1 H0) -g1
+    cases (sor_inv_npx … Hf2 … Hy2 H0) -g2
+    cases (sor_inv_npx … Hf … Hy H0) -g
+  | cases (sor_inv_npx … Hf1 … Hy1 H0) -g1
+    cases (sor_inv_npx … Hf2 … Hy2 H0) -g2
+    cases (sor_inv_npx … Hf … Hy H0) -g
+  ] -g0 #y #Hy #H #y2 #Hy2 #H2 #y1 #Hy1 #H1
+  /3 width=8 by sor_nn, sor_np, sor_pn, sor_pp/
+| #H #f1 #f2 #f #Hf1 #Hf2 #Hf
+  cases (sor_xnx_tl … Hf1 … H0) -Hf1
+  cases (sor_xnx_tl … Hf2 … H0) -Hf2
+  cases (sor_xnx_tl … Hf … H0) -Hf
+  -g0 #y #x #Hx #Hy #H #y2 #x2 #Hx2 #Hy2 #H2 #y1 #x1 #Hx1 #Hy1 #H1
+  /4 width=8 by sor_tl, sor_nn/
+]
+qed-.
-- 
2.39.2