update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta_ind.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
index 4f9b52385aa9f66de95b70727bbc951118120652..74f376e7b4adfaa5bc9fcc00386cf2a536889d51 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -22,31 +22,31 @@ include "basic_2/dynamic/nta_preserve.ma".
 (* 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
@@ -79,35 +79,35 @@ lemma nta_ind_rest_cnv (h) (Q:relation4 …):
 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.
-        â¦\83G,Kâ¦\84 â\8a¢ V :*[h] W â\86\92 â¬\86*[1] W ≘ U →
+        â\9dªG,Kâ\9d« â\8a¢ V :[h,ð\9d\9b\9a] 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\9b\9a] â\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\9b\9a] 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\9b\9a] â\86\92 â\9dªG,K.â\93\91[I]Vâ\9d« â\8a¢ T :[h,ð\9d\9b\9a] 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\9b\9a] W â\86\92 â\9dªG,Lâ\9d« â\8a¢ T :[h,ð\9d\9b\9a] â\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)
       ) →
       (∀G,L,V,T,U.
-        â¦\83G,Lâ¦\84 â\8a¢ T :*[h] U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.U !*[h] →
+        â\9dªG,Lâ\9d« â\8a¢ T :[h,ð\9d\9b\9a] U â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\90V.U ![h,ð\9d\9b\9a] →
         Q G L T U → Q G L (ⓐV.T) (ⓐV.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\9b\9a] 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\9b\9a] U1 â\86\92 â\9dªG,Lâ\9d« â\8a¢ U1 â¬\8c*[h] U2 â\86\92 â\9dªG,Lâ\9d« â\8a¢ U2 ![h,ð\9d\9b\9a] →
         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\9b\9a] 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
@@ -144,35 +144,35 @@ lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
 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.
-        â¦\83G,Kâ¦\84 â\8a¢ V :*[h] W â\86\92 â¬\86*[1] W ≘ U →
+        â\9dªG,Kâ\9d« â\8a¢ V :[h,ð\9d\9b\9a] 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\9b\9a] â\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\9b\9a] 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\9b\9a] â\86\92 â\9dªG,K.â\93\91[I]Vâ\9d« â\8a¢ T :[h,ð\9d\9b\9a] 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.
-        â¦\83G,Kâ¦\84 â\8a¢ V :*[h] W â\86\92 â¦\83G,K.â\93\9bWâ¦\84 â\8a¢ 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)
+        â\9dªG,Kâ\9d« â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â\9dªG,K.â\93\9bWâ\9d« â\8a¢ T :[h,ð\9d\9b\9a] 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.
-        â¦\83G,Lâ¦\84 â\8a¢ T :*[h] U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.U !*[h] →
+        â\9dªG,Lâ\9d« â\8a¢ T :[h,ð\9d\9b\9a] U â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\90V.U ![h,ð\9d\9b\9a] →
         Q G L T U → Q G L (ⓐV.T) (ⓐV.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\9b\9a] 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\9b\9a] U1 â\86\92 â\9dªG,Lâ\9d« â\8a¢ U1 â¬\8c*[h] U2 â\86\92 â\9dªG,Lâ\9d« â\8a¢ U2 ![h,ð\9d\9b\9a] →
         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\9b\9a] 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