#h #g #G #L #T1 #T2 #l1 #H @(lsstas_ind_dx … H) -T2 -l1 //
#l1 #T #T2 #HT1 #HT2 #IHT1 #l2 #Hl2 #Hl12
lapply (lsstas_da_conf … HT1 … Hl2) -HT1
->(plus_minus_m_m (l2-l1) 1 ?) [2: /2 width=1/ ]
-/4 width=5 by cpxs_strap1, ssta_cpx, lt_to_le/
+>(plus_minus_m_m (l2-l1) 1 ?)
+[ /4 width=5 by cpxs_strap1, ssta_cpx, lt_to_le/
+| /2 width=1 by monotonic_le_minus_r/
+]
qed.
lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i.
⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡*[h, g] V2 →
∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2.
-#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9/ ]
-#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
-lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
-elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
+#h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2
+[ /3 width=9 by cpx_cpxs, cpx_delta/
+| #V1 lapply (ldrop_fwd_ldrop2 … HLK) -HLK
+ elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
+]
qed.
(* Advanced inversion lemmas ************************************************)
T2 = #i ∨
∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ➡*[h, g] T1 &
⇧[0, i + 1] T1 ≡ T2.
-#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1/
+#h #g #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
#T #T2 #_ #HT2 *
[ #H destruct
- elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1/
- * /4 width=7/
+ elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
+ * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
| * #I #K #V1 #T1 #HLK #HVT1 #HT1
lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
- elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=7/
+ elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T
+ /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
]
qed-.
(* Relocation properties ****************************************************)
lemma cpxs_lift: ∀h,g,G. l_liftable (cpxs h g G).
-/3 width=9/ qed.
+/3 width=9 by cpx_lift, cpxs_strap1, l_liftable_LTC/ qed.
lemma cpxs_inv_lift1: ∀h,g,G. l_deliftable_sn (cpxs h g G).
/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/
lemma fsupq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 [ /3 width=3/ ]
-#T #T2 #HT2 #_ #IHTU2 #T1 #HT1
-elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
-elim (IHTU2 … HT2) -T2 /3 width=3/
+#h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2
+[ /3 width=3 by fsupq_fsups, ex2_intro/
+| #T #T2 #HT2 #_ #IHTU2 #T1 #HT1
+ elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
+ elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/
+]
qed-.
lemma fsupq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
lemma fsups_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 [ /2 width=3/ ]
-#G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
-elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
-elim (IHT1 … HT2) -T #T #HT1 #HT2
-lapply (fsups_trans … HT2 … HTU2) -G -L -T2 /2 width=3/
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2
+[ /2 width=3 by ex2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
+ elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2
+ elim (IHT1 … HT2) -T /3 width=7 by fsups_trans, ex2_intro/
+]
qed-.
lemma fsups_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
/3 width=7 by fsups_cpxs_trans, lsstas_cpxs/ qed-.
+
+lemma fsups_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2
+[ /2 width=3 by ex2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2
+ elim (fsupq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2
+ elim (IHT1 … HT2) -T /3 width=7 by fsups_strap1, ex2_intro/
+]
+qed-.
\ No newline at end of file
lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ →
∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ]
-#G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #L2
+#G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #HL02
[ elim (fsupq_cpxs_trans … HT0 … HG1) -T
/3 width=7 by fsups_trans, ex3_2_intro/
| /3 width=5 by cpxs_strap2, ex3_2_intro/
-| lapply (lpx_cpxs_trans … HT0 … HL1) -HT0 #HT10
+| lapply (lpx_cpxs_trans … HT0 … HL1) -HT0
+ elim (lpx_fsups_trans … HG2 … HL1) -L
+ /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
]
+qed-.
(* Main properties **********************************************************)
theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2.
⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 *
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 *
/4 width=5 by fpbs_trans, fsups_fpbs, cpxs_fpbs, lpxs_fpbs/
qed-.
lemma cpxs_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 →
∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[h, g] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[h, g] ⓑ{a,I}V2.T2.
-#h #g #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12
-lapply (lpxs_cpxs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
-qed.
+/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
(* Inversion lemmas on context-sensitive ext parallel computation for terms *)
lemma cpxs_inv_abst1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡*[h, g] U2 →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h, g] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[h, g] T2 &
U2 = ⓛ{a}V2.T2.
-#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5/
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
-lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) /2 width=1/ -HT02 #HT02
-lapply (cpxs_strap1 … HV10 … HV02) -V0
-lapply (cpxs_trans … HT10 … HT02) -T0 /2 width=5/
+lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/
qed-.
lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h, g] U2 → (
U2 = ⓓ{a}V2.T2
) ∨
∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[h, g] T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
+#h #g #a #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
#U0 #U2 #_ #HU02 * *
[ #V0 #T0 #HV10 #HT10 #H destruct
elim (cpx_inv_abbr1 … HU02) -HU02 *
[ #V2 #T2 #HV02 #HT02 #H destruct
- lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02
- lapply (cpxs_strap1 … HV10 … HV02) -V0
- lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=5/
+ lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?)
+ /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
| #T2 #HT02 #HUT2
- lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02
- lapply (cpxs_trans … HT10 … HT02) -T0 /3 width=3/
+ lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
+ /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/
]
| #U1 #HTU1 #HU01
elim (lift_total U2 0 1) #U #HU2
- lapply (cpx_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/
+ /6 width=11 by cpxs_strap1, cpx_lift, ldrop_ldrop, ex3_intro, or_intror/
]
qed-.
lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, g] L2.ⓑ{I}V2.
/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed.
+
+(* Properties on supclosure *************************************************)
+
+lemma lpxs_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
+[ /2 width=5 by ex3_2_intro/
+| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
+ lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
+ elim (lpx_fsupq_trans … HT2 … HK1) -K
+ /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpxs_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fsupq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpxs_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_trans, fsups_strap1, ex3_2_intro/
+qed-.
+
+lemma lpx_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fsupq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpx_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_strap1, fsups_strap1, ex3_2_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+(*
+include "basic_2/reduction/lpr_ldrop.ma".
+
+include "basic_2/unfold/fsups.ma".
+include "basic_2/reducibility/lpr_ldrop.ma".
+
+lamma pippo: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀V1,i. ⇧[i, 1] V1 ≡ T1 → T2 = #i → ⊥.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
+[ #I #L1 #V #W1 #j #H1 #H2
+ elim (lift_inv_lref2 … H1) -H1 * #H1 #H3
+
+ HVT2 : ()
+ HV2 : (K2⊢V➡V2)
+
+
+thaorem cpr_trans_lpr: ∀L1,T1,T. L1 ⊢ T1 ➡ T → ∀L2. L1 ⊢ ➡ L2 →
+ ∀T2. L2 ⊢ T ➡ T2 →
+ (⦃L2, T2⦄ ⊃* ⦃L1, T1⦄ → ⊥) ∨ T1 = T.
+#L1 #T1 @(fsupp_wf_ind … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
+[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct -IH
+ elim (cpr_inv_atom1 … H1) -H1
+ [ #H destruct
+ elim (cpr_inv_atom1 … HT2) -HT2
+ [ #H destruct //
+ | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct //
+ ]
+ | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+ elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
+ elim (lpr_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -V0 #HLK2
+ elim (cpr_inv_lift1 … HT2 … HLK2 … HVT) -HT2 -HLK2 -HVT #V2 #HVT2 #HV2
+ @or_introl #H
+
+
+
+
+
+
+ elim (lift_inv_lref2 … HVT2) -HVT2 * #H #_
+ [ elim (lt_zero_false … H)
+ | >commutative_plus in H; >plus_plus_comm_23 #H
+ elim (le_plus_xySz_x_false … H)
+ ]
+ ]
+| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpr_inv_bind1 … H1) -H1 *
+ [ #V #T #HV1 #HT1 #H destruct
+ elim (cpr_inv_bind1 … H2) -H2 *
+ [ #V2 #T2 #HV2 #HT2 #H destruct
+ elim (IH … HV1 … HV2) // #HV12 destruct
+ [ @or_introl #H destruct /2 width=1/
+ | elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct
+ @or_introl #H destruct /2 width=1/
+ ]
+ | #T2 #HT2 #HXT2 #H1 #H2 destruct
+ elim (IH … HT1 … HT2) // /2 width=1/ -L1 -L2 #HT12 destruct
+ | elim (term_eq_dec V1 V) #HV1 destruct
+
+ ]
+ | #Y1 #HTY1 #HXY1 #H11 #H12 destruct
+ elim (lift_total (+ⓓV1.T1) 0 1) #Y2 #HXY2
+ lapply (cpr_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/
+ ]
+| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpr_inv_flat1 … H1) -H1 *
+ [ #V #T #HV1 #HT1 #H destruct
+ elim (cpr_inv_flat1 … H2) -H2 *
+ [ #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+ | #HX2 #H destruct /3 width=5/
+ ]
+ | #HX1 #H destruct /3 width=5/
+]
+qed-.
+*)
--- /dev/null
+(* Advanced inversion lemmas on plus-iterated supclosure ********************)
+
+lamma fsupp_inv_bind1_fsups: ∀b,J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃G2, L2, T2⦄.
+#b #J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H
+ elim (fsup_inv_bind1 … H) -H * #H1 #H2 #H3 destruct /2 width=1/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/
+]
+qad-.
+
+lamma fsupp_inv_flat1_fsups: ∀J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓕ{J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃G1, L1, U⦄ ⊃* ⦃G2, L2, T2⦄.
+#J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H
+ elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
+| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/
+]
+qad-.
+
+lamma fsupp_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
+/2 width=1 by tri_inj/ qed.
+
+lamma fsups_lref: ∀I,G,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃* ⦃G, K, V⦄.
+/3 width=5 by _/ qed.
+
+lamma fsups_lref_S_lt: ∀I,G1,G2,L,K,V,T,i.
+ 0 < i → ⦃G1, L, #(i-1)⦄ ⊃* ⦃G2, K, T⦄ → ⦃G1, L.ⓑ{I}V, #i⦄ ⊃+ ⦃G2, K, T⦄.
+/3 width=7 by _/ qed.
- first letter
+b: bi contex-sensitive for local environments
c: contex-sensitive for terms
f: context-freee for closures
l: sn contex-sensitive for local environments
(**************************************************************************)
include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/relocation/fsupq.ma".
+include "basic_2/relocation/fsupq_alt.ma".
include "basic_2/static/ssta.ma".
include "basic_2/reduction/cpx.ma".
(* Properties on supclosure *************************************************)
+lemma fsup_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=3 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
+[ #I #G #L #V2 #U2 #HVU2
+ elim (lift_total U2 0 1)
+ /4 width=9 by fsup_drop, cpx_append, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
+| #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
+ elim (lift_total T2 0 (e+1))
+ /3 width=11 by cpx_lift, fsup_drop, ex2_intro/
+]
+qed-.
+
+lemma fsup_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
+ ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃ ⦃G2, L2, U2⦄.
+/3 width=5 by fsup_cpx_trans, ssta_cpx/ qed-.
+
lemma fsupq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=3 by fsup_fsupq, fsupq_refl, cpx_pair_sn, cpx_bind, cpx_flat, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, ex2_intro/
-[ #I #G #L1 #V2 #U2 #HVU2
- elim (lift_total U2 0 1)
- /4 width=9 by fsupq_refl, fsupq_ldrop, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
-| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
- elim (IHT12 … HTU2) -IHT12 -HTU2 #T
- elim (lift_total T d e)
- /3 width=11 by cpx_lift, fsupq_ldrop, ex2_intro/
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H
+[ #HT12 elim (fsup_cpx_trans … HT12 … HTU2) /3 width=3 by fsup_fsupq, ex2_intro/
+| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
]
qed-.
∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
/3 width=5 by fsupq_cpx_trans, ssta_cpx/ qed-.
-
-lemma fsup_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-/3 width=3 by fsupq_cpx_trans, fsup_fsupq/ qed-.
-
-lemma fsup_ssta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
- ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h, g] U2 →
- ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
- ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
-/3 width=5 by fsupq_ssta_trans, fsup_fsupq/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/fsup.ma".
+include "basic_2/relocation/fsupq_alt.ma".
include "basic_2/relocation/ldrop_lpx_sn.ma".
include "basic_2/reduction/cpr_lift.ma".
include "basic_2/reduction/lpr.ma".
lemma fsup_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
-[ #G #L #K #U #T #d #e #HLK #HUT #He #U2 #HU2
- elim (lift_total U2 d e) #T2 #HUT2
- lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9/
-| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
- elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
- elim (lift_total T d e) #U #HTU
- elim (ldrop_lpr_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K
- lapply (cpr_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/
+#G #L #K #U #T #e #HLK #HUT #U2 #HU2
+elim (lift_total U2 0 (e+1)) #T2 #HUT2
+lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fsup_drop, ex3_2_intro/
+qed-.
+
+lemma fsupq_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 →
+ ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃⸮ ⦃G2, L2, U2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fsupq_inv_gen … H) -H
+[ #HT12 elim (fsup_cpr_trans … HT12 … HTU2) /3 width=5 by fsup_fsupq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* Properties on supclosure *************************************************)
-lemma fsupq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
+lemma fsup_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄.
#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fsup_fsupq, fsupq_refl, lpx_pair, fsup_lref_O, fsup_pair_sn, fsup_flat_dx, ex3_2_intro/
+/3 width=5 by fsup_lref_O, fsup_pair_sn, fsup_flat_dx, lpx_pair, ex3_2_intro/
[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
#K2 #W2 #HLK2 #HVW2 #H destruct
/3 width=5 by fsup_fsupq, cpx_pair_sn, fsup_bind_dx, ex3_2_intro/
-| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IH12 #K0 #HK20
- elim (IH12 … HK20) -K2 #K2 #T #HK12
- elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
- elim (lift_total T d e)
- /3 width=11 by cpx_lift, fsupq_ldrop, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
+ elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
+ /3 width=7 by fsup_drop, ex3_2_intro/
+]
+qed-.
+
+lemma fsupq_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, g] K2 →
+ ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, g] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fsupq_inv_gen … H) -H
+[ #HT12 elim (fsup_lpx_trans … HT12 … HLK2) /3 width=5 by fsup_fsupq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fsup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/3 width=7 by fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, lpx_pair, ex3_2_intro/
+[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
+ #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
+ /4 width=7 by cpx_delta, fsup_drop, ldrop_ldrop, ex3_2_intro/
+| #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
+ elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
+ /3 width=5 by fsup_drop, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fsupq_inv_gen … H) -H
+[ #HT12 elim (lpx_fsup_trans … HT12 … HKL1) /3 width=5 by fsup_fsupq, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
]
qed-.
(* activate genv *)
inductive fsup: tri_relation genv lenv term ≝
-| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V
-| fsup_pair_sn : ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V
-| fsup_bind_dx : ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
-| fsup_flat_dx : ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T
-| fsup_ldrop_lt: ∀G,L,K,T,U,d,e.
- ⇩[d, e] L ≡ K → ⇧[d, e] T ≡ U → 0 < e → fsup G L U G K T
-| fsup_ldrop : ∀G1,G2,L1,K1,K2,T1,T2,U1,d,e.
- ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
- fsup G1 K1 T1 G2 K2 T2 → fsup G1 L1 U1 G2 K2 T2
+| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V
+| fsup_pair_sn: ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V
+| fsup_bind_dx: ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
+| fsup_flat_dx: ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T
+| fsup_drop : ∀G,L,K,T,U,e.
+ ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fsup G L U G K T
.
interpretation
(* Basic properties *********************************************************)
-lemma fsup_lref_S_lt: ∀I,G1,G2,L,K,V,T,i. 0 < i → ⦃G1, L, #(i-1)⦄ ⊃ ⦃G2, K, T⦄ → ⦃G1, L.ⓑ{I}V, #i⦄ ⊃ ⦃G2, K, T⦄.
-#I #G1 #G2 #L #K #V #T #i #Hi #H /3 width=7 by fsup_ldrop, ldrop_ldrop, lift_lref_ge_minus/ (**) (* auto too slow without trace *)
+lemma fsup_drop_lt: ∀G,L,K,T,U,e. 0 < e →
+ ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsup G L U G K T.
+#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fsup_drop/
qed.
-lemma fsup_lref: ∀I,G,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃ ⦃G, K, V⦄.
-#I #G #K #V #i @(nat_elim1 i) -i #i #IH #L #H
-elim (ldrop_inv_O1_pair2 … H) -H *
-[ #H1 #H2 destruct //
-| #I1 #K1 #V1 #HK1 #H #Hi destruct
- lapply (IH … HK1) /2 width=1/
-]
+lemma fsup_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄.
+/3 width=3 by fsup_drop, ldrop_ldrop, lift_lref_ge_minus/
qed.
(* Basic forward lemmas *****************************************************)
lemma fsup_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
-[ #G #L #K #T #U #d #e #HLK #HTU #HKL
- lapply (ldrop_fwd_lw_lt … HLK HKL) -HKL -HLK #HKL
- lapply (lift_fwd_tw … HTU) -d -e #H
- normalize in ⊢ (?%%); /2 width=1/
-| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
- lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
- lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
- @(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
-]
+#G #L #K #T #U #e #HLK #HTU
+lapply (ldrop_fwd_lw_lt … HLK ?) -HLK // #HKL
+lapply (lift_fwd_tw … HTU) -e #H
+normalize in ⊢ (?%%); /2 width=1 by lt_minus_to_plus/
qed-.
fact fsup_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
[1: normalize //
|3: #a
|5: /2 width=4 by ldrop_fwd_length_lt4/
-|6: #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
- lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 #HLK1
- elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
- @(lt_to_le_to_lt … HLK1) /2 width=2/
] #I #G #L #V #T #j #H destruct
qed-.
(* activate genv *)
inductive fsupq: tri_relation genv lenv term ≝
-| fsupq_refl : ∀G,L,T. fsupq G L T G L T
| fsupq_lref_O : ∀I,G,L,V. fsupq G (L.ⓑ{I}V) (#0) G L V
| fsupq_pair_sn: ∀I,G,L,V,T. fsupq G L (②{I}V.T) G L V
| fsupq_bind_dx: ∀a,I,G,L,V,T. fsupq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
| fsupq_flat_dx: ∀I,G, L,V,T. fsupq G L (ⓕ{I}V.T) G L T
-| fsupq_ldrop : ∀G1,G2,L1,K1,K2,T1,T2,U1,d,e.
- ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
- fsupq G1 K1 T1 G2 K2 T2 → fsupq G1 L1 U1 G2 K2 T2
+| fsupq_drop : ∀G,L,K,T,U,e.
+ ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsupq G L U G K T
.
interpretation
(* Basic properties *********************************************************)
-lemma fsup_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=7/ qed.
-
-(* Basic properties *********************************************************)
+lemma fsupq_refl: tri_reflexive … fsupq.
+/2 width=3 by fsupq_drop/ qed.
-lemma fsupq_lref_S_lt: ∀I,G1,G2,L,K,V,T,i.
- 0 < i → ⦃G1, L, #(i-1)⦄ ⊃⸮ ⦃G2, K, T⦄ → ⦃G1, L.ⓑ{I}V, #i⦄ ⊃⸮ ⦃G2, K, T⦄.
-/3 width=7/ qed.
-
-lemma fsupq_lref: ∀I,G,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃⸮ ⦃G, K, V⦄.
-/3 width=2/ qed.
+lemma fsup_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fsupq_drop/
+qed.
(* Basic forward lemmas *****************************************************)
lemma fsupq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // [1,2,3: /2 width=1/ ]
-#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
-lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
-lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
-@(transitive_le … IHT12) -IHT12 /2 width=1/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /2 width=1 by lt_to_le/
+#G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1
+lapply (ldrop_fwd_lw … HLK1) -HLK1
+lapply (lift_fwd_tw … HTU1) -HTU1
+/2 width=1 by le_plus, le_n/
qed-.
fact fsupq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
∀i. T1 = #i → |L2| ≤ |L1|.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 //
[ #a #I #G #L #V #T #j #H destruct
-| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
- lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 #HLK1
- elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
- @(transitive_le … HLK1) /2 width=2/
+| #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #i #H destruct
+ /2 width=3 by ldrop_fwd_length_le4/
]
qed-.
lemma fsupqa_refl: tri_reflexive … fsupqa.
// qed.
-lemma fsupqa_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄ →
- ∀L1,d,e. ⇩[d, e] L1 ≡ K1 →
- ∀U1. ⇧[d, e] T1 ≡ U1 → ⦃G1, L1, U1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄.
-#G1 #G2 #K1 #K2 #T1 #T2 * [ /3 width=7/ ] * #H1 #H2 #H3 destruct
-#L1 #d #e #HLK #U1 #HTU elim (eq_or_gt e)
-/3 width=5 by fsup_ldrop_lt, or_introl/ #H destruct
->(ldrop_inv_O2 … HLK) -L1 >(lift_inv_O2 … HTU) -T2 -d //
+lemma fsupqa_drop: ∀G,L,K,T,U,e.
+ ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄.
+#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e)
+/3 width=5 by fsup_drop_lt, or_introl/ #H destruct
+>(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
qed.
(* Main properties **********************************************************)
theorem fsupq_fsupqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/2 width=7 by fsupqa_ldrop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/
+/2 width=3 by fsupqa_drop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/
qed.
(* Main inversion properties ************************************************)
(* Basic properties *********************************************************)
lemma fsup_fsupp: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-/2 width=1/ qed.
+/2 width=1 by tri_inj/ qed.
lemma fsupp_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2.
⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-/2 width=5/ qed.
+/2 width=5 by tri_step/ qed.
lemma fsupp_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2.
⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-/2 width=5/ qed.
+/2 width=5 by tri_TC_strap/ qed.
+
+lemma fsupp_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+ ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄.
+#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct
+[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 //
+| /3 width=5 by fsupp_strap2, fsup_drop_lt/
+]
+qed-.
lemma fsupp_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄.
-/3 width=2/ qed.
+/3 width=6 by fsup_lref_O, fsup_fsupp, lift_lref_ge, fsupp_ldrop/ qed.
lemma fsupp_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄.
-/2 width=1/ qed.
+/2 width=1 by fsup_pair_sn, fsup_fsupp/ qed.
lemma fsupp_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄.
-/2 width=1/ qed.
+/2 width=1 by fsup_bind_dx, fsup_fsupp/ qed.
lemma fsupp_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄.
-/2 width=1/ qed.
+/2 width=1 by fsup_flat_dx, fsup_fsupp/ qed.
lemma fsupp_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄.
-/2 width=5/ qed.
+/2 width=5 by fsup_pair_sn, fsupp_strap1/ qed.
lemma fsupp_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄.
-/2 width=5/ qed.
+/2 width=5 by fsup_flat_dx, fsupp_strap1/ qed.
lemma fsupp_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄.
-/2 width=5/ qed.
+/2 width=5 by fsup_bind_dx, fsupp_strap1/ qed.
(* Basic eliminators ********************************************************)
(* Main propertis ***********************************************************)
theorem fsupp_trans: tri_transitive … fsupp.
-/2 width=5/ qed-.
+/2 width=5 by tri_TC_transitive/ qed-.
(* Basic properties *********************************************************)
lemma fsups_refl: tri_reflexive … fsups.
-/2 width=1/ qed.
+/2 width=1 by tri_inj/ qed.
lemma fsupq_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=1/ qed.
+/2 width=1 by tri_inj/ qed.
lemma fsups_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=5/ qed.
+/2 width=5 by tri_step/ qed.
lemma fsups_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄.
-/2 width=5/ qed.
+/2 width=5 by tri_TC_strap/ qed.
+
+lemma fsups_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
+ ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+ ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
+#G1 #G2 #K1 #K2 #T1 #T2 #H @(fsups_ind … H) -G2 -K2 -T2
+/3 width=5 by fsups_strap1, fsupq_fsups, fsupq_drop/
+qed-.
(* Basic forward lemmas *****************************************************)
lemma fsups_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}.
-#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 //
-/3 width=3 by fsupq_fwd_fw, transitive_le/ (**) (* slow even with trace *)
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2
+/3 width=3 by fsupq_fwd_fw, transitive_le/
qed-.
-(*
-(* Advanced inversion lemmas on plus-iterated supclosure ********************)
-
-lamma fsupp_inv_bind1_fsups: ∀b,J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃G2, L2, T2⦄.
-#b #J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H
- elim (fsup_inv_bind1 … H) -H * #H1 #H2 #H3 destruct /2 width=1/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/
-]
-qad-.
-
-lamma fsupp_inv_flat1_fsups: ∀J,G1,G2,L1,L2,W,U,T2. ⦃G1, L1, ⓕ{J}W.U⦄ ⊃+ ⦃G2, L2, T2⦄ →
- ⦃G1, L1, W⦄ ⊃* ⦃G2, L2, T2⦄ ∨ ⦃G1, L1, U⦄ ⊃* ⦃G2, L2, T2⦄.
-#J #G1 #G2 #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H
- elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
-| #G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=4/
-]
-qad-.
-*)
(* Main properties **********************************************************)
theorem fsups_trans: tri_transitive … fsups.
-/2 width=5/ qed-.
+/2 width=5 by tri_TC_transitive/ qed-.
projects / helm.git / commitdiff