(* 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.
- ⦃G,K⦄ ⊢ V :[h] W → ⬆*[1] 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) →
+ (∀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 →
+ ⦃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 →
+ ⦃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 →
+ ⦃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,T,U. ⦃G,L⦄ ⊢ T :[h] U → Q G L T U → Q G L (ⓝU.T) 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] →
+ ⦃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.
+ ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h,𝟐] 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
qed-.
lemma nta_ind_ext_cnv_mixed (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.
- ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] 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) →
+ (∀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 →
+ ⦃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 →
+ ⦃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 →
+ ⦃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] →
+ ⦃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,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] →
+ ⦃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.
+ ∀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
qed-.
lemma nta_ind_ext_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.
- ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] 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) →
+ (∀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 →
+ ⦃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 →
+ ⦃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 →
+ ⦃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] →
+ ⦃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,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] →
+ ⦃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.
+ ∀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