(* *)
(**************************************************************************)
-include "basic_2/multiple/lifts_lifts.ma".
-include "basic_2/multiple/drops_drops.ma".
-include "basic_2/static/aaa_lifts.ma".
include "basic_2/static/aaa_aaa.ma".
-include "basic_2/computation/lsubc_drops.ma".
+include "basic_2/rt_computation/lsubc_drops.ma".
(* GENERIC COMPUTATION PROPERTIES *******************************************)
(* Basic_1: was: sc3_arity_csubc *)
theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
gcp RR RS RP → gcr RR RS RP RP →
- ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,cs. ⬇*[Ⓕ, cs] L0 ≡ L1 →
- ∀T0. ⬆*[cs] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+ ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 →
+ ∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
-#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
-[ #G #L #s #L0 #cs #HL0 #X #H #L2 #HL20
- >(lifts_inv_sort1 … H) -H
+#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq … G L1 T) -G -L1 -T
+#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
+[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
+ lapply (aaa_inv_sort … HA) -HA #H destruct
+ >(lifts_inv_sort1 … H0) -H0
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
- lapply (b4 … HAtom G L2 (◊)) /2 width=1 by/
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #cs #HL01 #X #H #L2 #HL20
- lapply (acr_gcr … H1RP H2RP B) #HB
- elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
- lapply (drop_fwd_drop2 … HLK1) #HK1b
- elim (drops_drop_trans … HL01 … HLK1) #X #cs1 #i0 #HL0 #H #Hi0 #Hcs1
- >(at_mono … Hi1 … Hi0) -i1
- elim (drops_inv_skip2 … Hcs1 … H) -cs1 #K0 #V0 #cs0 #Hcs0 #HK01 #HV10 #H destruct
- elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
+ lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/
+| #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+ elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
+ elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
+ lapply (acr_gcr … H1RP H2RP A) #HA
+ lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
+ elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+ lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
+ elim (drops_inv_skip2 … HY) -HY #K0 #V0 #HK01 #HV10 #H destruct
+ elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0
+ elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
elim (lsubc_inv_pair2 … H) -H *
[ #K2 #HK20 #H destruct
- elim (lift_total V0 0 (i0 +1)) #V #HV0
- elim (lifts_lift_trans … Hi0 … Hcs0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
- lapply (b5 … HB ? G ? ? (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
- | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hcs0
- #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
- lapply (drop_fwd_drop2 … HLK2) #HLK2b
- lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
- lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B
- elim (lift_total V0 0 (i0 +1)) #V3 #HV03
- elim (lift_total V2 0 (i0 +1)) #V #HV2
- lapply (b5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/
- lapply (b7 … HB G L2 (◊)) /3 width=7 by gcr_lift/
+ lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
+ lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA
+ /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
+ | #K2 #V2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1
+ lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
+ lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
+ lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
+ elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23
+ lapply (s5 … HA … G … (◊) … (ⓝV0.V2) (ⓝV.V3) ????)
+ [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
+ lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/
]
-| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
- elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+| #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
+ elim (aaa_inv_gref … HA)
+| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+ elim (aaa_inv_abbr … HA) -HA #B #HV #HT
+ elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (acr_gcr … H1RP H2RP B) #HB
- lapply (b1 … HB) -HB #HB
- lapply (b6 … HA G L2 (◊) (◊)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/
-| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL02
- elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
- @(acr_abst … H1RP H2RP) /2 width=5 by/
- #L3 #V3 #W3 #T3 #cs3 #HL32 #HW03 #HT03 #H1B #H2B
- elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts … L2 W3 … (cs @@ cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
- @(IHA (L2. ⓛW3) … (cs + 1 @@ cs3 + 1)) -IHA
- /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
-| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
- elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
- /3 width=10 by drops_nil, lifts_nil/
-| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #cs #HL0 #X #H #L2 #HL20
- elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+ lapply (s1 … HB) -HB #HB
+ lapply (s6 … HA G L2 (◊) (◊)) /4 width=10 by lsubc_pair, liftsv_nil, drops_skip/
+| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+ elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
+ elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
+ @(acr_abst … H1RP H2RP) /2 width=10 by/
+ #b3 #f3 #L3 #V3 #W3 #T3 #HL32 #HW03 #HT03 #H1B #H2B
+ elim (drops_lsubc_trans … H1RP … HL32 … HL20) -L2 #L2 #HL32 #HL20
+ lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW
+ [4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3
+ @(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH
+ /3 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
+| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+ elim (aaa_inv_appl … HA) -HA #B #HV #HT
+ elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
+ lapply (IH … HT … HL01 … HT0 … HL20) -HT -HT0
+ /3 width=10 by drops_refl, lifts_refl/
+| #W #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+ elim (aaa_inv_cast … HA) -HA #HW #HT
+ elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
- lapply (b7 … HA G L2 (◊)) /3 width=5 by/
+ lapply (s7 … HA G L2 (◊)) /3 width=10 by/
]
qed.
(* Basic_1: was: sc3_arity *)
lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
-/2 width=8 by drops_nil, lifts_nil, acr_aaa_csubc_lifts/ qed.
+/3 width=9 by drops_refl, lifts_refl, acr_aaa_csubc_lifts/ qed.
lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
lapply (acr_gcr … H1RP H2RP A) #HA
-@(b1 … HA) /2 width=4 by acr_aaa/
+@(s1 … HA) /2 width=4 by acr_aaa/
qed.
projects / helm.git / blobdiff