(* Advanced eliminators *****************************************************)
lemma nta_ind_rest_cnv (h) (Q:relation4 …):
- (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+ (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
- â¦\83G,Kâ¦\84 â\8a¢ V :[h] W â\86\92 â¬\86*[1] W ≘ U →
+ â\9dªG,Kâ\9d« â\8a¢ V :[h,ð\9d\9f\90] W â\86\92 â\87§*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
) →
- (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (â\88\80G,K,W,U. â\9dªG,Kâ\9d« â\8a¢ W ![h,ð\9d\9f\90] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
(∀I,G,K,W,U,i.
- â¦\83G,Kâ¦\84 â\8a¢ #i :[h] W â\86\92 â¬\86*[1] W ≘ U →
- Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
+ â\9dªG,Kâ\9d« â\8a¢ #i :[h,ð\9d\9f\90] W â\86\92 â\87§*[1] W ≘ U →
+ Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
) →
(∀p,I,G,K,V,T,U.
- â¦\83G,Kâ¦\84 â\8a¢ V ![h] â\86\92 â¦\83G,K.â\93\91{I}Vâ¦\84 â\8a¢ T :[h] U →
- Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
+ â\9dªG,Kâ\9d« â\8a¢ V ![h,ð\9d\9f\90] â\86\92 â\9dªG,K.â\93\91[I]Vâ\9d« â\8a¢ T :[h,ð\9d\9f\90] U →
+ Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
) →
(∀p,G,L,V,W,T,U.
- â¦\83G,Lâ¦\84 â\8a¢ V :[h] W â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T :[h] â\93\9b{p}W.U →
- Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U)
+ â\9dªG,Lâ\9d« â\8a¢ V :[h,ð\9d\9f\90] W â\86\92 â\9dªG,Lâ\9d« â\8a¢ T :[h,ð\9d\9f\90] â\93\9b[p]W.U →
+ Q G L V W → Q G L T (ⓛ[p]W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
) →
- (â\88\80G,L,T,U. â¦\83G,Lâ¦\84 â\8a¢ T :[h] U → Q G L T U → Q G L (ⓝU.T) U
+ (â\88\80G,L,T,U. â\9dªG,Lâ\9d« â\8a¢ T :[h,ð\9d\9f\90] U → Q G L T U → Q G L (ⓝU.T) U
) →
(∀G,L,T,U1,U2.
- â¦\83G,Lâ¦\84 â\8a¢ T :[h] U1 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ U1 â¬\8c*[h] U2 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ U2 ![h] →
+ â\9dªG,Lâ\9d« â\8a¢ T :[h,ð\9d\9f\90] U1 â\86\92 â\9dªG,Lâ\9d« â\8a¢ U1 â¬\8c*[h] U2 â\86\92 â\9dªG,Lâ\9d« â\8a¢ U2 ![h,ð\9d\9f\90] →
Q G L T U1 → Q G L T U2
) →
- â\88\80G,L,T,U. â¦\83G,Lâ¦\84 â\8a¢ T :[h] U → Q G L T U.
+ â\88\80G,L,T,U. â\9dªG,Lâ\9d« â\8a¢ T :[h,ð\9d\9f\90] U → Q G L T U.
#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #G #L #T
@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
[ #s #HG #HL #HT #X #H destruct -IH
/4 width=4 by nta_cast/
]
qed-.
+
+lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
+ (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
+ (∀G,K,V,W,U.
+ ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧*[1] W ≘ U →
+ Q G K V W → Q G (K.ⓓV) (#0) U
+ ) →
+ (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (∀I,G,K,W,U,i.
+ ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧*[1] W ≘ U →
+ Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
+ ) →
+ (∀p,I,G,K,V,T,U.
+ ❪G,K❫ ⊢ V ![h,𝛚] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝛚] U →
+ Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
+ ) →
+ (∀p,G,L,V,W,T,U.
+ ❪G,L❫ ⊢ V :[h,𝛚] W → ❪G,L❫ ⊢ T :[h,𝛚] ⓛ[p]W.U →
+ Q G L V W → Q G L T (ⓛ[p]W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ[p]W.U)
+ ) →
+ (∀G,L,V,T,U.
+ ❪G,L❫ ⊢ T :[h,𝛚] U → ❪G,L❫ ⊢ ⓐV.U ![h,𝛚] →
+ Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
+ ) →
+ (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
+ ) →
+ (∀G,L,T,U1,U2.
+ ❪G,L❫ ⊢ T :[h,𝛚] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝛚] →
+ Q G L T U1 → Q G L T U2
+ ) →
+ ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T
+@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
+[ #s #HG #HL #HT #X #H destruct -IH
+ elim (nta_inv_sort_sn … H) -H #HUX #HX
+ /2 width=4 by/
+| * [| #i ] #HG #HL #HT #X #H destruct
+ [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
+ [ #K #V #W #U #H #HVW #HWU #HUX #HX
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
+ | #K #W #U #H #HW #HWU #HUX #HX
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /3 width=4 by nta_ldec_cnv/
+ ]
+ | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
+ /5 width=7 by nta_lref, fqu_fqup/
+ ]
+| #l #HG #HL #HT #U #H destruct -IH
+ elim (nta_inv_gref_sn … H)
+| #p #I #V #T #HG #HL #HT #X #H destruct
+ elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
+ /4 width=5 by nta_bind_cnv/
+| #V #T #HG #HL #HT #X #H destruct
+ elim (nta_inv_pure_sn_cnv … H) -H *
+ [ #p #W #U #HVW #HTU #HUX #HX
+ /4 width=9 by nta_appl/
+ | #U #HTU #HVU #HUX #HX
+ /4 width=6 by nta_pure_cnv/
+ ]
+| #U #T #HG #HL #HT #X #H destruct
+ elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
+ /4 width=4 by nta_cast/
+]
+qed-.
+
+lemma nta_ind_ext_cnv (h) (Q:relation4 …):
+ (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
+ (∀G,K,V,W,U.
+ ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧*[1] W ≘ U →
+ Q G K V W → Q G (K.ⓓV) (#0) U
+ ) →
+ (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (∀I,G,K,W,U,i.
+ ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧*[1] W ≘ U →
+ Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
+ ) →
+ (∀p,I,G,K,V,T,U.
+ ❪G,K❫ ⊢ V ![h,𝛚] → ❪G,K.ⓑ[I]V❫ ⊢ T :[h,𝛚] U →
+ Q G (K.ⓑ[I]V) T U → Q G K (ⓑ[p,I]V.T) (ⓑ[p,I]V.U)
+ ) →
+ (∀p,G,K,V,W,T,U.
+ ❪G,K❫ ⊢ V :[h,𝛚] W → ❪G,K.ⓛW❫ ⊢ T :[h,𝛚] U →
+ Q G K V W → Q G (K.ⓛW) T U → Q G K (ⓐV.ⓛ[p]W.T) (ⓐV.ⓛ[p]W.U)
+ ) →
+ (∀G,L,V,T,U.
+ ❪G,L❫ ⊢ T :[h,𝛚] U → ❪G,L❫ ⊢ ⓐV.U ![h,𝛚] →
+ Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
+ ) →
+ (∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U → Q G L (ⓝU.T) U
+ ) →
+ (∀G,L,T,U1,U2.
+ ❪G,L❫ ⊢ T :[h,𝛚] U1 → ❪G,L❫ ⊢ U1 ⬌*[h] U2 → ❪G,L❫ ⊢ U2 ![h,𝛚] →
+ Q G L T U1 → Q G L T U2
+ ) →
+ ∀G,L,T,U. ❪G,L❫ ⊢ T :[h,𝛚] U → Q G L T U.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T #U #H
+@(nta_ind_ext_cnv_mixed … IH1 IH2 IH3 IH4 IH5 … IH7 IH8 IH9 … H) -G -L -T -U -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
+#p #G #L #V #W #T #U #HVW #HTU #_ #IHTU
+lapply (nta_fwd_cnv_dx … HTU) #H
+elim (cnv_inv_bind … H) -H #_ #HU
+elim (cnv_nta_sn … HU) -HU #X #HUX
+/4 width=2 by nta_appl_abst, nta_fwd_cnv_sn/
+qed-.