From 42705ef31dd3513a998533e02b5f20fb38dd4fb2 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 24 Feb 2018 21:16:46 +0100
Subject: [PATCH] advances on cpx_lfxs_conf_fle

+ transitivities for fle
+ minor additions
---
 .../basic_2/rt_computation/lfpxs_etc.ma       |  4 +++
 .../basic_2/rt_transition/cpx_etc.ma          | 18 ++++++++++--
 .../lambdadelta/basic_2/static/fle_fle.ma     | 29 +++++++++++++++----
 3 files changed, 43 insertions(+), 8 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
index d19718058..0f34a15b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma
@@ -3,6 +3,10 @@ include "basic_2/static/lfxs_lex.ma".
 include "basic_2/rt_transition/cpx_etc.ma".
 include "basic_2/rt_computation/lfpxs_lpxs.ma".
 
+lemma R_fle_comp_LTC: ∀R. R_fle_compatible R → R_fle_compatible (LTC … R).
+#R #HR #L #T1 #T2 #H elim H -T2
+/3 width=3 by fle_trans_dx/
+qed-.
 lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G).
 #h #G #L1 #T1 #T2 #HT12 #L2 #H
 elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma
index a10376a89..19999ed9b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma
@@ -18,6 +18,16 @@ include "basic_2/static/fle_fle.ma".
 include "basic_2/static/lfxs_length.ma".
 include "basic_2/rt_transition/cpx.ma".
 
+
+lemma fle_zero_bi: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ →
+                   ∀I1,I2. ⦃K1.ⓑ{I1}V1, #O⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄.
+#K1 #K2 #HK #V1 #V2
+* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12
+#I1 #I2
+elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct
+/3 width=12 by frees_pair, lveq_bind, sle_next, ex4_4_intro/
+qed.
+
 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
 
 (* Properties with context-sensitive free variables *************************)
@@ -42,11 +52,13 @@ axiom cpx_lfxs_conf_fle: ∀R,h. c_reflexive … R →
       elim (lfxs_inv_zero … HY) -HY *
       [ #H1 #H2 destruct -IH /2 width=1 by and3_intro/
       | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct
+        lapply (lfxs_fwd_length … HK02) #HK
         elim H2R -H2R #H2R
         [ <(H2R G0) in HV02; -H2R #HV02
-          elim (IH … HV02 … HK02) /2 width=2 by fqu_fqup, fqu_lref_O/ -IH -HV02 -HK02 #H1V #H2V #H3V
-        | lapply (H2R … HV02) -H2R -HV02 #HV20
-          elim (IH … V0 … HK02) [|*: /2 width=4 by fqu_fqup, fqu_lref_O/ ] -IH -HK02 #H1V #_ #_
+          elim (IH … HV02 … HK02) /2 width=2 by fqu_fqup, fqu_lref_O/ -IH -HV02 -HK02 #H1V #H2V #_
+          /4 width=1 by fle_trans_tc, fle_zero_bi, and3_intro/
+        | lapply (H2R … HV02 … HK02) -H2R -HV02 -HK02 -IH #HKV20
+          /3 width=1 by fle_zero_bi, and3_intro/
         ]
       | #f #I #K0 #K2 #Hf #HK02 #H1 #H2 destruct
       ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma
index 18574be3d..daa61f75a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma
@@ -40,12 +40,31 @@ elim (lveq_inj_length … H2L) // -L2 #H1 #H2 destruct
 qed-.
 
 (* Main properties **********************************************************)
-(*
-theorem fle_trans: bi_transitive … fle.
-#L1 #L #T1 #T * #f1 #f #HT1 #HT #Hf1 #L2 #T2 * #g #f2 #Hg #HT2 #Hf2
-/5 width=8 by frees_mono, sle_trans, sle_eq_repl_back2, ex3_2_intro/
+
+theorem fle_trans_sn: ∀L1,L2,T1,T. ⦃L1, T1⦄ ⊆ ⦃L2, T⦄ →
+                      ∀T2. ⦃L2, T⦄ ⊆ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄.
+#L1 #L2 #T1 #T
+* #m1 #m0 #g1 #g0 #Hg1 #Hg0 #Hm #Hg
+#T2
+* #n0 #n2 #f0 #f2 #Hf0 #Hf2 #Hn #Hf
+lapply (frees_mono … Hf0 … Hg0) -Hf0 -Hg0 #Hfg0
+elim (lveq_inj_length … Hn) // -Hn #H1 #H2 destruct
+lapply (sle_eq_repl_back1 … Hf … Hfg0) -f0
+/4 width=10 by sle_tls, sle_trans, ex4_4_intro/
+qed-.
+
+theorem fle_trans_dx: ∀L1,T1,T. ⦃L1, T1⦄ ⊆ ⦃L1, T⦄ →
+                      ∀L2,T2. ⦃L1, T⦄ ⊆ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄.
+#L1 #T1 #T
+* #m1 #m0 #g1 #g0 #Hg1 #Hg0 #Hm #Hg
+#L2 #T2
+* #n0 #n2 #f0 #f2 #Hf0 #Hf2 #Hn #Hf
+lapply (frees_mono … Hg0 … Hf0) -Hg0 -Hf0 #Hgf0
+elim (lveq_inj_length … Hm) // -Hm #H1 #H2 destruct
+lapply (sle_eq_repl_back2 … Hg … Hgf0) -g0
+/4 width=10 by sle_tls, sle_trans, ex4_4_intro/
 qed-.
-*)
+
 theorem fle_bind_sn_ge: ∀L1,L2. |L2| ≤ |L1| →
                         ∀V1,T1,T. ⦃L1, V1⦄ ⊆ ⦃L2, T⦄ → ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2, T⦄ →
                         ∀p,I. ⦃L1, ⓑ{p,I}V1.T1⦄ ⊆ ⦃L2, T⦄.
-- 
2.39.2