(**************************************************************************) (* ___ *) (* ||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/relocation/drops_weight.ma". include "basic_2/s_computation/fqup_weight.ma". include "basic_2/s_computation/fqus_fqup.ma". include "basic_2/static/frees.ma". corec lemma sle_refl: ∀f. f ⊆ f. #f cases (pn_split f) * #g #H [ @(sle_push … H H) | @(sle_next … H H) ] -H // qed. lemma sle_inv_tl1: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2. #f1 elim (pn_split f1) * #g #H destruct /2 width=5 by sle_next, sle_weak/ qed-. axiom sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≡ ⫱*[n]f. axiom sor_sle1: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g ⊆ f. axiom sor_sle2: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f2 → g ⊆ f. lemma fqus_inv_refl_atom3: ∀I,G,L,X. ⦃G, L, ⓪{I}⦄ ⊐* ⦃G, L, X⦄ → ⓪{I} = X. #I #G #L #X #H elim (fqus_inv_fqup … H) -H [2: * // ] #H lapply (fqup_fwd_fw … H) -H #H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/ qed-. axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0. axiom fqus_split_fqu: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨ ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊐ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄. axiom fqus_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐* ⦃G2, L2, T2⦄ → ∧∧ G1 = G2 & ⋆ = L2 & ⓪{I} = T2. axiom fqus_inv_sort1: ∀G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐* ⦃G2, L2, T2⦄ → ∧∧ G1 = G2 & L1 = L2 & ⋆s = T2. axiom fqus_inv_zero1: ∀I,G1,G2,L1,L2,V1,T2. ⦃G1, L1.ⓑ{I}V1, #0⦄ ⊐* ⦃G2, L2, T2⦄ → (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #0 = T2) ∨ ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄. axiom fqus_inv_lref1: ∀I,G1,G2,L1,L2,V1,T2,i. ⦃G1, L1.ⓑ{I}V1, #⫯i⦄ ⊐* ⦃G2, L2, T2⦄ → (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #(⫯i) = T2) ∨ ⦃G1, L1, #i⦄ ⊐* ⦃G2, L2, T2⦄. axiom fqus_inv_gref1: ∀G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐* ⦃G2, L2, T2⦄ → ∧∧ G1 = G2 & L1 = L2 & §l = T2. axiom fqus_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓑ{p,I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ → ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2 | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄ | ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐* ⦃G2, L2, T2⦄. axiom fqus_inv_flat1: ∀I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓕ{I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ → ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2 | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄ | ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄. (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) lemma frees_drops_sle: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀L2,T2. ⦃G, L1, T1⦄ ⊐* ⦃G, L2, T2⦄ → ∀I,n. ⬇*[n] L1 ≡ L2.ⓑ{I}T2 → ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ ⫱*[⫯n] f1. #f1 #G #L1 #T1 #H elim H -f1 -L1 -T1 [ #f1 #J #Hf1 #L2 #T2 #H12 #I #n #HL12 elim (fqus_inv_atom1 … H12) -H12 #H1 #H2 #H3 destruct lapply (drops_fwd_lw … HL12) -HL12 #HL12 elim (lt_le_false … HL12) -HL12 // | #f1 #J #L1 #V1 #s #_ #_ #L2 #T2 #H12 #I #n #HL12 elim (fqus_inv_sort1 … H12) -H12 #H1 #H2 #H3 destruct lapply (drops_fwd_lw … HL12) -HL12 #HL12 elim (lt_le_false … HL12) -HL12 // | #f1 #J #L1 #V1 #Hf1 #IH #L2 #T2 #H12 elim (fqus_inv_zero1 … H12) -H12 [ * | #H12 #I * ] [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct lapply (drops_fwd_lw … HL12) -HL12 #HL12 elim (lt_le_false … HL12) -HL12 // | -IH -H12 #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // #H destruct /3 width=3 by sle_refl, ex2_intro/ | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12 #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/ ] | #f1 #J #L1 #V1 #i #Hf1 #IH #L2 #T2 #H12 elim (fqus_inv_lref1 … H12) -H12 [ * | #H12 #I * ] [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct lapply (drops_fwd_lw … HL12) -HL12 #HL12 elim (lt_le_false … HL12) -HL12 // | -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // #H destruct <(fqus_inv_refl_atom3 … H12) -H12 /2 width=3 by sle_refl, ex2_intro/ | -Hf1 #I #HL12 lapply (drops_inv_drop1 … HL12) -HL12 #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/ ] | #f1 #J #L1 #V1 #l #_ #_ #L2 #T2 #H12 #I #n #HL12 elim (fqus_inv_gref1 … H12) -H12 #H1 #H2 #H3 destruct lapply (drops_fwd_lw … HL12) -HL12 #HL12 elim (lt_le_false … HL12) -HL12 // | #f1V #f1T #f1 #p #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12 elim (fqus_inv_bind1 … H12) -H12 [ * |*: #H12 ] [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct lapply (drops_fwd_lw … HL12) -HL12 #HL12 elim (lt_le_false … HL12) -HL12 // | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12 /4 width=6 by sor_tls, sor_sle1, ex2_intro/ | -IHV elim (IHT … H12 I (⫯n)) -IHT -H12 /2 width=1 by drops_drop/ -HL12