(* Basic inversion lemmas ***************************************************)
-lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥.
-/3 width=3/ qed-.
+lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥.
+/3 width=3 by crr_delta/ qed-.
lemma cir_inv_ri2: ∀I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈⦃②{I}V.T⦄ → ⊥.
-/3 width=1/ qed-.
+/3 width=1 by crr_ri2/ qed-.
lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
⦃G, L⦄ ⊢ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄.
-/4 width=1/ qed-.
+/4 width=1 by crr_ib2_sn, crr_ib2_dx, conj/ qed-.
lemma cir_inv_bind: ∀a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ & ib2 a I.
#a * [ elim a -a ]
-#G #L #V #T #H [ elim H -H /3 width=1/ ]
-elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+#G #L #V #T #H [ elim H -H /3 width=1 by crr_ri2, or_introl/ ]
+elim (cir_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/
qed-.
lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄ →
∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄.
#G #L #V #T #HVT @and3_intro /3 width=1/
generalize in match HVT; -HVT elim T -T //
-* // #a * #U #T #_ #_ #H elim H -H /2 width=1/
+* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/
qed-.
lemma cir_inv_flat: ∀I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓕ{I}V.T⦄ →
∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
* #G #L #V #T #H
-[ elim (cir_inv_appl … H) -H /2 width=1/
-| elim (cir_inv_ri2 … H) -H /2 width=1/
+[ elim (cir_inv_appl … H) -H /2 width=1 by and4_intro/
+| elim (cir_inv_ri2 … H) -H //
]
qed-.
lemma cir_ib2: ∀a,I,G,L,V,T.
ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
#a #I #G #L #V #T #HI #HV #HT #H
-elim (crr_inv_ib2 … HI H) -HI -H /2 width=1/
+elim (crr_inv_ib2 … HI H) -HI -H /2 width=1 by/
qed.
lemma cir_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄.
#G #L #V #T #HV #HT #H1 #H2
-elim (crr_inv_appl … H2) -H2 /2 width=1/
+elim (crr_inv_appl … H2) -H2 /2 width=1 by/
qed.
(* Properties on relocation *************************************************)
-lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈⦃U⦄.
-/3 width=7 by crr_inv_lift/ qed.
+/3 width=8 by crr_inv_lift/ qed.
-lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈⦃T⦄.
-/3 width=7/ qed-.
+/3 width=8 by crr_lift/ qed-.
(* Basic inversion lemmas ***************************************************)
lemma cix_inv_sort: ∀h,g,G,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄ → ⊥.
-/3 width=2/ qed-.
+/3 width=2 by crx_sort/ qed-.
-lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥.
-/3 width=4/ qed-.
+lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥.
+/3 width=4 by crx_delta/ qed-.
lemma cix_inv_ri2: ∀h,g,I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃②{I}V.T⦄ → ⊥.
-/3 width=1/ qed-.
+/3 width=1 by crx_ri2/ qed-.
lemma cix_inv_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ →
⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄.
-/4 width=1/ qed-.
+/4 width=1 by crx_ib2_sn, crx_ib2_dx, conj/ qed-.
lemma cix_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ →
∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ & ib2 a I.
#h #g #a * [ elim a -a ]
-#G #L #V #T #H [ elim H -H /3 width=1/ ]
-elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=1/
+#G #L #V #T #H [ elim H -H /3 width=1 by crx_ri2, or_introl/ ]
+elim (cix_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/
qed-.
lemma cix_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄ →
∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄.
#h #g #G #L #V #T #HVT @and3_intro /3 width=1/
generalize in match HVT; -HVT elim T -T //
-* // #a * #U #T #_ #_ #H elim H -H /2 width=1/
+* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crx_beta, crx_theta/
qed-.
lemma cix_inv_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓕ{I}V.T⦄ →
∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
#h #g * #G #L #V #T #H
-[ elim (cix_inv_appl … H) -H /2 width=1/
-| elim (cix_inv_ri2 … H) -H /2 width=1/
+[ elim (cix_inv_appl … H) -H /2 width=1 by and4_intro/
+| elim (cix_inv_ri2 … H) -H //
]
qed-.
(* Basic forward lemmas *****************************************************)
lemma cix_inv_cir: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄.
-/3 width=1/ qed-.
+/3 width=1 by crr_crx/ qed-.
(* Basic properties *********************************************************)
lemma cix_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ →
⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄.
#h #g #a #I #G #L #V #T #HI #HV #HT #H
-elim (crx_inv_ib2 … HI H) -HI -H /2 width=1/
+elim (crx_inv_ib2 … HI H) -HI -H /2 width=1 by/
qed.
lemma cix_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄.
#h #g #G #L #V #T #HV #HT #H1 #H2
-elim (crx_inv_appl … H2) -H2 /2 width=1/
+elim (crx_inv_appl … H2) -H2 /2 width=1 by/
qed.
(* Advanced properties ******************************************************)
-lemma cix_lref: ∀h,g,G,L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄.
+lemma cix_lref: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄.
#h #g #G #L #i #HL #H elim (crx_inv_lref … H) -h #I #K #V #HLK
lapply (ldrop_mono … HLK … HL) -L -i #H destruct
qed.
(* Properties on relocation *************************************************)
-lemma cix_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma cix_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄.
-/3 width=7 by crx_inv_lift/ qed.
+/3 width=8 by crx_inv_lift/ qed.
-lemma cix_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma cix_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄.
-/3 width=7/ qed-.
+/3 width=8 by crx_lift/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄ → ⊥.
+lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄ → ⊥.
#G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=6/ ] -HLK #H destruct
+lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct
elim (lift_inv_lref2_be … HVW) -HVW //
qed-.
lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍⦃T⦄.
#a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
]
qed-.
lemma cnr_inv_abbr: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃-ⓓV.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍⦃T⦄.
#G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
]
qed-.
lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
#G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
- lapply (H U ?) -H /2 width=3/ #H destruct
+ lapply (H U ?) -H /2 width=3 by cpr_zeta/ #H destruct
elim (lift_inv_pair_xy_y … HTU)
| #HT
- elim (cpr_delift G (⋆) V T (⋆. ⓓV) 0) // #T2 #T1 #HT2 #HT12
- lapply (H (+ⓓV.T2) ?) -H /4 width=1/ -HT2 #H destruct /3 width=2/
+ elim (cpr_delift G (⋆) V T (⋆. ⓓV) 0) //
+ #T2 #T1 #HT2 #HT12 lapply (H (+ⓓV.T2) ?) -H /4 width=1 by tpr_cpr, cpr_bind/ -HT2
+ #H destruct /3 width=2 by ex_intro/
]
qed-.
lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
#G #L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct //
| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
[ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
- | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
+ lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by tpr_cpr, cpr_theta/ -HV12 #H destruct
+ | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by tpr_cpr, cpr_beta/ #H destruct
]
qed-.
lemma cnr_inv_tau: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
-#G #L #V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
+#G #L #V #T #H lapply (H T ?) -H
+/2 width=4 by cpr_tau, discr_tpair_xy_y/
qed-.
(* Basic properties *********************************************************)
(* Advanced properties ******************************************************)
(* Basic_1: was only: nf2_csort_lref *)
-lemma cnr_lref_atom: ∀G,L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
+lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
#G #L #i #HL #X #H
elim (cpr_inv_lref1 … H) -H // *
#K #V1 #V2 #HLK #_ #_
qed.
(* Basic_1: was: nf2_lref_abst *)
-lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
+lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
#G #L #K #V #i #HLK #X #H
elim (cpr_inv_lref1 … H) -H // *
#K0 #V1 #V2 #HLK0 #_ #_
(* Relocation properties ****************************************************)
(* Basic_1: was: nf2_lift *)
-lemma cnr_lift: ∀G,L0,L,T,T0,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ →
- ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄.
-#G #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
+lemma cnr_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ →
+ ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄.
+#G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
<(HLT … HT1) in HT0; -L #HT0
>(lift_mono … HT10 … HT0) -T1 -X //
qed.
(* Note: this was missing in basic_1 *)
-lemma cnr_inv_lift: ∀G,L0,L,T,T0,d,e. ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄ →
- ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
-#G #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H
+lemma cnr_inv_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄ →
+ ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
+#G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
elim (lift_total X d e) #X0 #HX0
lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0
>(HLT0 … HTX0) in HX0; -L0 -X0 #H
->(lift_inj … H … HT0) -T0 -X -d -e //
+>(lift_inj … H … HT0) -T0 -X -s -d -e //
qed-.
lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄ → deg h g k 0.
#h #g #G #L #k #H elim (deg_total h g k)
#l @(nat_ind_plus … l) -l // #l #_ #Hkl
-lapply (H (⋆(next h k)) ?) -H /2 width=2/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
+lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_sort/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H)
qed-.
-lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥.
+lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥.
#h #g #I #G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=7/ ] -HLK #H destruct
+lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct
elim (lift_inv_lref2_be … HVW) -HVW //
qed-.
lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓛ{a}V.T⦄ →
⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍[h, g]⦃T⦄.
#h #g #a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
]
qed-.
lemma cnx_inv_abbr: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃-ⓓV.T⦄ →
⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍[h, g]⦃T⦄.
#h #g #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
]
qed-.
lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃+ⓓV.T⦄ → ⊥.
#h #g #G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
- lapply (H U ?) -H /2 width=3/ #H destruct
+ lapply (H U ?) -H /2 width=3 by cpx_zeta/ #H destruct
elim (lift_inv_pair_xy_y … HTU)
| #HT
elim (cpr_delift G(⋆) V T (⋆.ⓓV) 0) // #T2 #T1 #HT2 #HT12
- lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/
+ lapply (H (+ⓓV.T2) ?) -H /5 width=1 by cpr_cpx, tpr_cpr, cpr_bind/ -HT2
+ #H destruct /3 width=2 by ex_intro/
]
qed-.
[ elim (lift_total V1 0 1) #V2 #HV12
lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
| lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
+ ]
]
qed-.
lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓝV.T⦄ → ⊥.
-#h #g #G #L #V #T #H lapply (H T ?) -H /2 width=1/ #H
-@discr_tpair_xy_y //
+#h #g #G #L #V #T #H lapply (H T ?) -H
+/2 width=4 by cpx_tau, discr_tpair_xy_y/
qed-.
(* Basic forward lemmas *****************************************************)
lemma cnx_fwd_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
#h #g #G #L #T #H #U #HTU
-@H /2 width=1/ (**) (* auto fails because a δ-expansion gets in the way *)
+@H /2 width=1 by cpr_cpx/ (**) (* auto fails because a δ-expansion gets in the way *)
qed-.
(* Basic properties *********************************************************)
lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆((next h)^l k)⦄.
#h #g #G #L #k #l #Hkl
-lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1/
+lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1 by cnx_sort/
qed.
lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍[h, g]⦃T⦄ →
(* Advanced properties ******************************************************)
-lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄.
+lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄.
#h #g #G #L #i #HL #X #H
elim (cpx_inv_lref1 … H) -H // *
#I #K #V1 #V2 #HLK #_ #_
(* Relocation properties ****************************************************)
-lemma cnx_lift: ∀h,g,G,L0,L,T,T0,d,e. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⇩[d, e] L0 ≡ L →
+lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⇩[s, d, e] L0 ≡ L →
⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄.
-#h #g #G #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
+#h #g #G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
<(HLT … HT1) in HT0; -L #HT0
>(lift_mono … HT10 … HT0) -T1 -X //
qed.
-lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,d,e. ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[d, e] L0 ≡ L →
+lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[s, d, e] L0 ≡ L →
⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄.
-#h #g #G #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H
+#h #g #G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
elim (lift_total X d e) #X0 #HX0
lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
>(HLT0 … HTX0) in HX0; -L0 -X0 #H
inductive cpr: relation4 genv lenv term term ≝
| cpr_atom : ∀I,G,L. cpr G L (⓪{I}) (⓪{I})
| cpr_delta: ∀G,L,K,V,V2,W2,i.
- ⇩[0, i] L ≡ K. ⓓV → cpr G K V V2 →
+ ⇩[i] L ≡ K. ⓓV → cpr G K V V2 →
⇧[0, i + 1] V2 ≡ W2 → cpr G L (#i) W2
| cpr_bind : ∀a,I,G,L,V1,V2,T1,T2.
cpr G L V1 V2 → cpr G (L.ⓑ{I}V1) T1 T2 →
#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2
[ //
| #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 * /3 width=6/
-|3,7: /4 width=1/
-|4,6: /3 width=1/
-|5,8: /4 width=3/
+ elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 *
+ /3 width=6 by cpr_delta/
+|3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/
+|4,6: /3 width=1 by cpr_flat, cpr_tau/
+|5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/
]
qed-.
(* Basic_1: includes by definition: pr0_refl *)
lemma cpr_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ➡ T.
-#G #T elim T -T // * /2 width=1/
+#G #T elim T -T // * /2 width=1 by cpr_bind, cpr_flat/
qed.
(* Basic_1: was: pr2_head_1 *)
lemma cpr_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 →
∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡ ②{I}V2.T.
-* /2 width=1/ qed.
+* /2 width=1 by cpr_bind, cpr_flat/ qed.
-lemma cpr_delift: ∀G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓓV) →
+lemma cpr_delift: ∀G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓓV) →
∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⇧[d, 1] T ≡ T2.
#G #K #V #T1 elim T1 -T1
-[ * #i #L #d #HLK /2 width=4/
- elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4/ ]
+[ * /2 width=4 by cpr_atom, lift_sort, lift_gref, ex2_2_intro/
+ #i #L #d #HLK elim (lt_or_eq_or_gt i d)
+ #Hid [1,3: /3 width=4 by cpr_atom, lift_lref_ge_minus, lift_lref_lt, ex2_2_intro/ ]
destruct
elim (lift_total V 0 (i+1)) #W #HVW
- elim (lift_split … HVW i i) // /3 width=6/
+ elim (lift_split … HVW i i) /3 width=6 by cpr_delta, ex2_2_intro/
| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /2 width=1/ -HLK /3 width=9/
- | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
+ [ elim (IHU1 (L. ⓑ{I}W1) (d+1)) -IHU1 /3 width=9 by ldrop_drop, cpr_bind, lift_bind, ex2_2_intro/
+ | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpr_flat, lift_flat, ex2_2_intro/
]
]
qed-.
lemma cpr_append: ∀G. l_appendable_sn … (cpr G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2 // /2 width=1/ /2 width=3/
+#G #K #T1 #T2 #H elim H -G -K -T1 -T2
+/2 width=3 by cpr_bind, cpr_flat, cpr_zeta, cpr_tau, cpr_beta, cpr_theta/
#G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
lapply (ldrop_fwd_length_lt2 … HK0) #H
@(cpr_delta … (L@@K0) V1 … HVW2) //
-@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
+@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
qed.
(* Basic inversion lemmas ***************************************************)
fact cpr_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀I. T1 = ⓪{I} →
T2 = ⓪{I} ∨
- ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
+ ∃∃K,V,V2,i. ⇩[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
⇧[O, i + 1] V2 ≡ T2 & I = LRef i.
#G #L #T1 #T2 * -G -L -T1 -T2
-[ #I #G #L #J #H destruct /2 width=1/
-| #L #G #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8/
+[ #I #G #L #J #H destruct /2 width=1 by or_introl/
+| #L #G #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8 by ex4_4_intro, or_intror/
| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
| #G #L #V #T1 #T #T2 #_ #_ #J #H destruct
lemma cpr_inv_atom1: ∀I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡ T2 →
T2 = ⓪{I} ∨
- ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
+ ∃∃K,V,V2,i. ⇩[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
⇧[O, i + 1] V2 ≡ T2 & I = LRef i.
/2 width=3 by cpr_inv_atom1_aux/ qed-.
(* Basic_1: includes: pr0_gen_lref pr2_gen_lref *)
lemma cpr_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡ T2 →
T2 = #i ∨
- ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
+ ∃∃K,V,V2. ⇩[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 &
⇧[O, i + 1] V2 ≡ T2.
#G #L #T2 #i #H
-elim (cpr_inv_atom1 … H) -H /2 width=1/
-* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6/
+elim (cpr_inv_atom1 … H) -H /2 width=1 by or_introl/
+* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6 by ex3_3_intro, or_intror/
qed-.
lemma cpr_inv_gref1: ∀G,L,T2,p. ⦃G, L⦄ ⊢ §p ➡ T2 → T2 = §p.
#G #L #U1 #U2 * -L -U1 -U2
[ #I #G #L #b #J #W1 #U1 #H destruct
| #L #G #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct
-| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /3 width=5/
+| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /3 width=5 by ex3_2_intro, or_introl/
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct
-| #G #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W #U1 #H destruct /3 width=3/
+| #G #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W #U1 #H destruct /3 width=3 by ex4_intro, or_intror/
| #G #L #V #T1 #T2 #_ #b #J #W #U1 #H destruct
| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #b #J #W #U1 #H destruct
| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W #U1 #H destruct
) ∨
∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true.
#a #G #L #V1 #T1 #U2 #H
-elim (cpr_inv_bind1 … H) -H * /3 width=3/ /3 width=5/
+elim (cpr_inv_bind1 … H) -H *
+/3 width=5 by ex3_2_intro, ex3_intro, or_introl, or_intror/
qed-.
(* Basic_1: includes: pr0_gen_abst pr2_gen_abst *)
U2 = ⓛ{a}V2.T2.
#a #G #L #V1 #T1 #U2 #H
elim (cpr_inv_bind1 … H) -H *
-[ /3 width=5/
+[ /3 width=5 by ex3_2_intro/
| #T #_ #_ #_ #H destruct
]
qed-.
[ #I #G #L #J #W1 #U1 #H destruct
| #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct
| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
-| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=5/
+| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=5 by or4_intro0, ex3_2_intro/
| #G #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct
-| #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=1/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11/
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13/
+| #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=1 by or4_intro1, conj/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11 by or4_intro2, ex6_6_intro/
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13 by or4_intro3, ex7_7_intro/
]
qed-.
⦃G, L⦄ ⊢ W1 ➡ W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡ T2 &
U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2.ⓐV2.T2.
#G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H *
-[ /3 width=5/
+[ /3 width=5 by or3_intro0, ex3_2_intro/
| #_ #H destruct
-| /3 width=11/
-| /3 width=13/
+| /3 width=11 by or3_intro1, ex5_6_intro/
+| /3 width=13 by or3_intro2, ex6_7_intro/
]
qed-.
U2 = ⓝ V2. T2
) ∨ ⦃G, L⦄ ⊢ U1 ➡ U2.
#G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H *
-[ /3 width=5/
-| /2 width=1/
+[ /3 width=5 by ex3_2_intro, or_introl/
+| /2 width=1 by or_intror/
| #a #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #H destruct
| #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct
]
T = -ⓑ{I}V2.T2.
#I #G #L #V1 #T1 #T #H #b
elim (cpr_inv_bind1 … H) -H *
-[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpr_bind, ex2_2_intro/
| #T2 #_ #_ #H destruct
]
qed-.
[ #V0 #T0 #_ #HT10 #H destruct
elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
>append_length >HL12 -HL12
- @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
+ @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
| #T #_ #_ #H destruct
]
]
(* Basic_1: includes: pr0_lift pr2_lift *)
lemma cpr_lift: ∀G. l_liftable (cpr G).
#G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2
+[ #I #G #K #L #s #d #e #_ #U1 #H1 #U2 #H2
>(lift_mono … H1 … H2) -H1 -H2 //
-| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hid #H destruct
[ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
- elim (ldrop_trans_le … HLK … HKV) -K /2 width=2/ #X #HLK #H
- elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K #Y #HKV #HVY #H destruct /3 width=8/
- | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 // /2 width=1/ >plus_plus_comm_23 #HVU2
- lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/
+ elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
+ elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid
+ #K #Y #HKV #HVY #H destruct /3 width=9 by cpr_delta/
+ | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
+ lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6 by cpr_delta, ldrop_inv_gen/
]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
- elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpr_bind, ldrop_skip/
+| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
- elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
-| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2
+ elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpr_flat/
+| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #H #U2 #HTU2
elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
- elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/
-| #G #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
- elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/
-| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+ elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpr_zeta, ldrop_skip/
+| #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2
+ elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpr_tau/
+| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct
- elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5/
-| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpr_beta, ldrop_skip/
+| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
- elim (lift_trans_ge … HV2 … HV3) -V2 // /4 width=5/
+ elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpr_theta, ldrop_skip/
]
qed.
(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
lemma cpr_inv_lift1: ∀G. l_deliftable_sn (cpr G).
#G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #d #e #_ #T1 #H
- [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
- | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
- | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
+[ * #G #L #i #K #s #d #e #_ #T1 #H
+ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by ex2_intro/
+ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by lift_lref_ge_minus, lift_lref_lt, ex2_intro/
+ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by ex2_intro/
]
-| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
[ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
- elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m // -Hid /3 width=8/
+ elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m /3 width=8 by cpr_delta, ex2_intro/
| elim (le_inv_plus_l … Hid) #Hdie #Hei
lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
- elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
- #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O /3 width=8/
+ elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [2,3,4: /2 width=1 by le_S_S, le_S/ ] -Hid -Hdie
+ #V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O
+ /3 width=8 by cpr_delta, ex2_intro/
]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
- elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+ elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpr_bind, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHV12 … HLK … HWV1) -V1
- elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5/
-| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #X #H
+ elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=6 by cpr_flat, lift_flat, ex2_intro/
+| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #X #H
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHU1 (K.ⓓW1) … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
- elim (lift_div_le … HU2 … HTU) -U // /3 width=5/
-| #G #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
+ elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1 by ldrop_skip/ -L -U1 #T #HTU #HT1
+ elim (lift_div_le … HU2 … HTU) -U /3 width=6 by cpr_zeta, ex2_intro/
+| #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+ elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpr_tau, ex2_intro/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
- elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
- elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
- elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
- @ex2_intro [2: /3 width=2/ | skip |3: /2 width=1/ ] (**) (* /4 width=6/ is slow *)
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+ elim (IHV12 … HLK … HV01) -V1
+ elim (IHT12 (K.ⓛW0) s … HT01) -T1 /2 width=1 by ldrop_skip/
+ elim (IHW12 … HLK … HW01) -W1 /4 width=7 by cpr_beta, lift_flat, lift_bind, ex2_intro/
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
- elim (IHT12 (K.ⓓW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
- elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
- elim (lift_trans_le … HV3 … HV2) -V // #V #HV3 #HV2
- @ex2_intro [2: /3 width=2/ | skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
+ elim (IHT12 (K.ⓓW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+ elim (IHW12 … HLK … HW01) -W1
+ elim (lift_trans_le … HV3 … HV2) -V
+ /4 width=9 by cpr_theta, lift_flat, lift_bind, ex2_intro/
]
qed-.
| cpx_atom : ∀I,G,L. cpx h g G L (⓪{I}) (⓪{I})
| cpx_sort : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
| cpx_delta: ∀I,G,L,K,V,V2,W2,i.
- ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
- ⇧[0, i + 1] V2 ≡ W2 → cpx h g G L (#i) W2
+ ⇩[i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
+ ⇧[0, i+1] V2 ≡ W2 → cpx h g G L (#i) W2
| cpx_bind : ∀a,I,G,L,V1,V2,T1,T2.
cpx h g G L V1 V2 → cpx h g G (L.ⓑ{I}V1) T1 T2 →
cpx h g G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
[ //
| /2 width=2 by cpx_sort/
| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubr_fwd_drop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+ elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
/4 width=7 by cpx_delta, cpx_ti/
|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/
|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
#h #g * /2 width=1 by cpx_bind, cpx_flat/
qed.
-lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
+lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓑ{I}V) →
∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & ⇧[d, 1] T ≡ T2.
#h #g #I #G #K #V #T1 elim T1 -T1
[ * #i #L #d /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/
fact cpx_inv_atom1_aux: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ∀J. T1 = ⓪{J} →
∨∨ T2 = ⓪{J}
| ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
- | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
- ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+ | ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+ ⇧[O, i+1] V2 ≡ T2 & J = LRef i.
#G #h #g #L #T1 #T2 * -L -T1 -T2
[ #I #G #L #J #H destruct /2 width=1 by or3_intro0/
| #G #L #k #l #Hkl #J #H destruct /3 width=5 by or3_intro1, ex3_2_intro/
lemma cpx_inv_atom1: ∀h,g,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h, g] T2 →
∨∨ T2 = ⓪{J}
| ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
- | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
- ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+ | ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+ ⇧[O, i+1] V2 ≡ T2 & J = LRef i.
/2 width=3 by cpx_inv_atom1_aux/ qed-.
lemma cpx_inv_sort1: ∀h,g,G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ➡[h, g] T2 → T2 = ⋆k ∨
lemma cpx_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, g] T2 →
T2 = #i ∨
- ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
- ⇧[O, i + 1] V2 ≡ T2.
+ ∃∃I,K,V,V2. ⇩[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+ ⇧[O, i+1] V2 ≡ T2.
#h #g #G #L #T2 #i #H
elim (cpx_inv_atom1 … H) -H /2 width=1 by or_introl/ *
[ #k #l #_ #_ #H destruct
--- /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/substitution/cpys_alt.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Properties on context-sensitive extended multiple substitution for terms *)
+
+lemma cpys_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T2 #d #e #H @(cpys_ind_alt … H) -G -L -T1 -T2 -d -e
+/2 width=7 by cpx_delta, cpx_bind, cpx_flat/
+qed.
+
+lemma cpy_cpx: ∀h,g,G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+/3 width=3 by cpy_cpys, cpys_cpx/ qed.
lemma cpx_lift: ∀h,g,G. l_liftable (cpx h g G).
#h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2
-[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2
+[ #I #G #K #L #s #d #e #_ #U1 #H1 #U2 #H2
>(lift_mono … H1 … H2) -H1 -H2 //
-| #G #K #k #l #Hkl #L #d #e #_ #U1 #H1 #U2 #H2
+| #G #K #k #l #Hkl #L #s #d #e #_ #U1 #H1 #U2 #H2
>(lift_inv_sort1 … H1) -U1
>(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_sort/
-| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #s #d #e #HLK #U1 #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hid #H destruct
[ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
elim (ldrop_trans_le … HLK … HKV) -K /2 width=2 by lt_to_le/ #X #HLK #H
- elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9 by cpx_delta/
+ elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid
+ #K #Y #HKV #HVY #H destruct /3 width=10 by cpx_delta/
| lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by le_S/ >plus_plus_comm_23 #HVU2
- lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta/
+ lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta, ldrop_inv_gen/
]
-| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
- elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5 by cpx_bind, ldrop_skip/
-| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=6 by cpx_bind, ldrop_skip/
+| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #s #d #e #HLK #U1 #H1 #U2 #H2
elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6 by cpx_flat/
-| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2
+| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #s #d #e #HLK #U1 #H #U2 #HTU2
elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
- elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5 by cpx_zeta, ldrop_skip/
-| #G #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
- elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5 by cpx_tau/
-| #G #K #V1 #V2 #T #_ #IHV12 #L #d #e #HLK #U1 #H #U2 #HVU2
- elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5 by cpx_ti/
-| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+ elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=6 by cpx_zeta, ldrop_skip/
+| #G #K #V #T1 #T2 #_ #IHT12 #L #s #d #e #HLK #U1 #H #U2 #HTU2
+ elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_tau/
+| #G #K #V1 #V2 #T #_ #IHV12 #L #s #d #e #HLK #U1 #H #U2 #HVU2
+ elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_ti/
+| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct
- elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5 by cpx_beta, ldrop_skip/
-| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=6 by cpx_beta, ldrop_skip/
+| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #s #d #e #HLK #X1 #HX1 #X2 #HX2
elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct
elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct
- elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=5 by cpx_theta, ldrop_skip/
+ elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpx_theta, ldrop_skip/
]
qed.
lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G).
#h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2
-[ * #G #L #i #K #d #e #_ #T1 #H
+[ * #G #L #i #K #s #d #e #_ #T1 #H
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_sort, ex2_intro/
| elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/
]
-| #G #L #k #l #Hkl #K #d #e #_ #T1 #H
+| #G #L #k #l #Hkl #K #s #d #e #_ #T1 #H
lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_sort, lift_sort, ex2_intro/
-| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #s #d #e #HLK #T1 #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
[ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
elim (lift_split … HVW2 d (i - e + 1)) -HVW2 /3 width=1 by le_S, le_S_S/ -Hid -Hdie
#V1 #HV1 >plus_minus // <minus_minus /2 width=1 by le_S/ <minus_n_n <plus_n_O /3 width=9 by cpx_delta, ex2_intro/
]
-| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+| #a #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
- elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5 by cpx_bind, ldrop_skip, lift_bind, ex2_intro/
-| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+ elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=6 by cpx_bind, ldrop_skip, lift_bind, ex2_intro/
+| #I #G #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHV12 … HLK … HWV1) -V1
elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
-| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #X #H
+| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #d #e #HLK #X #H
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHU1 (K.ⓓW1) … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+ elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
-| #G #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
+| #G #L #V #U1 #U2 #_ #IHU12 #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3 by cpx_tau, ex2_intro/
-| #G #L #V1 #V2 #U1 #_ #IHV12 #K #d #e #HLK #X #H
+| #G #L #V1 #V2 #U1 #_ #IHV12 #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
elim (IHV12 … HLK … HWV1) -L -V1 /3 width=3 by cpx_ti, ex2_intro/
-| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
elim (IHV12 … HLK … HV01) -V1 #V3 #HV32 #HV03
- elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+ elim (IHT12 (K.ⓛW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
elim (IHW12 … HLK … HW01) -W1
/4 width=7 by cpx_beta, lift_bind, lift_flat, ex2_intro/
-| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #s #d #e #HLK #X #HX
elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
- elim (IHT12 (K.ⓓW0) … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
+ elim (IHT12 (K.ⓓW0) s … HT01) -T1 /2 width=1 by ldrop_skip/ #T3 #HT32 #HT03
elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
elim (lift_trans_le … HV3 … HV2) -V
/4 width=9 by cpx_theta, lift_bind, lift_flat, ex2_intro/
]
| #G #L #K #T1 #U1 #e #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (e+1))
#U2 #HTU2 @(ex3_intro … U2)
- [1,3: /2 width=9 by cpx_lift, fqu_drop/
+ [1,3: /2 width=10 by cpx_lift, fqu_drop/
| #H0 destruct /3 width=5 by lift_inj/
]
qed-.
(* activate genv *)
(* reducible terms *)
inductive crr (G:genv): relation2 lenv term ≝
-| crr_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crr G L (#i)
+| crr_delta : ∀L,K,V,i. ⇩[i] L ≡ K.ⓓV → crr G L (#i)
| crr_appl_sn: ∀L,V,T. crr G L V → crr G L (ⓐV.T)
| crr_appl_dx: ∀L,V,T. crr G L T → crr G L (ⓐV.T)
| crr_ri2 : ∀I,L,V,T. ri2 I → crr G L (②{I}V.T)
/2 width=6 by crr_inv_sort_aux/ qed-.
fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = #i →
- ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+ ∃∃K,V. ⇩[i] L ≡ K.ⓓV.
#G #L #T #j * -L -T
-[ #L #K #V #i #HLK #H destruct /2 width=3/
+[ #L #K #V #i #HLK #H destruct /2 width=3 by ex1_2_intro/
| #L #V #T #_ #H destruct
| #L #V #T #_ #H destruct
| #I #L #V #T #_ #H destruct
]
qed-.
-lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[0, i] L ≡ K.ⓓV.
+lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[i] L ≡ K.ⓓV.
/2 width=4 by crr_inv_lref_aux/ qed-.
fact crr_inv_gref_aux: ∀G,L,T,p. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = §p → ⊥.
| #I #L #V #T #H1 #H2 destruct
elim H1 -H1 #H destruct
elim HI -HI #H destruct
-| #a #I #L #V #T #_ #HV #H destruct /2 width=1/
-| #a #I #L #V #T #_ #HT #H destruct /2 width=1/
+| #a #I #L #V #T #_ #HV #H destruct /2 width=1 by or_introl/
+| #a #I #L #V #T #_ #HT #H destruct /2 width=1 by or_intror/
| #a #L #V #W #T #H destruct
| #a #L #V #W #T #H destruct
]
∨∨ ⦃G, L⦄ ⊢ 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
#G #L #W0 #U #T * -L -T
[ #L #K #V #i #_ #H destruct
-| #L #V #T #HV #H destruct /2 width=1/
-| #L #V #T #HT #H destruct /2 width=1/
+| #L #V #T #HV #H destruct /2 width=1 by or3_intro0/
+| #L #V #T #HT #H destruct /2 width=1 by or3_intro1/
| #I #L #V #T #H1 #H2 destruct
elim H1 -H1 #H destruct
| #a #I #L #V #T #_ #_ #H destruct
(* Properties on relocation *************************************************)
-lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑⦃U⦄.
#G #K #T #H elim H -K -T
-[ #K #K0 #V #i #HK0 #L #d #e #HLK #X #H
+[ #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H
elim (lift_inv_lref1 … H) -H * #Hid #H destruct
- [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/
- | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // /2 width=4/
+ [ elim (ldrop_trans_lt … HLK … HK0) -K /2 width=4 by crr_delta/
+ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K /3 width=4 by crr_delta, ldrop_inv_gen/
]
-| #K #V #T #_ #IHV #L #d #e #HLK #X #H
- elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #K #V #T #_ #IHT #L #d #e #HLK #X #H
- elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=4/
-| #I #K #V #T #HI #L #d #e #_ #X #H
- elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1/
-| #a #I #K #V #T #HI #_ #IHV #L #d #e #HLK #X #H
- elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #a #I #K #V #T #HI #_ #IHT #L #d #e #HLK #X #H
- elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+| #K #V #T #_ #IHV #L #s #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crr_appl_sn/
+| #K #V #T #_ #IHT #L #s #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=5 by crr_appl_dx/
+| #I #K #V #T #HI #L #s #d #e #_ #X #H
+ elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1 by crr_ri2/
+| #a #I #K #V #T #HI #_ #IHV #L #s #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crr_ib2_sn/
+| #a #I #K #V #T #HI #_ #IHT #L #s #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=5 by crr_ib2_dx, ldrop_skip/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
- elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crr_beta/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
- elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crr_theta/
]
qed.
-lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑⦃T⦄.
#G #L #U #H elim H -L -U
-[ #L #L0 #W #i #HK0 #K #d #e #HLK #X #H
+[ #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
- [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/
- | lapply (ldrop_conf_ge … HLK … HK0 ?) -L // /2 width=4/
+ [ elim (ldrop_conf_lt … HLK … HK0) -L /2 width=4 by crr_delta/
+ | lapply (ldrop_conf_ge … HLK … HK0 ?) -L /2 width=4 by crr_delta/
]
-| #L #W #U #_ #IHW #K #d #e #HLK #X #H
- elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #L #W #U #_ #IHU #K #d #e #HLK #X #H
- elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=4/
-| #I #L #W #U #HI #K #d #e #_ #X #H
- elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1/
-| #a #I #L #W #U #HI #_ #IHW #K #d #e #HLK #X #H
- elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #a #I #L #W #U #HI #_ #IHU #K #d #e #HLK #X #H
- elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+| #L #W #U #_ #IHW #K #s #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crr_appl_sn/
+| #L #W #U #_ #IHU #K #s #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=5 by crr_appl_dx/
+| #I #L #W #U #HI #K #s #d #e #_ #X #H
+ elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1 by crr_ri2/
+| #a #I #L #W #U #HI #_ #IHW #K #s #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crr_ib2_sn/
+| #a #I #L #W #U #HI #_ #IHU #K #s #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=5 by crr_ib2_dx, ldrop_skip/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
- elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crr_beta/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
- elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crr_theta/
]
qed-.
(* extended reducible terms *)
inductive crx (h) (g) (G:genv): relation2 lenv term ≝
| crx_sort : ∀L,k,l. deg h g k (l+1) → crx h g G L (⋆k)
-| crx_delta : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g G L (#i)
+| crx_delta : ∀I,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → crx h g G L (#i)
| crx_appl_sn: ∀L,V,T. crx h g G L V → crx h g G L (ⓐV.T)
| crx_appl_dx: ∀L,V,T. crx h g G L T → crx h g G L (ⓐV.T)
| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g G L (②{I}V.T)
(* Basic properties *********************************************************)
lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄.
-#h #g #G #L #T #H elim H -L -T // /2 width=1/ /2 width=4/
+#h #g #G #L #T #H elim H -L -T
+/2 width=4 by crx_delta, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
qed.
(* Basic inversion lemmas ***************************************************)
fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⋆k →
∃l. deg h g k (l+1).
#h #g #G #L #T #k0 * -L -T
-[ #L #k #l #Hkl #H destruct /2 width=2/
+[ #L #k #l #Hkl #H destruct /2 width=2 by ex_intro/
| #I #L #K #V #i #HLK #H destruct
| #L #V #T #_ #H destruct
| #L #V #T #_ #H destruct
/2 width=5 by crx_inv_sort_aux/ qed-.
fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i →
- ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+ ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V.
#h #g #G #L #T #j * -L -T
[ #L #k #l #_ #H destruct
-| #I #L #K #V #i #HLK #H destruct /2 width=4/
+| #I #L #K #V #i #HLK #H destruct /2 width=4 by ex1_3_intro/
| #L #V #T #_ #H destruct
| #L #V #T #_ #H destruct
| #I #L #V #T #_ #H destruct
]
qed-.
-lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V.
/2 width=6 by crx_inv_lref_aux/ qed-.
fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = §p → ⊥.
lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ →
∃∃k,l. deg h g k (l+1) & I = Sort k.
#h #g * #i #G #H
-[ elim (crx_inv_sort … H) -H /2 width=4/
+[ elim (crx_inv_sort … H) -H /2 width=4 by ex2_2_intro/
| elim (crx_inv_lref … H) -H #I #L #V #H
elim (ldrop_inv_atom1 … H) -H #H destruct
| elim (crx_inv_gref … H)
| #I #L #V #T #H1 #H2 destruct
elim H1 -H1 #H destruct
elim HI -HI #H destruct
-| #a #I #L #V #T #_ #HV #H destruct /2 width=1/
-| #a #I #L #V #T #_ #HT #H destruct /2 width=1/
+| #a #I #L #V #T #_ #HV #H destruct /2 width=1 by or_introl/
+| #a #I #L #V #T #_ #HT #H destruct /2 width=1 by or_intror/
| #a #L #V #W #T #H destruct
| #a #L #V #W #T #H destruct
]
#h #g #G #L #W0 #U #T * -L -T
[ #L #k #l #_ #H destruct
| #I #L #K #V #i #_ #H destruct
-| #L #V #T #HV #H destruct /2 width=1/
-| #L #V #T #HT #H destruct /2 width=1/
+| #L #V #T #HV #H destruct /2 width=1 by or3_intro0/
+| #L #V #T #HT #H destruct /2 width=1 by or3_intro1/
| #I #L #V #T #H1 #H2 destruct
elim H1 -H1 #H destruct
| #a #I #L #V #T #_ #_ #H destruct
(* Properties on relocation *************************************************)
-lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K →
+lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄.
#h #g #G #K #T #H elim H -K -T
-[ #K #k #l #Hkl #L #d #e #_ #X #H
- >(lift_inv_sort1 … H) -X /2 width=2/
-| #I #K #K0 #V #i #HK0 #L #d #e #HLK #X #H
+[ #K #k #l #Hkl #L #s #d #e #_ #X #H
+ >(lift_inv_sort1 … H) -X /2 width=2 by crx_sort/
+| #I #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H
elim (lift_inv_lref1 … H) -H * #Hid #H destruct
- [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/
- | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // /2 width=4/
+ [ elim (ldrop_trans_lt … HLK … HK0) -K /2 width=4 by crx_delta/
+ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K /3 width=5 by crx_delta, ldrop_inv_gen/
]
-| #K #V #T #_ #IHV #L #d #e #HLK #X #H
- elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #K #V #T #_ #IHT #L #d #e #HLK #X #H
- elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=4/
-| #I #K #V #T #HI #L #d #e #_ #X #H
- elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1/
-| #a #I #K #V #T #HI #_ #IHV #L #d #e #HLK #X #H
- elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=4/
-| #a #I #K #V #T #HI #_ #IHT #L #d #e #HLK #X #H
- elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+| #K #V #T #_ #IHV #L #s #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crx_appl_sn/
+| #K #V #T #_ #IHT #L #s #d #e #HLK #X #H
+ elim (lift_inv_flat1 … H) -H #W #U #_ #HTU #H destruct /3 width=5 by crx_appl_dx/
+| #I #K #V #T #HI #L #s #d #e #_ #X #H
+ elim (lift_fwd_pair1 … H) -H #W #U #_ #H destruct /2 width=1 by crx_ri2/
+| #a #I #K #V #T #HI #_ #IHV #L #s #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #_ #H destruct /3 width=5 by crx_ib2_sn/
+| #a #I #K #V #T #HI #_ #IHT #L #s #d #e #HLK #X #H
+ elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=5 by crx_ib2_dx, ldrop_skip/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
- elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
-| #a #K #V #V0 #T #L #d #e #_ #X #H
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crx_beta/
+| #a #K #V #V0 #T #L #s #d #e #_ #X #H
elim (lift_inv_flat1 … H) -H #W #X0 #_ #H0 #H destruct
- elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1/
+ elim (lift_inv_bind1 … H0) -H0 #W0 #U #_ #_ #H0 destruct /2 width=1 by crx_theta/
]
qed.
-lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K →
+lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄.
#h #g #G #L #U #H elim H -L -U
-[ #L #k #l #Hkl #K #d #e #_ #X #H
- >(lift_inv_sort2 … H) -X /2 width=2/
-| #I #L #L0 #W #i #HK0 #K #d #e #HLK #X #H
+[ #L #k #l #Hkl #K #s #d #e #_ #X #H
+ >(lift_inv_sort2 … H) -X /2 width=2 by crx_sort/
+| #I #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
- [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/
- | lapply (ldrop_conf_ge … HLK … HK0 ?) -L // /2 width=4/
+ [ elim (ldrop_conf_lt … HLK … HK0) -L /2 width=4 by crx_delta/
+ | lapply (ldrop_conf_ge … HLK … HK0 ?) -L /2 width=4 by crx_delta/
]
-| #L #W #U #_ #IHW #K #d #e #HLK #X #H
- elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #L #W #U #_ #IHU #K #d #e #HLK #X #H
- elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=4/
-| #I #L #W #U #HI #K #d #e #_ #X #H
- elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1/
-| #a #I #L #W #U #HI #_ #IHW #K #d #e #HLK #X #H
- elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=4/
-| #a #I #L #W #U #HI #_ #IHU #K #d #e #HLK #X #H
- elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+| #L #W #U #_ #IHW #K #s #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crx_appl_sn/
+| #L #W #U #_ #IHU #K #s #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #V #T #_ #HTU #H destruct /3 width=5 by crx_appl_dx/
+| #I #L #W #U #HI #K #s #d #e #_ #X #H
+ elim (lift_fwd_pair2 … H) -H #V #T #_ #H destruct /2 width=1 by crx_ri2/
+| #a #I #L #W #U #HI #_ #IHW #K #s #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #_ #H destruct /3 width=5 by crx_ib2_sn/
+| #a #I #L #W #U #HI #_ #IHU #K #s #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=5 by crx_ib2_dx, ldrop_skip/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
- elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
-| #a #L #W #W0 #U #K #d #e #_ #X #H
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crx_beta/
+| #a #L #W #W0 #U #K #s #d #e #_ #X #H
elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct
- elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/
+ elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1 by crx_theta/
]
-qed.
+qed-.
(* Basic_1: includes: wcpr0_drop *)
lemma lpr_ldrop_conf: ∀G. dropable_sn (lpr G).
-/3 width=5 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-.
+/3 width=6 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-.
(* Basic_1: includes: wcpr0_drop_back *)
lemma ldrop_lpr_trans: ∀G. dedropable_sn (lpr G).
-/3 width=9 by lpx_sn_liftable_dedropable, cpr_lift/ qed-.
+/3 width=10 by lpx_sn_liftable_dedropable, cpr_lift/ qed-.
lemma lpr_ldrop_trans_O1: ∀G. dropable_dx (lpr G).
/2 width=3 by lpx_sn_dropable/ qed-.
∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
) →
- ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+ ∀K0,V0. ⇩[i] L0 ≡ K0.ⓓV0 →
∀V2. ⦃G, K0⦄ ⊢ V0 ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
∃∃T. ⦃G, L1⦄ ⊢ #i ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T.
lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
elim (lift_total V 0 (i+1))
-/3 width=11 by cpr_lift, cpr_delta, ex2_intro/
+/3 width=12 by cpr_lift, cpr_delta, ex2_intro/
qed-.
(* Basic_1: includes: pr0_delta_delta pr2_delta_delta *)
∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
) →
- ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+ ∀K0,V0. ⇩[i] L0 ≡ K0.ⓓV0 →
∀V1. ⦃G, K0⦄ ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 →
- ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX →
+ ∀KX,VX. ⇩[i] L0 ≡ KX.ⓓVX →
∀V2. ⦃G, KX⦄ ⊢ VX ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T.
lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2
lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (lift_total V 0 (i+1)) /3 width=11 by cpr_lift, ex2_intro/
+elim (lift_total V 0 (i+1)) /3 width=12 by cpr_lift, ex2_intro/
qed-.
fact cpr_conf_lpr_bind_bind:
#G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2
-elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1 by ldrop_drop/ #T1 #HT1 #HXT1
-elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1 by ldrop_drop/ #T2 #HT2 #HXT2
+elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=2 by ldrop_drop/ #T1 #HT1 #HXT1
+elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=2 by ldrop_drop/ #T2 #HT2 #HXT2
lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/
qed-.
#V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/ #HU2
+lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_drop/ #HU2
elim (cpr_inv_abbr1 … H) -H *
[ #W1 #T1 #HW01 #HT01 #H destruct
elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/
elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/
elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0
elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1 by ldrop_drop/
-lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/
+lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=2 by ldrop_drop/
+lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_drop/
/4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
qed-.
elim (cpx_inv_lref1 … H) -H
[ #H destruct
elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
- elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
+ elim (lpx_inv_pair1 … H) -H
+ #K2 #V2 #HK12 #HV12 #H destruct /3 width=6 by aaa_lref/
| * #J #Y #Z #V2 #H #HV12 #HV2
lapply (ldrop_mono … H … HLK1) -H #H destruct
elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
- lapply (ldrop_fwd_drop2 … HLK2) -V0 /3 width=7/
+ /3 width=8 by aaa_lift, ldrop_fwd_drop2/
]
| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
elim (cpx_inv_abbr1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/
| #T2 #HT12 #HT2 #H destruct -IHV1
- @(aaa_inv_lift … (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/
+ /4 width=8 by lpx_pair, aaa_inv_lift, ldrop_drop/
]
| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/
+ elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=1 by lpx_pair, aaa_abst/
| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
elim (cpx_inv_appl1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/
+ [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/
| #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
- lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
+ lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
- lapply (lsuba_aaa_trans … HU2 (L2.ⓓⓝW2.V2) ?) -HU2 /3 width=3/
+ /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/
| #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
- lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2
- lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
- elim (aaa_inv_abbr … H) -H /3 width=3/
+ lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2
+ lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
+ elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/
]
| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
elim (cpx_inv_cast1 … H) -H
- [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/
- | -IHV1 /2 width=1/
- | -IHT1 /2 width=1/
+ [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/
+ | -IHV1 /2 width=1 by/
+ | -IHT1 /2 width=1 by/
]
]
qed-.
(* Properies on local environment slicing ***********************************)
lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G).
-/3 width=5 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G).
-/3 width=9 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G).
/2 width=3 by lpx_sn_dropable/ qed-.
| cpy_subst: ∀I,G,L,K,V,W,i,d,e. d ≤ yinj i → i < d+e →
⇩[i] L ≡ K.ⓑ{I}V → ⇧[0, i+1] V ≡ W → cpy d e G L (#i) W
| cpy_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
- cpy d e G L V1 V2 → cpy (⫯d) e G (L.ⓑ{I}V2) T1 T2 →
+ cpy d e G L V1 V2 → cpy (⫯d) e G (L.ⓑ{I}V1) T1 T2 →
cpy d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
| cpy_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
cpy d e G L V1 V2 → cpy d e G L T1 T2 →
/4 width=5 by cpy_subst, ylt_inj, ex2_2_intro/
| * [ #a ] #J #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L.ⓑ{J}W2) (d+1)) -IHU1
+ [ elim (IHU1 (L.ⓑ{J}W1) (d+1)) -IHU1
/3 width=9 by cpy_bind, ldrop_drop, lift_bind, ex2_2_intro/
| elim (IHU1 … HLK) -IHU1 -HLK
/3 width=8 by cpy_flat, lift_flat, ex2_2_intro/
elim (IHV12 i) -IHV12 // #V
elim (IHT12 (i+1)) -IHT12 /2 width=1 by yle_succ/ -Hide
>yplus_SO2 >yplus_succ1 #T #HT1 #HT2
- lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V) ?) -HT1
+ lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2
/3 width=5 by lsuby_succ, ex2_intro, cpy_bind/
| #I #G #L #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hide
elim (IHV12 i) -IHV12 // elim (IHT12 i) -IHT12 // -Hide
elim (IHV12 i) -IHV12 // #V
elim (IHT12 (i+1)) -IHT12 /2 width=1 by yle_succ/ -Hide
>yplus_SO2 >yplus_succ1 #T #HT1 #HT2
- lapply (lsuby_cpy_trans … HT1 (L. ⓑ{I} V) ?) -HT1
+ lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2
/3 width=5 by lsuby_succ, ex2_intro, cpy_bind/
| #I #G #L #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hide
elim (IHV12 i) -IHV12 // elim (IHT12 i) -IHT12 // -Hide
fact cpy_inv_bind1_aux: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 →
∀a,I,V1,T1. U1 = ⓑ{a,I}V1.T1 →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 &
- ⦃G, L. ⓑ{I}V2⦄ ⊢ T1 ▶×[⫯d, e] T2 &
+ ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ▶×[⫯d, e] T2 &
U2 = ⓑ{a,I}V2.T2.
#G #L #U1 #U2 #d #e * -G -L -U1 -U2 -d -e
[ #I #G #L #d #e #b #J #W1 #U1 #H destruct
lemma cpy_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I} V1. T1 ▶×[d, e] U2 →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶×[d, e] V2 &
- ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶×[⫯d, e] T2 &
+ ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶×[⫯d, e] T2 &
U2 = ⓑ{a,I}V2.T2.
/2 width=3 by cpy_inv_bind1_aux/ qed-.
]
| #a #I #G #L #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
- lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
- elim (IHV01 … HV02) -V0 #V #HV1 #HV2
+ elim (IHV01 … HV02) -IHV01 -HV02 #V #HV1 #HV2
elim (IHT01 … HT02) -T0 #T #HT1 #HT2
- lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V) ?) -HT1 /2 width=1 by lsuby_succ/
- lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
+ lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V1) ?) -HT1 /2 width=1 by lsuby_succ/
+ lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V2) ?) -HT2
+ /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
| #I #G #L #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
elim (IHV01 … HV02) -V0
]
| #a #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
- elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
+ elim (IHV01 … HV02 H) -IHV01 -HV02 #V #HV1 #HV2
elim (IHT01 … HT02) -T0
[ -H #T #HT1 #HT2
- lapply (lsuby_cpy_trans … HT1 (L2.ⓑ{I}V) ?) -HT1 /2 width=1 by lsuby_succ/
- lapply (lsuby_cpy_trans … HT2 (L1.ⓑ{I}V) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
+ lapply (lsuby_cpy_trans … HT1 (L2.ⓑ{I}V1) ?) -HT1 /2 width=1 by lsuby_succ/
+ lapply (lsuby_cpy_trans … HT2 (L1.ⓑ{I}V2) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
| -HV1 -HV2 elim H -H /3 width=1 by yle_succ, or_introl, or_intror/
]
| #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
>yplus_inj #HVT2 <(cpy_inv_lift1_eq … HVW … HVT2) -HVT2 /2 width=5 by cpy_subst/
| #a #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
- lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V0) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
- lapply (IHT10 … HT02 He) -T0 #HT12
- lapply (lsuby_cpy_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /3 width=1 by cpy_bind, lsuby_succ/
+ lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
+ lapply (IHT10 … HT02 He) -T0 /3 width=1 by cpy_bind/
| #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1 by cpy_flat/
]
>yplus_inj #HWT2 <(cpy_inv_lift1_eq … HVW … HWT2) -HWT2 /3 width=9 by cpy_subst, ex2_intro/
| #a #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
- lapply (lsuby_cpy_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
+ lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
elim (IHV10 … HV02) -IHV10 -HV02 // #V
elim (IHT10 … HT02) -T0 /2 width=1 by yle_succ/ #T #HT1 #HT2
- lapply (lsuby_cpy_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1 by lsuby_succ/
- lapply (lsuby_cpy_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /3 width=6 by cpy_bind, lsuby_succ, ex2_intro/
+ lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /3 width=6 by cpy_bind, lsuby_succ, ex2_intro/
| #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
elim (IHV10 … HV02) -V0 //
elim (lift_trans_le … HUV … HVW) -V // >minus_plus <plus_minus_m_m // -Hid /3 width=5 by cpy_subst, ex2_intro/
| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
- elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
+ elim (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
elim (IHU12 … HTU1) -IHU12 -HTU1
/3 width=6 by cpy_bind, yle_succ, ldrop_skip, lift_bind, ex2_intro/
| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
]
| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
- elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
+ elim (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
elim (IHU12 … HTU1) -U1
/3 width=6 by cpy_bind, ldrop_skip, lift_bind, yle_succ, ex2_intro/
| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdtd #Hdedet
| #a #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
elim (lift_inv_bind2 … H) -H #V1 #T1 #HVW1 #HTU1 #H destruct
elim (yle_inv_plus_inj2 … Hdetd) #_ #Hedt
- elim (IHW12 … HLK … HVW1) -W1 // #V2 #HV12 #HVW2
+ elim (IHW12 … HLK … HVW1) -IHW12 // #V2 #HV12 #HVW2
elim (IHU12 … HTU1) -U1 [4: @ldrop_skip // |2,5: skip |3: /2 width=1 by yle_succ/ ]
>yminus_succ1_inj /3 width=5 by cpy_bind, lift_bind, ex2_intro/
| #I #G #L #W1 #W2 #U1 #U2 #dt #et #_ #_ #IHW12 #IHU12 #K #s #d #e #HLK #X #H #Hdetd
/2 width=1 by cpy_cpys/ qed.
lemma cpys_bind: ∀G,L,V1,V2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
- ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] ⓑ{a,I}V2.T2.
#G #L #V1 #V2 #d #e #HV12 @(cpys_ind … HV12) -V2
[ #I #T1 #T2 #HT12 @(cpys_ind … HT12) -T2 /3 width=5 by cpys_strap1, cpy_bind/
-| #V #V2 #_ #HV2 #IHV1 #I #T1 #T2 #HT12 #a
- lapply (lsuby_cpys_trans … HT12 (L.ⓑ{I}V) ?) -HT12
- /3 width=5 by cpys_strap1, cpy_bind, lsuby_succ/
+| /3 width=5 by cpys_strap1, cpy_bind/
]
qed.
lemma cpys_inv_bind1: ∀a,I,G,L,V1,T1,U2,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*×[d, e] U2 →
∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 &
- ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 &
+ ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 &
U2 = ⓑ{a,I}V2.T2.
#a #I #G #L #V1 #T1 #U2 #d #e #H @(cpys_ind … H) -U2
[ /2 width=5 by ex3_2_intro/
| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
elim (cpy_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
- lapply (lsuby_cpys_trans … HT1 (L.ⓑ{I}V2) ?) -HT1
+ lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V1) ?) -HT2
/3 width=5 by cpys_strap1, lsuby_succ, ex3_2_intro/
]
qed-.
⇩[i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 →
⇧[0, i+1] V2 ≡ W2 → cpysa d e G L (#i) W2
| cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
- cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V2) T1 T2 →
+ cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V1) T1 T2 →
cpysa d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
| cpysa_flat : ∀I,G,L,V1,V2,T1,T2,d,e.
cpysa d e G L V1 V2 → cpysa d e G L T1 T2 →
/3 width=7 by cpysa_subst, ylt_fwd_le_succ/
| #a #I #G #L #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
- lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1 by lsuby_succ/ #HT2
- lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
- lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
- lapply (lsuby_cpysa_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1 by lsuby_succ, cpysa_bind/
+ /5 width=5 by cpysa_bind, lsuby_cpy_trans, lsuby_succ/
| #I #G #L #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1 by cpysa_flat/
]
⇧[O, i+1] V2 ≡ W2 → R O (⫰(d+e-i)) G K V1 V2 → R d e G L (#i) W2
) →
(∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
- ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ▶*×[⫯d, e] T2 → R d e G L V1 V2 →
- R (⫯d) e G (L.ⓑ{I}V2) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+ ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*×[⫯d, e] T2 → R d e G L V1 V2 →
+ R (⫯d) e G (L.ⓑ{I}V1) T1 T2 → R d e G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
) →
(∀I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →
⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → R d e G L V1 V2 →
#a #I #L1 #L2 #V #T #d * #HL12 #IHV * #_ #IHT @conj // -HL12
#X @conj #H elim (cpys_inv_bind1 … H) -H
#W #U #HVW #HTU #H destruct
-elim (IHV W) -IHV #H1VW #H1WV
-elim (IHT U) -IHT #H1TU #H1UT
-@cpys_bind /2 width=1 by/ -HVW -H1VW -H1WV
-[ @(lsuby_cpys_trans … (L2.ⓑ{I}V))
-| @(lsuby_cpys_trans … (L1.ⓑ{I}V))
-] /4 width=5 by lsuby_cpys_trans, lsuby_succ/ (**) (* full auto too slow *)
+elim (IHV W) -IHV elim (IHT U) -IHT /3 width=1 by cpys_bind/
qed.
lemma lleq_flat: ∀I,L1,L2,V,T,d.
]
[ { "context-sensitive extended reduction" * } {
[ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_lleq" + "cpx_cix" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ]
}
]
[ { "context-sensitive extended irreducible forms" * } {
projects / helm.git / commitdiff